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
@@ -34,6 +34,7 @@
 import Type.Class.HFunctor
 import Type.Class.Known
 import Type.Class.Witness
+import Type.Family.Tuple
 
 import Control.Applicative
 
@@ -293,6 +294,66 @@
 
 flipped :: (f a b -> g c d) -> Flip f b a -> Flip g d c
 flipped f = Flip . f . getFlip
+
+-- }}}
+
+-- Cur {{{
+
+newtype Cur (p :: (k,l) -> *) :: k -> l -> * where
+  Cur :: { getCur :: p (a#b) } -> 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
+
+instance Witness q r (p (a#b)) => Witness q r (Cur p a b) where
+  type WitnessC q r (Cur p a b) = Witness q r (p (a#b))
+  r \\ Cur p = r \\ p
+
+-- }}}
+
+-- Uncur {{{
+
+data Uncur (p :: k -> l -> *) :: (k,l) -> * where
+  Uncur :: { getUncur :: p a b } -> Uncur p (a#b)
+
+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
+
+instance (Witness r s (p a b),q ~ (a#b)) => Witness r s (Uncur p q) where
+  type WitnessC r s (Uncur p q) = Witness r s (p (Fst q) (Snd q))
+  r \\ Uncur p = r \\ p
+
+-- }}}
+
+-- Cur {{{
+
+newtype Cur3 (p :: (k,l,m) -> *) :: k -> l -> m -> * where
+  Cur3 :: { getCur3 :: p '(a,b,c) } -> 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
+
+instance Witness q r (p '(a,b,c)) => Witness q r (Cur3 p a b c) where
+  type WitnessC q r (Cur3 p a b c) = Witness q r (p '(a,b,c))
+  r \\ Cur3 p = r \\ p
+
+-- }}}
+
+-- Uncur3 {{{
+
+data Uncur3 (p :: k -> l -> m -> *) :: (k,l,m) -> * where
+  Uncur3 :: { getUncur3 :: p a b c } -> Uncur3 p '(a,b,c)
+
+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
+
+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
 
 -- }}}
 
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
@@ -35,7 +35,7 @@
 import Type.Class.HFunctor
 import Type.Class.Known
 import Type.Class.Witness
-import Type.Family.Pair
+import Type.Family.Tuple
 
 -- (:&:) {{{
 
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
@@ -33,8 +33,6 @@
 import Type.Family.List
 import Type.Family.Nat
 
--- | 'IZ' indexes the head of the list,
--- and 'IS' indexes into the tail of the list.
 data Index :: [k] -> k -> * where
   IZ :: Index (a :< as) a
   IS :: !(Index as a) -> Index (b :< as) a
diff --git a/src/Data/Type/Index/Quote.hs b/src/Data/Type/Index/Quote.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Index/Quote.hs
@@ -0,0 +1,48 @@
+{-# 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  = error "ix: quotePat not defined"
+  , 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) |]
+
diff --git a/src/Data/Type/Nat/Quote.hs b/src/Data/Type/Nat/Quote.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Nat/Quote.hs
@@ -0,0 +1,89 @@
+{-# 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/Product.hs b/src/Data/Type/Product.hs
--- a/src/Data/Type/Product.hs
+++ b/src/Data/Type/Product.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE StandaloneDeriving #-}
@@ -37,7 +38,7 @@
 
 module Data.Type.Product where
 
-import Data.Type.Combinator ((:.:)(..),IT(..))
+import Data.Type.Combinator ((:.:)(..),IT(..),I(..))
 import Data.Type.Index
 import Data.Type.Length
 import Type.Class.HFunctor
@@ -46,49 +47,88 @@
 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 :<
 
+-- | Construct a two element Prod.
+--   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) -> f (b :: k) -> Prod f '[a,b]
 pattern a :> b = a :< b :< Ø
 infix 6 :>
 
+-- | Build a singleton Prod.
 only :: f a -> Prod f '[a]
 only = (:< Ø)
 
-head' :: Prod f (a :< as) -> f a
-head' (a :< _) = a
-
-tail' :: Prod f (a :< as) -> Prod f as
-tail' (_ :< as) = as
-
+-- | snoc function. insert an element at the end of the list.
 (>:) :: Prod f as -> f a -> Prod f (as >: a)
 (>:) = \case
   Ø       -> only
   b :< as -> (b :<) . (as >:)
 infixl 6 >:
 
-reverse' :: Prod f as -> Prod f (Reverse as)
-reverse' = \case
-  Ø       -> Ø
-  a :< as -> reverse' as >: a
+head' :: Prod f (a :< as) -> f a
+head' (a :< _) = a
 
+tail' :: Prod f (a :< as) -> Prod f as
+tail' (_ :< as) = as
+
+-- | Get all but the last element of a non-empty Prod.
 init' :: Prod f (a :< as) -> Prod f (Init' a as)
 init' (a :< as) = case as of
   Ø      -> Ø
   (:<){} -> a :< init' as
 
+-- | Get the last element of a non-empty Prod.
 last' :: Prod f (a :< as) -> f (Last' a as)
 last' (a :< as) = case as of
   Ø      -> a
   (:<){} -> last' as
 
+reverse' :: Prod f as -> Prod f (Reverse as)
+reverse' = \case
+  Ø       -> Ø
+  a :< as -> reverse' as >: a
+
 append' :: Prod f as -> Prod f bs -> Prod f (as ++ bs)
 append' = \case
   Ø       -> id
   a :< as -> (a :<) . append' as
+
+-- Tuple {{{
+
+-- | A Prod of simple Haskell types.
+type Tuple = Prod I
+
+-- | Singleton Tuple.
+only_ :: a -> Tuple '[a]
+only_ = only . I
+
+-- | Cons onto a Tuple.
+pattern (::<) :: a -> Tuple as -> Tuple (a :< as)
+pattern a ::< as = I a :< as
+infixr 5 ::<
+
+-- | Snoc onto a Tuple.
+(>::) :: Tuple as -> a -> Tuple (as >: a)
+(>::) = \case
+  Ø       -> only_
+  b :< as -> (b :<) . (as >::)
+infixl 6 >::
+
+-- }}}
 
 onHead' :: (f a -> f b) -> Prod f (a :< as) -> Prod f (b :< as)
 onHead' f (a :< as) = f a :< as
diff --git a/src/Data/Type/Product/Dual.hs b/src/Data/Type/Product/Dual.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Product/Dual.hs
@@ -0,0 +1,184 @@
+{-# 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/Quantifier.hs b/src/Data/Type/Quantifier.hs
--- a/src/Data/Type/Quantifier.hs
+++ b/src/Data/Type/Quantifier.hs
@@ -40,14 +40,18 @@
 
 -- | An eliminator for a 'Some' type.
 --
--- NB: the result type of the eliminating function may
--- not refer to the universally quantified type index @a@.
+-- Consider this function akin to a Monadic bind, except
+-- instead of binding into a Monad with a sequent function,
+-- we're binding into the existential quantification with
+-- a universal eliminator function.
 --
--- This function deserves more documentation. It is a powerful
--- basis for working with correct-by-construction data.
 -- It serves as an explicit delimiter in a program of where
 -- the type index may be used and depended on, and where it may
 -- not.
+--
+-- NB: the result type of the eliminating function may
+-- not refer to the universally quantified type index @a@.
+--
 some :: Some f -> (forall a. f a -> r) -> r
 some (Some a) f = f a
 
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
@@ -22,10 +22,9 @@
 -- Stability   :  experimental
 -- Portability :  RankNTypes
 --
--- 'Sum' and 'SumF' are type combinators for representing disjoint sums of
--- indices @(as :: [k])@ of a single functor @(f :: k -> *), or of
--- many functors @(fs :: [k -> *])@ at a single index @(a :: k)@,
--- respectively.
+-- 'Sum' is a type combinators for representing disjoint sums of
+-- indices @(as :: [k])@ of a single functor @(f :: k -> *).
+-- Contrast to the many-functors-one-index 'FSum'
 --
 -----------------------------------------------------------------------------
 
@@ -43,6 +42,10 @@
   InL :: !(f a) -> Sum f (a :< as)
   InR :: !(Sum f as) -> Sum f (a :< as)
 
+-- | There are no possible values of the type @Sum f Ø@.
+nilSum :: Sum f Ø -> Void
+nilSum = impossible
+
 decomp :: Sum f (a :< as) -> Either (f a) (Sum f as)
 decomp = \case
   InL a -> Left  a
@@ -113,38 +116,4 @@
     InR s -> r \\ s
 
 -- }}}
-
-data SumF :: [k -> *] -> k -> * where
-  InLF :: !(f a) -> SumF (f :< fs) a
-  InRF :: !(SumF fs a) -> SumF (f :< fs) a
-
-instance ListC (Functor <$> fs) => Functor (SumF fs) where
-  fmap f = \case
-    InLF a -> InLF $ f <$> a
-    InRF s -> InRF $ f <$> s
-
-decompF :: SumF (f :< fs) a -> Either (f a) (SumF fs a)
-decompF = \case
-  InLF a -> Left  a
-  InRF s -> Right s
-
-injF :: (f ∈ fs) => f a -> SumF fs a
-injF = injectSumF elemIndex
-
-prjF :: (f ∈ fs) => SumF fs a -> Maybe (f a)
-prjF = indexF elemIndex
-
-injectSumF :: Index fs f -> f a -> SumF fs a
-injectSumF = \case
-  IZ   -> InLF
-  IS x -> InRF . injectSumF x
-
-indexF :: Index fs f -> SumF fs a -> Maybe (f a)
-indexF = \case
-  IZ -> \case
-    InLF a -> Just a
-    _      -> Nothing
-  IS x -> \case
-    InRF s -> indexF x s
-    _      -> Nothing
 
diff --git a/src/Data/Type/Sum/Dual.hs b/src/Data/Type/Sum/Dual.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Sum/Dual.hs
@@ -0,0 +1,125 @@
+{-# 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/Type/Class/Witness.hs b/src/Type/Class/Witness.hs
--- a/src/Type/Class/Witness.hs
+++ b/src/Type/Class/Witness.hs
@@ -77,6 +77,9 @@
   id              = Sub Wit
   Sub bc . Sub ab = Sub $ bc \\ ab
 
+type (:-:) = Bij (:-)
+infixr 4 :-:
+
 -- | A general eliminator for entailment.
 --
 -- Given a term of type @t@ with an instance @Witness p q t@
@@ -159,6 +162,7 @@
   id    = Bij id id
   g . f = Bij (fwd g . fwd f) (bwd f . bwd g)
 
+{-
 class Category c => Monoidal (c :: k -> k -> *) where
   type Tensor c :: k -> k -> k
   type Unit   c :: k
@@ -193,6 +197,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 <->
diff --git a/src/Type/Family/Pair.hs b/src/Type/Family/Pair.hs
deleted file mode 100644
--- a/src/Type/Family/Pair.hs
+++ /dev/null
@@ -1,58 +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.Family.Pair
--- Copyright   :  Copyright (C) 2015 Kyle Carter
--- License     :  BSD3
---
--- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
--- Stability   :  experimental
--- Portability :  RankNTypes
---
--- Type-level pairs, along with some convenient aliases and type families
--- over them.
---
------------------------------------------------------------------------------
-
-module Type.Family.Pair where
-
-import Type.Family.Monoid
-
-type (#) = '(,)
-infixr 6 #
-
-type family Fst (p :: (k,l)) :: k where
-  Fst '(a,b) = a
-
-type family Snd (p :: (k,l)) :: l where
-  Snd '(a,b) = b
-
-type family (f :: k -> l) <$> (a :: (m,k)) :: (m,l) where
-  f <$> (a#b) = a # f b
-infixr 4 <$>
-
-type family (f :: (m,k -> l)) <&> (a :: k) :: (m,l) where
-  (r#f) <&> a = r # f a
-infixr 4 <&>
-
-type family (f :: (m,k -> l)) <*> (a :: (m,k)) :: (m,l) where
-  (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)
-
diff --git a/src/Type/Family/Tuple.hs b/src/Type/Family/Tuple.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Family/Tuple.hs
@@ -0,0 +1,70 @@
+{-# 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.Tuple
+-- Copyright   :  Copyright (C) 2015 Kyle Carter
+-- License     :  BSD3
+--
+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
+-- Stability   :  experimental
+-- Portability :  RankNTypes
+--
+-- Type-level pairs and triples, along with some convenient aliases and type families
+-- over them.
+--
+-----------------------------------------------------------------------------
+
+module Type.Family.Tuple where
+
+import Type.Family.Monoid
+
+type (#) = '(,)
+infixr 6 #
+
+type family Fst (p :: (k,l)) :: k where
+  Fst '(a,b) = a
+
+type family Snd (p :: (k,l)) :: l where
+  Snd '(a,b) = b
+
+type family (f :: k -> l) <$> (a :: (m,k)) :: (m,l) where
+  f <$> (a#b) = a # f b
+infixr 4 <$>
+
+type family (f :: (m,k -> l)) <&> (a :: k) :: (m,l) where
+  (r#f) <&> a = r # f a
+infixr 4 <&>
+
+type family (f :: (m,k -> l)) <*> (a :: (m,k)) :: (m,l) where
+  (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,24 +1,16 @@
 name: type-combinators
+version: 0.1.2.0
 category: Data
-synopsis: A collection of data types for type-level programming.
-description: I put this library together first and foremost so that
-             I wouldn't need to constantly rewrite the same code
-             that uses these types, but also because I noticed a
-             growing trend of writing and rewriting bits and pieces
-             of code for these types all over the Haskell community.
-             Hopefully, this helps! Contributions, criticisms, and
-             thoughts are very welcome.  -kylcarte
-homepage:      http://github.com/kylcarte/type-combinators
-bug-reports:   http://github.com/type-combinators/issues
-version: 0.1.0.1
+synopsis: A collection of data types for type-level programming
 cabal-version: >=1.10
 build-type: Simple
 license: BSD3
 license-file: LICENSE
 maintainer: kylcarte@gmail.com
 author: Kyle Carter
+homepage: https://github.com/kylcarte/type-combinators
 
-source-repository head
+Source-Repository head
     type: git
     location: git://github.com/kylcarte/type-combinators.git
 
@@ -29,12 +21,16 @@
         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.Quantifier
+        Data.Type.Product.Dual
         Data.Type.Sum
+        Data.Type.Sum.Dual
+        Data.Type.Quantifier
         Data.Type.Vector
         Type.Class.HFunctor
         Type.Class.Known
@@ -44,9 +40,13 @@
         Type.Family.Maybe
         Type.Family.Monoid
         Type.Family.Nat
-        Type.Family.Pair
+        Type.Family.Tuple
     build-depends:
-        base >=4.8 && <4.9
+        base >=4.8 && <4.9,
+        containers,
+        template-haskell,
+        transformers,
+        mtl
     default-language: Haskell2010
     hs-source-dirs: src