diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2015, Kyle Carter
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Kyle Carter nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/src/Data/Type/Combinator.hs b/src/Data/Type/Combinator.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Combinator.hs
@@ -0,0 +1,298 @@
+{-# 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.Combinator
+-- Copyright   :  Copyright (C) 2015 Kyle Carter
+-- License     :  BSD3
+--
+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
+-- Stability   :  experimental
+-- Portability :  RankNTypes
+--
+-- A collection of simple type combinators,
+-- such as @Identity@ 'I', @Constant@ 'C', @Compose@ '(:.:)',
+-- left unnest 'LL', right unnest 'RR', the @S Combinator@ 'SS',
+-- etc.
+--
+-----------------------------------------------------------------------------
+
+module Data.Type.Combinator where
+
+import Type.Class.HFunctor
+import Type.Class.Known
+import Type.Class.Witness
+
+import Control.Applicative
+
+-- (:.:) {{{
+
+data ((f :: l -> *) :.: (g :: k -> l)) :: k -> * where
+  Comp :: { getComp :: f (g a) } -> (f :.: g) a
+infixr 6 :.:
+
+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 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 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
+
+-- }}}
+
+-- 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
+
+instance Applicative I where
+  pure = I
+  I f <*> I a = I $ f a
+
+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
+
+instance Num a => Num (I a) where
+  (*)         = liftA2 (*)
+  (+)         = liftA2 (+)
+  (-)         = liftA2 (-)
+  abs         = fmap abs
+  signum      = fmap signum
+  fromInteger = pure . fromInteger
+
+-- }}}
+
+-- 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
+
+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 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
+
+instance Num r => Num (C r a) where
+  C a * C b    = C $ a * b
+  C a + C b    = C $ a + b
+  C a - C b    = C $ a - b
+  abs    (C a) = C $ abs a
+  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
+  
+
+-- }}}
+
+-- Flip {{{
+
+newtype Flip p b a = Flip
+  { getFlip :: p a b
+  } deriving (Eq,Ord,Show)
+
+instance Known (p a) b => Known (Flip p b) a where
+  type KnownC (Flip p b) a = Known (p a) b
+  known = Flip known
+
+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
+
+-- }}}
+
diff --git a/src/Data/Type/Conjunction.hs b/src/Data/Type/Conjunction.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Conjunction.hs
@@ -0,0 +1,149 @@
+{-# 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.Conjunction
+-- Copyright   :  Copyright (C) 2015 Kyle Carter
+-- License     :  BSD3
+--
+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
+-- Stability   :  experimental
+-- Portability :  RankNTypes
+--
+-- Two type combinators for working with conjunctions:
+-- A /fanout/ combinator '(:&:)', and a /par/ combinator '(:*:)'.
+--
+-- These are analogous to '(&&&)' and '(***)' from 'Control.Arrow',
+-- respectively.
+--
+-----------------------------------------------------------------------------
+
+module Data.Type.Conjunction where
+
+import Type.Class.HFunctor
+import Type.Class.Known
+import Type.Class.Witness
+import Type.Family.Pair
+
+-- (:&:) {{{
+
+data ((f :: k -> *) :&: (g :: k -> *)) :: k -> * where
+  (:&:) :: !(f a) -> !(g a) -> (f :&: g) a
+infixr 5 :&:
+
+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)
+
+fanFst :: (f :&: g) a -> f a
+fanFst (a :&: _) = a
+
+fanSnd :: (f :&: g) a -> g a
+fanSnd (_ :&: b) = b
+
+uncurryFan :: (f a -> g a -> r) -> (f :&: g) a -> r
+uncurryFan f (a :&: b) = f a b
+
+curryFan :: ((f :&: g) a -> r) -> f a -> g a -> r
+curryFan f a b = f (a :&: b)
+
+instance DecEquality f => DecEquality (f :&: g) where
+  decideEquality (a :&: _) (c :&: _) = decideEquality a c
+
+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 HFoldable ((:&:) f) where
+  foldMap' f (_ :&: b) = f b
+
+instance HTraversable ((:&:) f) where
+  traverse' f (a :&: b) = (:&:) a <$> f b
+
+instance HBifunctor (:&:) where
+  bimap' 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
+-}
+
+-- }}}
+
+-- (:*:) {{{
+
+data ((f :: k -> *) :*: (g :: l -> *)) :: (k,l) -> * where
+  (:*:) :: !(f a) -> !(g b) -> (f :*: g) (a#b)
+infixr 5 :*:
+
+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)
+
+parFst :: (f :*: g) p -> f (Fst p)
+parFst (a :*: _) = a
+
+parSnd :: (f :*: g) p -> g (Snd p)
+parSnd (_ :*: b) = b
+
+uncurryPar :: (forall a b. (p ~ (a#b)) => f a -> g b -> r) -> (f :*: g) p -> r
+uncurryPar f (a :*: b) = f a b
+
+curryPar :: ((f :*: g) (a#b) -> r) -> f a -> g b -> r
+curryPar f a b = f (a :*: b)
+
+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 HFoldable ((:*:) f) where
+  foldMap' f (_ :*: b) = f b
+
+instance HTraversable ((:*:) f) where
+  traverse' f (a :*: b) = (:*:) a <$> f b
+
+instance HBifunctor (:*:) where
+  bimap' f g (a :*: b) = f a :*: g b
+
+_fst :: (a#b) :~: (c#d) -> a :~: c
+_fst Refl = Refl
+
+_snd :: (a#b) :~: (c#d) -> b :~: d
+_snd Refl = Refl
+
+instance (DecEquality f, DecEquality g) => DecEquality (f :*: g) where
+  decideEquality (a :*: b) (c :*: d) = case decideEquality a c of
+    Proven    p -> case decideEquality b d of
+      Proven  q -> Proven  $ Refl \\ p \\ q
+      Refuted q -> Refuted $ q . _snd
+    Refuted   p -> Refuted $ p . _fst
+
+instance (Witness p q (f a), Witness s t (g b), x ~ (a#b)) => Witness (p,s) (q,t) ((f :*: g) x) where
+  type WitnessC (p,s) (q,t) ((f :*: g) x) = (Witness p q (f (Fst x)), Witness s t (g (Snd x)))
+  r \\ a :*: b = r \\ a \\ b
+
+-- }}}
+
diff --git a/src/Data/Type/Disjunction.hs b/src/Data/Type/Disjunction.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Disjunction.hs
@@ -0,0 +1,130 @@
+{-# 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.Disjunction
+-- Copyright   :  Copyright (C) 2015 Kyle Carter
+-- License     :  BSD3
+--
+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
+-- Stability   :  experimental
+-- Portability :  RankNTypes
+--
+-- Two type combinators for working with disjunctions:
+-- A /branch/ combinator '(:+:)', and a /choice/ combinator '(:|:)'.
+--
+-- These are analogous to '(+++)' and '(|||)' from 'Control.Arrow',
+-- respectively.
+--
+-----------------------------------------------------------------------------
+
+module Data.Type.Disjunction where
+
+import Type.Class.HFunctor
+import Type.Class.Known
+import Type.Class.Witness
+
+-- (:+:) {{{
+
+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
+  L a -> f a
+  R b -> g b
+infixr 2 >+<
+
+instance HFunctor ((:+:) f) where
+  map' f = \case
+    L a -> L a
+    R b -> R $ f b
+
+instance HFoldable ((:+:) f) where
+  foldMap' f = \case
+    L _ -> mempty
+    R b -> f b
+
+instance HTraversable ((:+:) f) where
+  traverse' f = \case
+    L a -> pure $ L a
+    R b -> R <$> f b
+
+instance HBifunctor (:+:) where
+  bimap' 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))
+  (\\) 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 :|:
+
+(>|<) :: (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 >|<
+
+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
+  known = R' known
+
+instance HFunctor ((:|:) f) where
+  map' f = \case
+    L' a -> L' a
+    R' b -> R' $ f b
+
+instance HFoldable ((:|:) f) where
+  foldMap' f = \case
+    L' _ -> mempty
+    R' b -> f b
+
+instance HTraversable ((:|:) f) where
+  traverse' f = \case
+    L' a -> pure $ L' a
+    R' b -> R' <$> f b
+
+instance HBifunctor (:|:) where
+  bimap' 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)
+  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)
+  r \\ R' b = r \\ b
+
+-- }}}
+
diff --git a/src/Data/Type/Fin.hs b/src/Data/Type/Fin.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Fin.hs
@@ -0,0 +1,114 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# 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.Fin
+-- Copyright   :  Copyright (C) 2015 Kyle Carter
+-- License     :  BSD3
+--
+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
+-- Stability   :  experimental
+-- Portability :  RankNTypes
+--
+-- A @singleton@-esque type for representing members of finite sets.
+--
+-----------------------------------------------------------------------------
+
+module Data.Type.Fin where
+
+import Data.Type.Combinator
+import Data.Type.Nat
+import Type.Class.Known
+import Type.Class.Witness
+import Type.Family.Constraint
+import Type.Family.Nat
+import Data.Type.Quantifier
+
+data Fin :: N -> * where
+  FZ :: Fin (S n)
+  FS :: !(Fin n) -> Fin (S n)
+
+deriving instance Eq   (Fin n)
+deriving instance Ord  (Fin n)
+deriving instance Show (Fin n)
+
+-- | Gives the list of all members of the finite set of size @n@.
+fins :: Nat n -> [Fin n]
+fins = \case
+  Z_   -> []
+  S_ x -> FZ : map FS (fins x)
+
+fin :: Fin n -> Int
+fin = \case
+  FZ   -> 0
+  FS x -> succ $ fin x
+
+-- | There are no members of @Fin Z@.
+finZ :: Fin Z -> Void
+finZ = impossible
+
+weaken :: Fin n -> Fin (S n)
+weaken = \case
+  FZ   -> FZ
+  FS n -> FS $ weaken n
+
+-- | Map a finite set to a lower finite set without
+-- one of its members.
+without :: Fin n -> Fin n -> Maybe (Fin (Pred n))
+without = \case
+  FZ -> \case
+    FZ   -> Nothing
+    FS y -> Just y
+  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
+finNat = \case
+  FZ   -> Some Z_
+  FS x -> withSome (Some . S_) $ finNat x
+
+-- | A @Fin n@ is a 'Witness' that @n >= 1@.
+--
+-- That is, @'Pred' n@ is well defined.
+instance (n' ~ Pred n) => Witness ØC (S n' ~ n) (Fin n) where
+  type WitnessC ØC (S n' ~ n) (Fin n) = (n' ~ Pred n)
+  (\\) r = \case
+    FZ   -> r
+    FS _ -> r
+
diff --git a/src/Data/Type/Index.hs b/src/Data/Type/Index.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Index.hs
@@ -0,0 +1,63 @@
+{-# 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
+-- Copyright   :  Copyright (C) 2015 Kyle Carter
+-- License     :  BSD3
+--
+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
+-- Stability   :  experimental
+-- Portability :  RankNTypes
+--
+-- A @singleton@-esque type for representing indices in a type-level list.
+--
+-----------------------------------------------------------------------------
+
+module Data.Type.Index where
+
+import Type.Class.HFunctor
+import Type.Class.Known
+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
+
+deriving instance Eq   (Index as a)
+deriving instance Ord  (Index as a)
+deriving instance Show (Index as a)
+
+type a ∈ as = Elem as a
+infix 6 ∈
+
+class Elem (as :: [k]) (a :: k) where
+  elemIndex :: Index as a
+
+instance {-# OVERLAPPING #-} Elem (a :< as) a where
+  elemIndex = IZ
+
+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/Length.hs b/src/Data/Type/Length.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Length.hs
@@ -0,0 +1,57 @@
+{-# 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.Length
+-- Copyright   :  Copyright (C) 2015 Kyle Carter
+-- License     :  BSD3
+--
+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
+-- Stability   :  experimental
+-- Portability :  RankNTypes
+--
+-- A @singleton@-esque type for representing lengths of type-level lists,
+-- irrespective of the actual types in that list.
+--
+-----------------------------------------------------------------------------
+
+module Data.Type.Length where
+
+import Type.Class.Known
+import Type.Family.List
+
+data Length :: [k] -> * where
+  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 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
+
diff --git a/src/Data/Type/Nat.hs b/src/Data/Type/Nat.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Nat.hs
@@ -0,0 +1,154 @@
+{-# 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.Nat
+-- Copyright   :  Copyright (C) 2015 Kyle Carter
+-- License     :  BSD3
+--
+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
+-- Stability   :  experimental
+-- Portability :  RankNTypes
+--
+-- A @singleton@-esque type for representing Peano natural numbers.
+--
+-----------------------------------------------------------------------------
+
+module Data.Type.Nat where
+
+import Data.Type.Equality
+import Data.Type.Product
+import Type.Class.Known
+import Type.Class.Witness
+import Type.Family.Constraint
+import Type.Family.List
+import Type.Family.Nat
+
+data Nat :: N -> * where
+  Z_ :: Nat Z
+  S_ :: !(Nat n) -> Nat (S n)
+
+deriving instance Eq   (Nat n)
+deriving instance Ord  (Nat n)
+deriving instance Show (Nat n)
+
+-- | @'Z_'@ is the canonical construction of a @'Nat' Z@.
+instance Known Nat Z where
+  known = Z_
+
+-- | If @n@ is a canonical construction of @Nat n@,
+-- @'S_' n@ is the canonical construction of @Nat (S n)@.
+instance Known Nat n => Known Nat (S n) where
+  type KnownC Nat (S n) = Known Nat n
+  known = S_ known
+
+-- | A @Nat n@ is a 'Witness' that there is a canonical
+-- construction for @Nat n@.
+instance Witness ØC (Known Nat n) (Nat n) where
+  (\\) r = \case
+    Z_   -> r
+    S_ x -> r \\ x
+
+instance TestEquality Nat where
+  testEquality = \case
+    Z_ -> \case
+      Z_   -> Just Refl
+      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
+
+_Z :: Z :~: Z
+_Z = Refl
+
+_S :: x :~: y -> S x :~: S y
+_S Refl = Refl
+
+_s :: S x :~: S y -> x :~: y
+_s Refl = Refl
+
+_ZneS :: Z :~: S x -> Void
+_ZneS = impossible
+
+-- | A proof that 'Z' is also a right identity
+-- for the addition of type-level 'Nat's.
+addZ :: Nat x -> (x + Z) :~: x
+addZ = \case
+  Z_   -> Refl
+  S_ x -> _S $ addZ x
+{-# INLINE addZ #-}
+
+addS :: Nat x -> Nat y -> S (x + y) :~: (x + S y)
+addS = \case
+  Z_   -> pure Refl
+  S_ x -> _S . addS x
+{-# INLINE addS #-}
+
+(.+) :: Nat x -> Nat y -> Nat (x + y)
+(.+) = \case
+  Z_   -> id
+  S_ x -> S_ . (x .+)
+infixr 6 .+
+
+(.*) :: Nat x -> Nat y -> Nat (x * y)
+(.*) = \case
+  Z_   -> const Z_
+  S_ x -> (.+) <$> (x .*) <*> id
+infixr 7 .*
+
+(.^) :: Nat x -> Nat y -> Nat (x ^ y)
+(.^) x = \case
+  Z_   -> S_ Z_
+  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
+
+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
+
diff --git a/src/Data/Type/Option.hs b/src/Data/Type/Option.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Option.hs
@@ -0,0 +1,76 @@
+{-# 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.Option
+-- Copyright   :  Copyright (C) 2015 Kyle Carter
+-- License     :  BSD3
+--
+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
+-- Stability   :  experimental
+-- Portability :  RankNTypes
+--
+-- A type combinator for type-level @Maybe@s,
+-- lifting @(f :: k -> *)@ to @(Option f :: Maybe k -> *)@.
+--
+-----------------------------------------------------------------------------
+
+module Data.Type.Option where
+
+import Type.Class.HFunctor
+import Type.Class.Known
+import Type.Class.Witness
+import Type.Family.Maybe
+
+data Option (f :: k -> *) :: Maybe k -> * where
+  Nothing_ :: Option f Nothing
+  Just_    :: !(f a) -> Option f (Just a)
+
+-- | Eliminator for @'Option' f@.
+option :: (forall a. (m ~ Just a) => f a -> r) -> ((m ~ Nothing) => r) -> Option f m -> r
+option j n = \case
+  Just_ a  -> j a
+  Nothing_ -> n
+
+-- | 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
+    Just_ a  -> Just_ $ f a
+    Nothing_ -> Nothing_
+
+instance HFoldable Option where
+  foldMap' f = \case
+    Just_ a  -> f a
+    Nothing_ -> mempty
+
+instance HTraversable Option where
+  traverse' f = \case
+    Just_ a  -> Just_ <$> f a
+    Nothing_ -> pure Nothing_
+
+instance Known (Option f) Nothing where
+  known = Nothing_
+
+instance Known f a => Known (Option f) (Just a) where
+  type KnownC (Option f) (Just a) = Known f a
+  known = Just_ known
+
+instance (Witness p q (f a), x ~ Just a) => Witness p q (Option f x) where
+  type WitnessC p q (Option f x) = Witness p q (f (FromJust x))
+  (\\) r = \case
+    Just_ a -> r \\ a
+    _       -> error "impossible type"
+
diff --git a/src/Data/Type/Product.hs b/src/Data/Type/Product.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Product.hs
@@ -0,0 +1,148 @@
+{-# 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.Product
+-- Copyright   :  Copyright (C) 2015 Kyle Carter
+-- License     :  BSD3
+--
+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
+-- Stability   :  experimental
+-- Portability :  RankNTypes
+--
+-- Type combinators for type-level lists,
+-- lifting @(f :: k -> *)@ to @(Prod f :: [k] -> *)@,
+-- as well as its constructions, manipulations, and
+-- eliminations.
+--
+-- 'Prod' is similar in nature to a few others in the Haskell ecosystem, such as:
+--
+-- Oleg's 'HList', from <http://hackage.haskell.org/package/HList>, and
+-- 
+-- Kenneth Foner's 'ConicList', from <http://hackage.haskell.org/package/IndexedList-0.1.0.1/docs/Data-List-Indexed-Conic.html>.
+--
+-----------------------------------------------------------------------------
+
+module Data.Type.Product where
+
+import Data.Type.Combinator ((:.:)(..),IT(..))
+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
+
+data Prod (f :: k -> *) :: [k] -> * where
+  Ø    :: Prod f Ø
+  (:<) :: !(f a) -> !(Prod f as) -> Prod f (a :< as)
+infixr 5 :<
+
+pattern (:>) :: (f :: k -> *) (a :: k) -> f (b :: k) -> Prod f '[a,b]
+pattern a :> b = a :< b :< Ø
+infix 6 :>
+
+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
+
+(>:) :: 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
+
+init' :: Prod f (a :< as) -> Prod f (Init' a as)
+init' (a :< as) = case as of
+  Ø      -> Ø
+  (:<){} -> a :< init' as
+
+last' :: Prod f (a :< as) -> f (Last' a as)
+last' (a :< as) = case as of
+  Ø      -> a
+  (:<){} -> last' as
+
+append' :: Prod f as -> Prod f bs -> Prod f (as ++ bs)
+append' = \case
+  Ø       -> id
+  a :< as -> (a :<) . append' as
+
+onHead' :: (f a -> f b) -> Prod f (a :< as) -> Prod f (b :< as)
+onHead' f (a :< as) = f a :< as
+
+onTail' :: (Prod f as -> Prod f bs) -> Prod f (a :< as) -> Prod f (a :< bs)
+onTail' f (a :< as) = a :< f as
+
+uncurry' :: (f a -> Prod f as -> r) -> Prod f (a :< as) -> r
+uncurry' f (a :< as) = f a as
+
+curry' :: (l ~ (a :< as)) => (Prod f l -> r) -> f a -> Prod f as -> r
+curry' f a as = f $ a :< as
+
+index :: Index as a -> Prod f as -> f a
+index = \case
+  IZ -> head'
+  IS x -> index x . tail'
+
+instance HFunctor Prod where
+  map' f = \case
+    Ø -> Ø
+    a :< as -> f a :< map' f as
+
+instance HIxFunctor Index Prod where
+  imap' f = \case
+    Ø -> Ø
+    a :< as -> f IZ a :< imap' (f . IS) as
+
+instance HFoldable Prod where
+  foldMap' f = \case
+    Ø       -> mempty
+    a :< as -> f a `mappend` foldMap' f as
+
+instance HIxFoldable Index Prod where
+  ifoldMap' f = \case
+    Ø       -> mempty
+    a :< as -> f IZ a `mappend` ifoldMap' (f . IS) as
+
+instance HTraversable Prod where
+  traverse' f = \case
+    Ø       -> pure Ø
+    a :< as -> (:<) <$> f a <*> traverse' f as
+
+instance Known (Prod f) Ø where
+  known = Ø
+
+instance (Known f a, Known (Prod f) as) => Known (Prod f) (a :< as) where
+  type KnownC (Prod f) (a :< as) = (Known f a, Known (Prod f) as)
+  known = known :< known
+
+instance Witness ØC ØC (Prod f Ø) where
+  r \\ _ = r
+
+instance (Witness p q (f a), Witness s t (Prod f as)) => Witness (p,s) (q,t) (Prod f (a :< as)) where
+  type WitnessC (p,s) (q,t) (Prod f (a :< as)) = (Witness p q (f a), Witness s t (Prod f as))
+  r \\ (a :< as) = r \\ a \\ as
+
diff --git a/src/Data/Type/Quantifier.hs b/src/Data/Type/Quantifier.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Quantifier.hs
@@ -0,0 +1,76 @@
+{-# 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.Quantifier
+-- Copyright   :  Copyright (C) 2015 Kyle Carter
+-- License     :  BSD3
+--
+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
+-- Stability   :  experimental
+-- Portability :  RankNTypes
+--
+-- Types for working with (and under) existentially and universally
+-- quantified types.
+--
+-- The 'Some' type can be very useful when working with type-indexed GADTs,
+-- where defining instances for classes like 'Read' can be tedious at best,
+-- and frequently impossible, for the GADT itself.
+--
+-----------------------------------------------------------------------------
+
+module Data.Type.Quantifier where
+
+import Data.Type.Combinator
+
+data Some (f :: k -> *) :: * where
+  Some :: f a -> Some f
+
+-- | An eliminator for a 'Some' type.
+--
+-- NB: the result type of the eliminating function may
+-- not refer to the universally quantified type index @a@.
+--
+-- 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.
+some :: Some f -> (forall a. f a -> r) -> r
+some (Some a) f = f a
+
+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 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))
+
+data All (f :: k -> *) :: * where
+  All :: { instAll :: forall (a :: k). f a } -> All f
+
+-- | A data type for natural transformations.
+data (f :: k -> *) :-> (g :: k -> *) where
+  NT :: (forall a. f a -> g a) -> f :-> g
+infixr 4 :->
+
+data (p :: k -> l -> *) :--> (q :: k -> l -> *) where
+  NT2 :: (forall a b. p a b -> q a b) -> p :--> q
+infixr 4 :-->
+
diff --git a/src/Data/Type/Sum.hs b/src/Data/Type/Sum.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Sum.hs
@@ -0,0 +1,150 @@
+{-# 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
+-- Copyright   :  Copyright (C) 2015 Kyle Carter
+-- License     :  BSD3
+--
+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
+-- 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.
+--
+-----------------------------------------------------------------------------
+
+module Data.Type.Sum where
+
+import Data.Type.Index
+
+import Type.Class.HFunctor
+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)
+
+decomp :: Sum f (a :< as) -> Either (f a) (Sum f as)
+decomp = \case
+  InL a -> Left  a
+  InR s -> Right s
+
+injectSum :: Index as a -> f a -> Sum f as
+injectSum = \case
+  IZ   -> InL
+  IS x -> InR . injectSum x
+
+inj :: (a ∈ as) => f a -> Sum f as
+inj = injectSum elemIndex
+
+prj :: (a ∈ as) => Sum f as -> Maybe (f a)
+prj = index elemIndex
+
+index :: Index as a -> Sum f as -> Maybe (f a)
+index = \case
+  IZ -> \case
+    InL a -> Just a
+    _     -> Nothing
+  IS x -> \case
+    InR s -> index x s
+    _     -> Nothing
+
+-- instances {{{
+
+instance HFunctor Sum where
+  map' f = \case
+    InL a -> InL $ f a
+    InR s -> InR $ map' f s
+
+instance HIxFunctor Index Sum where
+  imap' f = \case
+    InL a -> InL $ f IZ a
+    InR s -> InR $ imap' (f . IS) s
+
+instance HFoldable Sum where
+  foldMap' f = \case
+    InL a -> f a
+    InR s -> foldMap' f s
+
+instance HIxFoldable Index Sum where
+  ifoldMap' f = \case
+    InL a -> f IZ a
+    InR s -> ifoldMap' (f . IS) s
+
+instance HTraversable Sum where
+  traverse' f = \case
+    InL a -> InL <$> f a
+    InR s -> InR <$> traverse' f s
+
+instance HIxTraversable Index Sum where
+  itraverse' f = \case
+    InL a -> InL <$> f IZ a
+    InR s -> InR <$> itraverse' (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)
+  (\\) r = \case
+    InL a -> r \\ a
+    _     -> error "impossible type"
+
+instance (Witness p q (f a), Witness p q (Sum f (b :< as))) => Witness p q (Sum f (a :< b :< as)) where
+  type WitnessC p q (Sum f (a :< b :< as)) = (Witness p q (f a), Witness p q (Sum f (b :< as)))
+  (\\) r = \case
+    InL a -> r \\ a
+    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/Vector.hs b/src/Data/Type/Vector.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Vector.hs
@@ -0,0 +1,400 @@
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# 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.Vector
+-- Copyright   :  Copyright (C) 2015 Kyle Carter
+-- License     :  BSD3
+--
+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
+-- Stability   :  experimental
+-- Portability :  RankNTypes
+--
+-- 'V' and its combinator analog 'VT' represent lists
+-- of known length, characterized by the index @(n :: N)@ in
+-- @'V' n a@ or @'VT' n f a@.
+--
+-- The classic example used ad nauseum for type-level programming.
+--
+-- The operations on 'V' and 'VT' correspond to the type level arithmetic
+-- operations on the kind 'N'.
+--
+-----------------------------------------------------------------------------
+
+module Data.Type.Vector where
+
+import Data.Type.Combinator
+import Data.Type.Fin
+import Data.Type.Length
+import Data.Type.Nat
+import Data.Type.Product (Prod(..),curry',pattern (:>))
+
+import Type.Class.HFunctor
+import Type.Class.Known
+import Type.Class.Witness
+
+import Type.Family.Constraint
+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 :*
+
+type V n = VT n I
+pattern (:+) :: a -> V n a -> V (S n) a
+pattern a :+ as = I a :* as
+infixr 4 :+
+
+deriving instance Eq   (f a) => Eq   (VT n f a)
+deriving instance Ord  (f a) => Ord  (VT n f a)
+deriving instance Show (f a) => Show (VT n f a)
+
+(.++) :: VT x f a -> VT y f a -> VT (x + y) f a
+(.++) = \case
+  ØV      -> id
+  a :* as -> (a :*) . (as .++)
+infixr 5 .++
+
+vrep :: forall n f a. Known Nat n => f a -> VT n f a
+vrep a = go (known :: Nat n)
+  where
+  go :: Nat x -> VT x f a
+  go = \case
+    Z_   -> ØV
+    S_ x -> a :* go x
+
+head' :: VT (S n) f a -> f a
+head' (a :* _) = a
+
+tail' :: VT (S n) f a -> VT n f a
+tail' (_ :* as) = as
+
+onTail :: (VT m f a -> VT n f a) -> VT (S m) f a -> VT (S n) f a
+onTail f (a :* as) = a :* f as
+
+vDel :: Fin n -> VT n f a -> VT (Pred n) f a
+vDel = \case
+  FZ   -> tail'
+  FS x -> onTail (vDel x) \\ x
+
+imap :: (Fin n -> f a -> g b) -> VT n f a -> VT n g b
+imap f = \case
+  ØV      -> ØV
+  a :* as -> f FZ a :* imap (f . FS) as
+
+ifoldMap :: Monoid m => (Fin n -> f a -> m) -> VT n f a -> m
+ifoldMap f = \case
+  ØV      -> mempty
+  a :* as -> f FZ a <> ifoldMap (f . FS) as
+
+itraverse :: Applicative h => (Fin n -> f a -> h (g b)) -> VT n f a -> h (VT n g b)
+itraverse f = \case
+  ØV      -> pure ØV
+  a :* as -> (:*) <$> f FZ a <*> itraverse (f . FS) as
+
+index :: Fin n -> VT n f a -> f a
+index = \case
+  FZ   -> head'
+  FS x -> index x . tail'
+
+vmap :: (f a -> g b) -> VT n f a -> VT n g b
+vmap f = \case
+  ØV      -> ØV
+  a :* as -> f a :* vmap f as
+
+vap :: (f a -> g b -> h c) -> VT n f a -> VT n g b -> VT n h c
+vap f = \case
+  ØV  -> \_ -> ØV
+  a :* as -> \case
+    b :* bs -> f a b :* vap f as bs
+    _       -> error "impossible type"
+
+vfoldr :: (f a -> b -> b) -> b -> VT n f a -> b
+vfoldr s z = \case
+  ØV      -> z
+  a :* as -> s a $ vfoldr s z as
+
+vfoldMap' :: (b -> b -> b) -> b -> (f a -> b) -> VT n f a -> b
+vfoldMap' j z f = \case
+  ØV       -> z
+  a :* ØV  -> f a
+  a :* as  -> j (f a) $ vfoldMap' j z f as
+
+vfoldMap :: Monoid m => (f a -> m) -> VT n f a -> m
+vfoldMap f = \case
+  ØV      -> mempty
+  a :* as -> f a <> vfoldMap f as
+
+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
+
+withV :: [a] -> (forall n. V n a -> r) -> r
+withV as k = withVT (I <$> as) k
+
+findV :: Eq a => a -> V n a -> Maybe (Fin n)
+findV = findVT . I
+
+findVT :: Eq (f a) => f a -> VT n f a -> Maybe (Fin n)
+findVT a = \case
+  ØV      -> Nothing
+  b :* as -> if a == b
+    then Just FZ
+    else FS <$> findVT a as
+
+instance Functor f => Functor (VT n f) where
+  fmap = vmap . fmap
+
+instance (Applicative f, Known Nat n) => Applicative (VT n f) where
+  pure  = vrep . pure
+  (<*>) = vap (<*>)
+
+instance (Monad f, Known Nat n) => Monad (VT n f) where
+  v >>= f = imap (\x -> (>>= index x . f)) v
+
+instance Foldable f => Foldable (VT n f) where
+  foldMap f = \case
+    ØV      -> mempty
+    a :* as -> foldMap f a <> foldMap f as
+
+instance Traversable f => Traversable (VT n f) where
+  traverse f = \case
+    ØV      -> pure ØV
+    a :* as -> (:*) <$> traverse f a <*> traverse f as
+
+{-
+instance (Witness p q (f a), n ~ S x) => Witness p q (VT n f a) where
+  type WitnessC p q (VT n f a) = Witness p q (f a)
+  (\\) r = \case
+    a :* _ -> r \\ a
+    _      -> error "impossible type"
+-}
+
+instance Witness ØC (Known Nat n) (VT n f a) where
+  (\\) r = \case
+    ØV      -> r
+    _ :* as -> r \\ as
+
+instance (Num (f a), Known Nat n) => Num (VT n f a) where
+  (*)         = vap (*)
+  (+)         = vap (+)
+  (-)         = vap (-)
+  negate      = vmap negate
+  abs         = vmap abs
+  signum      = vmap signum
+  fromInteger = vrep . fromInteger
+
+newtype M ns a = M { getMatrix :: Matrix ns a }
+
+deriving instance Eq   (Matrix ns a) => Eq   (M ns a)
+deriving instance Ord  (Matrix ns a) => Ord  (M ns a)
+deriving instance Show (Matrix ns a) => Show (M ns a)
+
+instance Num (Matrix ns a) => Num (M ns a) where
+  fromInteger  = M . fromInteger
+  M a * M b    = M $ a * b
+  M a + M b    = M $ a + b
+  M a - M b    = M $ a - b
+  abs (M a)    = M $ abs a
+  signum (M a) = M $ signum a
+
+type family Matrix (ns :: [N]) :: * -> * where
+  Matrix Ø         = I
+  Matrix (n :< ns) = VT n (Matrix ns)
+
+vgen_ :: Known Nat n => (Fin n -> f a) -> VT n f a
+vgen_ = vgen known
+
+vgen :: Nat n -> (Fin n -> f a) -> VT n f a
+vgen x f = case x of
+  Z_   -> ØV
+  S_ y -> f FZ :* vgen y (f . FS)
+
+mgen_ :: Known (Prod Nat) ns => (Prod Fin ns -> a) -> M ns a
+mgen_ = mgen known
+
+mgen :: Prod Nat ns -> (Prod Fin ns -> a) -> M ns a
+mgen ns f = case ns of
+  Ø        -> M $ I $ f Ø
+  n :< ns' -> M $ vgen n $ getMatrix . mgen ns' . curry' f
+
+onMatrix :: (Matrix ms a -> Matrix ns b) -> M ms a -> M ns b
+onMatrix f = M . f . getMatrix
+
+diagonal :: VT n (VT n f) a -> VT n f a
+diagonal = imap index
+
+vtranspose :: Known Nat n => VT m (VT n f) a -> VT n (VT m f) a
+vtranspose v = vgen_ $ \x -> vmap (index x) v
+
+transpose :: Known Nat n => M (m :< n :< ns) a -> M (n :< m :< ns) a
+transpose = onMatrix vtranspose
+
+m0 :: M Ø Int
+m0 = 1
+
+m1 :: M '[N2] Int
+m1 = 2
+
+m2 :: M '[N2,N4] Int
+m2 = 3
+
+m3 :: M '[N2,N3,N4] (Int,Int,Int)
+m3 = mgen_ $ \(x :< y :> z) -> (fin x,fin y,fin z)
+
+m4 :: M '[N2,N3,N4,N5] (Int,Int,Int,Int)
+m4 = mgen_ $ \(w :< x :< y :> z) -> (fin w,fin x,fin y,fin z)
+
+ppVec :: (VT n ((->) String) String -> ShowS) -> (f a -> ShowS) -> VT n f a -> ShowS
+ppVec pV pF = pV . vmap pF
+
+ppMatrix :: forall ns a. (Show a, Known Length ns) => M ns a -> IO ()
+ppMatrix = putStrLn . ($ "") . ppMatrix' (known :: Length ns) . getMatrix
+
+ppMatrix' :: Show a => Length ns -> Matrix ns a -> ShowS
+ppMatrix' = \case
+  LZ   -> shows . getI
+  LS l -> ppVec
+    ( vfoldMap'
+      ( if lEven l
+        then zipLines $ \x y -> x . showChar '|'  . y
+        else            \x y -> x . showChar '\n' . y
+      ) (showString "[]") id
+    ) $ ppMatrix' l
+
+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
+
+zipLines :: (ShowS -> ShowS -> ShowS) -> ShowS -> ShowS -> ShowS
+zipLines f a b = compose $ L.intersperse (showChar '\n') $ mzipWith
+  (\(Endo x) (Endo y) -> f x y)
+  (Endo . showString <$> lines (a ""))
+  (Endo . showString <$> lines (b ""))
+
+{-
+juxtLines :: (ShowS -> ShowS -> ShowS) -> ShowS -> ShowS -> ShowS
+juxtLines f a b = appEndo $ foldMap id $ mzip (\x y -> Endo $ f (appEndo x) (appEndo y)) as bs
+  where
+  as = map (Endo . showString) $ lines $ a ""
+  bs = map (Endo . showString) $ lines $ b ""
+-}
+
+compose :: Foldable f => f (a -> a) -> a -> a
+compose = appEndo . foldMap Endo
+
+{-
+-- Linear {{{
+
+class Functor f => Additive f where
+  zero   :: Num a => f a
+  (^+^)  :: Num a => f a -> f a -> f a
+  (^-^)  :: Num a => f a -> f a -> f a
+  lerp   :: Num a =>   a -> f a -> f a -> f a
+  liftU2 :: (a -> a -> a) -> f a -> f a -> f a
+  liftI2 :: (a -> b -> c) -> f a -> f b -> f c
+  --------
+  default zero :: (Applicative f, Num a) => f a
+  zero = pure 0
+  (^+^)   = liftU2 (+)
+  a ^-^ b = a ^+^ negated b
+  lerp alpha a b = alpha *^ a ^+^ (1 - alpha) *^ b
+  default liftU2 :: Applicative f => (a -> a -> a) -> f a -> f a -> f a
+  liftU2 = liftA2
+  default liftI2 :: Applicative f => (a -> b -> c) -> f a -> f b -> f c
+  liftI2 = liftA2
+infixl 6 ^+^, ^-^
+
+instance Additive I
+instance (Additive f, Known Nat n) => Additive (VT n f) where
+  zero   = vrep zero
+  liftU2 = vap . liftU2
+  liftI2 = vap . liftI2
+
+class Additive (Diff f) => Affine f where
+  type Diff f :: * -> *
+  type Diff f = f
+  (.-.) :: Num a => f a -> f a -> Diff f a
+  (.+^) :: Num a => f a -> Diff f a -> f a
+  (.-^) :: Num a => f a -> Diff f a -> f a
+  --------
+  p .-^ d = p .+^ negated d
+  default (.-.) :: (Affine f, Diff f ~ f, Num a) => f a -> f a -> Diff f a
+  (.-.) = (^-^)
+  default (.+^) :: (Affine f, Diff f ~ f, Num a) => f a -> f a -> Diff f a
+  (.+^) = (^+^)
+infixl 6 .-., .+^, .-^
+
+instance Affine I
+instance (Affine f, Known Nat n) => Affine (VT n f) where
+  type Diff (VT n f) = VT n (Diff f)
+  (.-.) = vap (.-.)
+  (.+^) = vap (.+^)
+  (.-^) = vap (.-^)
+
+class Additive f => Metric f where
+  dot       :: Num a => f a -> f a -> a
+  quadrance :: Num a => f a -> a
+  qd        :: Num a => f a -> f a -> a
+  distance  :: Floating a => f a -> f a -> a
+  norm      :: Floating a => f a -> a
+  signorm   :: Floating a => f a -> f a
+  --------
+  default dot :: (Foldable f, Num a) => f a -> f a -> a
+  dot       a b = F.sum $ liftI2 (*) a b
+  quadrance     = join dot
+  qd        a b = quadrance $ a ^-^ b
+  distance  a b = norm $ a ^-^ b
+  norm          = sqrt . quadrance
+  signorm   a   = (/ norm a) <$> a
+
+instance Metric I where
+  dot (I a) (I b) = a * b
+
+instance (Metric f, Known Nat n) => Metric (VT n f) where
+  dot a b = getSum $ foldMap Sum $ vap ((I .) . dot) a b
+
+(*^) :: (Functor f, Num a) => a -> f a -> f a
+(*^) a = fmap (a*)
+infixl 7 *^
+
+negated :: (Functor f, Num a) => f a -> f a
+negated = fmap negate
+
+qdA :: (Affine f, Foldable (Diff f), Num a) => f a -> f a -> a
+qdA a b = F.sum $ join (*) <$> a .-. b
+
+distanceA :: (Affine f, Foldable (Diff f), Floating a) => f a -> f a -> a
+distanceA a b = sqrt $ qdA a b
+
+-- }}}
+-}
+
diff --git a/src/Type/Class/HFunctor.hs b/src/Type/Class/HFunctor.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Class/HFunctor.hs
@@ -0,0 +1,56 @@
+{-# 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/Known.hs b/src/Type/Class/Known.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Class/Known.hs
@@ -0,0 +1,51 @@
+{-# 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.Known
+-- Copyright   :  Copyright (C) 2015 Kyle Carter
+-- License     :  BSD3
+--
+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
+-- Stability   :  experimental
+-- Portability :  RankNTypes
+--
+-- The 'Known' class, among others in this library, use an associated
+-- 'Constraint' to maintain a bidirectional chain of inference.
+--
+-- For instance, given evidence of @Known Nat n@, if @n@ later gets refined
+-- to @n'@, we can correctly infer @Known Nat n'@, as per the type instance
+-- defined for @KnownC Nat (S n')@.
+----------------------------------------------------------------------------
+
+module Type.Class.Known where
+
+import Type.Family.Constraint
+
+import Data.Type.Equality
+
+-- | Each instance of 'Known' provides a canonical construction
+-- of a type at a particular index.
+--
+-- Useful for working with singleton-esque GADTs.
+class KnownC f a => Known (f :: k -> *) (a :: k) where
+  type KnownC f a :: Constraint
+  type KnownC (f :: k -> *) (a :: k) = ØC
+  known :: f a
+
+instance (a ~ b) => Known ((:~:) a) b where
+  type KnownC ((:~:) a) b = (a ~ b)
+  known = Refl
+
diff --git a/src/Type/Class/Witness.hs b/src/Type/Class/Witness.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Class/Witness.hs
@@ -0,0 +1,208 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# 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.Witness
+-- Copyright   :  Copyright (C) 2015 Kyle Carter
+-- License     :  BSD3
+--
+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
+-- Stability   :  experimental
+-- Portability :  RankNTypes
+--
+-- A type @t@ that is a @'Witness' p q t@ provides a 'Constraint' entailment
+-- of @q@, given that @p@ holds.
+--
+-- The 'Witness' class uses an associated 'Constraint' @WitnessC@ to
+-- maintain backwards inference of 'Witness' instances with respect
+-- to type refinement. See the 'Known' class for more information.
+--
+-- Heavily inspired by ekmett's constraints library:
+-- <http://hackage.haskell.org/package/constraints>
+--
+-- The code provided here does not /quite/ subsume the @constraints@
+-- library, as we do not give classes and instances for representing
+-- the standard library's class heirarchy and instance definitions.
+----------------------------------------------------------------------------
+
+module Type.Class.Witness
+  ( module Type.Class.Witness
+  , module Exports
+  ) where
+
+import Type.Class.Known
+import Type.Family.Constraint
+
+import Data.Type.Equality as Exports
+import Data.Void          as Exports
+
+import Prelude hiding (id,(.))
+import Control.Category
+import Unsafe.Coerce
+
+-- | A reified 'Constraint'.
+data Wit :: Constraint -> * where
+  Wit :: c => Wit c
+
+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
+-- if @p@ holds.
+--
+-- Entailment of 'Constraint's form a 'Category':
+--
+-- >>> id  :: p :- p
+-- >>> (.) :: (q :- r) -> (p :-> q) -> (p :- r)
+data (:-) :: Constraint -> Constraint -> * where
+  Sub :: { getSub :: p => Wit q } -> p :- q
+infixr 4 :-
+
+instance Category (:-) where
+  id              = Sub Wit
+  Sub bc . Sub ab = Sub $ bc \\ ab
+
+-- | A general eliminator for entailment.
+--
+-- Given a term of type @t@ with an instance @Witness p q t@
+-- and a term of type @r@ that depends on 'Constraint' @q@,
+-- we can reduce the Constraint to @p@.
+--
+-- If @p@ is @ØC@, i.e. the empty 'Constraint' @()@, then
+-- a Witness @t@ can completely discharge the Constraint @q@.
+class WitnessC p q t => Witness (p :: Constraint) (q :: Constraint) (t :: *) | t -> p q where
+  type WitnessC p q t :: Constraint
+  type WitnessC p q t = ØC
+  (\\) :: p => (q => r) -> t -> r
+infixl 1 \\
+
+-- | 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
+
+instance Witness ØC c (Wit c) where
+  r \\ Wit = r
+
+-- | An entailment @p :- q@ is a Witness of @q@, given @p@.
+instance Witness p q (p :- q) where
+  r \\ Sub Wit = r
+
+-- | A type equality @a ':~:' b@ is a Witness that @(a ~ b)@.
+instance Witness ØC (a ~ b) (a :~: b) where
+  r \\ Refl = r
+
+-- | If the constraint @c@ holds, there is a canonical construction
+-- for a term of type @'Wit' c@, viz. the constructor @Wit@.
+instance c => Known Wit c where
+  type KnownC Wit c = c
+  known = Wit
+
+-- | Constraint chaining under @Maybe@.
+(/?) :: (Witness p q t, p) => Maybe t -> (q => Maybe r) -> Maybe r
+(/?) = \case
+  Just t -> (\\ t)
+  _      -> \_ -> Nothing
+infixr 0 /?
+
+qed :: Maybe (a :~: a)
+qed = Just Refl
+
+impossible :: a -> Void
+impossible = unsafeCoerce
+
+data Dec a
+  = Proven   a
+  | Refuted (a -> Void)
+
+class DecEquality (f :: k -> *) where
+  decideEquality :: f a -> f b -> Dec (a :~: b)
+
+decCase :: Dec a
+  -> (a -> r)
+  -> ((a -> Void) -> r)
+  -> r
+decCase d y n = case d of
+  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)
+
+class Category c => Monoidal (c :: k -> k -> *) where
+  type Tensor c :: k -> k -> k
+  type Unit   c :: k
+  (.*.) :: c v w -> c x y -> c (Tensor c v x) (Tensor c w y)
+  assoc  :: c (Tensor c (Tensor c x y) z) (Tensor c x (Tensor c y z))
+  unitL  :: c (Tensor c (Unit c) x) x
+  unitR  :: c (Tensor c x (Unit c)) x
+infixr 3 .*.
+
+class Category c => Symmetric (c :: k -> k -> *) where
+  symm :: c a b -> c b a
+
+instance Category p => Symmetric (Bij p) where
+  symm p = bwd p <-> fwd p
+
+instance Monoidal (->) where
+  type Tensor (->) = (,)
+  type Unit   (->) = ()
+  (f .*. g) (a,b) = (f a,g b)
+  assoc ((x,y),z) = (x,(y,z))
+  unitL (_,x) = x
+  unitR (x,_) = x
+
+instance (Symmetric p, Monoidal p) => Monoidal (Bij p) where
+  type Tensor (Bij p) = Tensor p
+  type Unit   (Bij p) = Unit p
+  (.*.) = (***)
+  assoc = assoc <-> symm assoc
+  unitL = unitL <-> symm unitL
+  unitR = unitR <-> symm unitR
+
+(***) :: 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/Constraint.hs b/src/Type/Family/Constraint.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Family/Constraint.hs
@@ -0,0 +1,45 @@
+{-# 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.Constraint
+-- Copyright   :  Copyright (C) 2015 Kyle Carter
+-- License     :  BSD3
+--
+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
+-- Stability   :  experimental
+-- Portability :  RankNTypes
+--
+-- Reexports the kind 'GHC.Exts.Constraint', as well as some
+-- conveniences for working with 'Constraint's.
+----------------------------------------------------------------------------
+
+module Type.Family.Constraint
+  ( module Type.Family.Constraint
+  , Constraint
+  ) where
+
+import GHC.Exts (Constraint)
+
+-- | The empty 'Constraint'.
+type ØC = (() :: Constraint)
+
+class IffC b t f => Iff (b :: Bool) (t :: Constraint) (f :: Constraint) where
+  type IffC b t f :: Constraint
+instance t => Iff True  t f where
+  type IffC True  t f = t
+instance f => Iff False t f where
+  type IffC False t f = f
+
diff --git a/src/Type/Family/List.hs b/src/Type/Family/List.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Family/List.hs
@@ -0,0 +1,99 @@
+{-# 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.List
+-- Copyright   :  Copyright (C) 2015 Kyle Carter
+-- License     :  BSD3
+--
+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
+-- Stability   :  experimental
+-- Portability :  RankNTypes
+--
+-- Convenient aliases and type families for working with
+-- type-level lists.
+----------------------------------------------------------------------------
+
+module Type.Family.List
+  ( module Type.Family.List
+  , (==)
+  ) where
+
+import Type.Family.Constraint
+import Type.Family.Monoid
+
+import Data.Type.Bool
+import Data.Type.Equality
+
+type Ø    = '[]
+type (:<) = '(:)
+infixr 5 :<
+
+-- | Type-level singleton list.
+type Only a = '[a]
+
+-- | Appends two type-level lists.
+type family (as :: [k]) ++ (bs :: [k]) :: [k] where
+  Ø         ++ bs = bs
+  (a :< as) ++ bs = a :< (as ++ bs)
+infixr 5 ++
+
+-- | Type-level list snoc.
+type family (as :: [k]) >: (a :: k) :: [k] where
+  Ø         >: a = Only a
+  (b :< as) >: a = b :< (as >: a)
+infixl 6 >:
+
+type family Reverse (as :: [k]) :: [k] where
+  Reverse  Ø        = Ø
+  Reverse (a :< as) = Reverse as >: a
+
+type family Init' (a :: k) (as :: [k]) :: [k] where
+  Init' a Ø = Ø
+  Init' a (b :< as) = a :< Init' b as
+
+type family Last' (a :: k) (as :: [k]) :: k where
+  Last' a Ø         = a
+  Last' a (b :< as) = Last' b as
+
+-- | Takes a type-level list of 'Constraint's to a single
+-- 'Constraint', where @ListC cs@ holds iff all elements
+-- of @cs@ hold.
+type family ListC (cs :: [Constraint]) :: Constraint where
+  ListC  Ø        = ØC
+  ListC (c :< cs) = (c, ListC cs)
+
+-- | 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
+  f <$> Ø         = Ø
+  f <$> (a :< as) = f a :< (f <$> as)
+infixr 4 <$>
+
+-- | 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
+  Ø         <&> a = Ø
+  (f :< fs) <&> a = f a :< (fs <&> a)
+infixl 5 <&>
+
+type family (f :: [k -> l]) <*> (a :: [k]) :: [l] where
+  fs <*> Ø         = Ø
+  fs <*> (a :< as) = (fs <&> a) ++ (fs <*> as)
+infixr 4 <*>
+
+type instance Mempty = Ø
+type instance a <> b = a ++ b
+
diff --git a/src/Type/Family/Maybe.hs b/src/Type/Family/Maybe.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Family/Maybe.hs
@@ -0,0 +1,71 @@
+{-# 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.Maybe
+-- 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 @Maybe@s.
+----------------------------------------------------------------------------
+
+module Type.Family.Maybe
+  ( module Type.Family.Maybe
+  , type (==)
+  ) where
+
+import Type.Family.Constraint
+import Type.Family.Monoid
+
+import Data.Type.Equality
+
+-- | Take a @Maybe Constraint@ to a @Constraint@.
+type family MaybeC (mc :: Maybe Constraint) :: Constraint where
+  MaybeC Nothing  = ØC
+  MaybeC (Just c) = c
+
+-- | 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 <$>
+
+type family (f :: Maybe (k -> l)) <&> (a :: k) :: Maybe l where
+  Nothing <&> a = Nothing
+  Just f  <&> a = Just (f a)
+infixl 5 <&>
+
+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 <*>
+
+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 <|>
+
+type family FromJust (m :: Maybe k) :: k where
+  FromJust (Just a) = a
+
+type instance Mempty = Nothing
+type instance a <> b = a <|> b
+
diff --git a/src/Type/Family/Monoid.hs b/src/Type/Family/Monoid.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Family/Monoid.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Type.Family.Monoid
+-- Copyright   :  Copyright (C) 2015 Kyle Carter
+-- License     :  BSD3
+--
+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
+-- Stability   :  experimental
+-- Portability :  RankNTypes
+--
+-- Type-level @Monoid@, defined as an open type family.
+--
+-----------------------------------------------------------------------------
+
+module Type.Family.Monoid where
+
+type family Mempty :: k
+type family (a :: k) <> (b :: k) :: k
+
diff --git a/src/Type/Family/Nat.hs b/src/Type/Family/Nat.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Family/Nat.hs
@@ -0,0 +1,84 @@
+{-# 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.Nat
+-- Copyright   :  Copyright (C) 2015 Kyle Carter
+-- License     :  BSD3
+--
+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
+-- Stability   :  experimental
+-- Portability :  RankNTypes
+--
+-- Type-level natural numbers, along with frequently used
+-- type families over them.
+--
+-----------------------------------------------------------------------------
+
+module Type.Family.Nat
+  ( module Type.Family.Nat
+  , type (==)
+  ) where
+
+import Data.Type.Equality
+import Type.Family.List
+
+data N
+  = Z
+  | S N
+  deriving (Eq,Ord,Show)
+
+type family NatEq (x :: N) (y :: N) :: Bool where
+  NatEq  Z     Z    = True
+  NatEq  Z    (S y) = False
+  NatEq (S x)  Z    = False
+  NatEq (S x) (S y) = NatEq x y
+type instance x == y = NatEq x y
+
+type family Iota (x :: N) :: [N] where
+  Iota Z     = Ø
+  Iota (S x) = x :< Iota x
+
+type family Pred (x :: N) :: N where
+  Pred (S n) = n
+
+type family (x :: N) + (y :: N) :: N where
+  Z   + y = y
+  S x + y = S (x + y)
+infixr 6 +
+
+type family (x :: N) * (y :: N) :: N where
+  Z   * y = Z
+  S x * y = (x * y) + y
+infixr 7 *
+
+type family (x :: N) ^ (y :: N) :: N where
+  x ^   Z = S Z
+  x ^ S y = (x ^ y) * x
+infixl 8 ^
+
+-- | Convenient aliases for low-value Peano numbers.
+type N0  = Z
+type N1  = S N0
+type N2  = S N1
+type N3  = S N2
+type N4  = S N3
+type N5  = S N4
+type N6  = S N5
+type N7  = S N6
+type N8  = S N7
+type N9  = S N8
+type N10 = S N9
+
diff --git a/src/Type/Family/Pair.hs b/src/Type/Family/Pair.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Family/Pair.hs
@@ -0,0 +1,58 @@
+{-# 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/type-combinators.cabal b/type-combinators.cabal
new file mode 100644
--- /dev/null
+++ b/type-combinators.cabal
@@ -0,0 +1,50 @@
+name: type-combinators
+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
+version: 0.1.0.0
+cabal-version: >=1.10
+build-type: Simple
+license: BSD3
+license-file: LICENSE
+maintainer: kylcarte@gmail.com
+author: Kyle Carter
+
+source-repository head
+    type: git
+    location: git://github.com/kylcarte/type-combinators.git
+
+library
+    exposed-modules:
+        Data.Type.Combinator
+        Data.Type.Conjunction
+        Data.Type.Disjunction
+        Data.Type.Fin
+        Data.Type.Index
+        Data.Type.Length
+        Data.Type.Nat
+        Data.Type.Option
+        Data.Type.Product
+        Data.Type.Quantifier
+        Data.Type.Sum
+        Data.Type.Vector
+        Type.Class.HFunctor
+        Type.Class.Known
+        Type.Class.Witness
+        Type.Family.Constraint
+        Type.Family.List
+        Type.Family.Maybe
+        Type.Family.Monoid
+        Type.Family.Nat
+        Type.Family.Pair
+    build-depends:
+        base >=4.8 && <4.9
+    default-language: Haskell2010
+    hs-source-dirs: src
+