diff --git a/src/Data/Type/Combinator.hs b/src/Data/Type/Combinator.hs
--- a/src/Data/Type/Combinator.hs
+++ b/src/Data/Type/Combinator.hs
@@ -1,9 +1,14 @@
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE LambdaCase #-}
@@ -24,14 +29,14 @@
 --
 -- A collection of simple type combinators,
 -- such as @Identity@ 'I', @Constant@ 'C', @Compose@ '(:.:)',
--- left unnest 'LL', right unnest 'RR', the @S Combinator@ 'SS',
--- etc.
+-- Currying/Uncurrying, etc.
 --
 -----------------------------------------------------------------------------
 
 module Data.Type.Combinator where
 
-import Type.Class.HFunctor
+import Data.Type.Quantifier
+import Type.Class.Higher
 import Type.Class.Known
 import Type.Class.Witness
 import Type.Family.Tuple
@@ -40,75 +45,43 @@
 
 -- (:.:) {{{
 
-data ((f :: l -> *) :.: (g :: k -> l)) :: k -> * where
-  Comp :: { getComp :: f (g a) } -> (f :.: g) a
-infixr 6 :.:
+newtype ((f :: l -> *) :.: (g :: k -> l)) (a :: k) = Comp
+  { getComp :: f (g a)
+  } deriving
+  ( Eq , Ord , Show , Read
+  )
 
-deriving instance Eq   (f (g a)) => Eq   ((f :.: g) a)
-deriving instance Ord  (f (g a)) => Ord  ((f :.: g) a)
-deriving instance Show (f (g a)) => Show ((f :.: g) a)
+instance Eq1 f => Eq1 (f :.: g) where
+  Comp a `eq1` Comp b = a `eq1` b
 
+instance Ord1 f => Ord1 (f :.: g) where
+  Comp a `compare1` Comp b = a `compare1` b
+
+instance Show1 f => Show1 (f :.: g) where
+  showsPrec1 d (Comp a) = showParen (d > 10)
+    $ showString "Comp "
+    . showsPrec1 11 a
+
 instance Witness p q (f (g a)) => Witness p q ((f :.: g) a) where
   type WitnessC p q ((f :.: g) a) = Witness p q (f (g a))
   r \\ Comp a = r \\ a
 
-data ((f :: m -> *) :..: (g :: k -> l -> m)) :: k -> l -> * where
-  Comp2 :: f (g a b) -> (f :..: g) a b
-infixr 6 :..:
-
-deriving instance Eq   (f (g a b)) => Eq   ((f :..: g) a b)
-deriving instance Ord  (f (g a b)) => Ord  ((f :..: g) a b)
-deriving instance Show (f (g a b)) => Show ((f :..: g) a b)
-
-instance Witness p q (f (g a b)) => Witness p q ((f :..: g) a b) where
-  type WitnessC p q ((f :..: g) a b) = Witness p q (f (g a b))
-  r \\ Comp2 a = r \\ a
-
--- }}}
-
--- IT {{{
-
-data IT :: (k -> *) -> k -> * where
-  IT :: { getIT :: f a } -> IT f a
-
-deriving instance Eq   (f a) => Eq   (IT f a)
-deriving instance Ord  (f a) => Ord  (IT f a)
-deriving instance Show (f a) => Show (IT f a)
-
-instance HFunctor IT where
-  map' f = IT . f . getIT
-
-instance HFoldable IT where
-  foldMap' f = f . getIT
-
-instance HTraversable IT where
-  traverse' f = fmap IT . f . getIT
-
-instance Witness p q (f a) => Witness p q (IT f a) where
-  type WitnessC p q (IT f a) = Witness p q (f a)
-  r \\ IT a = r \\ a
+instance TestEquality f => TestEquality (f :.: g) where
+  testEquality (Comp a) (Comp b) = a =?= b //? qed
 
-instance Num (f a) => Num (IT f a) where
-  IT a * IT b   = IT $ a * b
-  IT a + IT b   = IT $ a + b
-  IT a - IT b   = IT $ a - b
-  abs    (IT a) = IT $ abs a
-  signum (IT a) = IT $ signum a
-  fromInteger   = IT . fromInteger
+instance TestEquality f => TestEquality1 ((:.:) f) where
+  testEquality1 (Comp a) (Comp b) = a =?= b //? qed
 
 -- }}}
 
 -- I {{{
 
-data I :: * -> * where
-  I :: { getI :: a } -> I a
-
-deriving instance Eq   a => Eq   (I a)
-deriving instance Ord  a => Ord  (I a)
-deriving instance Show a => Show (I a)
-
-instance Functor I where
-  fmap f (I a) = I $ f a
+newtype I a = I
+  { getI :: a
+  } deriving
+  ( Eq , Ord , Show
+  , Functor , Foldable , Traversable
+  )
 
 instance Applicative I where
   pure = I
@@ -117,12 +90,6 @@
 instance Monad I where
   I a >>= f = f a
 
-instance Foldable I where
-  foldMap f (I a) = f a
-
-instance Traversable I where
-  traverse f (I a) = I <$> f a
-
 instance Witness p q a => Witness p q (I a) where
   type WitnessC p q (I a) = Witness p q a
   r \\ I a = r \\ a
@@ -137,112 +104,26 @@
 
 -- }}}
 
--- LL {{{
-
-newtype LL (a :: k) (f :: l -> *) (g :: k -> l) = LL
-  { getLL :: f (g a)
-  }
-
-deriving instance Eq   (f (g a)) => Eq   (LL a f g)
-deriving instance Ord  (f (g a)) => Ord  (LL a f g)
-deriving instance Show (f (g a)) => Show (LL a f g)
-
-instance HFunctor (LL a) where
-  map' f = LL . f . getLL
-
-instance HFoldable (LL a) where
-  foldMap' f = f . getLL
-
-instance HTraversable (LL a) where
-  traverse' f = fmap LL . f . getLL
-
-instance Witness p q (f (g a)) => Witness p q (LL a f g) where
-  type WitnessC p q (LL a f g) = Witness p q (f (g a))
-  r \\ LL a = r \\ a
-
--- }}}
-
--- RR {{{
-
-newtype RR (g :: k -> l) (f :: l -> *) (a :: k) = RR
-  { getRR :: f (g a)
-  }
-
-deriving instance Eq   (f (g a)) => Eq   (RR g f a)
-deriving instance Ord  (f (g a)) => Ord  (RR g f a)
-deriving instance Show (f (g a)) => Show (RR g f a)
-
-instance HFunctor (RR g) where
-  map' f = RR . f . getRR
-
-instance HFoldable (RR g) where
-  foldMap' f = f . getRR
-
-instance HTraversable (RR g) where
-  traverse' f = fmap RR . f . getRR
-
-instance Witness p q (f (g a)) => Witness p q (RR g f a) where
-  type WitnessC p q (RR g f a) = Witness p q (f (g a))
-  r \\ RR a = r \\ a
-
--- }}}
-
--- SS {{{
-
-newtype SS (f :: k -> l -> *) (g :: k -> l) :: k -> * where
-  SS :: { getSS :: f a (g a) } -> SS f g a
-
-deriving instance Eq   (f a (g a)) => Eq   (SS f g a)
-deriving instance Ord  (f a (g a)) => Ord  (SS f g a)
-deriving instance Show (f a (g a)) => Show (SS f g a)
-
-instance Witness p q (f a (g a)) => Witness p q (SS f g a) where
-  type WitnessC p q (SS f g a) = Witness p q (f a (g a))
-  r \\ SS a = r \\ a
-
--- }}}
-
--- CT {{{
-
-data CT :: * -> (k -> *) -> l -> * where
-  CT :: { getCT :: r } -> CT r f a
-
-deriving instance Eq   r => Eq   (CT r f a)
-deriving instance Ord  r => Ord  (CT r f a)
-deriving instance Show r => Show (CT r f a)
-
-instance HFunctor (CT r) where
-  map' _ (CT r) = CT r
-
-instance HFoldable (CT r) where
-  foldMap' _ _ = mempty
-
-instance HTraversable (CT r) where
-  traverse' _ (CT r) = pure $ CT r
-
-instance Witness p q r => Witness p q (CT r f a) where
-  type WitnessC p q (CT r f a) = Witness p q r
-  r \\ CT a = r \\ a
-
-instance Num r => Num (CT r f a) where
-  CT a * CT b   = CT $ a * b
-  CT a + CT b   = CT $ a + b
-  CT a - CT b   = CT $ a - b
-  abs    (CT a) = CT $ abs a
-  signum (CT a) = CT $ signum a
-  fromInteger   = CT . fromInteger
-
--- }}}
-
 -- C {{{
 
-data C :: * -> k -> * where
-  C :: { getC :: r } -> C r a
+newtype C r a = C
+  { getC :: r
+  } deriving
+  ( Eq , Ord , Show , Read
+  , Functor , Foldable , Traversable
+  )
 
-deriving instance Eq   r => Eq   (C r a)
-deriving instance Ord  r => Ord  (C r a)
-deriving instance Show r => Show (C r a)
+instance Eq   r => Eq1   (C r)
+instance Ord  r => Ord1  (C r)
+instance Show r => Show1 (C r)
 
+instance Read r => Read1 (C r) where
+  readsPrec1 d = readParen (d > 10) $ \s0 ->
+    [ (Some $ C r,s2)
+    | ("C",s1) <- lex s0
+    , (r,s2)   <- readsPrec 11 s1
+    ]
+
 instance Witness p q r => Witness p q (C r a) where
   type WitnessC p q (C r a) = Witness p q r
   r \\ C a = r \\ a
@@ -255,26 +136,8 @@
   signum (C a) = C $ signum a
   fromInteger  = C . fromInteger
 
--- }}}
-
--- Join {{{
-
-newtype Join f a = Join
-  { getJoin :: f a a
-  }
-
-deriving instance Eq   (f a a) => Eq   (Join f a)
-deriving instance Ord  (f a a) => Ord  (Join f a)
-deriving instance Show (f a a) => Show (Join f a)
-
-instance Known (f a) a => Known (Join f) a where
-  type KnownC (Join f) a = Known (f a) a
-  known = Join known
-
-instance Witness p q (f a a) => Witness p q (Join f a) where
-  type WitnessC p q (Join f a) = Witness p q (f a a)
-  r \\ Join a = r \\ a
-  
+mapC :: (r -> s) -> C r a -> C s b
+mapC f = C . f . getC
 
 -- }}}
 
@@ -282,26 +145,40 @@
 
 newtype Flip p b a = Flip
   { getFlip :: p a b
-  } deriving (Eq,Ord,Show)
+  } deriving
+  ( Eq , Ord , Show , Read
+  )
 
-instance Known (p a) b => Known (Flip p b) a where
-  type KnownC (Flip p b) a = Known (p a) b
-  known = Flip known
+flipTestEquality1 :: TestEquality (p c) => Flip p a c -> Flip p b c -> Maybe (a :~: b)
+flipTestEquality1 (Flip a) (Flip b) = a =?= b
 
+instance TestEquality1 p => TestEquality (Flip p b) where
+  testEquality (Flip a) (Flip b) = a =??= b
+
 instance Witness p q (f a b) => Witness p q (Flip f b a) where
   type WitnessC p q (Flip f b a) = Witness p q (f a b)
   r \\ Flip a = r \\ a
 
-flipped :: (f a b -> g c d) -> Flip f b a -> Flip g d c
-flipped f = Flip . f . getFlip
+instance Known (p a) b => Known (Flip p b) a where
+  type KnownC (Flip p b) a = Known (p a) b
+  known = Flip known
 
