diff --git a/src/Data/Type/Boolean.hs b/src/Data/Type/Boolean.hs
--- a/src/Data/Type/Boolean.hs
+++ b/src/Data/Type/Boolean.hs
@@ -30,9 +30,9 @@
 
 import Data.Type.Quantifier (Some(..))
 import Type.Family.Bool
-import Type.Family.Constraint
 import Type.Class.Known
 import Type.Class.Higher
+import Type.Class.Witness
 
 data Boolean :: Bool -> * where
   False_ :: Boolean False
@@ -55,53 +55,62 @@
     | ("False_",s1) <- lex s0
     ]
 
+if' :: Boolean b -> ((b ~ True) => a) -> ((b ~ False) => a) -> a
+if' t c a = case t of
+  True_  -> c
+  False_ -> a
+
+(.?) :: ((b ~ True) => a) -> ((b ~ False) => a) -> Boolean b -> a
+(c .? a) t = if' t c a
+infix 4 .?
+
 not' :: Boolean a -> Boolean (Not a)
-not' = \case
-  False_ -> True_
-  True_  -> False_
+not' = False_ .? True_
 
 (.||) :: Boolean a -> Boolean b -> Boolean (a || b)
-(.||) = \case
-  False_ -> id
-  True_  -> const True_
+(.||) = (True_ .? True_ )
+     .? (True_ .? False_)
 infixr 2 .||
 
 (.&&) :: Boolean a -> Boolean b -> Boolean (a && b)
-(.&&) = \case
-  False_ -> const False_
-  True_  -> id
+(.&&) = (True_  .? False_)
+     .? (False_ .? False_)
 infixr 3 .&&
 
 (.^^) :: Boolean a -> Boolean b -> Boolean (a ^^ b)
-a .^^ b = (a .|| b) .&& not' (a .&& b)
+(.^^) = (False_ .? True_ )
+     .? (True_  .? False_)
 infixr 4 .^^
 
 (==>) :: Boolean a -> Boolean b -> Boolean (a ==> b)
-a ==> b = not' a .|| b
+(==>) = (True_ .? False_)
+     .? (True_ .? True_ )
 infixr 1 ==>
 
 (<==>) :: Boolean a -> Boolean b -> Boolean (a <==> b)
-(<==>) = (.==)
+(<==>) = (True_  .? False_)
+      .? (False_ .? True_ )
 infixr 1 <==>
 
 class BoolEquality (f :: k -> *) where
-  type BoolEqC f (a :: k) (b :: k) :: Constraint
-  type BoolEqC f a b = ØC
-  (.==) :: BoolEqC f a b => f a -> f b -> Boolean (a == b)
+  boolEquality :: f a -> f b -> Boolean (a == b)
+
+(.==) :: BoolEquality f => f a -> f b -> Boolean (a == b)
+(.==) = boolEquality
 infix 4 .==
 
 instance BoolEquality Boolean where
-  (.==) = \case
-    False_ -> \case
-      False_ -> True_
-      True_  -> False_
-    True_  -> \case
-      False_ -> False_
-      True_  -> True_
+  boolEquality = (<==>)
 
+instance TestEquality Boolean where
+  testEquality = (qed .? Nothing) .? (Nothing .? qed)
+
 instance Known Boolean True where
   known = True_
 
 instance Known Boolean False where
   known = False_
+
+toBool :: Boolean b -> Bool
+toBool = True .? False
 
diff --git a/src/Data/Type/Combinator.hs b/src/Data/Type/Combinator.hs
--- a/src/Data/Type/Combinator.hs
+++ b/src/Data/Type/Combinator.hs
@@ -36,12 +36,24 @@
 module Data.Type.Combinator where
 
 import Data.Type.Quantifier
+import Data.Type.Index.Trans
 import Type.Class.Higher
 import Type.Class.Known
 import Type.Class.Witness
 import Type.Family.Tuple
 
 import Control.Applicative
