diff --git a/src/Data/Type/Boolean.hs b/src/Data/Type/Boolean.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Boolean.hs
@@ -0,0 +1,104 @@
+{-# 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.Boolean
+-- Copyright   :  Copyright (C) 2015 Kyle Carter
+-- License     :  BSD3
+--
+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
+-- Stability   :  experimental
+-- Portability :  RankNTypes
+--
+-- A @singleton@-esque type for type-level Bool values.
+--
+-----------------------------------------------------------------------------
+
+module Data.Type.Boolean where
+
+import Data.Type.Quantifier (Some(..))
+import Type.Family.Bool
+import Type.Class.Known
+import Type.Class.Higher
+
+data Boolean :: Bool -> * where
+  False_ :: Boolean False
+  True_  :: Boolean True
+
+deriving instance Eq   (Boolean b)
+deriving instance Ord  (Boolean b)
+deriving instance Show (Boolean b)
+
+instance Eq1   Boolean
+instance Ord1  Boolean
+instance Show1 Boolean
+
+instance Read1 Boolean where
+  readsPrec1 _ s0 =
+    [ (Some True_,s1)
+    | ("True_",s1) <- lex s0
+    ] ++
+    [ (Some False_,s1)
+    | ("False_",s1) <- lex s0
+    ]
+
+not' :: Boolean a -> Boolean (Not a)
+not' = \case
+  False_ -> True_
+  True_  -> False_
+
+(.||) :: Boolean a -> Boolean b -> Boolean (a || b)
+(.||) = \case
+  False_ -> id
+  True_  -> const True_
+infixr 2 .||
+
+(.&&) :: Boolean a -> Boolean b -> Boolean (a && b)
+(.&&) = \case
+  False_ -> const False_
+  True_  -> id
+infixr 3 .&&
+
+(.^^) :: Boolean a -> Boolean b -> Boolean (a ^^ b)
+a .^^ b = (a .|| b) .&& not' (a .&& b)
+infixr 4 .^^
+
+(==>) :: Boolean a -> Boolean b -> Boolean (a ==> b)
+a ==> b = not' a .|| b
+infixr 1 ==>
+
+(<==>) :: Boolean a -> Boolean b -> Boolean (a <==> b)
+(<==>) = (.==)
+infixr 1 <==>
+
+class BoolEq (f :: k -> *) where
+  (.==) :: f a -> f b -> Boolean (a == b)
+infix 4 .==
+
+instance BoolEq Boolean where
+  (.==) = \case
+    False_ -> \case
+      False_ -> True_
+      True_  -> False_
+    True_  -> \case
+      False_ -> False_
+      True_  -> True_
+
+instance Known Boolean True where
+  known = True_
+
+instance Known Boolean False where
+  known = False_
+
diff --git a/src/Data/Type/Fin/Indexed.hs b/src/Data/Type/Fin/Indexed.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Fin/Indexed.hs
@@ -0,0 +1,179 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE GADTs #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Type.Fin.Indexed
+-- 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,
+-- indexed by its Nat value.
+--
+-----------------------------------------------------------------------------
+
+module Data.Type.Fin.Indexed where
+
+import Data.Type.Nat
+import Type.Class.Higher
+-- import Type.Class.Known
+import Type.Class.Witness
+import Type.Family.Constraint
+import Type.Family.Nat
+import Data.Type.Quantifier
+
+data IFin :: N -> N -> * where
+  IFZ :: IFin (S x) Z
+  IFS :: !(IFin x y) -> IFin (S x) (S y)
+
+deriving instance Eq   (IFin x y)
+deriving instance Ord  (IFin x y)
+deriving instance Show (IFin x y)
+
+instance Eq1   (IFin x)
+instance Ord1  (IFin x)
+instance Show1 (IFin x)
+
+instance Eq2   IFin
+instance Ord2  IFin
+instance Show2 IFin
+
+instance Read2 IFin where
+  readsPrec2 d = readParen (d > 10) $ \s0 ->
+    [ (Some2 IFZ,s1)
+    | ("IFZ",s1) <- lex s0
+    ] ++ 
+    [ (n >>-- Some2 . IFS,s2)
+    | ("IFS",s1) <- lex s0
+    , (n,s2)    <- readsPrec2 11 s1
+    ]
+
+class LTC x y => LessEq (x :: N) (y :: N) where
+  type LTC x y :: Constraint
+  liftIFin :: IFin x z -> IFin y z
+
+instance LessEq Z y where
+  type LTC Z y = ØC
+  liftIFin = absurd . ifinZ
+
+instance (y ~ S (Pred y), LessEq x (Pred y)) => LessEq (S x) y where
+  type LTC (S x) y = (y ~ S (Pred y), LessEq x (Pred y))
+  liftIFin = \case
+    IFZ   -> IFZ
+    IFS x -> IFS $ liftIFin x
+
+ifinZ :: IFin Z x -> Void
+ifinZ = impossible
+
+weaken :: IFin x y -> IFin (S x) y
+weaken = \case
+  IFZ   -> IFZ
+  IFS n -> IFS $ weaken n
+
+ifinNat :: IFin x y -> Nat y
+ifinNat = \case
+  IFZ   -> Z_
+  IFS n -> S_ $ ifinNat n
+
+ifinVal :: IFin x y -> Int
+ifinVal = natVal . ifinNat
+
+onIFinPred :: (forall x. IFin m x -> IFin n x) -> IFin (S m) y -> IFin (S n) y
+onIFinPred f = \case
+  IFZ   -> IFZ
+  IFS m -> IFS $ f m
+
+{-
+-- | Map a finite set to a lower finite set without
+-- one of its members.
+without :: IFin n x -> IFin n y -> Maybe (IFin (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
+-}
+
+-- | An @IFin x y@ is a 'Witness' that @x >= 1@.
+--
+-- That is, @'Pred' x@ is well defined.
+instance (x' ~ Pred x) => Witness ØC (S x' ~ x) (IFin x y) where
+  type WitnessC ØC (S x' ~ x) (IFin x y) = (x' ~ Pred x)
+  (\\) r = \case
+    IFZ   -> r
+    IFS _ -> r
+
+{-
+elimFin :: (forall x. p (S x))
+        -> (forall x. Fin x -> p x -> p (S x))
+        -> Fin n -> p n
+elimFin z s = \case
+  FZ   -> z
+  FS n -> s n $ elimFin z s n
+
+-- | Gives the list of all members of the finite set of size @n@.
+fins :: Nat n -> [Fin n]
+fins = \case
+  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
+
+-- | 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/Nat.hs b/src/Data/Type/Nat.hs
--- a/src/Data/Type/Nat.hs
+++ b/src/Data/Type/Nat.hs
@@ -85,6 +85,12 @@
       Z_   -> Nothing
       S_ y -> testEquality x y //? qed
 
+pred' :: Nat (S x) -> Nat x
+pred' (S_ x) = x
+
+onNatPred :: (Nat x -> Nat y) -> Nat (S x) -> Nat (S y)
+onNatPred f (S_ x) = S_ $ f x
+
 _Z :: Z :~: Z
 _Z = Refl
 
diff --git a/src/Data/Type/Nat/Inequality.hs b/src/Data/Type/Nat/Inequality.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Nat/Inequality.hs
@@ -0,0 +1,82 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE LambdaCase #-}
+
+module Data.Type.Nat.Inequality where
+
+import Data.Type.Nat
+import Type.Class.Known
+import Type.Class.Witness
+import Type.Family.Constraint
+import Type.Family.Nat
+
+type family (x :: N) < (y :: N) :: Bool where
+  Z   < Z   = False
+  Z   < S y = True
+  S x < Z   = False
+  S x < S y = x < y
+infix 4 <
+
+type family (x :: N) > (y :: N) :: Bool where
+  Z   > Z   = False
+  Z   > S y = False
+  S x > Z   = True
+  S x > S y = x > y
+infix 4 >
+
+data NatLT :: N -> N -> * where
+  LTZ :: NatLT Z (S y)
+  LTS :: !(NatLT x y)
+      -> NatLT (S x) (S y)
+
+data NatEQ :: N -> N -> * where
+  EQZ :: NatEQ Z Z
+  EQS :: !(NatEQ x y)
+      -> NatEQ (S x) (S y)
+
+data NatGT :: N -> N -> * where
+  GTZ :: NatGT (S x) Z
+  GTS :: !(NatGT x y)
+      -> NatGT (S x) (S y)
+
+instance (lt ~ (x < y), eq ~ (x == y), gt ~ (x > y), y' ~ Pred y) => Witness ØC (y ~ S y', Known Nat x, lt ~ True, eq ~ False, gt ~ False) (NatLT x y) where
+  type WitnessC ØC (y ~ S y', Known Nat x, lt ~ True, eq ~ False, gt ~ False) (NatLT x y) = (lt ~ (x < y), eq ~ (x == y), gt ~ (x > y), y' ~ Pred y)
+  (\\) r = \case
+    LTZ   -> r
+    LTS l -> r \\ l
+
+instance (lt ~ (x < y), eq ~ (x == y), gt ~ (x > y)) => Witness ØC (x ~ y, Known Nat x, lt ~ False, eq ~ True, gt ~ False) (NatEQ x y) where
+  type WitnessC ØC (x ~ y, Known Nat x, lt ~ False, eq ~ True, gt ~ False) (NatEQ x y) = (lt ~ (x < y), eq ~ (x == y), gt ~ (x > y))
+  (\\) r = \case
+    EQZ   -> r
+    EQS l -> r \\ l
+
+instance (lt ~ (x < y), eq ~ (x == y), gt ~ (x > y), x' ~ Pred x) => Witness ØC (x ~ S x', Known Nat y, lt ~ False, eq ~ False, gt ~ True) (NatGT x y) where
+  type WitnessC ØC (x ~ S x', Known Nat y, lt ~ False, eq ~ False, gt ~ True) (NatGT x y) = (lt ~ (x < y), eq ~ (x == y), gt ~ (x > y), x' ~ Pred x)
+  (\\) r = \case
+    GTZ   -> r
+    GTS l -> r \\ l
+
+natCompare :: Nat x -> Nat y -> Either (NatLT x y) (Either (NatEQ x y) (NatGT x y))
+natCompare = \case
+  Z_   -> \case
+    Z_   -> Right $ Left EQZ
+    S_ _ -> Left LTZ
+  S_ x -> \case
+    Z_   -> Right $ Right GTZ
+    S_ y -> case natCompare x y of
+      Left         lt  -> Left          $ LTS lt
+      Right (Left  eq) -> Right $ Left  $ EQS eq
+      Right (Right gt) -> Right $ Right $ GTS gt
+
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
@@ -59,6 +59,10 @@
 (>>-) = some
 infixl 1 >>-
 
+(>->) :: (forall x. f x -> Some g) -> (forall x. g x -> Some h) -> f a -> Some h
+(f >-> g) a = f a >>- g
+infixr 1 >->
+
 withSome :: (forall a. f a -> r) -> Some f -> r
 withSome f (Some a) = f a
 
@@ -79,6 +83,10 @@
 (>>--) = some2
 infixl 1 >>--
 
+(>-->) :: (forall x y. f x y -> Some2 g) -> (forall x y. g x y -> Some2 h) -> f a b -> Some2 h
+(f >--> g) a = f a >>-- g
+infixr 1 >-->
+
 withSome2 :: (forall a b. f a b -> r) -> Some2 f -> r
 withSome2 f (Some2 a) = f a
 
@@ -98,6 +106,10 @@
 (>>---) :: Some3 f -> (forall a b c. f a b c -> r) -> r
 (>>---) = some3
 infixl 1 >>---
+
+(>--->) :: (forall x y z. f x y z -> Some3 g) -> (forall x y z. g x y z -> Some3 h) -> f a b c -> Some3 h
+(f >---> g) a = f a >>--- g
+infixr 1 >--->
 
 withSome3 :: (forall a b c. f a b c -> r) -> Some3 f -> r
 withSome3 f (Some3 a) = f a
diff --git a/src/Data/Type/Sym.hs b/src/Data/Type/Sym.hs
--- a/src/Data/Type/Sym.hs
+++ b/src/Data/Type/Sym.hs
@@ -44,7 +44,7 @@
 
 instance Show (Sym x) where
   showsPrec d x = showParen (d > 0)
-    $ showString "Sym :: Sym "
+    $ showString "Sym "
     . shows (symbol x)
 
 instance Eq1   Sym
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
@@ -106,6 +106,10 @@
   (\\) :: p => (q => r) -> t -> r
 infixl 1 \\
 
+(//) :: (Witness p q t, p) => t -> (q => r) -> r
+t // r = r \\ t
+infixr 0 //
+
 -- | Convert a 'Witness' to a canonical reified 'Constraint'.
 witnessed :: Witness ØC q t => t -> Wit q
 witnessed t = Wit \\ t
@@ -185,8 +189,6 @@
 top :: a :- ØC
 top = Sub Wit
 
-type Fail = (True ~ False)
-
 bottom :: Fail :- c
 bottom = falso
 
@@ -220,6 +222,12 @@
   Just t -> (\\ t)
   _      -> \_ -> Nothing
 infixr 0 //?
+
+(//?+) :: (Witness p q t, p) => Either e t -> (q => Either e r) -> Either e r
+(//?+) = \case
+  Left  e -> \_ -> Left e
+  Right t -> (\\ t)
+infixr 0 //?+
 
 witMaybe :: (Witness p q t, p) => Maybe t -> (q => Maybe r) -> Maybe r -> Maybe r
 witMaybe mt y n = case mt of
diff --git a/src/Type/Family/Bool.hs b/src/Type/Family/Bool.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Family/Bool.hs
@@ -0,0 +1,62 @@
+{-# 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.Bool
+-- 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 @Bool@s.
+----------------------------------------------------------------------------
+
+module Type.Family.Bool
+  ( module Type.Family.Bool
+  , type (==)
+  ) where
+
+import Type.Family.Constraint
+import Type.Class.Witness (type (==))
+
+type family BoolC (b :: Bool) :: Constraint where
+  BoolC True  = ØC
+  BoolC False = Fail
+
+type family (a :: Bool) || (b :: Bool) :: Bool where
+  True  || b = True
+  False || b = b
+infixr 2 ||
+
+type family (a :: Bool) && (b :: Bool) :: Bool where
+  True  && b = b
+  False && b = False
+infixr 3 &&
+
+type family Not (a :: Bool) :: Bool where
+  Not True  = False
+  Not False = True
+
+type a ==> b = Not a || b
+infixr 1 ==>
+
+type a <==> b = a == b
+infixr 1 <==>
+
+type a ^^ b = (a || b) && Not (a && b)
+infixr 4 ^^
+
diff --git a/src/Type/Family/Constraint.hs b/src/Type/Family/Constraint.hs
--- a/src/Type/Family/Constraint.hs
+++ b/src/Type/Family/Constraint.hs
@@ -34,7 +34,8 @@
 import GHC.Exts (Constraint)
 
 -- | The empty 'Constraint'.
-type ØC = (() :: Constraint)
+type ØC   = (() :: Constraint)
+type Fail = (True ~ False)
 
 class IffC b t f => Iff (b :: Bool) (t :: Constraint) (f :: Constraint) where
   type IffC b t f :: Constraint
diff --git a/src/Type/Family/List.hs b/src/Type/Family/List.hs
--- a/src/Type/Family/List.hs
+++ b/src/Type/Family/List.hs
@@ -40,7 +40,7 @@
 -- | Type-level singleton list.
 type Only a = '[a]
 
--- Null,Append {{{
+-- Null,Append,Concat {{{
 
 type family Null (as :: [k]) :: Bool where
   Null Ø         = True
@@ -60,6 +60,13 @@
 
 appendCong :: (a ~ b,c ~ d) :- ((a ++ c) ~ (b ++ d))
 appendCong = Sub Wit
+
+type family Concat (ls :: [[k]]) :: [k] where
+  Concat Ø         = Ø
+  Concat (l :< ls) = l ++ Concat ls
+
+concatCong :: (as ~ bs) :- (Concat as ~ Concat bs)
+concatCong = Sub Wit
 
 -- }}}
 
diff --git a/src/Type/Family/Nat.hs b/src/Type/Family/Nat.hs
--- a/src/Type/Family/Nat.hs
+++ b/src/Type/Family/Nat.hs
@@ -30,6 +30,7 @@
 module Type.Family.Nat where
 
 import Data.Type.Equality
+import Type.Family.Constraint
 import Type.Family.List
 import Type.Class.Witness
 
diff --git a/type-combinators.cabal b/type-combinators.cabal
--- a/type-combinators.cabal
+++ b/type-combinators.cabal
@@ -1,5 +1,5 @@
 name: type-combinators
-version: 0.2.0.0
+version: 0.2.1.0
 category: Data
 synopsis: A collection of data types for type-level programming
 cabal-version: >=1.10
@@ -7,6 +7,7 @@
 license: BSD3
 license-file: LICENSE
 maintainer: kylcarte@gmail.com
+copyright: (c) 2015 Kyle Carter, all rights reserved
 author: Kyle Carter
 homepage: https://github.com/kylcarte/type-combinators
 
@@ -16,13 +17,16 @@
 
 library
     exposed-modules:
+        Data.Type.Boolean
         Data.Type.Combinator
         Data.Type.Conjunction
         Data.Type.Disjunction
         Data.Type.Fin
+        Data.Type.Fin.Indexed
         Data.Type.Index
         Data.Type.Length
         Data.Type.Nat
+        Data.Type.Nat.Inequality
         Data.Type.Option
         Data.Type.Product
         Data.Type.Product.Lifted
@@ -34,6 +38,7 @@
         Type.Class.Higher
         Type.Class.Known
         Type.Class.Witness
+        Type.Family.Bool
         Type.Family.Constraint
         Type.Family.Either
         Type.Family.List