+mapFlip :: (f a b -> g c d) -> Flip f b a -> Flip g d c
+mapFlip f = Flip . f . getFlip
+
 -- }}}
 
 -- Cur {{{
 
-newtype Cur (p :: (k,l) -> *) :: k -> l -> * where
-  Cur :: { getCur :: p (a#b) } -> Cur p a b
+newtype Cur (p :: (k,l) -> *) (a :: k) (b :: l) = Cur
+  { getCur :: p (a#b)
+  }
 
+deriving instance Eq   (p (a#b)) => Eq   (Cur p a b)
+deriving instance Ord  (p (a#b)) => Ord  (Cur p a b)
+deriving instance Show (p (a#b)) => Show (Cur p a b)
+deriving instance Read (p (a#b)) => Read (Cur p a b)
+
 instance Known p (a#b) => Known (Cur p a) b where
   type KnownC (Cur p a) b = Known p (a#b)
   known = Cur known
@@ -310,6 +187,9 @@
   type WitnessC q r (Cur p a b) = Witness q r (p (a#b))
   r \\ Cur p = r \\ p
 
+mapCur :: (p '(a,b) -> q '(c,d)) -> Cur p a b -> Cur q c d
+mapCur f = Cur . f . getCur
+
 -- }}}
 
 -- Uncur {{{
@@ -317,6 +197,18 @@
 data Uncur (p :: k -> l -> *) :: (k,l) -> * where
   Uncur :: { getUncur :: p a b } -> Uncur p (a#b)
 
+deriving instance Eq   (p (Fst x) (Snd x)) => Eq   (Uncur p x)
+deriving instance Ord  (p (Fst x) (Snd x)) => Ord  (Uncur p x)
+deriving instance Show (p (Fst x) (Snd x)) => Show (Uncur p x)
+deriving instance (x ~ (a#b), Read (p a b)) => Read (Uncur p x)
+
+instance Read2 p => Read1 (Uncur p) where
+  readsPrec1 d = readParen (d > 10) $ \s0 ->
+    [ (p >>-- Some . Uncur,s2)
+    | ("Uncur",s1) <- lex s0
+    , (p,s2)       <- readsPrec2 11 s1
+    ]
+
 instance (Known (p a) b,q ~ (a#b)) => Known (Uncur p) q where
   type KnownC (Uncur p) q = Known (p (Fst q)) (Snd q)
   known = Uncur known
@@ -325,13 +217,22 @@
   type WitnessC r s (Uncur p q) = Witness r s (p (Fst q) (Snd q))
   r \\ Uncur p = r \\ p
 
+mapUncur :: (p (Fst a) (Snd a) -> q b c) -> Uncur p a -> Uncur q '(b,c)
+mapUncur f (Uncur a) = Uncur $ f a
+
 -- }}}
 
--- Cur {{{
+-- Cur3 {{{
 
-newtype Cur3 (p :: (k,l,m) -> *) :: k -> l -> m -> * where
-  Cur3 :: { getCur3 :: p '(a,b,c) } -> Cur3 p a b c
+newtype Cur3 (p :: (k,l,m) -> *) (a :: k) (b :: l) (c :: m) = Cur3
+  { getCur3 :: p '(a,b,c)
+  }
 
+deriving instance Eq   (p '(a,b,c)) => Eq   (Cur3 p a b c)
+deriving instance Ord  (p '(a,b,c)) => Ord  (Cur3 p a b c)
+deriving instance Show (p '(a,b,c)) => Show (Cur3 p a b c)
+deriving instance Read (p '(a,b,c)) => Read (Cur3 p a b c)
+
 instance Known p '(a,b,c) => Known (Cur3 p a b) c where
   type KnownC (Cur3 p a b) c = Known p '(a,b,c)
   known = Cur3 known
@@ -340,6 +241,9 @@
   type WitnessC q r (Cur3 p a b c) = Witness q r (p '(a,b,c))
   r \\ Cur3 p = r \\ p
 
+mapCur3 :: (p '(a,b,c) -> q '(d,e,f)) -> Cur3 p a b c -> Cur3 q d e f
+mapCur3 f = Cur3 . f . getCur3
+
 -- }}}
 
 -- Uncur3 {{{
@@ -347,6 +251,18 @@
 data Uncur3 (p :: k -> l -> m -> *) :: (k,l,m) -> * where
   Uncur3 :: { getUncur3 :: p a b c } -> Uncur3 p '(a,b,c)
 
+deriving instance Eq   (p (Fst3 x) (Snd3 x) (Thd3 x)) => Eq   (Uncur3 p x)
+deriving instance Ord  (p (Fst3 x) (Snd3 x) (Thd3 x)) => Ord  (Uncur3 p x)
+deriving instance Show (p (Fst3 x) (Snd3 x) (Thd3 x)) => Show (Uncur3 p x)
+deriving instance (x ~ '(a,b,c), Read (p a b c)) => Read (Uncur3 p x)
+
+instance Read3 p => Read1 (Uncur3 p) where
+  readsPrec1 d = readParen (d > 10) $ \s0 ->
+    [ (p >>--- Some . Uncur3,s2)
+    | ("Uncur",s1) <- lex s0
+    , (p,s2)       <- readsPrec3 11 s1
+    ]
+
 instance (Known (p a b) c,q ~ '(a,b,c)) => Known (Uncur3 p) q where
   type KnownC (Uncur3 p) q = Known (p (Fst3 q) (Snd3 q)) (Thd3 q)
   known = Uncur3 known
@@ -354,6 +270,44 @@
 instance (Witness r s (p a b c),q ~ '(a,b,c)) => Witness r s (Uncur3 p q) where
   type WitnessC r s (Uncur3 p q) = Witness r s (p (Fst3 q) (Snd3 q) (Thd3 q))
   r \\ Uncur3 p = r \\ p
+
+mapUncur3 :: (p (Fst3 x) (Snd3 x) (Thd3 x) -> q d e f) -> Uncur3 p x -> Uncur3 q '(d,e,f)
+mapUncur3 f (Uncur3 a) = Uncur3 $ f a
+
+-- }}}
+
+-- Join {{{
+
+newtype Join f a = Join
+  { getJoin :: f a a
+  }
+
+deriving instance Eq   (f a a) => Eq   (Join f a)
+deriving instance Ord  (f a a) => Ord  (Join f a)
+deriving instance Show (f a a) => Show (Join f a)
+deriving instance Read (f a a) => Read (Join f a)
+
+instance Eq2 f => Eq1 (Join f) where
+  Join a `eq1` Join b = a `eq2` b
+
+instance Ord2 f => Ord1 (Join f) where
+  Join a `compare1` Join b = a `compare2` b
+
+instance Show2 f => Show1 (Join f) where
+  showsPrec1 d (Join a) = showParen (d > 10)
+    $ showString "Join "
+    . showsPrec2 11 a
+
+instance Known (f a) a => Known (Join f) a where
+  type KnownC (Join f) a = Known (f a) a
+  known = Join known
+
+instance Witness p q (f a a) => Witness p q (Join f a) where
+  type WitnessC p q (Join f a) = Witness p q (f a a)
+  r \\ Join a = r \\ a
+
+mapJoin :: (f a a -> g b b) -> Join f a -> Join g b
+mapJoin f = Join . f . getJoin
 
 -- }}}
 
diff --git a/src/Data/Type/Conjunction.hs b/src/Data/Type/Conjunction.hs
--- a/src/Data/Type/Conjunction.hs
+++ b/src/Data/Type/Conjunction.hs
@@ -32,7 +32,7 @@
 
 module Data.Type.Conjunction where
 
-import Type.Class.HFunctor
+import Type.Class.Higher
 import Type.Class.Known
 import Type.Class.Witness
 import Type.Family.Tuple
@@ -46,13 +46,33 @@
 deriving instance (Eq   (f a), Eq   (g a)) => Eq   ((f :&: g) a)
 deriving instance (Ord  (f a), Ord  (g a)) => Ord  ((f :&: g) a)
 deriving instance (Show (f a), Show (g a)) => Show ((f :&: g) a)
+deriving instance (Read (f a), Read (g a)) => Read ((f :&: g) a)
 
+instance (Eq1 f, Eq1 g) => Eq1 (f :&: g) where
+  eq1 (a :&: b) (c :&: d) = a =#= c && b =#= d
+
+instance (Ord1 f, Ord1 g) => Ord1 (f :&: g) where
+  compare1 (a :&: b) (c :&: d) = compare1 a c `mappend` compare1 b d
+
+instance (Show1 f, Show1 g) => Show1 (f :&: g) where
+  showsPrec1 d (a :&: b) = showParen (d > 5)
+    $ showsPrec1 11 a
+    . showString " :&: "
+    . showsPrec1 11 b
+
 fanFst :: (f :&: g) a -> f a
 fanFst (a :&: _) = a
 
 fanSnd :: (f :&: g) a -> g a
 fanSnd (_ :&: b) = b
 
+(.&.) :: (f a -> h b) -> (g a -> i b) -> (f :&: g) a -> (h :&: i) b
+(f .&. g) (a :&: b) = f a :&: g b
+infixr 3 .&.
+
+fanFirst :: (f a -> g a) -> (f :&: h) a -> (g :&: h) a
+fanFirst f (a :&: b) = f a :&: b
+
 uncurryFan :: (f a -> g a -> r) -> (f :&: g) a -> r
 uncurryFan f (a :&: b) = f a b
 
@@ -65,30 +85,22 @@
 instance (Known f a, Known g a) => Known (f :&: g) a where
   known = known :&: known
 
-instance HFunctor ((:&:) f) where
-  map' f (a :&: b) = a :&: f b
+instance Functor1 ((:&:) f) where
+  map1 f (a :&: b) = a :&: f b
 
-instance HFoldable ((:&:) f) where
-  foldMap' f (_ :&: b) = f b
+instance Foldable1 ((:&:) f) where
+  foldMap1 f (_ :&: b) = f b
 
-instance HTraversable ((:&:) f) where
-  traverse' f (a :&: b) = (:&:) a <$> f b
+instance Traversable1 ((:&:) f) where
+  traverse1 f (a :&: b) = (:&:) a <$> f b
 
-instance HBifunctor (:&:) where
-  bimap' f g (a :&: b) = f a :&: g b
+instance Bifunctor1 (:&:) where
+  bimap1 f g (a :&: b) = f a :&: g b
 
 instance (Witness p q (f a), Witness s t (g a)) => Witness (p,s) (q,t) ((f :&: g) a) where
   type WitnessC (p,s) (q,t) ((f :&: g) a) = (Witness p q (f a), Witness s t (g a))
   r \\ a :&: b = r \\ a \\ b
 
-{-
-instance Witness p q (f a) => Witness p q (WitFst (:&:) f g a) where
-  r \\ WitFst (a :&: _) = r \\ a
-
-instance Witness p q (g a) => Witness p q (WitSnd (:&:) f g a) where
-  r \\ WitSnd (_ :&: b) = r \\ b
--}
-
 -- }}}
 
 -- (:*:) {{{
@@ -100,7 +112,20 @@
 deriving instance (Eq   (f (Fst p)), Eq   (g (Snd p))) => Eq   ((f :*: g) p)
 deriving instance (Ord  (f (Fst p)), Ord  (g (Snd p))) => Ord  ((f :*: g) p)
 deriving instance (Show (f (Fst p)), Show (g (Snd p))) => Show ((f :*: g) p)
+deriving instance (p ~ (a#b), Read (f a), Read (g b)) => Read ((f :*: g) p)
 
+instance (Eq1 f, Eq1 g) => Eq1 (f :*: g) where
+  eq1 (a :*: b) (c :*: d) = a =#= c && b =#= d
+
+instance (Ord1 f, Ord1 g) => Ord1 (f :*: g) where
+  compare1 (a :*: b) (c :*: d) = compare1 a c `mappend` compare1 b d
+
+instance (Show1 f, Show1 g) => Show1 (f :*: g) where
+  showsPrec1 d (a :*: b) = showParen (d > 5)
+    $ showsPrec1 11 a
+    . showString " :*: "
+    . showsPrec1 11 b
+
 parFst :: (f :*: g) p -> f (Fst p)
 parFst (a :*: _) = a
 
@@ -116,17 +141,17 @@
 instance (p ~ (a#b), Known f a, Known g b) => Known (f :*: g) p where
   known = known :*: known
 
-instance HFunctor ((:*:) f) where
-  map' f (a :*: b) = a :*: f b
+instance Functor1 ((:*:) f) where
+  map1 f (a :*: b) = a :*: f b
 
-instance HFoldable ((:*:) f) where
-  foldMap' f (_ :*: b) = f b
+instance Foldable1 ((:*:) f) where
+  foldMap1 f (_ :*: b) = f b
 
-instance HTraversable ((:*:) f) where
-  traverse' f (a :*: b) = (:*:) a <$> f b
+instance Traversable1 ((:*:) f) where
+  traverse1 f (a :*: b) = (:*:) a <$> f b
 
-instance HBifunctor (:*:) where
-  bimap' f g (a :*: b) = f a :*: g b
+instance Bifunctor1 (:*:) where
+  bimap1 f g (a :*: b) = f a :*: g b
 
 _fst :: (a#b) :~: (c#d) -> a :~: c
 _fst Refl = Refl
diff --git a/src/Data/Type/Disjunction.hs b/src/Data/Type/Disjunction.hs
--- a/src/Data/Type/Disjunction.hs
+++ b/src/Data/Type/Disjunction.hs
@@ -1,9 +1,9 @@
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE LambdaCase #-}
@@ -23,107 +23,190 @@
 -- Portability :  RankNTypes
 --
 -- Two type combinators for working with disjunctions:
--- A /branch/ combinator '(:+:)', and a /choice/ combinator '(:|:)'.
+-- A /branch/ combinator '(:|:)', and a /choice/ combinator '(:+:)'.
 --
--- These are analogous to '(+++)' and '(|||)' from 'Control.Arrow',
+-- These are analogous to '(|||)' and '(+++)' from 'Control.Arrow',
 -- respectively.
 --
 -----------------------------------------------------------------------------
 
 module Data.Type.Disjunction where
 
-import Type.Class.HFunctor
+import Data.Type.Quantifier
+import Type.Class.Higher
 import Type.Class.Known
 import Type.Class.Witness
+import Type.Family.Either
 
--- (:+:) {{{
+-- (:|:) {{{
 
-data ((f :: k -> *) :+: (g :: k -> *)) :: k -> * where
-  L :: !(f a) -> (f :+: g) a
-  R :: !(g a) -> (f :+: g) a
-infixr 4 :+:
+data ((f :: k -> *) :|: (g :: k -> *)) :: k -> * where
+  L :: !(f a) -> (f :|: g) a
+  R :: !(g a) -> (f :|: g) a
+infixr 4 :|:
 
-(>+<) :: (f a -> r) -> (g a -> r) -> (f :+: g) a -> r
-f >+< g = \case
+deriving instance (Eq   (f a), Eq   (g a)) => Eq   ((f :|: g) a)
+deriving instance (Ord  (f a), Ord  (g a)) => Ord  ((f :|: g) a)
+deriving instance (Show (f a), Show (g a)) => Show ((f :|: g) a)
+deriving instance (Read (f a), Read (g a)) => Read ((f :|: g) a)
+
+instance (Eq1 f, Eq1 g) => Eq1 (f :|: g) where
+  eq1 = \case
+    L a -> \case
+      L b -> a =#= b
+      _   -> False
+    R a -> \case
+      R b -> a =#= b
+      _   -> False
+
+instance (Ord1 f, Ord1 g) => Ord1 (f :|: g) where
+  compare1 = \case
+    L a -> \case
+      L b -> compare1 a b
+      R _ -> LT
+    R a -> \case
+      L _ -> GT
+      R b -> compare1 a b
+
+instance (Show1 f, Show1 g) => Show1 (f :|: g) where
+  showsPrec1 d = showParen (d > 10) . \case
+    L a -> showString "L "
+         . showsPrec1 11 a
+    R b -> showString "R "
+         . showsPrec1 11 b
+
+instance (Read1 f, Read1 g) => Read1 (f :|: g) where
+  readsPrec1 d = readParen (d > 10) $ \s0 ->
+    [ (a >>- Some . L,s2)
+    | ("L",s1) <- lex s0
+    , (a,s2)   <- readsPrec1 11 s1
+    ] ++
+    [ (a >>- Some . R,s2)
+    | ("R",s1) <- lex s0
+    , (a,s2)   <- readsPrec1 11 s1
+    ]
+
+(>|<) :: (f a -> r) -> (g a -> r) -> (f :|: g) a -> r
+f >|< g = \case
   L a -> f a
   R b -> g b
-infixr 2 >+<
+infixr 2 >|<
 
-instance HFunctor ((:+:) f) where
-  map' f = \case
+instance Functor1 ((:|:) f) where
+  map1 f = \case
     L a -> L a
     R b -> R $ f b
 
-instance HFoldable ((:+:) f) where
-  foldMap' f = \case
+instance Foldable1 ((:|:) f) where
+  foldMap1 f = \case
     L _ -> mempty
     R b -> f b
 
-instance HTraversable ((:+:) f) where
-  traverse' f = \case
+instance Traversable1 ((:|:) f) where
+  traverse1 f = \case
     L a -> pure $ L a
     R b -> R <$> f b
 
-instance HBifunctor (:+:) where
-  bimap' f g = \case
+instance Bifunctor1 (:|:) where
+  bimap1 f g = \case
     L a -> L $ f a
     R b -> R $ g b
 
-instance (Witness p q (f a), Witness p q (g a)) => Witness p q ((f :+: g) a) where
-  type WitnessC p q ((f :+: g) a) = (Witness p q (f a), Witness p q (g a))
+instance (Witness p q (f a), Witness p q (g a)) => Witness p q ((f :|: g) a) where
+  type WitnessC p q ((f :|: g) a) = (Witness p q (f a), Witness p q (g a))
   (\\) r = \case
     L a -> r \\ a
     R b -> r \\ b
 
 -- }}}
 
--- (:|:) {{{
+-- (:+:) {{{
 
-data ((f :: k -> *) :|: (g :: l -> *)) :: Either k l -> * where
-  L' :: !(f a) -> (f :|: g) (Left  a)
-  R' :: !(g b) -> (f :|: g) (Right b)
-infixr 4 :|:
+data ((f :: k -> *) :+: (g :: l -> *)) :: Either k l -> * where
+  L' :: !(f a) -> (f :+: g) (Left  a)
+  R' :: !(g b) -> (f :+: g) (Right b)
+infixr 4 :+:
 
-(>|<) :: (forall a. (e ~ Left a) => f a -> r) -> (forall b. (e ~ Right b) => g b -> r) -> (f :|: g) e -> r
-f >|< g = \case
+deriving instance (Eq   (f (FromLeft e)), Eq   (g (FromRight e))) => Eq   ((f :+: g) e)
+deriving instance (Ord  (f (FromLeft e)), Ord  (g (FromRight e))) => Ord  ((f :+: g) e)
+deriving instance (Show (f (FromLeft e)), Show (g (FromRight e))) => Show ((f :+: g) e)
+
+instance (Eq1 f, Eq1 g) => Eq1 (f :+: g) where
+  eq1 = \case
+    L' a -> \case
+      L' b -> a =#= b
+      _    -> False
+    R' a -> \case
+      R' b -> a =#= b
+      _    -> False
+
+instance (Ord1 f, Ord1 g) => Ord1 (f :+: g) where
+  compare1 = \case
+    L' a -> \case
+      L' b -> compare1 a b
+      _    -> LT
+    R' a -> \case
+      R' b -> compare1 a b
+      _    -> GT
+
+instance (Show1 f, Show1 g) => Show1 (f :+: g) where
+  showsPrec1 d = showParen (d > 10) . \case
+    L' a -> showString "L' "
+          . showsPrec1 11 a
+    R' b -> showString "R' "
+          . showsPrec1 11 b
+
+instance (Read1 f, Read1 g) => Read1 (f :+: g) where
+  readsPrec1 d = readParen (d > 10) $ \s0 ->
+    [ (a >>- Some . L',s2)
+    | ("L'",s1) <- lex s0
+    , (a,s2)    <- readsPrec1 11 s1
+    ] ++
+    [ (a >>- Some . R',s2)
+    | ("R'",s1) <- lex s0
+    , (a,s2)    <- readsPrec1 11 s1
+    ]
+
+(>+<) :: (forall a. (e ~ Left a) => f a -> r) -> (forall b. (e ~ Right b) => g b -> r) -> (f :+: g) e -> r
+f >+< g = \case
   L' a -> f a
   R' b -> g b
-infixr 2 >|<
+infixr 2 >+<
 
-instance Known f a => Known (f :|: g) (Left a) where
-  type KnownC (f :|: g) (Left a) = Known f a
+instance Known f a => Known (f :+: g) (Left a) where
+  type KnownC (f :+: g) (Left a) = Known f a
   known = L' known
 
-instance Known g b => Known (f :|: g) (Right b) where
-  type KnownC (f :|: g) (Right b) = Known g b
+instance Known g b => Known (f :+: g) (Right b) where
+  type KnownC (f :+: g) (Right b) = Known g b
   known = R' known
 
-instance HFunctor ((:|:) f) where
-  map' f = \case
+instance Functor1 ((:+:) f) where
+  map1 f = \case
     L' a -> L' a
     R' b -> R' $ f b
 
-instance HFoldable ((:|:) f) where
-  foldMap' f = \case
+instance Foldable1 ((:+:) f) where
+  foldMap1 f = \case
     L' _ -> mempty
     R' b -> f b
 
-instance HTraversable ((:|:) f) where
-  traverse' f = \case
+instance Traversable1 ((:+:) f) where
+  traverse1 f = \case
     L' a -> pure $ L' a
     R' b -> R' <$> f b
 
-instance HBifunctor (:|:) where
-  bimap' f g = \case
+instance Bifunctor1 (:+:) where
+  bimap1 f g = \case
     L' a -> L' $ f a
     R' b -> R' $ g b
 
-instance Witness p q (f a) => Witness p q ((f :|: g) (Left a)) where
-  type WitnessC p q ((f :|: g) (Left a)) = Witness p q (f a)
+instance Witness p q (f a) => Witness p q ((f :+: g) (Left a)) where
+  type WitnessC p q ((f :+: g) (Left a)) = Witness p q (f a)
   r \\ L' a = r \\ a
 
-instance Witness p q (g b) => Witness p q ((f :|: g) (Right b)) where
-  type WitnessC p q ((f :|: g) (Right b)) = Witness p q (g b)
+instance Witness p q (g b) => Witness p q ((f :+: g) (Right b)) where
+  type WitnessC p q ((f :+: g) (Right b)) = Witness p q (g b)
   r \\ R' b = r \\ b
 
 -- }}}
diff --git a/src/Data/Type/Fin.hs b/src/Data/Type/Fin.hs
--- a/src/Data/Type/Fin.hs
+++ b/src/Data/Type/Fin.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE PatternSynonyms #-}
@@ -5,7 +6,6 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE LambdaCase #-}
@@ -30,9 +30,8 @@
 
 module Data.Type.Fin where
 
-import Data.Type.Combinator
 import Data.Type.Nat
-import Type.Class.Known
+import Type.Class.Higher
 import Type.Class.Witness
 import Type.Family.Constraint
 import Type.Family.Nat
@@ -46,6 +45,27 @@
 deriving instance Ord  (Fin n)
 deriving instance Show (Fin n)
 
+instance Eq1   Fin
+instance Ord1  Fin
+instance Show1 Fin
+
+instance Read1 Fin where
+  readsPrec1 d = readParen (d > 10) $ \s0 ->
+    [ (Some FZ,s1)
+    | ("FZ",s1) <- lex s0
+    ] ++ 
+    [ (n >>- Some . FS,s2)
+    | ("FS",s1) <- lex s0
+    , (n,s2)    <- readsPrec1 11 s1
+    ]
+
+elimFin :: (forall x. p (S x))
+        -> (forall x. Fin x -> p x -> p (S x))
+        -> Fin n -> p n
+elimFin z s = \case
+  FZ   -> z
+  FS n -> s n $ elimFin z s n
+
 -- | Gives the list of all members of the finite set of size @n@.
 fins :: Nat n -> [Fin n]
 fins = \case
@@ -76,26 +96,6 @@
   FS x -> \case
     FZ   -> Just FZ \\ x
     FS y -> FS <$> without x y \\ x
-
-class (x :: N) <= (y :: N) where
-  weakenN :: Fin x -> Fin y
-
-instance {-# OVERLAPPING #-} x <= x where
-  weakenN = id
-
-instance {-# OVERLAPPABLE #-} (x <= y) => x <= S y where
-  weakenN = weaken . weakenN
-
-{-
-instance Known Nat n => Known ([] :.: Fin) n where
-  type KnownC ([] :.: Fin) n = Known Nat n
-  known = Comp $ go (known :: Nat n)
-    where
-    go :: Nat x -> [Fin x]
-    go = \case
-      Z_   -> []
-      S_ x -> FZ : map FS (go x)
--}
 
 -- | Take a 'Fin' to an existentially quantified 'Nat'.
 finNat :: Fin x -> Some Nat
diff --git a/src/Data/Type/Index.hs b/src/Data/Type/Index.hs
--- a/src/Data/Type/Index.hs
+++ b/src/Data/Type/Index.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE RankNTypes #-}
@@ -28,10 +29,11 @@
 
 module Data.Type.Index where
 
-import Type.Class.HFunctor
+import Data.Type.Quantifier
+import Type.Class.Higher
 import Type.Class.Known
+import Type.Class.Witness
 import Type.Family.List
-import Type.Family.Nat
 
 data Index :: [k] -> k -> * where
   IZ :: Index (a :< as) a
@@ -41,6 +43,47 @@
 deriving instance Ord  (Index as a)
 deriving instance Show (Index as a)
 
+instance Eq1   (Index as)
+instance Ord1  (Index as)
+instance Show1 (Index as)
+
+instance Read2 Index where
+  readsPrec2 d = readParen (d > 10) $ \s0 ->
+    [ (Some2 IZ,s1)
+    | ("IZ",s1) <- lex s0
+    ] ++
+    [ (i >>-- Some2 . IS,s2)
+    | ("IS",s1) <- lex s0
+    , (i,s2)    <- readsPrec2 11 s1
+    ]
+
+instance TestEquality (Index as) where
+  testEquality = \case
+    IZ -> \case
+      IZ -> qed
+      _  -> Nothing
+    IS x -> \case
+      IS y -> x =?= y //? qed
+      _    -> Nothing
+
+elimIndex :: (forall   xs. p (a :< xs) a)
+          -> (forall x xs. Index xs a -> p xs a -> p (x :< xs) a)
+          -> Index as a
+          -> p as a
+elimIndex z s = \case
+  IZ   -> z
+  IS x -> s x $ elimIndex z s x
+
+ixNil :: Index Ø a -> Void
+ixNil = impossible
+
+onIxPred :: (Index as a -> Index bs a) -> Index (b :< as) a -> Index (b :< bs) a
+onIxPred f = \case
+  IZ   -> IZ
+  IS x -> IS $ f x
+
+-- Elem {{{
+
 type a ∈ as = Elem as a
 infix 6 ∈
 
@@ -53,9 +96,12 @@
 instance {-# OVERLAPPABLE #-} Elem as a => Elem (b :< as) a where
   elemIndex = IS elemIndex
 
+
 instance {-# OVERLAPPING #-} Known (Index (a :< as)) a where
   known = IZ
 
 instance {-# OVERLAPPABLE #-} Known (Index as) a => Known (Index (b :< as)) a where
   known = IS known
+
+-- }}}
 
diff --git a/src/Data/Type/Index/Quote.hs b/src/Data/Type/Index/Quote.hs
deleted file mode 100644
--- a/src/Data/Type/Index/Quote.hs
+++ /dev/null
@@ -1,62 +0,0 @@
-{-# LANGUAGE TemplateHaskell #-}
-{-# LANGUAGE QuasiQuotes #-}
-{-# LANGUAGE LambdaCase #-}
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Type.Index.Quote
--- Copyright   :  Copyright (C) 2015 Kyle Carter
--- License     :  BSD3
---
--- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
--- Stability   :  experimental
--- Portability :  RankNTypes
---
--- A 'QuasiQuoter' for the 'Index' type.
---
------------------------------------------------------------------------------
-
-module Data.Type.Index.Quote where
-
-import Data.Type.Index
-import Language.Haskell.TH
-import Language.Haskell.TH.Lib
-import Language.Haskell.TH.Quote
-import Text.Read (readMaybe)
-import Control.Monad
-
-ix :: QuasiQuoter
-ix = QuasiQuoter
-  { quoteExp  = parseIxExp
-  , quotePat  = parseIxPat
-  , quoteType = error "ix: quoteType not defined"
-  , quoteDec  = error "ix: quoteDec not defined"
-  }
-
-parseIxExp :: String -> Q Exp
-parseIxExp s = maybe (fail $ "ix: couldn't parse Int: " ++ show s)
-  (notNeg >=> go)
-  $ readMaybe s
-  where
-  notNeg :: Int -> Q Int
-  notNeg n
-    | n < 0 = fail $ "ix: negative index: " ++ show n
-    | True  = return n
-  go :: Int -> Q Exp
-  go = \case
-    0 -> [| IZ |]
-    n -> [| IS $(go $ n-1) |]
-
-parseIxPat :: String -> Q Pat
-parseIxPat s = maybe (fail $ "ix: couldn't parse Int: " ++ show s)
-  (notNeg >=> go)
-  $ readMaybe s
-  where
-  notNeg :: Int -> Q Int
-  notNeg n
-    | n < 0 = fail $ "ix: negative index: " ++ show n
-    | True  = return n
-  go :: Int -> Q Pat
-  go = \case
-    0 -> [p| IZ |]
-    n -> [p| IS $(go $ n-1) |]
-
diff --git a/src/Data/Type/Length.hs b/src/Data/Type/Length.hs
--- a/src/Data/Type/Length.hs
+++ b/src/Data/Type/Length.hs
@@ -29,6 +29,8 @@
 
 module Data.Type.Length where
 
+import Data.Type.Quantifier
+import Type.Class.Higher
 import Type.Class.Known
 import Type.Family.List
 
@@ -36,22 +38,44 @@
   LZ :: Length Ø
   LS :: !(Length as) -> Length (a :< as)
 
-lOdd, lEven :: Length as -> Bool
-lOdd = \case
-  LZ   -> False
-  LS l -> lEven l
-lEven = \case
-  LZ   -> True
-  LS l -> lOdd l
-
 deriving instance Eq   (Length as)
 deriving instance Ord  (Length as)
 deriving instance Show (Length as)
 
+instance Eq1   Length
+instance Ord1  Length
+instance Show1 Length
+
+instance Read1 Length where
+  readsPrec1 d = readParen (d > 10) $ \s0 ->
+    [ (Some LZ,s1)
+    | ("LZ",s1) <- lex s0
+    ] ++
+    [ (l >>- Some . LS,s2)
+    | ("LS",s1) <- lex s0
+    , (l,s2) <- readsPrec1 11 s1
+    ]
+
 instance Known Length Ø where
   known = LZ
 
 instance Known Length as => Known Length (a :< as) where
   type KnownC Length (a :< as) = Known Length as
   known = LS known
+
+elimLength :: p Ø
+           -> (forall x xs. Length xs -> p xs -> p (x :< xs))
+           -> Length as
+           -> p as
+elimLength z s = \case
+  LZ   -> z
+  LS l -> s l $ elimLength z s l
+
+lOdd, lEven :: Length as -> Bool
+lOdd = \case
+  LZ   -> False
+  LS l -> lEven l
+lEven = \case
+  LZ   -> True
+  LS l -> lOdd l
 
diff --git a/src/Data/Type/Nat.hs b/src/Data/Type/Nat.hs
--- a/src/Data/Type/Nat.hs
+++ b/src/Data/Type/Nat.hs
@@ -29,12 +29,13 @@
 module Data.Type.Nat where
 
 import Data.Type.Equality
-import Data.Type.Product
+import Data.Type.Quantifier
+import Type.Class.Higher
 import Type.Class.Known
 import Type.Class.Witness
 import Type.Family.Constraint
-import Type.Family.List
 import Type.Family.Nat
+-- import Type.Class.Categories
 
 data Nat :: N -> * where
   Z_ :: Nat Z
@@ -44,6 +45,20 @@
 deriving instance Ord  (Nat n)
 deriving instance Show (Nat n)
 
+instance Eq1   Nat
+instance Ord1  Nat
+instance Show1 Nat
+
+instance Read1 Nat where
+  readsPrec1 d = readParen (d > 10) $ \s0 ->
+    [ (Some Z_,s1)
+    | ("Z_",s1) <- lex s0
+    ] ++
+    [ (n >>- Some . S_,s2)
+    | ("S_",s1) <- lex s0
+    , (n,s2) <- readsPrec1 11 s1
+    ]
+
 -- | @'Z_'@ is the canonical construction of a @'Nat' Z@.
 instance Known Nat Z where
   known = Z_
@@ -68,16 +83,7 @@
       S_ _ -> Nothing
     S_ x -> \case
       Z_   -> Nothing
-      S_ y -> testEquality x y /? qed
-
-instance DecEquality Nat where
-  decideEquality = \case
-    Z_ -> \case
-      Z_   -> Proven  _Z
-      S_ _ -> Refuted _ZneS
-    S_ x -> \case
-      Z_   -> Refuted $ _ZneS . sym
-      S_ y -> (_S <-> _s) <?> decideEquality x y
+      S_ y -> testEquality x y //? qed
 
 _Z :: Z :~: Z
 _Z = Refl
@@ -123,32 +129,13 @@
   S_ y -> (x .^ y) .* x
 infixl 8 .^
 
-nat :: Nat n -> Int
-nat = \case
-  Z_   -> 0
-  S_ x -> succ $ nat x
-
-n0  :: Nat N0
-n1  :: Nat N1
-n2  :: Nat N2
-n3  :: Nat N3
-n4  :: Nat N4
-n5  :: Nat N5
-n6  :: Nat N6
-n7  :: Nat N7
-n8  :: Nat N8
-n9  :: Nat N9
-n10 :: Nat N10
+elimNat :: p Z -> (forall x. Nat x -> p x -> p (S x)) -> Nat n -> p n
+elimNat z s = \case
+  Z_   -> z
+  S_ x -> s x $ elimNat z s x
 
-n0  = Z_
-n1  = S_ n0
-n2  = S_ n1
-n3  = S_ n2
-n4  = S_ n3
-n5  = S_ n4
-n6  = S_ n5
-n7  = S_ n6
-n8  = S_ n7
-n9  = S_ n8
-n10 = S_ n9
+natVal :: Nat n -> Int
+natVal = \case
+  Z_   -> 0
+  S_ x -> succ $ natVal x
 
diff --git a/src/Data/Type/Nat/Quote.hs b/src/Data/Type/Nat/Quote.hs
deleted file mode 100644
--- a/src/Data/Type/Nat/Quote.hs
+++ /dev/null
@@ -1,89 +0,0 @@
-{-# LANGUAGE QuasiQuotes #-}
-{-# LANGUAGE TemplateHaskell #-}
-{-# LANGUAGE PatternSynonyms #-}
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE GADTs #-}
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Type.Index.Quote
--- Copyright   :  Copyright (C) 2015 Kyle Carter
--- License     :  BSD3
---
--- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
--- Stability   :  experimental
--- Portability :  RankNTypes
---
--- A 'QuasiQuoter' for the 'N' kind and the 'Nat' type.
---
------------------------------------------------------------------------------
-
-module Data.Type.Nat.Quote where
-
-import Data.Type.Nat
-import Type.Family.Nat
-import Language.Haskell.TH
-import Language.Haskell.TH.Quote
-import Control.Monad
-import Text.Read (readMaybe)
-
-n :: QuasiQuoter
-n = QuasiQuoter
-  { quoteExp  = parseNatExp
-  , quotePat  = parseNatPat
-  , quoteType = parseNatType
-  , quoteDec  = error "n: quoteDec not defined"
-  }
-
-parseNatExp :: String -> Q Exp
-parseNatExp s = maybe (fail $ "n: couldn't parse Int: " ++ show s)
-  (notNeg >=> go)
-  $ readMaybe s
-  where
-  notNeg :: Int -> Q Int
-  notNeg n
-    | n < 0 = fail $ "n: negative: " ++ show n
-    | True  = return n
-  go :: Int -> Q Exp
-  go = \case
-    0 -> [| Z_ |]
-    n -> [| S_ $(go $ n-1) |]
-
-parseNatPat :: String -> Q Pat
-parseNatPat s = maybe (fail $ "n: couldn't parse Int: " ++ show s)
-  (notNeg >=> go)
-  $ readMaybe s
-  where
-  notNeg :: Int -> Q Int
-  notNeg n
-    | n < 0 = fail $ "n: negative: " ++ show n
-    | True  = return n
-  go :: Int -> Q Pat
-  go = \case
-    0 -> [p| Z_ |]
-    n -> [p| S_ $(go $ n-1) |]
-
-parseNatType :: String -> Q Type
-parseNatType s = maybe (fail $ "n: couldn't parse Int: " ++ show s)
-  (notNeg >=> go)
-  $ readMaybe s
-  where
-  notNeg :: Int -> Q Int
-  notNeg n
-    | n < 0 = fail $ "n: negative: " ++ show n
-    | True  = return n
-  go :: Int -> Q Type
-  go = \case
-    0 -> [t| Z |]
-    n -> [t| S $(go $ n-1) |]
-
diff --git a/src/Data/Type/Option.hs b/src/Data/Type/Option.hs
--- a/src/Data/Type/Option.hs
+++ b/src/Data/Type/Option.hs
@@ -1,9 +1,9 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE LambdaCase #-}
@@ -29,7 +29,7 @@
 
 module Data.Type.Option where
 
-import Type.Class.HFunctor
+import Type.Class.Higher
 import Type.Class.Known
 import Type.Class.Witness
 import Type.Family.Maybe
@@ -46,18 +46,18 @@
 
 -- | We can take a natural transformation of @(forall x. f x -> g x)@ to
 -- a natural transformation of @(forall mx. 'Option' f mx -> 'Option' g mx)@.
-instance HFunctor Option where
-  map' f = \case
+instance Functor1 Option where
+  map1 f = \case
     Just_ a  -> Just_ $ f a
     Nothing_ -> Nothing_
 
-instance HFoldable Option where
-  foldMap' f = \case
+instance Foldable1 Option where
+  foldMap1 f = \case
     Just_ a  -> f a
     Nothing_ -> mempty
 
-instance HTraversable Option where
-  traverse' f = \case
+instance Traversable1 Option where
+  traverse1 f = \case
     Just_ a  -> Just_ <$> f a
     Nothing_ -> pure Nothing_
 
diff --git a/src/Data/Type/Product.hs b/src/Data/Type/Product.hs
--- a/src/Data/Type/Product.hs
+++ b/src/Data/Type/Product.hs
@@ -1,10 +1,11 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE PatternSynonyms #-}
-{-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE LambdaCase #-}
@@ -38,22 +39,76 @@
 
 module Data.Type.Product where
 
-import Data.Type.Combinator ((:.:)(..),IT(..),I(..))
+import Data.Type.Combinator
+import Data.Type.Conjunction
 import Data.Type.Index
 import Data.Type.Length
-import Type.Class.HFunctor
+import Data.Type.Quantifier
+import Type.Class.Higher
 import Type.Class.Known
 import Type.Class.Witness
 import Type.Family.Constraint
 import Type.Family.List
 
-import Control.Arrow ((&&&))
-
 data Prod (f :: k -> *) :: [k] -> * where
   Ø    :: Prod f Ø
   (:<) :: !(f a) -> !(Prod f as) -> Prod f (a :< as)
 infixr 5 :<
 
+deriving instance ListC (Eq   <$> f <$> as) => Eq   (Prod f as)
+deriving instance
+  ( ListC (Eq   <$> f <$> as)
+  , ListC (Ord  <$> f <$> as)
+  ) => Ord  (Prod f as)
+deriving instance ListC (Show <$> f <$> as) => Show (Prod f as)
+
+instance Eq1 f => Eq1 (Prod f) where
+  eq1 = \case
+    Ø -> \case
+      Ø -> True
+      _ -> False
+    a :< as -> \case
+      b :< bs -> a =#= b && as =#= bs
+      _       -> False
+
+instance Ord1 f => Ord1 (Prod f) where
+  compare1 = \case
+    Ø -> \case
+      Ø -> EQ
+      _ -> LT
+    a :< as -> \case
+      b :< bs -> compare1 a b `mappend` compare1 as bs
+      _       -> GT
+
+instance Show1 f => Show1 (Prod f) where
+  showsPrec1 d = \case
+    Ø -> showString "Ø"
+    a :< as -> showParen (d > 5)
+      $ showsPrec1 6 a
+      . showString " :< "
+      . showsPrec1 6 as
+
+instance Read1 f => Read1 (Prod f) where
+  readsPrec1 d s0 =
+    [ (Some Ø,s1)
+    | ("Ø",s1) <- lex s0
+    ] ++ readParen (d > 5) ( \s1 ->
+      [ (x >>- \a -> xs >>- \as -> Some $ a :< as,s4)
+      | (x,s2) <- readsPrec1 6 s1
+      , (":<",s3) <- lex s2
+      , (xs,s4) <- readsPrec1 5 s3
+      ]
+    ) s0
+
+instance TestEquality f => TestEquality (Prod f) where
+  testEquality = \case
+    Ø -> \case
+      Ø -> qed
+      _ -> Nothing
+    a :< as -> \case
+      b :< bs -> a =?= b //? as =?= bs //? qed
+      _       -> Nothing
+
 -- | Construct a two element Prod.
 --   Since the precedence of (:>) is higher than (:<),
 --   we can conveniently write lists like:
@@ -107,6 +162,24 @@
   Ø       -> id
   a :< as -> (a :<) . append' as
 
+lookup' :: TestEquality f => f a -> Prod (f :&: g) as -> Maybe (g a)
+lookup' a = \case
+  Ø               -> Nothing
+  (b :&: v) :< bs -> witMaybe (a =?= b) (Just v) $ lookup' a bs
+
+lookupPar :: TestEquality f => f a -> Prod (f :*: g) as -> Maybe (Some g)
+lookupPar a = \case
+  Ø               -> Nothing
+  (b :*: v) :< bs -> witMaybe (a =?= b) (Just $ Some v) $ lookupPar a bs
+
+permute :: Known Length bs => (forall x. Index bs x -> Index as x) -> Prod f as -> Prod f bs
+permute f as = permute' f as known
+
+permute' :: (forall x. Index bs x -> Index as x) -> Prod f as -> Length bs -> Prod f bs
+permute' f as = \case
+  LZ   -> Ø
+  LS l -> index (f IZ) as :< permute' (f . IS) as l
+
 -- Tuple {{{
 
 -- | A Prod of simple Haskell types.
@@ -130,6 +203,11 @@
 
 -- }}}
 
+elimProd :: p Ø -> (forall x xs. Index as x -> f x -> p xs -> p (x :< xs)) -> Prod f as -> p as
+elimProd n c = \case
+  Ø       -> n
+  a :< as -> c IZ a $ elimProd n (c . IS) as
+
 onHead' :: (f a -> f b) -> Prod f (a :< as) -> Prod f (b :< as)
 onHead' f (a :< as) = f a :< as
 
@@ -147,30 +225,40 @@
   IZ -> head'
   IS x -> index x . tail'
 
-instance HFunctor Prod where
-  map' f = \case
+select :: Prod (Index as) bs -> Prod f as -> Prod f bs
+select = \case
+  Ø     -> pure Ø
+  x:<xs -> (:<) <$> index x <*> select xs
+
+instance Functor1 Prod where
+  map1 f = \case
     Ø -> Ø
-    a :< as -> f a :< map' f as
+    a :< as -> f a :< map1 f as
 
-instance HIxFunctor Index Prod where
-  imap' f = \case
+instance IxFunctor1 Index Prod where
+  imap1 f = \case
     Ø -> Ø
-    a :< as -> f IZ a :< imap' (f . IS) as
+    a :< as -> f IZ a :< imap1 (f . IS) as
 
-instance HFoldable Prod where
-  foldMap' f = \case
+instance Foldable1 Prod where
+  foldMap1 f = \case
     Ø       -> mempty
-    a :< as -> f a `mappend` foldMap' f as
+    a :< as -> f a `mappend` foldMap1 f as
 
-instance HIxFoldable Index Prod where
-  ifoldMap' f = \case
+instance IxFoldable1 Index Prod where
+  ifoldMap1 f = \case
     Ø       -> mempty
-    a :< as -> f IZ a `mappend` ifoldMap' (f . IS) as
+    a :< as -> f IZ a `mappend` ifoldMap1 (f . IS) as
 
-instance HTraversable Prod where
-  traverse' f = \case
+instance Traversable1 Prod where
+  traverse1 f = \case
     Ø       -> pure Ø
-    a :< as -> (:<) <$> f a <*> traverse' f as
+    a :< as -> (:<) <$> f a <*> traverse1 f as
+
+instance IxTraversable1 Index Prod where
+  itraverse1 f = \case
+    Ø       -> pure Ø
+    a :< as -> (:<) <$> f IZ a <*> itraverse1 (f . IS) as
 
 instance Known (Prod f) Ø where
   known = Ø
diff --git a/src/Data/Type/Product/Dual.hs b/src/Data/Type/Product/Dual.hs
deleted file mode 100644
--- a/src/Data/Type/Product/Dual.hs
+++ /dev/null
@@ -1,184 +0,0 @@
-{-# LANGUAGE PatternSynonyms #-}
-{-# LANGUAGE ViewPatterns #-}
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE GADTs #-}
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Type.Product.Dual
--- Copyright   :  Copyright (C) 2015 Kyle Carter
--- License     :  BSD3
---
--- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
--- Stability   :  experimental
--- Portability :  RankNTypes
---
--- Type combinators for type-level lists,
--- where we have many functors with a single index.
---
------------------------------------------------------------------------------
-
-module Data.Type.Product.Dual where
-
-import Data.Type.Combinator ((:.:)(..),IT(..),I(..))
-import Data.Type.Index
-import Data.Type.Length
-import Type.Class.HFunctor
-import Type.Class.Known
-import Type.Class.Witness
-import Type.Family.Constraint
-import Type.Family.List
-
-import Control.Arrow ((&&&))
-import Data.Monoid ((<>))
-
-data FProd (fs :: [k -> *]) :: k -> * where
-  ØF   :: FProd Ø a
-  (:<<) :: !(f a) -> !(FProd fs a) -> FProd (f :< fs) a
-infixr 5 :<<
-
--- | Construct a two element FProd.
---   Since the precedence of (:>>) is higher than (:<<),
---   we can conveniently write lists like:
---
---   >>> a :<< b :>> c
---
---   Which is identical to:
---
---   >>> a :<< b :<< c :<< Ø
---
-pattern (:>>) :: (f :: k -> *) (a :: k) -> (g :: k -> *) a -> FProd '[f,g] a
-pattern a :>> b = a :<< b :<< ØF
-infix 6 :>>
-
--- | Build a singleton FProd.
-onlyF :: f a -> FProd '[f] a
-onlyF = (:<< ØF)
-
--- | snoc function. insert an element at the end of the FProd.
-(>>:) :: FProd fs a -> f a -> FProd (fs >: f) a
-(>>:) = \case
-  ØF       -> onlyF
-  b :<< as -> (b :<<) . (as >>:)
-infixl 6 >>:
-
-headF :: FProd (f :< fs) a -> f a
-headF (a :<< _) = a
-
-tailF :: FProd (f :< fs) a -> FProd fs a
-tailF (_ :<< as) = as
-
--- | Get all but the last element of a non-empty FProd.
-initF :: FProd (f :< fs) a -> FProd (Init' f fs) a
-initF (a :<< as) = case as of
-  ØF     -> ØF
-  (:<<){} -> a :<< initF as
-
--- | Get the last element of a non-empty FProd.
-lastF :: FProd (f :< fs) a -> Last' f fs a
-lastF (a :<< as) = case as of
-  ØF      -> a
-  (:<<){} -> lastF as
-
--- | Reverse the elements of an FProd.
-reverseF :: FProd fs a -> FProd (Reverse fs) a
-reverseF = \case
-  ØF       -> ØF
-  a :<< as -> reverseF as >>: a
-
--- | Append two FProds.
-appendF :: FProd fs a -> FProd gs a -> FProd (fs ++ gs) a
-appendF = \case
-  ØF       -> id
-  a :<< as -> (a :<<) . appendF as
-
--- | Map over the head of a non-empty FProd.
-onHeadF :: (f a -> g a) -> FProd (f :< fs) a -> FProd (g :< fs) a
-onHeadF f (a :<< as) = f a :<< as
-
--- | Map over the tail of a non-empty FProd.
-onTailF :: (FProd fs a -> FProd gs a) -> FProd (f :< fs) a -> FProd (f :< gs) a
-onTailF f (a :<< as) = a :<< f as
-
-uncurryF :: (f a -> FProd fs a -> r) -> FProd (f :< fs) a -> r
-uncurryF f (a :<< as) = f a as
-
-curryF :: (l ~ (f :< fs)) => (FProd l a -> r) -> f a -> FProd fs a -> r
-curryF f a as = f $ a :<< as
-
-indexF :: Index fs f -> FProd fs a -> f a
-indexF = \case
-  IZ -> headF
-  IS x -> indexF x . tailF
-
--- | If all @f@ in @fs@ are @Functor@s, then @FProd fs@ is a @Functor@.
-instance ListC (Functor <$> fs) => Functor (FProd fs) where
-  fmap f = \case
-    ØF       -> ØF
-    a :<< as -> fmap f a :<< fmap f as
-
--- | If all @f@ in @fs@ are @Foldable@s, then @FProd fs@ is a @Foldable@.
-instance ListC (Foldable <$> fs) => Foldable (FProd fs) where
-  foldMap f = \case
-    ØF       -> mempty
-    a :<< as -> foldMap f a <> foldMap f as
-
--- | If all @f@ in @fs@ are @Traversable@s, then @FProd fs@ is a @Traversable@.
-instance
-  ( ListC (Functor     <$> fs)
-  , ListC (Foldable    <$> fs)
-  , ListC (Traversable <$> fs)
-  ) => Traversable (FProd fs) where
-  traverse f = \case
-    ØF       -> pure ØF
-    a :<< as -> (:<<) <$> traverse f a <*> traverse f as
-
--- | Map over all elements of an FProd with access to the element's index.
-imapF :: (forall f. Index fs f -> f a -> f b)
-  -> FProd fs a -> FProd fs b
-imapF f = \case
-  ØF       -> ØF
-  a :<< as -> f IZ a :<< imapF (f . IS) as
-
--- | Fold over all elements of an FProd with access to the element's index.
-ifoldMapF :: Monoid m
-  => (forall f. Index fs f -> f a -> m)
-  -> FProd fs a -> m
-ifoldMapF f = \case
-  ØF       -> mempty
-  a :<< as -> f IZ a <> ifoldMapF (f . IS) as
-
--- | Traverse over all elements of an FProd with access to the element's index.
-itraverseF :: Applicative g
-  => (forall f. Index fs f -> f a -> g (f b))
-  -> FProd fs a -> g (FProd fs b)
-itraverseF f = \case
-  ØF       -> pure ØF
-  a :<< as -> (:<<) <$> f IZ a <*> itraverseF (f . IS) as
-
-instance Known (FProd Ø) a where
-  known = ØF
-
-instance (Known f a, Known (FProd fs) a) => Known (FProd (f :< fs)) a where
-  type KnownC (FProd (f :< fs)) a = (Known f a, Known (FProd fs) a)
-  known = known :<< known
-
--- | An empty FProd is a no-op Witness.
-instance Witness ØC ØC (FProd Ø a) where
-  r \\ _ = r
-
--- | A non-empty FProd is a Witness if both its head and tail are Witnesses.
-instance (Witness p q (f a), Witness s t (FProd fs a)) => Witness (p,s) (q,t) (FProd (f :< fs) a) where
-  type WitnessC (p,s) (q,t) (FProd (f :< fs) a) = (Witness p q (f a), Witness s t (FProd fs a))
-  r \\ (a :<< as) = r \\ a \\ as
-
diff --git a/src/Data/Type/Product/Lifted.hs b/src/Data/Type/Product/Lifted.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Product/Lifted.hs
@@ -0,0 +1,178 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE GADTs #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Type.Product.Lifted
+-- Copyright   :  Copyright (C) 2015 Kyle Carter
+-- License     :  BSD3
+--
+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
+-- Stability   :  experimental
+-- Portability :  RankNTypes
+--
+-- Type combinators for type-level lists,
+-- where we have many functors with a single index.
+--
+-----------------------------------------------------------------------------
+
+module Data.Type.Product.Lifted where
+
+import Data.Type.Index
+import Type.Class.Known
+import Type.Class.Witness
+import Type.Family.Constraint
+import Type.Family.List
+
+import Data.Monoid ((<>))
+
+data FProd (fs :: [k -> *]) :: k -> * where
+  ØF   :: FProd Ø a
+  (:<<) :: !(f a) -> !(FProd fs a) -> FProd (f :< fs) a
+infixr 5 :<<
+
+-- | Construct a two element FProd.
+--   Since the precedence of (:>>) is higher than (:<<),
+--   we can conveniently write lists like:
+--
+--   >>> a :<< b :>> c
+--
+--   Which is identical to:
+--
+--   >>> a :<< b :<< c :<< Ø
+--
+pattern (:>>) :: (f :: k -> *) (a :: k) -> (g :: k -> *) a -> FProd '[f,g] a
+pattern a :>> b = a :<< b :<< ØF
+infix 6 :>>
+
+-- | Build a singleton FProd.
+onlyF :: f a -> FProd '[f] a
+onlyF = (:<< ØF)
+
+-- | snoc function. insert an element at the end of the FProd.
+(>>:) :: FProd fs a -> f a -> FProd (fs >: f) a
+(>>:) = \case
+  ØF       -> onlyF
+  b :<< as -> (b :<<) . (as >>:)
+infixl 6 >>:
+
+headF :: FProd (f :< fs) a -> f a
+headF (a :<< _) = a
+
+tailF :: FProd (f :< fs) a -> FProd fs a
+tailF (_ :<< as) = as
+
+-- | Get all but the last element of a non-empty FProd.
+initF :: FProd (f :< fs) a -> FProd (Init' f fs) a
+initF (a :<< as) = case as of
+  ØF     -> ØF
+  (:<<){} -> a :<< initF as
+
+-- | Get the last element of a non-empty FProd.
+lastF :: FProd (f :< fs) a -> Last' f fs a
+lastF (a :<< as) = case as of
+  ØF      -> a
+  (:<<){} -> lastF as
+
+-- | Reverse the elements of an FProd.
+reverseF :: FProd fs a -> FProd (Reverse fs) a
+reverseF = \case
+  ØF       -> ØF
+  a :<< as -> reverseF as >>: a
+
+-- | Append two FProds.
+appendF :: FProd fs a -> FProd gs a -> FProd (fs ++ gs) a
+appendF = \case
+  ØF       -> id
+  a :<< as -> (a :<<) . appendF as
+
+-- | Map over the head of a non-empty FProd.
+onHeadF :: (f a -> g a) -> FProd (f :< fs) a -> FProd (g :< fs) a
+onHeadF f (a :<< as) = f a :<< as
+
+-- | Map over the tail of a non-empty FProd.
+onTailF :: (FProd fs a -> FProd gs a) -> FProd (f :< fs) a -> FProd (f :< gs) a
+onTailF f (a :<< as) = a :<< f as
+
+uncurryF :: (f a -> FProd fs a -> r) -> FProd (f :< fs) a -> r
+uncurryF f (a :<< as) = f a as
+
+curryF :: (l ~ (f :< fs)) => (FProd l a -> r) -> f a -> FProd fs a -> r
+curryF f a as = f $ a :<< as
+
+indexF :: Index fs f -> FProd fs a -> f a
+indexF = \case
+  IZ -> headF
+  IS x -> indexF x . tailF
+
+-- | If all @f@ in @fs@ are @Functor@s, then @FProd fs@ is a @Functor@.
+instance ListC (Functor <$> fs) => Functor (FProd fs) where
+  fmap f = \case
+    ØF       -> ØF
+    a :<< as -> fmap f a :<< fmap f as
+
+-- | If all @f@ in @fs@ are @Foldable@s, then @FProd fs@ is a @Foldable@.
+instance ListC (Foldable <$> fs) => Foldable (FProd fs) where
+  foldMap f = \case
+    ØF       -> mempty
+    a :<< as -> foldMap f a <> foldMap f as
+
+-- | If all @f@ in @fs@ are @Traversable@s, then @FProd fs@ is a @Traversable@.
+instance
+  ( ListC (Functor     <$> fs)
+  , ListC (Foldable    <$> fs)
+  , ListC (Traversable <$> fs)
+  ) => Traversable (FProd fs) where
+  traverse f = \case
+    ØF       -> pure ØF
+    a :<< as -> (:<<) <$> traverse f a <*> traverse f as
+
+-- | Map over all elements of an FProd with access to the element's index.
+imapF :: (forall f. Index fs f -> f a -> f b)
+  -> FProd fs a -> FProd fs b
+imapF f = \case
+  ØF       -> ØF
+  a :<< as -> f IZ a :<< imapF (f . IS) as
+
+-- | Fold over all elements of an FProd with access to the element's index.
+ifoldMapF :: Monoid m
+  => (forall f. Index fs f -> f a -> m)
+  -> FProd fs a -> m
+ifoldMapF f = \case
+  ØF       -> mempty
+  a :<< as -> f IZ a <> ifoldMapF (f . IS) as
+
+-- | Traverse over all elements of an FProd with access to the element's index.
+itraverseF :: Applicative g
+  => (forall f. Index fs f -> f a -> g (f b))
+  -> FProd fs a -> g (FProd fs b)
+itraverseF f = \case
+  ØF       -> pure ØF
+  a :<< as -> (:<<) <$> f IZ a <*> itraverseF (f . IS) as
+
+instance Known (FProd Ø) a where
+  known = ØF
+
+instance (Known f a, Known (FProd fs) a) => Known (FProd (f :< fs)) a where
+  type KnownC (FProd (f :< fs)) a = (Known f a, Known (FProd fs) a)
+  known = known :<< known
+
+-- | An empty FProd is a no-op Witness.
+instance Witness ØC ØC (FProd Ø a) where
+  r \\ _ = r
+
+-- | A non-empty FProd is a Witness if both its head and tail are Witnesses.
+instance (Witness p q (f a), Witness s t (FProd fs a)) => Witness (p,s) (q,t) (FProd (f :< fs) a) where
+  type WitnessC (p,s) (q,t) (FProd (f :< fs) a) = (Witness p q (f a), Witness s t (FProd fs a))
+  r \\ (a :<< as) = r \\ a \\ as
+
diff --git a/src/Data/Type/Quantifier.hs b/src/Data/Type/Quantifier.hs
--- a/src/Data/Type/Quantifier.hs
+++ b/src/Data/Type/Quantifier.hs
@@ -1,9 +1,7 @@
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE LambdaCase #-}
@@ -33,8 +31,10 @@
 
 module Data.Type.Quantifier where
 
-import Data.Type.Combinator
+import Type.Family.Constraint
 
+-- Some {{{
+
 data Some (f :: k -> *) :: * where
   Some :: f a -> Some f
 
@@ -55,26 +55,82 @@
 some :: Some f -> (forall a. f a -> r) -> r
 some (Some a) f = f a
 
+(>>-) :: Some f -> (forall a. f a -> r) -> r
+(>>-) = some
+infixl 1 >>-
+
 withSome :: (forall a. f a -> r) -> Some f -> r
 withSome f (Some a) = f a
 
-onSome :: (forall a. f a -> g b) -> Some f -> Some g
+onSome :: (forall a. f a -> g x) -> Some f -> Some g
 onSome f (Some a) = Some (f a)
 
-type Some2 f = Some (Some :.: f)
+-- }}}
 
-pattern Some2 :: f a b -> Some2 f
-pattern Some2 a = Some (Comp (Some a))
+-- Some2 {{{
 
-data All (f :: k -> *) :: * where
-  All :: { instAll :: forall (a :: k). f a } -> All f
+data Some2 (f :: k -> l -> *) :: * where
+  Some2 :: f a b -> Some2 f
 
--- | A data type for natural transformations.
-data (f :: k -> *) :-> (g :: k -> *) where
-  NT :: (forall a. f a -> g a) -> f :-> g
-infixr 4 :->
+some2 :: Some2 f -> (forall a b. f a b -> r) -> r
+some2 (Some2 a) f = f a
 
-data (p :: k -> l -> *) :--> (q :: k -> l -> *) where
-  NT2 :: (forall a b. p a b -> q a b) -> p :--> q
-infixr 4 :-->
+(>>--) :: Some2 f -> (forall a b. f a b -> r) -> r
+(>>--) = some2
+infixl 1 >>--
+
+withSome2 :: (forall a b. f a b -> r) -> Some2 f -> r
+withSome2 f (Some2 a) = f a
+
+onSome2 :: (forall a b. f a b -> g x y) -> Some2 f -> Some2 g
+onSome2 f (Some2 a) = Some2 (f a)
+
+-- }}}
+
+-- Some3 {{{
+
+data Some3 (f :: k -> l -> m -> *) :: * where
+  Some3 :: f a b c -> Some3 f
+
+some3 :: Some3 f -> (forall a b c. f a b c -> r) -> r
+some3 (Some3 a) f = f a
+
+(>>---) :: Some3 f -> (forall a b c. f a b c -> r) -> r
+(>>---) = some3
+infixl 1 >>---
+
+withSome3 :: (forall a b c. f a b c -> r) -> Some3 f -> r
+withSome3 f (Some3 a) = f a
+
+onSome3 :: (forall a b c. f a b c -> g x y z) -> Some3 f -> Some3 g
+onSome3 f (Some3 a) = Some3 (f a)
+
+-- }}}
+
+-- SomeC {{{
+
+data SomeC (c :: k -> Constraint) (f :: k -> *) where
+  SomeC :: c a => f a -> SomeC c f
+
+someC :: SomeC c f -> (forall a. c a => f a -> r) -> r
+someC (SomeC a) f = f a
+
+(>>~) :: SomeC c f -> (forall a. c a => f a -> r) -> r
+(>>~) = someC
+infixl 1 >>~
+
+-- }}}
+
+-- EveryN {{{
+
+data Every (f :: k -> *) :: * where
+  Every :: { instEvery :: forall a. f a } -> Every f
+
+data Every2 (f :: k -> l -> *) :: * where
+  Every2 :: { instEvery2 :: forall a b. f a b } -> Every2 f
+
+data Every3 (f :: k -> l -> m -> *) :: * where
+  Every3 :: { instEvery3 :: forall a b c. f a b c } -> Every3 f
+
+-- }}}
 
diff --git a/src/Data/Type/Sum.hs b/src/Data/Type/Sum.hs
--- a/src/Data/Type/Sum.hs
+++ b/src/Data/Type/Sum.hs
@@ -1,9 +1,10 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE LambdaCase #-}
@@ -31,17 +32,60 @@
 module Data.Type.Sum where
 
 import Data.Type.Index
+import Data.Type.Quantifier
 
-import Type.Class.HFunctor
+import Type.Class.Higher
 import Type.Class.Witness
 
-import Type.Family.Constraint
 import Type.Family.List
 
 data Sum (f :: k -> *) :: [k] -> * where
   InL :: !(f a) -> Sum f (a :< as)
   InR :: !(Sum f as) -> Sum f (a :< as)
 
+deriving instance ListC (Eq   <$> f <$> as) => Eq   (Sum f as)
+deriving instance
+  ( ListC (Eq   <$> f <$> as)
+  , ListC (Ord  <$> f <$> as)
+  ) => Ord  (Sum f as)
+deriving instance ListC (Show <$> f <$> as) => Show (Sum f as)
+
+instance Eq1 f => Eq1 (Sum f) where
+  eq1 = \case
+    InL a -> \case
+      InL b -> a =#= b
+      _     -> False
+    InR a -> \case
+      InR b -> a =#= b
+      _     -> False
+
+instance Ord1 f => Ord1 (Sum f) where
+  compare1 = \case
+    InL a -> \case
+      InL b -> compare1 a b
+      _     -> LT
+    InR a -> \case
+      InR b -> compare1 a b
+      _     -> GT
+
+instance Show1 f => Show1 (Sum f) where
+  showsPrec1 d = showParen (d > 10) . \case
+    InL a -> showString "InL "
+           . showsPrec1 11 a
+    InR b -> showString "InR "
+           . showsPrec1 11 b
+
+instance Read1 f => Read1 (Sum f) where
+  readsPrec1 d = readParen (d > 10) $ \s0 ->
+    [ (a >>- Some . InL,s2)
+    | ("InL",s1) <- lex s0
+    , (a,s2) <- readsPrec1 11 s1
+    ] ++
+    [ (a >>- Some . InR,s2)
+    | ("InR",s1) <- lex s0
+    , (a,s2) <- readsPrec1 11 s1
+    ]
+
 -- | There are no possible values of the type @Sum f Ø@.
 nilSum :: Sum f Ø -> Void
 nilSum = impossible
@@ -71,37 +115,45 @@
     InR s -> index x s
     _     -> Nothing
 
+elimSum :: (forall x xs. f x -> p (x :< xs))
+        -> (forall x xs. Index as x -> p xs -> p (x :< xs))
+        -> Sum f as
+        -> p as
+elimSum t n = \case
+  InL a -> t a
+  InR s -> n IZ $ elimSum t (n . IS) s
+
 -- instances {{{
 
-instance HFunctor Sum where
-  map' f = \case
+instance Functor1 Sum where
+  map1 f = \case
     InL a -> InL $ f a
-    InR s -> InR $ map' f s
+    InR s -> InR $ map1 f s
 
-instance HIxFunctor Index Sum where
-  imap' f = \case
+instance IxFunctor1 Index Sum where
+  imap1 f = \case
     InL a -> InL $ f IZ a
-    InR s -> InR $ imap' (f . IS) s
+    InR s -> InR $ imap1 (f . IS) s
 
-instance HFoldable Sum where
-  foldMap' f = \case
+instance Foldable1 Sum where
+  foldMap1 f = \case
     InL a -> f a
-    InR s -> foldMap' f s
+    InR s -> foldMap1 f s
 
-instance HIxFoldable Index Sum where
-  ifoldMap' f = \case
+instance IxFoldable1 Index Sum where
+  ifoldMap1 f = \case
     InL a -> f IZ a
-    InR s -> ifoldMap' (f . IS) s
+    InR s -> ifoldMap1 (f . IS) s
 
-instance HTraversable Sum where
-  traverse' f = \case
+instance Traversable1 Sum where
+  traverse1 f = \case
     InL a -> InL <$> f a
-    InR s -> InR <$> traverse' f s
+    InR s -> InR <$> traverse1 f s
 
-instance HIxTraversable Index Sum where
-  itraverse' f = \case
+instance IxTraversable1 Index Sum where
+  itraverse1 f = \case
     InL a -> InL <$> f IZ a
-    InR s -> InR <$> itraverse' (f . IS) s
+    InR s -> InR <$> itraverse1 (f . IS) s
 
 instance Witness p q (f a) => Witness p q (Sum f '[a]) where
   type WitnessC p q (Sum f '[a]) = Witness p q (f a)
diff --git a/src/Data/Type/Sum/Dual.hs b/src/Data/Type/Sum/Dual.hs
deleted file mode 100644
--- a/src/Data/Type/Sum/Dual.hs
+++ /dev/null
@@ -1,125 +0,0 @@
-{-# LANGUAGE PatternSynonyms #-}
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE GADTs #-}
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Type.Sum.Dual
--- Copyright   :  Copyright (C) 2015 Kyle Carter
--- License     :  BSD3
---
--- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
--- Stability   :  experimental
--- Portability :  RankNTypes
---
--- 'FSum' is a type combinators for representing disjoint sums of
--- many functors @(fs :: [k -> *])@ at a single index @(a :: k)@.
--- As opposed to one-functor-many-indices 'Sum'.
---
------------------------------------------------------------------------------
-
-module Data.Type.Sum.Dual where
-
-import Data.Type.Index
-
-import Type.Class.HFunctor
-import Type.Class.Witness
-
-import Type.Family.Constraint
-import Type.Family.List
-
-data FSum :: [k -> *] -> k -> * where
-  FInL :: !(f a) -> FSum (f :< fs) a
-  FInR :: !(FSum fs a) -> FSum (f :< fs) a
-
--- | There are no possible values of the type @FSum Ø a@.
-nilSumF :: FSum Ø a -> Void
-nilSumF = impossible
-
--- | Decompose a non-empty FSum into either its head or its tail.
-decompF :: FSum (f :< fs) a -> Either (f a) (FSum fs a)
-decompF = \case
-  FInL a -> Left  a
-  FInR s -> Right s
-
--- | Inject an element into an FSum.
-injF :: (f ∈ fs) => f a -> FSum fs a
-injF = injectFSum elemIndex
-
--- | Project an implicit index out of an FSum.
-prjF :: (f ∈ fs) => FSum fs a -> Maybe (f a)
-prjF = indexF elemIndex
-
--- | Inject an element into an FSum with an explicitly
---   specified Index.
-injectFSum :: Index fs f -> f a -> FSum fs a
-injectFSum = \case
-  IZ   -> FInL
-  IS x -> FInR . injectFSum x
-
--- | Project an explicit index out of an FSum.
-indexF :: Index fs f -> FSum fs a -> Maybe (f a)
-indexF = \case
-  IZ -> \case
-    FInL a -> Just a
-    _      -> Nothing
-  IS x -> \case
-    FInR s -> indexF x s
-    _      -> Nothing
-
-instance ListC (Functor <$> fs) => Functor (FSum fs) where
-  fmap f = \case
-    FInL a -> FInL $ f <$> a
-    FInR s -> FInR $ f <$> s
-
-instance ListC (Foldable <$> fs) => Foldable (FSum fs) where
-  foldMap f = \case
-    FInL a -> foldMap f a
-    FInR s -> foldMap f s
-
-instance
-  ( ListC (Functor     <$> fs)
-  , ListC (Foldable    <$> fs)
-  , ListC (Traversable <$> fs)
-  ) => Traversable (FSum fs) where
-  traverse f = \case
-    FInL a -> FInL <$> traverse f a
-    FInR s -> FInR <$> traverse f s
-
--- | Map over the single element in an FSum
---   with a function that can handle any possible
---   element, along with the element's index.
-imapF :: (forall f. Index fs f -> f a -> f b)
-  -> FSum fs a -> FSum fs b
-imapF f = \case
-  FInL a -> FInL $ f IZ a
-  FInR s -> FInR $ imapF (f . IS) s
-
--- | Fun fact: Since there is exactly one element in
---   an FSum, we don't need the @Monoid@ instance!
-ifoldMapF :: (forall f. Index fs f -> f a -> m)
-  -> FSum fs a -> m
-ifoldMapF f = \case
-  FInL a -> f IZ a
-  FInR s -> ifoldMapF (f . IS) s
-
--- | Another fun fact: Since there is exactly one element in
---   an FSum, we require only a @Functor@ instance on @g@, rather
---   than @Applicative@.
-itraverseF :: Functor g
-  => (forall f. Index fs f -> f a -> g (f b))
-  -> FSum fs a -> g (FSum fs b)
-itraverseF f = \case
-  FInL a -> FInL <$> f IZ a
-  FInR s -> FInR <$> itraverseF (f . IS) s
-
diff --git a/src/Data/Type/Sum/Lifted.hs b/src/Data/Type/Sum/Lifted.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Sum/Lifted.hs
@@ -0,0 +1,119 @@
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE GADTs #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Type.Sum.Lifted
+-- Copyright   :  Copyright (C) 2015 Kyle Carter
+-- License     :  BSD3
+--
+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
+-- Stability   :  experimental
+-- Portability :  RankNTypes
+--
+-- 'FSum' is a type combinators for representing disjoint sums of
+-- many functors @(fs :: [k -> *])@ at a single index @(a :: k)@.
+-- As opposed to one-functor-many-indices 'Sum'.
+--
+-----------------------------------------------------------------------------
+
+module Data.Type.Sum.Lifted where
+
+import Data.Type.Index
+import Type.Class.Witness
+import Type.Family.List
+
+data FSum :: [k -> *] -> k -> * where
+  FInL :: !(f a) -> FSum (f :< fs) a
+  FInR :: !(FSum fs a) -> FSum (f :< fs) a
+
+-- | There are no possible values of the type @FSum Ø a@.
+nilFSum :: FSum Ø a -> Void
+nilFSum = impossible
+
+-- | Decompose a non-empty FSum into either its head or its tail.
+fdecomp :: FSum (f :< fs) a -> Either (f a) (FSum fs a)
+fdecomp = \case
+  FInL a -> Left  a
+  FInR s -> Right s
+
+-- | Inject an element into an FSum.
+finj :: (f ∈ fs) => f a -> FSum fs a
+finj = injectFSum elemIndex
+
+-- | Project an implicit index out of an FSum.
+fprj :: (f ∈ fs) => FSum fs a -> Maybe (f a)
+fprj = findex elemIndex
+
+-- | Inject an element into an FSum with an explicitly
+--   specified Index.
+injectFSum :: Index fs f -> f a -> FSum fs a
+injectFSum = \case
+  IZ   -> FInL
+  IS x -> FInR . injectFSum x
+
+-- | Project an explicit index out of an FSum.
+findex :: Index fs f -> FSum fs a -> Maybe (f a)
+findex = \case
+  IZ -> \case
+    FInL a -> Just a
+    _      -> Nothing
+  IS x -> \case
+    FInR s -> findex x s
+    _      -> Nothing
+
+instance ListC (Functor <$> fs) => Functor (FSum fs) where
+  fmap f = \case
+    FInL a -> FInL $ f <$> a
+    FInR s -> FInR $ f <$> s
+
+instance ListC (Foldable <$> fs) => Foldable (FSum fs) where
+  foldMap f = \case
+    FInL a -> foldMap f a
+    FInR s -> foldMap f s
+
+instance
+  ( ListC (Functor     <$> fs)
+  , ListC (Foldable    <$> fs)
+  , ListC (Traversable <$> fs)
+  ) => Traversable (FSum fs) where
+  traverse f = \case
+    FInL a -> FInL <$> traverse f a
+    FInR s -> FInR <$> traverse f s
+
+-- | Map over the single element in an FSum
+--   with a function that can handle any possible
+--   element, along with the element's index.
+imapFSum :: (forall f. Index fs f -> f a -> f b)
+  -> FSum fs a -> FSum fs b
+imapFSum f = \case
+  FInL a -> FInL $ f IZ a
+  FInR s -> FInR $ imapFSum (f . IS) s
+
+-- | Fun fact: Since there is exactly one element in
+--   an FSum, we don't need the @Monoid@ instance!
+ifoldMapFSum :: (forall f. Index fs f -> f a -> m)
+  -> FSum fs a -> m
+ifoldMapFSum f = \case
+  FInL a -> f IZ a
+  FInR s -> ifoldMapFSum (f . IS) s
+
+-- | Another fun fact: Since there is exactly one element in
+--   an FSum, we require only a @Functor@ instance on @g@, rather
+--   than @Applicative@.
+itraverseFSum :: Functor g
+  => (forall f. Index fs f -> f a -> g (f b))
+  -> FSum fs a -> g (FSum fs b)
+itraverseFSum f = \case
+  FInL a -> FInL <$> f IZ a
+  FInR s -> FInR <$> itraverseFSum (f . IS) s
+
diff --git a/src/Data/Type/Sym.hs b/src/Data/Type/Sym.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Sym.hs
@@ -0,0 +1,66 @@
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE GADTs #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Type.Sym
+-- Copyright   :  Copyright (C) 2015 Kyle Carter
+-- License     :  BSD3
+--
+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
+-- Stability   :  experimental
+-- Portability :  RankNTypes
+--
+-- A @singleton@-esque type for representing type-level Symbols.
+--
+-----------------------------------------------------------------------------
+
+module Data.Type.Sym where
+
+import Type.Class.Higher
+import Type.Class.Known
+import Type.Class.Witness
+import Type.Family.Constraint
+import Type.Family.Symbol
+import Data.Proxy
+
+data Sym :: Symbol -> * where
+  Sym :: KnownSymbol x => Sym x
+
+deriving instance Eq   (Sym x)
+deriving instance Ord  (Sym x)
+
+instance Show (Sym x) where
+  showsPrec d x = showParen (d > 0)
+    $ showString "Sym :: Sym "
+    . shows (symbol x)
+
+instance Eq1   Sym
+instance Ord1  Sym
+instance Show1 Sym
+
+instance TestEquality Sym where
+  testEquality Sym Sym = sameSymbol Proxy Proxy
+
+instance KnownSymbol x => Known Sym x where
+  type KnownC Sym x = KnownSymbol x
+  known = Sym
+
+instance Witness ØC (KnownSymbol x) (Sym x) where
+  r \\ Sym = r
+
+symbol :: Sym x -> String
+symbol x = symbolVal x \\ x
+
diff --git a/src/Data/Type/Vector.hs b/src/Data/Type/Vector.hs
--- a/src/Data/Type/Vector.hs
+++ b/src/Data/Type/Vector.hs
@@ -6,7 +6,7 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE LambdaCase #-}
@@ -44,7 +44,6 @@
 import Data.Type.Nat
 import Data.Type.Product (Prod(..),curry',pattern (:>))
 
-import Type.Class.HFunctor
 import Type.Class.Known
 import Type.Class.Witness
 
@@ -52,18 +51,28 @@
 import Type.Family.List
 import Type.Family.Nat
 
-import Control.Applicative
-import Control.Arrow
-import Control.Monad (join)
 import qualified Data.List as L
 import Data.Monoid
-import qualified Data.Foldable as F
 
 data VT (n :: N) (f :: k -> *) :: k -> * where
   ØV   :: VT Z f a
   (:*) :: !(f a) -> !(VT n f a) -> VT (S n) f a
 infixr 4 :*
 
+elimVT :: p Z
+       -> (forall x. f a -> p x -> p (S x))
+       -> VT n f a
+       -> p n
+elimVT z s = \case
+  ØV      -> z
+  a :* as -> s a $ elimVT z s as
+
+elimV :: p Z
+      -> (forall x. a -> p x -> p (S x))
+      -> V n a
+      -> p n
+elimV z s = elimVT z $ s . getI
+
 type V n = VT n I
 pattern (:+) :: a -> V n a -> V (S n) a
 pattern a :+ as = I a :* as
@@ -151,8 +160,8 @@
 
 withVT :: [f a] -> (forall n. VT n f a -> r) -> r
 withVT as k = case as of
-  []     -> k ØV
-  a : as -> withVT as $ \v -> k $ a :* v
+  []      -> k ØV
+  a : as' -> withVT as' $ \v -> k $ a :* v
 
 withV :: [a] -> (forall n. V n a -> r) -> r
 withV as k = withVT (I <$> as) k
@@ -290,9 +299,9 @@
 mzipWith :: Monoid a => (a -> a -> b) -> [a] -> [a] -> [b]
 mzipWith f as bs = case (as,bs) of
   ([]  ,[]  ) -> []
-  (a:as,[]  ) -> f a      mempty : mzipWith f as []
-  ([]  ,b:bs) -> f mempty b      : mzipWith f [] bs
-  (a:as,b:bs) -> f a      b      : mzipWith f as bs
+  (a:as',[]  ) -> f a      mempty  : mzipWith f as' []
+  ([]   ,b:bs') -> f mempty b      : mzipWith f []  bs'
+  (a:as',b:bs') -> f a      b      : mzipWith f as' bs'
 
 zipLines :: (ShowS -> ShowS -> ShowS) -> ShowS -> ShowS -> ShowS
 zipLines f a b = compose $ L.intersperse (showChar '\n') $ mzipWith
diff --git a/src/Type/Class/HFunctor.hs b/src/Type/Class/HFunctor.hs
deleted file mode 100644
--- a/src/Type/Class/HFunctor.hs
+++ /dev/null
@@ -1,56 +0,0 @@
-{-# LANGUAGE PatternSynonyms #-}
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE GADTs #-}
------------------------------------------------------------------------------
--- |
--- Module      :  Type.Class.HFunctor
--- Copyright   :  Copyright (C) 2015 Kyle Carter
--- License     :  BSD3
---
--- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
--- Stability   :  experimental
--- Portability :  RankNTypes
---
--- Higher order functors, foldables, and traversables,
--- along with their indexed variants.
--- (oh, and bifunctors tacked on for good measure.)
-----------------------------------------------------------------------------
-
-module Type.Class.HFunctor where
-
-class HFunctor (t :: (k -> *) -> l -> *) where
-  -- | Take a natural transformation to a lifted natural transformation.
-  map' :: (forall (a :: k). f a -> g a) -> t f b -> t g b
-
-class HIxFunctor (i :: l -> k -> *) (t :: (k -> *) -> l -> *) | t -> i where
-  imap' :: (forall (a :: k). i b a -> f a -> g a) -> t f b -> t g b
-
-class HFoldable (t :: (k -> *) -> l -> *) where
-  foldMap' :: Monoid m => (forall (a :: k). f a -> m) -> t f b -> m
-
-class HIxFoldable (i :: l -> k -> *) (t :: (k -> *) -> l -> *) | t -> i where
-  ifoldMap' :: Monoid m => (forall (a :: k). i b a -> f a -> m) -> t f b -> m
-
-class (HFunctor t, HFoldable t) => HTraversable (t :: (k -> *) -> l -> *) where
-  traverse' :: Applicative h => (forall (a :: k). f a -> h (g a)) -> t f b -> h (t g b)
-
-class (HIxFunctor i t, HIxFoldable i t) => HIxTraversable (i :: l -> k -> *) (t :: (k -> *) -> l -> *) | t -> i where
-  itraverse' :: Applicative h => (forall (a :: k). i b a -> f a -> h (g a)) -> t f b -> h (t g b)
-
-class HBifunctor (t :: (k -> *) -> (l -> *) -> m -> *) where
-  bimap' :: (forall (a :: k). f a -> h a)
-         -> (forall (a :: l). g a -> i a)
-         -> t f g b
-         -> t h i b
-
diff --git a/src/Type/Class/Higher.hs b/src/Type/Class/Higher.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Class/Higher.hs
@@ -0,0 +1,236 @@
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE GADTs #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Type.Class.Higher
+-- Copyright   :  Copyright (C) 2015 Kyle Carter
+-- License     :  BSD3
+--
+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
+-- Stability   :  experimental
+-- Portability :  RankNTypes
+--
+-- Higher order analogs of type classes from the Prelude.
+----------------------------------------------------------------------------
+
+module Type.Class.Higher where
+
+import Data.Type.Quantifier
+
+-- EqN {{{
+
+class Eq1 (f :: k -> *) where
+  eq1 :: f a -> f a -> Bool
+  default eq1 :: Eq (f a) => f a -> f a -> Bool
+  eq1 = (==)
+  neq1 :: f a -> f a -> Bool
+  neq1 a b = not $ eq1 a b
+
+(=#=) :: Eq1 f => f a -> f a -> Bool
+(=#=) = eq1
+infix 4 =#=
+
+class Eq2 (f :: k -> l -> *) where
+  eq2 :: f a b -> f a b -> Bool
+  default eq2 :: Eq (f a b) => f a b -> f a b -> Bool
+  eq2 = (==)
+  neq2 :: f a b -> f a b -> Bool
+  neq2 a b = not $ eq2 a b
+
+(=##=) :: Eq2 f => f a b -> f a b -> Bool
+(=##=) = eq2
+infix 4 =##=
+
+class Eq3 (f :: k -> l -> m -> *) where
+  eq3 :: f a b c -> f a b c -> Bool
+  default eq3 :: Eq (f a b c ) => f a b c -> f a b c -> Bool
+  eq3 = (==)
+  neq3 :: f a b c -> f a b c -> Bool
+  neq3 a b = not $ eq3 a b
+
+(=###=) :: Eq3 f => f a b c -> f a b c -> Bool
+(=###=) = eq3
+infix 4 =###=
+
+-- }}}
+
+-- OrdN {{{
+
+class Eq1 f => Ord1 (f :: k -> *) where
+  compare1 :: f a -> f a -> Ordering
+  default compare1 :: Ord (f a) => f a -> f a -> Ordering
+  compare1 = compare
+  (<#) :: f a -> f a -> Bool
+  a <# b = compare1 a b == LT
+  (>#) :: f a -> f a -> Bool
+  a ># b = compare1 a b == GT
+  (<=#) :: f a -> f a -> Bool
+  a <=# b = compare1 a b /= GT
+  (>=#) :: f a -> f a -> Bool
+  a >=# b = compare1 a b /= LT
+infix 4 <#, >#, <=#, >=#
+
+class Eq2 f => Ord2 (f :: k -> l -> *) where
+  compare2 :: f a b -> f a b -> Ordering
+  default compare2 :: Ord (f a b) => f a b -> f a b -> Ordering
+  compare2 = compare
+  (<##) :: f a b -> f a b -> Bool
+  a <## b = compare2 a b == LT
+  (>##) :: f a b -> f a b -> Bool
+  a >## b = compare2 a b == GT
+  (<=##) :: f a b -> f a b -> Bool
+  a <=## b = compare2 a b /= GT
+  (>=##) :: f a b -> f a b -> Bool
+  a >=## b = compare2 a b /= LT
+infix 4 <##, >##, <=##, >=##
+
+class Eq3 f => Ord3 (f :: k -> l -> m -> *) where
+  compare3 :: f a b c -> f a b c -> Ordering
+  default compare3 :: Ord (f a b c) => f a b c -> f a b c -> Ordering
+  compare3 = compare
+  (<###) :: f a b c -> f a b c -> Bool
+  a <### b = compare3 a b == LT
+  (>###) :: f a b c -> f a b c -> Bool
+  a >### b = compare3 a b == GT
+  (<=###) :: f a b c -> f a b c -> Bool
+  a <=### b = compare3 a b /= GT
+  (>=###) :: f a b c -> f a b c -> Bool
+  a >=### b = compare3 a b /= LT
+infix 4 <###, >###, <=###, >=###
+
+-- }}}
+
+-- ShowN {{{
+
+class Show1 (f :: k -> *) where
+  showsPrec1 :: Int -> f a -> ShowS
+  default showsPrec1 :: Show (f a) => Int -> f a -> ShowS
+  showsPrec1 = showsPrec
+  show1 :: f a -> String
+  show1 = ($ "") . shows1
+
+shows1 :: Show1 f => f a -> ShowS
+shows1 = showsPrec1 0
+
+
+class Show2 (f :: k -> l -> *) where
+  showsPrec2 :: Int -> f a b -> ShowS
+  default showsPrec2 :: Show (f a b) => Int -> f a b -> ShowS
+  showsPrec2 = showsPrec
+  show2 :: f a b -> String
+  show2 = ($ "") . shows2
+
+shows2 :: Show2 f => f a b -> ShowS
+shows2 = showsPrec2 0
+
+
+class Show3 (f :: k -> l -> m -> *) where
+  showsPrec3 :: Int -> f a b c -> ShowS
+  default showsPrec3 :: Show (f a b c) => Int -> f a b c -> ShowS
+  showsPrec3 = showsPrec
+  show3 :: f a b c -> String
+  show3 = ($ "") . shows3
+
+shows3 :: Show3 f => f a b c -> ShowS
+shows3 = showsPrec3 0
+
+-- }}}
+
+-- ReadN {{{
+
+class Read1 (f :: k -> *) where
+  readsPrec1 :: Int -> ReadS (Some f)
+
+reads1 :: Read1 f => ReadS (Some f)
+reads1 = readsPrec1 0
+
+readMaybe1 :: Read1 f => String -> Maybe (Some f)
+readMaybe1 s = case reads1 s of
+  [(f,"")] -> Just f
+  _        -> Nothing
+
+
+class Read2 (f :: k -> l -> *) where
+  readsPrec2 :: Int -> ReadS (Some2 f)
+
+reads2 :: Read2 f => ReadS (Some2 f)
+reads2 = readsPrec2 0
+
+readMaybe2 :: Read2 f => String -> Maybe (Some2 f)
+readMaybe2 s = case reads2 s of
+  [(f,"")] -> Just f
+  _        -> Nothing
+
+
+class Read3 (f :: k -> l -> m -> *) where
+  readsPrec3 :: Int -> ReadS (Some3 f)
+
+reads3 :: Read3 f => ReadS (Some3 f)
+reads3 = readsPrec3 0
+
+readMaybe3 :: Read3 f => String -> Maybe (Some3 f)
+readMaybe3 s = case reads3 s of
+  [(f,"")] -> Just f
+  _        -> Nothing
+
+-- }}}
+
+-- FunctorN {{{
+
+class Functor1 (t :: (k -> *) -> l -> *) where
+  -- | Take a natural transformation to a lifted natural transformation.
+  map1 :: (forall (a :: k). f a -> g a) -> t f b -> t g b
+
+class IxFunctor1 (i :: l -> k -> *) (t :: (k -> *) -> l -> *) | t -> i where
+  imap1 :: (forall (a :: k). i b a -> f a -> g a) -> t f b -> t g b
+
+-- }}}
+
+-- FoldableN {{{
+
+class Foldable1 (t :: (k -> *) -> l -> *) where
+  foldMap1 :: Monoid m => (forall (a :: k). f a -> m) -> t f b -> m
+
+class IxFoldable1 (i :: l -> k -> *) (t :: (k -> *) -> l -> *) | t -> i where
+  ifoldMap1 :: Monoid m => (forall (a :: k). i b a -> f a -> m) -> t f b -> m
+
+-- }}}
+
+-- TraversableN {{{
+
+class (Functor1 t, Foldable1 t) => Traversable1 (t :: (k -> *) -> l -> *) where
+  traverse1 :: Applicative h => (forall (a :: k). f a -> h (g a)) -> t f b -> h (t g b)
+
+class (IxFunctor1 i t, IxFoldable1 i t) => IxTraversable1 (i :: l -> k -> *) (t :: (k -> *) -> l -> *) | t -> i where
+  itraverse1 :: Applicative h => (forall (a :: k). i b a -> f a -> h (g a)) -> t f b -> h (t g b)
+
+-- }}}
+
+-- BifunctorN {{{
+
+class Bifunctor1 (t :: (k -> *) -> (l -> *) -> m -> *) where
+  bimap1 :: (forall (a :: k). f a -> h a)
+         -> (forall (a :: l). g a -> i a)
+         -> t f g b
+         -> t h i b
+
+class IxBifunctor1 (i :: m -> k -> *) (j :: m -> l -> *) (t :: (k -> *) -> (l -> *) -> m -> *) | t -> i j where
+  ibimap1 :: (forall (a :: k). i b a -> f a -> f' a)
+          -> (forall (a :: l). j b a -> g a -> g' a)
+          -> t f  g  b
+          -> t f' g' b
+
+-- }}}
+
diff --git a/src/Type/Class/Known.hs b/src/Type/Class/Known.hs
--- a/src/Type/Class/Known.hs
+++ b/src/Type/Class/Known.hs
@@ -1,9 +1,8 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE LambdaCase #-}
diff --git a/src/Type/Class/Witness.hs b/src/Type/Class/Witness.hs
--- a/src/Type/Class/Witness.hs
+++ b/src/Type/Class/Witness.hs
@@ -1,3 +1,6 @@
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ConstraintKinds #-}
@@ -47,12 +50,16 @@
 import Type.Family.Constraint
 
 import Data.Type.Equality as Exports
-import Data.Void          as Exports
+import Data.Void          as Exports hiding (absurd)
+import qualified Data.Void as Void
 
 import Prelude hiding (id,(.))
 import Control.Category
+import Control.Arrow
 import Unsafe.Coerce
 
+-- Wit {{{
+
 -- | A reified 'Constraint'.
 data Wit :: Constraint -> * where
   Wit :: c => Wit c
@@ -60,6 +67,10 @@
 data Wit1 :: (k -> Constraint) -> k -> * where
   Wit1 :: c a => Wit1 c a
 
+-- }}}
+
+-- (:-) {{{
+
 -- | Reified evidence of 'Constraint' entailment.
 --
 -- Given a term of @p :- q@, the Constraint @q@ holds
@@ -77,9 +88,10 @@
   id              = Sub Wit
   Sub bc . Sub ab = Sub $ bc \\ ab
 
-type (:-:) = Bij (:-)
-infixr 4 :-:
+-- }}}
 
+-- Witness {{{
+
 -- | A general eliminator for entailment.
 --
 -- Given a term of type @t@ with an instance @Witness p q t@
@@ -94,17 +106,96 @@
   (\\) :: p => (q => r) -> t -> r
 infixl 1 \\
 
+-- | Convert a 'Witness' to a canonical reified 'Constraint'.
+witnessed :: Witness ØC q t => t -> Wit q
+witnessed t = Wit \\ t
+
 -- | Convert a 'Witness' to a canonical reified entailment.
 entailed :: Witness p q t => t -> p :- q
 entailed t = Sub (Wit \\ t)
 
--- | Convert a 'Witness' to a canonical reified 'Constraint'.
-witnessed :: Witness ØC q t => t -> Wit q
-witnessed t = Wit \\ t
+-- }}}
 
+-- Constraint Combinators {{{
+
+class Fails (c :: Constraint) where
+  failC :: c :- Fail
+
+absurdC :: Fails a => a :- b
+absurdC = contraC failC
+
+class c => Const (c :: Constraint) (d :: k) where
+  constC :: Wit c
+
+instance c => Const c d where
+  constC = Wit
+
+class f (g a) => (∘) (f :: l -> Constraint) (g :: k -> l) (a :: k) where
+  compC :: Wit (f (g a))
+
+instance f (g a) => (f ∘ g) a where
+  compC = Wit
+infixr 9 ∘
+
+class (f a,g a) => (∧) (f :: k -> Constraint) (g :: k -> Constraint) (a :: k) where
+  conjC :: (Wit (f a),Wit (g a))
+infixr 7 ∧
+
+instance (f a,g a) => (f ∧ g) a where
+  conjC = (Wit,Wit)
+
+class (∨) (f :: k -> Constraint) (g :: k -> Constraint) (a :: k) where
+  disjC :: Either (Wit (f a)) (Wit (g a))
+infixr 6 ∨
+
+eitherC :: forall f g a b. f a :- b -> g a :- b -> (f ∨ g) a :- b
+eitherC f g = Sub $ case ((disjC :: Either (Wit (f a)) (Wit (g a))),f,g) of
+  (Left  a,Sub b,_    ) -> b \\ a
+  (Right a,_    ,Sub b) -> b \\ a
+
+pureC :: b => a :- b
+pureC = Sub Wit
+
+contraC :: a :- Fail -> a :- b
+contraC = (bottom .)
+
+-- }}}
+
+-- Forall {{{
+
+class Forall (p :: k -> Constraint) (q :: k -> Constraint) where
+  forall :: p a :- q a
+  default forall :: q a => p a :- q a
+  forall = pureC
+
+-- }}}
+
+-- Initial/Terminal {{{
+
+commute :: (a ~ b) :- (b ~ a)
+commute = Sub Wit
+
+type family Holds (b :: Bool) (c :: Constraint) :: Constraint where
+  Holds True  c = c
+  Holds False c = ØC
+
+falso :: (b ~ False) :- Holds b c
+falso = Sub Wit
+
+top :: a :- ØC
+top = Sub Wit
+
+type Fail = (True ~ False)
+
+bottom :: Fail :- c
+bottom = falso
+
 instance Witness ØC c (Wit c) where
   r \\ Wit = r
 
+instance Witness ØC (c a) (Wit1 c a) where
+  r \\ Wit1 = r
+
 -- | An entailment @p :- q@ is a Witness of @q@, given @p@.
 instance Witness p q (p :- q) where
   r \\ Sub Wit = r
@@ -119,19 +210,43 @@
   type KnownC Wit c = c
   known = Wit
 
+instance c a => Known (Wit1 c) a where
+  type KnownC (Wit1 c) a = c a
+  known = Wit1
+
 -- | Constraint chaining under @Maybe@.
-(/?) :: (Witness p q t, p) => Maybe t -> (q => Maybe r) -> Maybe r
-(/?) = \case
+(//?) :: (Witness p q t, p) => Maybe t -> (q => Maybe r) -> Maybe r
+(//?) = \case
   Just t -> (\\ t)
   _      -> \_ -> Nothing
-infixr 0 /?
+infixr 0 //?
 
+witMaybe :: (Witness p q t, p) => Maybe t -> (q => Maybe r) -> Maybe r -> Maybe r
+witMaybe mt y n = case mt of
+  Just t -> y \\ t
+  _      -> n
+
 qed :: Maybe (a :~: a)
 qed = Just Refl
 
 impossible :: a -> Void
 impossible = unsafeCoerce
 
+(=?=) :: TestEquality f => f a -> f b -> Maybe (a :~: b)
+(=?=) = testEquality
+infix 4 =?=
+
+class TestEquality1 (f :: k -> l -> *) where
+  testEquality1 :: f a c -> f b c -> Maybe (a :~: b)
+
+(=??=) :: TestEquality1 f => f a c -> f b c -> Maybe (a :~: b)
+(=??=) = testEquality1
+infix 4 =??=
+
+-- }}}
+
+-- Dec {{{
+
 data Dec a
   = Proven   a
   | Refuted (a -> Void)
@@ -147,22 +262,14 @@
   Proven  a -> y a
   Refuted b -> n b
 
-data Bij p a b = Bij
-  { fwd :: p a b
-  , bwd :: p b a
-  }
-
-($->) :: Bij p a b -> p a b
-($->) = fwd
-(<-$) :: Bij p a b -> p b a
-(<-$) = bwd
-infixr 1 $->, <-$
+-- }}}
 
-instance Category p => Category (Bij p) where
-  id    = Bij id id
-  g . f = Bij (fwd g . fwd f) (bwd f . bwd g)
+absurd :: Arrow p => p Void a
+absurd = arr Void.absurd
 
 {-
+-- Category Classes {{{
+
 class Category c => Monoidal (c :: k -> k -> *) where
   type Tensor c :: k -> k -> k
   type Unit   c :: k
@@ -197,17 +304,7 @@
 (***) :: Monoidal p => Bij p a b -> Bij p c d -> Bij p (Tensor p a c) (Tensor p b d)
 f *** g = (fwd f .*. fwd g) <-> (bwd f .*. bwd g)
 infixr 3 ***
--}
 
-type (<->) = Bij (->)
-infixr 5 <->
-
-(<->) :: p a b -> p b a -> Bij p a b
-(<->) = Bij
-
-(<?>) :: r <-> s -> Dec r -> Dec s
-(<?>) p = \case
-  Proven  a -> Proven  $ p $-> a
-  Refuted f -> Refuted $ \a -> f $ p <-$ a
-infix 3 <?>
+-- }}}
+-}
 
diff --git a/src/Type/Family/Either.hs b/src/Type/Family/Either.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Family/Either.hs
@@ -0,0 +1,105 @@
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE GADTs #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Type.Family.Either
+-- Copyright   :  Copyright (C) 2015 Kyle Carter
+-- License     :  BSD3
+--
+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
+-- Stability   :  experimental
+-- Portability :  RankNTypes
+--
+-- Convenient type families for working with type-level @Either@s.
+----------------------------------------------------------------------------
+
+module Type.Family.Either where
+
+import Type.Family.Constraint
+import Type.Family.Monoid
+import Type.Class.Witness
+
+-- | Take a @Maybe Constraint@ to a @Constraint@.
+type family EitherC (ec :: Either k Constraint) :: Constraint where
+  EitherC (Left  a) = ØC
+  EitherC (Right c) = c
+
+type family IsLeft (a :: Either k l) :: Bool where
+  IsLeft (Left  a) = True
+  IsLeft (Right b) = False
+
+type family IsRight (a :: Either k l) :: Bool where
+  IsRight (Left  a) = False
+  IsRight (Right b) = True
+
+leftCong :: (a ~ b) :- (IsLeft a ~ IsLeft b)
+leftCong = Sub Wit
+
+rightCong :: (a ~ b) :- (IsRight a ~ IsRight b)
+rightCong = Sub Wit
+
+leftNotRight :: (Left a ~ Right b) :- Fail
+leftNotRight = leftCong
+
+-- | Map over a type-level @Maybe@.
+type family (f :: k -> l) <$> (a :: Either m k) :: Either m l where
+  f <$> Left  a = Left a
+  f <$> Right b = Right (f b)
+infixr 4 <$>
+
+eitherFmapCong :: (f ~ g,a ~ b) :- ((f <$> a) ~ (g <$> b))
+eitherFmapCong = Sub Wit
+
+type family (f :: Either m (k -> l)) <&> (a :: k) :: Either m l where
+  Left  x <&> a = Left x
+  Right f <&> a = Right (f a)
+infixl 5 <&>
+
+eitherPamfCong :: (f ~ g,a ~ b) :- ((f <&> a) ~ (g <&> b))
+eitherPamfCong = Sub Wit
+
+type family (f :: Either m (k -> l)) <*> (a :: Either m k) :: Either m l where
+  Left  x <*> Left y  = Left (x <> y)
+  Left  x <*> a       = Left x
+  f       <*> Left x  = Left x
+  Right f <*> Right a = Right (f a)
+infixr 4 <*>
+
+eitherApCong :: (f ~ g,a ~ b) :- ((f <*> a) ~ (g <*> b))
+eitherApCong = Sub Wit
+
+type family (a :: Either m k) <|> (b :: Either m k) :: Either m k where
+  Left  x <|> b = b
+  Right a <|> b = Right a
+infixr 4 <|>
+
+eitherAltCong :: (a ~ c,b ~ d) :- ((a <|> b) ~ (c <|> d))
+eitherAltCong = Sub Wit
+
+type family FromLeft (e :: Either k l) :: k where
+  FromLeft (Left a) = a
+
+type family FromRight (e :: Either k l) :: l where
+  FromRight (Right b) = b
+
+fromLeftCong :: (a ~ b) :- (FromLeft a ~ FromLeft b)
+fromLeftCong = Sub Wit
+
+fromRightCong :: (a ~ b) :- (FromRight a ~ FromRight b)
+fromRightCong = Sub Wit
+
+type instance Mempty = Left Mempty
+type instance a <> b = a <|> b
+
diff --git a/src/Type/Family/List.hs b/src/Type/Family/List.hs
--- a/src/Type/Family/List.hs
+++ b/src/Type/Family/List.hs
@@ -26,16 +26,12 @@
 -- type-level lists.
 ----------------------------------------------------------------------------
 
-module Type.Family.List
-  ( module Type.Family.List
-  , (==)
-  ) where
+module Type.Family.List where
 
 import Type.Family.Constraint
 import Type.Family.Monoid
-
-import Data.Type.Bool
-import Data.Type.Equality
+import Type.Family.Tuple hiding (type (<$>),type (<*>),type (<&>))
+import Type.Class.Witness
 
 type Ø    = '[]
 type (:<) = '(:)
@@ -44,30 +40,79 @@
 -- | Type-level singleton list.
 type Only a = '[a]
 
+-- Null,Append {{{
+
+type family Null (as :: [k]) :: Bool where
+  Null Ø         = True
+  Null (a :< as) = False
+
+nullCong :: (a ~ b) :- (Null a ~ Null b)
+nullCong = Sub Wit
+
+nilNotCons :: (Ø ~ (a :< as)) :- Fail
+nilNotCons = nullCong
+
 -- | Appends two type-level lists.
 type family (as :: [k]) ++ (bs :: [k]) :: [k] where
   Ø         ++ bs = bs
   (a :< as) ++ bs = a :< (as ++ bs)
 infixr 5 ++
 
+appendCong :: (a ~ b,c ~ d) :- ((a ++ c) ~ (b ++ d))
+appendCong = Sub Wit
+
+-- }}}
+
+-- Snoc,Reverse {{{
+
 -- | Type-level list snoc.
 type family (as :: [k]) >: (a :: k) :: [k] where
   Ø         >: a = Only a
   (b :< as) >: a = b :< (as >: a)
 infixl 6 >:
 
+snocCong :: (as ~ bs,a ~ b) :- ((as >: a) ~ (bs >: b))
+snocCong = Sub Wit
+
 type family Reverse (as :: [k]) :: [k] where
   Reverse  Ø        = Ø
   Reverse (a :< as) = Reverse as >: a
 
+reverseCong :: (as ~ bs) :- (Reverse as ~ Reverse bs)
+reverseCong = Sub Wit
+
+-- }}}
+
+-- Head,Tail,Init,Last {{{
+
+type family Head (as :: [k]) :: k where
+  Head (a :< as) = a
+
+type family Tail (as :: [k]) :: [k] where
+  Tail (a :< as) = as
+
+type family Init (as :: [k]) :: [k] where
+  Init (a :< as) = Init' a as
+
 type family Init' (a :: k) (as :: [k]) :: [k] where
   Init' a Ø = Ø
   Init' a (b :< as) = a :< Init' b as
 
+initCong :: (a ~ b,as ~ bs) :- (Init' a as ~ Init' b bs)
+initCong = Sub Wit
+
+type family Last (as :: [k]) :: k where
+  Last (a :< as) = Last' a as
+
 type family Last' (a :: k) (as :: [k]) :: k where
   Last' a Ø         = a
   Last' a (b :< as) = Last' b as
 
+lastCong :: (a ~ b,as ~ bs) :- (Last' a as ~ Last' b bs)
+lastCong = Sub Wit
+
+-- }}}
+
 -- | Takes a type-level list of 'Constraint's to a single
 -- 'Constraint', where @ListC cs@ holds iff all elements
 -- of @cs@ hold.
@@ -75,6 +120,8 @@
   ListC  Ø        = ØC
   ListC (c :< cs) = (c, ListC cs)
 
+-- Map et al {{{
+
 -- | Map an @(f :: k -> l)@ over a type-level list @(as :: [k])@,
 -- giving a list @(bs :: [l])@.
 type family (f :: k -> l) <$> (a :: [k]) :: [l] where
@@ -82,6 +129,9 @@
   f <$> (a :< as) = f a :< (f <$> as)
 infixr 4 <$>
 
+listMapCong :: (f ~ g,as ~ bs) :- ((f <$> as) ~ (g <$> bs))
+listMapCong = Sub Wit
+
 -- | Map a list of @(fs :: [k -> l])@ over a single @(a :: k)@,
 -- giving a list @(bs :: [l])@.
 type family (f :: [k -> l]) <&> (a :: k) :: [l] where
@@ -93,6 +143,36 @@
   fs <*> Ø         = Ø
   fs <*> (a :< as) = (fs <&> a) ++ (fs <*> as)
 infixr 4 <*>
+
+-- }}}
+
+-- Tuples {{{
+
+type family Fsts (ps :: [(k,l)]) :: [k] where
+  Fsts  Ø        = Ø
+  Fsts (p :< ps) = Fst p :< Fsts ps
+
+type family Snds (ps :: [(k,l)]) :: [l] where
+  Snds  Ø        = Ø
+  Snds (p :< ps) = Snd p :< Snds ps
+
+type family Zip (as :: [k]) (bs :: [l]) :: [(k,l)] where
+  Zip  Ø         Ø        = Ø
+  Zip (a :< as) (b :< bs) = a#b :< Zip as bs
+
+type family Fsts3 (ps :: [(k,l,m)]) :: [k] where
+  Fsts3  Ø        = Ø
+  Fsts3 (p :< ps) = Fst3 p :< Fsts3 ps
+
+type family Snds3 (ps :: [(k,l,m)]) :: [l] where
+  Snds3  Ø        = Ø
+  Snds3 (p :< ps) = Snd3 p :< Snds3 ps
+
+type family Thds3 (ps :: [(k,l,m)]) :: [m] where
+  Thds3  Ø        = Ø
+  Thds3 (p :< ps) = Thd3 p :< Thds3 ps
+
+-- }}}
 
 type instance Mempty = Ø
 type instance a <> b = a ++ b
diff --git a/src/Type/Family/Maybe.hs b/src/Type/Family/Maybe.hs
--- a/src/Type/Family/Maybe.hs
+++ b/src/Type/Family/Maybe.hs
@@ -25,46 +25,67 @@
 -- Convenient type families for working with type-level @Maybe@s.
 ----------------------------------------------------------------------------
 
-module Type.Family.Maybe
-  ( module Type.Family.Maybe
-  , type (==)
-  ) where
+module Type.Family.Maybe where
 
 import Type.Family.Constraint
 import Type.Family.Monoid
-
-import Data.Type.Equality
+import Type.Class.Witness
 
 -- | Take a @Maybe Constraint@ to a @Constraint@.
 type family MaybeC (mc :: Maybe Constraint) :: Constraint where
   MaybeC Nothing  = ØC
   MaybeC (Just c) = c
 
+type family IsNothing (a :: Maybe k) :: Bool where
+  IsNothing Nothing  = True
+  IsNothing (Just a) = False
+
+nothingCong :: (a ~ b) :- (IsNothing a ~ IsNothing b)
+nothingCong = Sub Wit
+
+nothingNotJust :: (Nothing ~ Just a) :- Fail
+nothingNotJust = nothingCong
+
 -- | Map over a type-level @Maybe@.
 type family (f :: k -> l) <$> (a :: Maybe k) :: Maybe l where
   f <$> Nothing = Nothing
   f <$> Just a  = Just (f a)
 infixr 4 <$>
 
+maybeFmapCong :: (f ~ g,a ~ b) :- ((f <$> a) ~ (g <$> b))
+maybeFmapCong = Sub Wit
+
 type family (f :: Maybe (k -> l)) <&> (a :: k) :: Maybe l where
   Nothing <&> a = Nothing
   Just f  <&> a = Just (f a)
 infixl 5 <&>
 
+maybePamfCong :: (f ~ g,a ~ b) :- ((f <&> a) ~ (g <&> b))
+maybePamfCong = Sub Wit
+
 type family (f :: Maybe (k -> l)) <*> (a :: Maybe k) :: Maybe l where
   Nothing <*> a       = Nothing
   f       <*> Nothing = Nothing
   Just f  <*> Just a  = Just (f a)
 infixr 4 <*>
 
+maybeApCong :: (f ~ g,a ~ b) :- ((f <*> a) ~ (g <*> b))
+maybeApCong = Sub Wit
+
 type family (a :: Maybe k) <|> (b :: Maybe k) :: Maybe k where
   Nothing <|> a       = a
   a       <|> Nothing = a
   Just a  <|> Just b  = Just a
 infixr 4 <|>
 
+maybeAltCong :: (a ~ c,b ~ d) :- ((a <|> b) ~ (c <|> d))
+maybeAltCong = Sub Wit
+
 type family FromJust (m :: Maybe k) :: k where
   FromJust (Just a) = a
+
+fromJustCong :: (a ~ b) :- (FromJust a ~ FromJust b)
+fromJustCong = Sub Wit
 
 type instance Mempty = Nothing
 type instance a <> b = a <|> b
diff --git a/src/Type/Family/Nat.hs b/src/Type/Family/Nat.hs
--- a/src/Type/Family/Nat.hs
+++ b/src/Type/Family/Nat.hs
@@ -27,19 +27,33 @@
 --
 -----------------------------------------------------------------------------
 
-module Type.Family.Nat
-  ( module Type.Family.Nat
-  , type (==)
-  ) where
+module Type.Family.Nat where
 
 import Data.Type.Equality
 import Type.Family.List
+import Type.Class.Witness
 
 data N
   = Z
   | S N
   deriving (Eq,Ord,Show)
 
+fromInt :: Int -> Maybe N
+fromInt n = case compare n 0 of
+  LT -> Nothing
+  EQ -> Just Z
+  GT -> S <$> fromInt (n-1)
+
+type family IsZero (x :: N) :: Bool where
+  IsZero Z     = True
+  IsZero (S x) = False
+
+zeroCong :: (x ~ y) :- (IsZero x ~ IsZero y)
+zeroCong = Sub Wit
+
+zNotS :: (Z ~ S x) :- Fail
+zNotS = zeroCong
+
 type family NatEq (x :: N) (y :: N) :: Bool where
   NatEq  Z     Z    = True
   NatEq  Z    (S y) = False
@@ -51,23 +65,52 @@
   Iota Z     = Ø
   Iota (S x) = x :< Iota x
 
+iotaCong :: (x ~ y) :- (Iota x ~ Iota y)
+iotaCong = Sub Wit
+
 type family Pred (x :: N) :: N where
   Pred (S n) = n
 
+predCong :: (x ~ y) :- (Pred x ~ Pred y)
+predCong = Sub Wit
+
 type family (x :: N) + (y :: N) :: N where
   Z   + y = y
   S x + y = S (x + y)
 infixr 6 +
 
+addCong :: (w ~ y,x ~ z) :- ((w + x) ~ (y + z))
+addCong = Sub Wit
+
 type family (x :: N) * (y :: N) :: N where
   Z   * y = Z
   S x * y = (x * y) + y
 infixr 7 *
 
+mulCong :: (w ~ y,x ~ z) :- ((w * x) ~ (y * z))
+mulCong = Sub Wit
+
 type family (x :: N) ^ (y :: N) :: N where
   x ^   Z = S Z
   x ^ S y = (x ^ y) * x
 infixl 8 ^
+
+expCong :: (w ~ y,x ~ z) :- ((w ^ x) ~ (y ^ z))
+expCong = Sub Wit
+
+type family Len (as :: [k]) :: N where
+  Len  Ø        = Z
+  Len (a :< as) = S (Len as)
+
+lenCong :: (as ~ bs) :- (Len as ~ Len bs)
+lenCong = Sub Wit
+
+type family Ix (x :: N) (as :: [k]) :: k where
+  Ix Z     (a :< as) = a
+  Ix (S x) (a :< as) = Ix x as
+
+ixCong :: (x ~ y,as ~ bs) :- (Ix x as ~ Ix y bs)
+ixCong = Sub Wit
 
 -- | Convenient aliases for low-value Peano numbers.
 type N0  = Z
diff --git a/src/Type/Family/Symbol.hs b/src/Type/Family/Symbol.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Family/Symbol.hs
@@ -0,0 +1,7 @@
+
+module Type.Family.Symbol
+  ( module GHC.TypeLits
+  ) where
+
+import GHC.TypeLits (Symbol,KnownSymbol,sameSymbol,symbolVal)
+
diff --git a/src/Type/Family/Tuple.hs b/src/Type/Family/Tuple.hs
--- a/src/Type/Family/Tuple.hs
+++ b/src/Type/Family/Tuple.hs
@@ -30,20 +30,54 @@
 module Type.Family.Tuple where
 
 import Type.Family.Monoid
+import Type.Class.Witness
 
 type (#) = '(,)
 infixr 6 #
 
+-- Fst,Snd,Thd et al {{{
+
 type family Fst (p :: (k,l)) :: k where
   Fst '(a,b) = a
 
+fstCong :: (p ~ q) :- (Fst p ~ Fst q)
+fstCong = Sub Wit
+
 type family Snd (p :: (k,l)) :: l where
   Snd '(a,b) = b
 
+sndCong :: (p ~ q) :- (Snd p ~ Snd q)
+sndCong = Sub Wit
+
+type family Fst3 (p :: (k,l,m)) :: k where
+  Fst3 '(a,b,c) = a
+
+fst3Cong :: (p ~ q) :- (Fst3 p ~ Fst3 q)
+fst3Cong = Sub Wit
+
+type family Snd3 (p :: (k,l,m)) :: l where
+  Snd3 '(a,b,c) = b
+
+snd3Cong :: (p ~ q) :- (Snd3 p ~ Snd3 q)
+snd3Cong = Sub Wit
+
+type family Thd3 (p :: (k,l,m)) :: m where
+  Thd3 '(a,b,c) = c
+
+thd3Cong :: (p ~ q) :- (Thd3 p ~ Thd3 q)
+thd3Cong = Sub Wit
+
+-- }}}
+
+-- Map et al {{{
+
 type family (f :: k -> l) <$> (a :: (m,k)) :: (m,l) where
   f <$> (a#b) = a # f b
 infixr 4 <$>
 
+pairMapCong :: (f ~ g,a ~ b) :- ((f <$> a) ~ (g <$> b))
+pairMapCong = Sub Wit
+
 type family (f :: (m,k -> l)) <&> (a :: k) :: (m,l) where
   (r#f) <&> a = r # f a
 infixr 4 <&>
@@ -52,18 +86,11 @@
   (r#f) <*> (s#a) = (r <> s) # f a
 infixr 4 <*>
 
+-- }}}
+
 -- | A type-level pair is a Monoid over its pairwise components.
 type instance Mempty = Mempty # Mempty
 type instance (r#a) <> (s#b) = (r <> s) # (a <> b)
-
-type family Fst3 (p :: (k,l,m)) :: k where
-  Fst3 '(a,b,c) = a
-
-type family Snd3 (p :: (k,l,m)) :: l where
-  Snd3 '(a,b,c) = b
-
-type family Thd3 (p :: (k,l,m)) :: m where
-  Thd3 '(a,b,c) = c
 
 type instance Mempty = '(Mempty,Mempty,Mempty)
 type instance '(a,b,c) <> '(d,e,f) = '(a<>d,b<>e,c<>f)
diff --git a/type-combinators.cabal b/type-combinators.cabal
--- a/type-combinators.cabal
+++ b/type-combinators.cabal
@@ -1,5 +1,5 @@
 name: type-combinators
-version: 0.1.2.1
+version: 0.2.0.0
 category: Data
 synopsis: A collection of data types for type-level programming
 cabal-version: >=1.10
@@ -21,32 +21,30 @@
         Data.Type.Disjunction
         Data.Type.Fin
         Data.Type.Index
-        Data.Type.Index.Quote
         Data.Type.Length
         Data.Type.Nat
-        Data.Type.Nat.Quote
         Data.Type.Option
         Data.Type.Product
-        Data.Type.Product.Dual
+        Data.Type.Product.Lifted
         Data.Type.Sum
-        Data.Type.Sum.Dual
+        Data.Type.Sum.Lifted
+        Data.Type.Sym
         Data.Type.Quantifier
         Data.Type.Vector
-        Type.Class.HFunctor
+        Type.Class.Higher
         Type.Class.Known
         Type.Class.Witness
         Type.Family.Constraint
+        Type.Family.Either
         Type.Family.List
         Type.Family.Maybe
         Type.Family.Monoid
         Type.Family.Nat
+        Type.Family.Symbol
         Type.Family.Tuple
     build-depends:
-        base >=4.8 && <4.9,
-        containers,
-        template-haskell,
-        transformers,
-        mtl
+        base >=4.8 && <4.9
     default-language: Haskell2010
     hs-source-dirs: src
+    ghc-options: -Wall -fno-warn-unticked-promoted-constructors