+
+data Comp1 (f :: l -> m -> *) (g :: k -> l) :: k -> m -> * where
+  Comp1 :: { getComp1 :: !(f (g h) a)
+           }
+        -> Comp1 f g h a
+
+instance (Functor1 f, Functor1 g) => Functor1 (Comp1 (f :: (l -> *) -> m -> *) (g :: (k -> *) -> l -> *)) where
+  map1 f (Comp1 a) = Comp1 $ map1 (map1 f) a
+
+instance (IxFunctor1 i f, IxFunctor1 j g) => IxFunctor1 (IxComp i j) (Comp1 (f :: (l -> *) -> m -> *) (g :: (k -> *) -> l -> *)) where
+  imap1 f = Comp1 . imap1 (\i -> imap1 $ \j -> f $ IxComp i j) . getComp1
 
 -- (:.:) {{{
 
diff --git a/src/Data/Type/Conjunction.hs b/src/Data/Type/Conjunction.hs
--- a/src/Data/Type/Conjunction.hs
+++ b/src/Data/Type/Conjunction.hs
@@ -32,17 +32,17 @@
 
 module Data.Type.Conjunction where
 
+import Data.Type.Index.Trans
 import Type.Class.Higher
 import Type.Class.Known
 import Type.Class.Witness
 import Type.Family.Tuple
-import Data.Type.Boolean
 
 -- (:&:) {{{
 
 data ((f :: k -> *) :&: (g :: k -> *)) :: k -> * where
   (:&:) :: !(f a) -> !(g a) -> (f :&: g) a
-infixr 5 :&:
+infixr 6 :&:
 
 deriving instance (Eq   (f a), Eq   (g a)) => Eq   ((f :&: g) a)
 deriving instance (Ord  (f a), Ord  (g a)) => Ord  ((f :&: g) a)
@@ -105,7 +105,7 @@
 
 data ((f :: k -> *) :*: (g :: l -> *)) :: (k,l) -> * where
   (:*:) :: !(f a) -> !(g b) -> (f :*: g) (a#b)
-infixr 5 :*:
+infixr 6 :*:
 
 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)
@@ -150,6 +150,11 @@
 
 instance Bifunctor1 (:*:) where
   bimap1 f g (a :*: b) = f a :*: g b
+
+instance IxFunctor1 (IxSecond (:~:)) ((:*:) f) where
+  imap1 f (a :*: b) = a :*: f (IxSecond Refl) b
+
+-- f :: (k -> *) ==> ((:*:) f) :: (l -> *) -> (k,l) -> *
 
 _fst :: (a#b) :~: (c#d) -> a :~: c
 _fst Refl = Refl
diff --git a/src/Data/Type/Index/Trans.hs b/src/Data/Type/Index/Trans.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Index/Trans.hs
@@ -0,0 +1,59 @@
+{-# LANGUAGE FunctionalDependencies #-}
+{-# 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.Index.Trans
+  ( module Data.Type.Index.Trans
+  , (:~:)(..)
+  ) where
+
+import Data.Type.Index
+import Type.Class.Witness ((:~:)(..))
+import Type.Family.List
+
+ixList :: Index a b -> i b c -> IxList i a c
+ixList = \case
+  IZ   -> IxHead
+  IS x -> IxTail . ixList x
+
+data IxList (i :: k -> l -> *) :: [k] -> l -> * where
+  IxHead :: !(i a b)
+         -> IxList i (a :< as) b
+  IxTail :: !(IxList i as b)
+         -> IxList i (a :< as) b
+
+data IxFirst (i :: k -> l -> *) :: (k,m) -> l -> * where
+  IxFirst :: !(i a b)
+          -> IxFirst i '(a,c) b
+
+data IxSecond (i :: k -> l -> *) :: (m,k) -> l -> * where
+  IxSecond :: !(i a b)
+           -> IxSecond i '(c,a) b
+
+data IxOr (i :: k -> m -> *) (j :: l -> m -> *) :: Either k l -> m -> * where
+  IxOrL :: !(i a b)
+        -> IxOr i j (Left a) b
+  IxOrR :: !(j a b)
+        -> IxOr i j (Right a) b
+
+data IxJust (i :: k -> l -> *) :: Maybe k -> l -> * where
+  IxJust :: !(i a b)
+         -> IxJust i (Just a) b
+
+data IxComp (i :: k -> l -> *) (j :: l -> m -> *) :: k -> m -> * where
+  IxComp :: !(i a b)
+         -> !(j b c)
+         -> IxComp i j a c
+
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
@@ -87,7 +87,7 @@
       S_ y -> testEquality x y //? qed
 
 instance BoolEquality Nat where
-  (.==) = \case
+  boolEquality = \case
     Z_ -> \case
       Z_   -> True_
       S_ _ -> False_
diff --git a/src/Data/Type/Option.hs b/src/Data/Type/Option.hs
--- a/src/Data/Type/Option.hs
+++ b/src/Data/Type/Option.hs
@@ -38,6 +38,13 @@
   Nothing_ :: Option f Nothing
   Just_    :: !(f a) -> Option f (Just a)
 
+deriving instance MaybeC (Eq   <$> f <$> m) => Eq   (Option f m)
+deriving instance
+  ( MaybeC (Eq   <$> f <$> m)
+  , MaybeC (Ord  <$> f <$> m)
+  ) => Ord (Option f m)
+deriving instance MaybeC (Show <$> f <$> m) => Show (Option f m)
+
 -- | Eliminator for @'Option' f@.
 option :: (forall a. (m ~ Just a) => f a -> r) -> ((m ~ Nothing) => r) -> Option f m -> r
 option j n = \case
diff --git a/src/Data/Type/Product.hs b/src/Data/Type/Product.hs
--- a/src/Data/Type/Product.hs
+++ b/src/Data/Type/Product.hs
@@ -31,7 +31,7 @@
 --
 -- '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
+-- Oleg Kiselyov'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>.
 --
@@ -39,6 +39,7 @@
 
 module Data.Type.Product where
 
+import Data.Type.Boolean
 import Data.Type.Combinator
 import Data.Type.Conjunction
 import Data.Type.Index
@@ -100,6 +101,19 @@
       ]
     ) s0
 
+instance BoolEquality f => BoolEquality (Prod f) where
+  boolEquality = \case
+    Ø -> \case
+      Ø      -> True_
+      (:<){} -> False_
+    a :< as -> \case
+      b :< bs -> case a .== b of
+        True_  -> case as .== bs of
+          True_  -> True_
+          False_ -> False_
+        False_ -> False_
+      Ø -> False_
+
 instance TestEquality f => TestEquality (Prod f) where
   testEquality = \case
     Ø -> \case
@@ -162,10 +176,12 @@
   Ø       -> id
   a :< as -> (a :<) . append' as
 
+{-
 lookup' :: TestEquality f => f a -> Prod (f :&: g) as -> Maybe (g a)
 lookup' a = \case
   Ø               -> Nothing
   (b :&: v) :< bs -> witMaybe (a =?= b) (Just v) $ lookup' a bs
+-}
 
 lookupPar :: TestEquality f => f a -> Prod (f :*: g) as -> Maybe (Some g)
 lookupPar a = \case
@@ -273,4 +289,9 @@
 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
+
+toList :: (forall a. f a -> r) -> Prod f as -> [r]
+toList f = \case
+  Ø       -> []
+  a :< as -> f a : toList f as
 
diff --git a/src/Data/Type/Product/Env.hs b/src/Data/Type/Product/Env.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Product/Env.hs
@@ -0,0 +1,113 @@
+{-# 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.Product.Env where
+
+import Data.Type.Combinator (Comp1(..))
+import Data.Type.Conjunction
+import Data.Type.Boolean
+import Data.Type.Index
+import Data.Type.Index.Trans
+import Data.Type.Option
+import Data.Type.Product
+import Type.Class.Higher
+import Type.Class.Witness
+import Type.Family.Bool
+import Type.Family.List
+
+newtype Env k v ps = Env
+  { getEnv :: Prod (k :*: v) ps
+  }
+
+type family Member (x :: k) (ps :: [(k,v)]) :: Bool where
+  Member x Ø              = False
+  Member x ('(y,a) :< ps) = (x == y) || Member x ps
+
+member' :: BoolEquality k => k x -> Env k v ps -> Boolean (Member x ps)
+member' x = (. getEnv) $ \case
+  Ø               -> False_
+  (y :*: _) :< ps -> (x .== y) .|| member' x (Env ps)
+
+type family Lookup (x :: k) (ps :: [(k,v)]) :: Maybe v where
+  Lookup x Ø              = Nothing
+  Lookup x ('(y,a) :< ps) = If (x == y) (Just a) (Lookup x ps)
+
+lookup' :: BoolEquality k => k x -> Env k v ps -> Option v (Lookup x ps)
+lookup' x = (. getEnv) $ \case
+  Ø              -> Nothing_
+  (y :*: a) :< ps -> if' (x .== y)
+    (Just_ a)
+    (lookup' x $ Env ps)
+
+type family Insert (x :: k) (a :: v) (ps :: [(k,v)]) :: [(k,v)] where
+  Insert x a Ø              = '[ '(x,a) ]
+  Insert x a ('(y,b) :< ps) = If (x == y) ('(x,a) :< ps) ('(y,b) :< Insert x a ps)
+
+insert' :: BoolEquality k => k x -> v a -> Env k v ps -> Env k v (Insert x a ps)
+insert' x a = (. getEnv) $ \case
+  Ø               -> Env $ (x :*: a) :< Ø
+  (y :*: b) :< ps -> if' (x .== y)
+    (Env $ (x :*: a) :< ps)
+    (Env $ (y :*: b) :< getEnv (insert' x a (Env ps)))
+
+type family Delete (x :: k) (ps :: [(k,v)]) :: [(k,v)] where
+  Delete x Ø              = Ø
+  Delete x ('(y,a) :< ps) = If (x == y) ps ('(y,a) :< Delete x ps)
+
+delete' :: BoolEquality k => k x -> Env k v ps -> Env k v (Delete x ps)
+delete' x = (. getEnv) $ \case
+  Ø               -> Env Ø
+  (y :*: a) :< ps -> if' (x .== y)
+    (Env ps)
+    (Env $ (y :*: a) :< getEnv (delete' x (Env ps)))
+
+type family Difference (ps :: [(k,v)]) (qs :: [(k,w)]) :: [(k,v)] where
+  Difference ps Ø              = ps
+  Difference ps ('(x,a) :< qs) = Delete x (Difference ps qs)
+
+difference' :: BoolEquality k => Env k v ps -> Env k w qs -> Env k v (Difference ps qs)
+difference' ps = (. getEnv) $ \case
+  Ø               -> ps
+  (x :*: _) :< qs -> delete' x $ difference' ps (Env qs)
+
+(.\\) :: BoolEquality k => Env k v ps -> Env k w qs -> Env k v (Difference ps qs)
+(.\\) = difference'
+
+type family Union (ps :: [(k,v)]) (qs :: [(k,v)]) :: [(k,v)] where
+  Union ps Ø              = ps
+  Union ps ('(x,a) :< qs) = Insert x a (Union ps qs)
+
+union' :: BoolEquality k => Env k v ps -> Env k v qs -> Env k v (Union ps qs)
+union' ps = (. getEnv) $ \case
+  Ø               -> ps
+  (x :*: a) :< qs -> insert' x a $ union' ps (Env qs)
+
+type family Intersection (ps :: [(k,v)]) (qs :: [(k,w)]) :: [(k,v)] where
+  Intersection Ø              qs = Ø
+  Intersection ('(x,a) :< ps) qs = If (Member x qs) ('(x,a) :< Intersection ps qs) (Intersection ps qs)
+
+intersection' :: BoolEquality k => Env k v ps -> Env k w qs -> Env k v (Intersection ps qs)
+intersection' ps qs = case getEnv ps of
+  Ø                -> Env Ø
+  (x :*: a) :< ps' -> if' (member' x qs) (Env $ (x :*: a) :< getEnv rest) rest
+    where
+    rest = intersection' (Env ps') qs
+
+instance Functor1 (Env k) where
+  map1 f = Env . getComp1 . map1 f . Comp1 . getEnv
+
+instance IxFunctor1 (IxList (IxSecond (:~:))) (Env k) where
+  imap1 f = Env . imap1 (\i -> imap1 $ \j -> f $ ixList i j) . getEnv
+
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
@@ -55,10 +55,6 @@
 instance TestEquality Sym where
   testEquality Sym Sym = sameSymbol Proxy Proxy
 
-instance BoolEquality Sym where
-  type BoolEqC Sym a b = Known Boolean (a == b)
-  Sym .== Sym = known
-
 instance KnownSymbol x => Known Sym x where
   type KnownC Sym x = KnownSymbol x
   known = Sym
diff --git a/src/Type/Family/Bool.hs b/src/Type/Family/Bool.hs
--- a/src/Type/Family/Bool.hs
+++ b/src/Type/Family/Bool.hs
@@ -32,7 +32,7 @@
 
 import Type.Family.Constraint
 import Type.Class.Witness as Exports (type (==))
-import Data.Type.Bool as Exports (type Not, type (||), type (&&))
+import Data.Type.Bool as Exports (type If, type Not, type (||), type (&&))
 
 type family BoolC (b :: Bool) :: Constraint where
   BoolC True  = ØC
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
@@ -92,12 +92,24 @@
 
 -- Head,Tail,Init,Last {{{
 
+type family HeadM (as :: [k]) :: Maybe k where
+  HeadM Ø         = Nothing
+  HeadM (a :< as) = Just a
+
 type family Head (as :: [k]) :: k where
   Head (a :< as) = a
 
+type family TailM (as :: [k]) :: Maybe [k] where
+  TailM Ø         = Nothing
+  TailM (a :< as) = Just as
+
 type family Tail (as :: [k]) :: [k] where
   Tail (a :< as) = as
 
+type family InitM (as :: [k]) :: Maybe [k] where
+  InitM Ø         = Nothing
+  InitM (a :< as) = Just (Init' a as)
+
 type family Init (as :: [k]) :: [k] where
   Init (a :< as) = Init' a as
 
@@ -107,6 +119,10 @@
 
 initCong :: (a ~ b,as ~ bs) :- (Init' a as ~ Init' b bs)
 initCong = Sub Wit
+
+type family LastM (as :: [k]) :: Maybe k where
+  LastM Ø         = Nothing
+  LastM (a :< as) = Just (Last' a as)
 
 type family Last (as :: [k]) :: k where
   Last (a :< as) = Last' a as
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.2.0
+version: 0.2.2.1
 category: Data
 synopsis: A collection of data types for type-level programming
 cabal-version: >=1.10
@@ -24,11 +24,13 @@
         Data.Type.Fin
         Data.Type.Fin.Indexed
         Data.Type.Index
+        Data.Type.Index.Trans
         Data.Type.Length
         Data.Type.Nat
         Data.Type.Nat.Inequality
         Data.Type.Option
         Data.Type.Product
+        Data.Type.Product.Env
         Data.Type.Product.Lifted
         Data.Type.Sum
         Data.Type.Sum.Lifted