diff --git a/compdata.cabal b/compdata.cabal
--- a/compdata.cabal
+++ b/compdata.cabal
@@ -1,5 +1,5 @@
 Name:			compdata
-Version:		0.9
+Version:		0.10
 Synopsis:            	Compositional Data Types
 Description:
 
@@ -145,6 +145,7 @@
                         Data.Comp.Mapping
                         Data.Comp.Thunk
                         Data.Comp.Ops
+                        Data.Comp.Projection
 
                         Data.Comp.Multi
                         Data.Comp.Multi.Term
@@ -163,6 +164,7 @@
                         Data.Comp.Multi.Derive
                         Data.Comp.Multi.Generic
                         Data.Comp.Multi.Desugar
+                        Data.Comp.Multi.Projection
 
   Other-Modules:        Data.Comp.SubsumeCommon
                         Data.Comp.Derive.Equality
@@ -185,8 +187,9 @@
                         Data.Comp.Multi.Derive.SmartConstructors
                         Data.Comp.Multi.Derive.SmartAConstructors
 
-  Build-Depends:	base >= 4.7, base < 5, template-haskell, containers, mtl, QuickCheck >= 2, derive,
+  Build-Depends:	base >= 4.7, base < 5, template-haskell, containers, mtl >= 2.2.1, QuickCheck >= 2 && < 2.8, derive,
                         deepseq, th-expand-syns, transformers, tree-view
+  Extensions:           FlexibleContexts
   hs-source-dirs:	src
   ghc-options:          -W
 
@@ -195,8 +198,8 @@
   Type:                 exitcode-stdio-1.0
   Main-is:		Data_Test.hs
   hs-source-dirs:	testsuite/tests examples src
-  Build-Depends:        base >= 4.7, base < 5, template-haskell, containers, mtl, QuickCheck >= 2, 
-                        HUnit, test-framework, test-framework-hunit, test-framework-quickcheck2, derive,
+  Build-Depends:        base >= 4.7, base < 5, template-haskell, containers, mtl >= 2.2.1, QuickCheck >= 2 && < 2.8, 
+                        HUnit, test-framework, test-framework-hunit, test-framework-quickcheck2 >= 0.3, derive,
                         th-expand-syns, deepseq, transformers
 
 Benchmark algebra
@@ -206,7 +209,7 @@
   ghc-options:          -W -O2
   -- Disable short-cut fusion rules in order to compare optimised and unoptimised code.
   cpp-options:          -DNO_RULES
-  Build-Depends:        base >= 4.7, base < 5, template-haskell, containers, mtl, QuickCheck >= 2, derive, deepseq, criterion, random, uniplate, th-expand-syns, transformers
+  Build-Depends:        base >= 4.7, base < 5, template-haskell, containers, mtl >= 2.2.1, QuickCheck >= 2 && < 2.8, derive, deepseq, criterion, random, uniplate, th-expand-syns, transformers
 
 
 source-repository head
diff --git a/examples/Examples/Common.hs b/examples/Examples/Common.hs
--- a/examples/Examples/Common.hs
+++ b/examples/Examples/Common.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE TemplateHaskell, TypeOperators #-}
+{-# LANGUAGE FlexibleContexts #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Examples.Common
diff --git a/src/Data/Comp/Derive/Arbitrary.hs b/src/Data/Comp/Derive/Arbitrary.hs
--- a/src/Data/Comp/Derive/Arbitrary.hs
+++ b/src/Data/Comp/Derive/Arbitrary.hs
@@ -49,7 +49,7 @@
   TyConI (DataD _cxt name args constrs _deriving) <- abstractNewtypeQ $ reify dt
   let argNames = map (VarT . tyVarBndrName) (tail args)
       complType = foldl AppT (ConT name) argNames
-      preCond = map (ClassP ''Arbitrary . (: [])) argNames
+      preCond = map (mkClassP ''Arbitrary . (: [])) argNames
       classType = AppT (ConT ''ArbitraryF) complType
   arbitraryDecl <- generateArbitraryFDecl constrs
   shrinkDecl <- generateShrinkFDecl constrs
diff --git a/src/Data/Comp/Derive/DeepSeq.hs b/src/Data/Comp/Derive/DeepSeq.hs
--- a/src/Data/Comp/Derive/DeepSeq.hs
+++ b/src/Data/Comp/Derive/DeepSeq.hs
@@ -35,7 +35,7 @@
   TyConI (DataD _cxt name args constrs _deriving) <- abstractNewtypeQ $ reify fname
   let argNames = map (VarT . tyVarBndrName) (init args)
       complType = foldl AppT (ConT name) argNames
-      preCond = map (ClassP ''NFData . (: [])) argNames
+      preCond = map (mkClassP ''NFData . (: [])) argNames
       classType = AppT (ConT ''NFDataF) complType
   constrs' <- mapM normalConExp constrs
   rnfFDecl <- funD 'rnfF (rnfFClauses constrs')
diff --git a/src/Data/Comp/Derive/Equality.hs b/src/Data/Comp/Derive/Equality.hs
--- a/src/Data/Comp/Derive/Equality.hs
+++ b/src/Data/Comp/Derive/Equality.hs
@@ -34,7 +34,7 @@
   TyConI (DataD _cxt name args constrs _deriving) <- abstractNewtypeQ $ reify fname
   let argNames = map (VarT . tyVarBndrName) (init args)
       complType = foldl AppT (ConT name) argNames
-      preCond = map (ClassP ''Eq . (: [])) argNames
+      preCond = map (mkClassP ''Eq . (: [])) argNames
       classType = AppT (ConT ''EqF) complType
   eqFDecl <- funD 'eqF  (eqFClauses constrs)
   return [InstanceD preCond classType [eqFDecl]]
diff --git a/src/Data/Comp/Derive/Ordering.hs b/src/Data/Comp/Derive/Ordering.hs
--- a/src/Data/Comp/Derive/Ordering.hs
+++ b/src/Data/Comp/Derive/Ordering.hs
@@ -40,7 +40,7 @@
   TyConI (DataD _cxt name args constrs _deriving) <- abstractNewtypeQ $ reify fname
   let argNames = map (VarT . tyVarBndrName) (init args)
       complType = foldl AppT (ConT name) argNames
-      preCond = map (ClassP ''Ord . (: [])) argNames
+      preCond = map (mkClassP ''Ord . (: [])) argNames
       classType = AppT (ConT ''OrdF) complType
   eqAlgDecl <- funD 'compareF  (compareFClauses constrs)
   return [InstanceD preCond classType [eqAlgDecl]]
diff --git a/src/Data/Comp/Derive/Show.hs b/src/Data/Comp/Derive/Show.hs
--- a/src/Data/Comp/Derive/Show.hs
+++ b/src/Data/Comp/Derive/Show.hs
@@ -40,7 +40,7 @@
   let fArg = VarT . tyVarBndrName $ last args
       argNames = map (VarT . tyVarBndrName) (init args)
       complType = foldl AppT (ConT name) argNames
-      preCond = map (ClassP ''Show . (: [])) argNames
+      preCond = map (mkClassP ''Show . (: [])) argNames
       classType = AppT (ConT ''ShowF) complType
   constrs' <- mapM normalConExp constrs
   showFDecl <- funD 'showF (showFClauses fArg constrs')
@@ -76,7 +76,7 @@
   let fArg = VarT . tyVarBndrName $ last args
       argNames = map (VarT . tyVarBndrName) (init args)
       complType = foldl AppT (ConT name) argNames
-      preCond = map (ClassP ''Show . (: [])) argNames
+      preCond = map (mkClassP ''Show . (: [])) argNames
       classType = AppT (ConT ''ShowConstr) complType
   constrs' <- mapM normalConExp constrs
   showConstrDecl <- funD 'showConstr (showConstrClauses fArg constrs')
diff --git a/src/Data/Comp/Derive/Utils.hs b/src/Data/Comp/Derive/Utils.hs
--- a/src/Data/Comp/Derive/Utils.hs
+++ b/src/Data/Comp/Derive/Utils.hs
@@ -27,7 +27,7 @@
 #endif
 
 {-|
-  This is the @Q@-lifted version of 'abstractNewtypeQ.
+  This is the @Q@-lifted version of 'abstractNewtype.
 -}
 abstractNewtypeQ :: Q Info -> Q Info
 abstractNewtypeQ = liftM abstractNewtype
@@ -125,6 +125,33 @@
 derive :: [Name -> Q [Dec]] -> [Name] -> Q [Dec]
 derive ders names = liftM concat $ sequence [der name | der <- ders, name <- names]
 
+{-| Apply a class name to type arguments to construct a type class
+    constraint.
+-}
+
+#if __GLASGOW_HASKELL__ < 710
+mkClassP :: Name -> [Type] -> Pred
+mkClassP = ClassP
+#else
+mkClassP :: Name -> [Type] -> Type
+mkClassP name = foldl AppT (ConT name)
+#endif
+
+{-| This function checks whether the given type constraint is an
+equality constraint. If so, the types of the equality constraint are
+returned. -}
+
+#if __GLASGOW_HASKELL__ < 710
+isEqualP :: Pred -> Maybe (Type, Type)
+isEqualP (EqualP x y) = Just (x, y)
+isEqualP _ = Nothing
+#else
+isEqualP :: Type -> Maybe (Type, Type)
+isEqualP (AppT (AppT EqualityT x) y) = Just (x, y)
+isEqualP _ = Nothing
+#endif
+
+
 -- | This function lifts type class instances over sums
 -- ofsignatures. To this end it assumes that it contains only methods
 -- with types of the form @f t1 .. tn -> t@ where @f@ is the signature
@@ -154,8 +181,8 @@
       let g = VarT $ mkName "g"
       let ts1 = map VarT ts1_
       let ts2 = map VarT ts2_
-      let cxt = [ClassP name (ts1 ++ f : ts2),
-                 ClassP name (ts1 ++ g : ts2)]
+      let cxt = [mkClassP name (ts1 ++ f : ts2),
+                 mkClassP name (ts1 ++ g : ts2)]
       let tp = ((ConT sumName `AppT` f) `AppT` g)
       let complType = foldl AppT (foldl AppT (ConT name) ts1 `AppT` tp) ts2
       decs' <- sequence $ concatMap decl decs
diff --git a/src/Data/Comp/Mapping.hs b/src/Data/Comp/Mapping.hs
--- a/src/Data/Comp/Mapping.hs
+++ b/src/Data/Comp/Mapping.hs
@@ -2,6 +2,9 @@
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE DeriveFoldable #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Mapping
@@ -22,11 +25,15 @@
     , number
     , Traversable ()
     , Mapping (..)
-    , lookupNumMap) where
+    , prodMap
+    , lookupNumMap
+    , lookupNumMap'
+    , NumMap) where
 
 import Data.IntMap (IntMap)
 import qualified Data.IntMap as IntMap
 import Data.Traversable
+import Data.Foldable
 
 import Control.Monad.State hiding (mapM)
 import Prelude hiding (mapM)
@@ -64,19 +71,25 @@
 
     -- | This function constructs the pointwise product of two maps each
     -- with a default value.
-    prodMap :: v1 -> v2 -> m v1 -> m v2 -> m (v1, v2)
+    prodMapWith :: (v1 -> v2 -> v) -> v1 -> v2 -> m v1 -> m v2 -> m v
 
     -- | Returns the value at the given key or returns the given
     -- default when the key is not an element of the map.
     findWithDefault :: a -> k -> m a -> a
 
-
+-- | This function constructs the pointwise product of two maps each
+-- with a default value.
+prodMap :: Mapping m k => v1 -> v2 -> m v1 -> m v2 -> m (v1, v2)
+prodMap = prodMapWith (,)
 
-newtype NumMap k v = NumMap (IntMap v) deriving Functor
+newtype NumMap k v = NumMap (IntMap v) deriving (Functor,Foldable,Traversable)
 
 lookupNumMap :: a -> Int -> NumMap t a -> a
 lookupNumMap d k (NumMap m) = IntMap.findWithDefault d k m
 
+lookupNumMap' :: Int -> NumMap t a -> Maybe a
+lookupNumMap' k (NumMap m) = IntMap.lookup k m
+
 instance Mapping (NumMap k) (Numbered k) where
     NumMap m1 & NumMap m2 = NumMap (IntMap.union m1 m2)
     Numbered k _ |-> v = NumMap $ IntMap.singleton k v
@@ -84,6 +97,6 @@
 
     findWithDefault d (Numbered i _) m = lookupNumMap d i m
 
-    prodMap p q (NumMap mp) (NumMap mq) = NumMap $ IntMap.mergeWithKey merge 
-                                          (IntMap.map (,q)) (IntMap.map (p,)) mp mq
-      where merge _ p q = Just (p,q)
+    prodMapWith f p q (NumMap mp) (NumMap mq) = NumMap $ IntMap.mergeWithKey merge 
+                                          (IntMap.map (`f` q)) (IntMap.map (p `f`)) mp mq
+      where merge _ p q = Just (p `f` q)
diff --git a/src/Data/Comp/Multi/Derive/Equality.hs b/src/Data/Comp/Multi/Derive/Equality.hs
--- a/src/Data/Comp/Multi/Derive/Equality.hs
+++ b/src/Data/Comp/Multi/Derive/Equality.hs
@@ -32,7 +32,7 @@
       argNames = map (VarT . tyVarBndrName) (init args')
       ftyp = VarT . tyVarBndrName $ last args'
       complType = foldl AppT (ConT name) argNames
-      preCond = map (ClassP ''Eq . (: [])) argNames
+      preCond = map (mkClassP ''Eq . (: [])) argNames
       classType = AppT (ConT ''EqHF) complType
   constrs' <- mapM normalConExp constrs
   eqFDecl <- funD 'eqHF  (eqFClauses ftyp constrs constrs')
diff --git a/src/Data/Comp/Multi/Derive/Show.hs b/src/Data/Comp/Multi/Derive/Show.hs
--- a/src/Data/Comp/Multi/Derive/Show.hs
+++ b/src/Data/Comp/Multi/Derive/Show.hs
@@ -49,7 +49,7 @@
       fArg = VarT . tyVarBndrName $ last args'
       argNames = map (VarT . tyVarBndrName) (init args')
       complType = foldl AppT (ConT name) argNames
-      preCond = map (ClassP ''Show . (: [])) argNames
+      preCond = map (mkClassP ''Show . (: [])) argNames
       classType = AppT (ConT ''ShowHF) complType
   constrs' <- mapM normalConExp constrs
   showFDecl <- funD 'showHF (showFClauses fArg constrs')
diff --git a/src/Data/Comp/Multi/Derive/SmartConstructors.hs b/src/Data/Comp/Multi/Derive/SmartConstructors.hs
--- a/src/Data/Comp/Multi/Derive/SmartConstructors.hs
+++ b/src/Data/Comp/Multi/Derive/SmartConstructors.hs
@@ -35,7 +35,7 @@
     liftM concat $ mapM (genSmartConstr (map tyVarBndrName targs) tname) cons
         where iTp iVar (ForallC _ cxt _) =
                   -- Check if the GADT phantom type is constrained
-                  case [y | EqualP x y <- cxt, x == VarT iVar] of
+                  case [y | Just (x, y) <- map isEqualP cxt, x == VarT iVar] of
                     [] -> Nothing
                     tp:_ -> Just tp
               iTp _ _ = Nothing
diff --git a/src/Data/Comp/Multi/HFunctor.hs b/src/Data/Comp/Multi/HFunctor.hs
--- a/src/Data/Comp/Multi/HFunctor.hs
+++ b/src/Data/Comp/Multi/HFunctor.hs
@@ -1,3 +1,7 @@
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE DeriveTraversable         #-}
+{-# LANGUAGE DeriveFoldable            #-}
+{-# LANGUAGE DeriveFunctor             #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE FlexibleInstances         #-}
 {-# LANGUAGE MultiParamTypeClasses     #-}
@@ -5,6 +9,7 @@
 {-# LANGUAGE ScopedTypeVariables       #-}
 {-# LANGUAGE TypeOperators             #-}
 {-# LANGUAGE UndecidableInstances      #-}
+{-# LANGUAGE IncoherentInstances       #-}
 
 --------------------------------------------------------------------------------
 -- |
@@ -34,17 +39,16 @@
      (:.:)(..)
      ) where
 
+import Data.Traversable
+import Data.Foldable
+import Data.Functor.Compose
+
 -- | The identity Functor.
-newtype I a = I {unI :: a}
+newtype I a = I {unI :: a} deriving (Functor, Foldable, Traversable)
 
-instance Functor I where
-    fmap f (I x) = I (f x)
 
 -- | The parametrised constant functor.
-newtype K a i = K {unK :: a}
-
-instance Functor (K a) where
-    fmap _ (K x) = K x
+newtype K a i = K {unK :: a} deriving (Functor, Foldable, Traversable)
 
 data E f = forall i. E {unE :: f i}
 
@@ -95,7 +99,9 @@
     -- @g :-> h@ to a natural transformation @f g :-> f h@
     hfmap :: (f :-> g) -> h f :-> h g
 
+instance (Functor f) => HFunctor (Compose f) where hfmap f (Compose xs) = Compose (fmap f xs)
+
 infixl 5 :.:
 
 -- | This data type denotes the composition of two functor families.
-data  (f :.: g) e t = Comp f (g e) t
+data (:.:) f (g :: (* -> *) -> (* -> *)) (e :: * -> *) t = Comp (f (g e) t)
diff --git a/src/Data/Comp/Multi/HTraversable.hs b/src/Data/Comp/Multi/HTraversable.hs
--- a/src/Data/Comp/Multi/HTraversable.hs
+++ b/src/Data/Comp/Multi/HTraversable.hs
@@ -36,7 +36,10 @@
     -- Alternative type in terms of natural transformations using
     -- functor composition @:.:@:
     --
-    -- @hmapM :: Monad m => (a :-> m :.: b) -> t a :-> m :.: (t b)@
+    -- @
+    -- hmapM :: Monad m => (a :-> m :.: b) -> t a :-> m :.: (t b)
+    -- @
+    -- 
     hmapM :: (Monad m) => NatM m a b -> NatM m (t a) (t b)
 
     htraverse :: (Applicative f) => NatM f a b -> NatM f (t a) (t b)
diff --git a/src/Data/Comp/Multi/Mapping.hs b/src/Data/Comp/Multi/Mapping.hs
--- a/src/Data/Comp/Multi/Mapping.hs
+++ b/src/Data/Comp/Multi/Mapping.hs
@@ -4,6 +4,7 @@
 {-# LANGUAGE TupleSections #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE FlexibleContexts #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Multi.Mapping
diff --git a/src/Data/Comp/Multi/Ops.hs b/src/Data/Comp/Multi/Ops.hs
--- a/src/Data/Comp/Multi/Ops.hs
+++ b/src/Data/Comp/Multi/Ops.hs
@@ -28,7 +28,12 @@
 --
 --------------------------------------------------------------------------------
 
-module Data.Comp.Multi.Ops where
+module Data.Comp.Multi.Ops 
+    ( module Data.Comp.Multi.Ops
+    , (O.:*:)(..)
+    , O.ffst
+    , O.fsnd
+    ) where
 
 import Control.Applicative
 import Control.Monad
@@ -90,25 +95,6 @@
     Elem f (g1 :+: g2) = Choose (Elem f g1) (Elem f g2)
     Elem f g = NotFound
 
-
-type family Choose (e1 :: Emb) (r :: Emb) :: Emb where
-    Choose (Found x) (Found y) = Ambiguous
-    Choose Ambiguous y = Ambiguous
-    Choose x Ambiguous = Ambiguous
-    Choose (Found x) y = Found (Le x)
-    Choose x (Found y) = Found (Ri y)
-    Choose x y = NotFound
-
-
-type family Sum' (e1 :: Emb) (r :: Emb) :: Emb where
-    Sum' (Found x) (Found y) = Found (Sum x y)
-    Sum' Ambiguous y = Ambiguous
-    Sum' x Ambiguous = Ambiguous
-    Sum' NotFound y = NotFound
-    Sum' x NotFound = NotFound
-
-data Proxy a = P
-
 class Subsume (e :: Emb) (f :: (* -> *) -> * -> *)
                          (g :: (* -> *) -> * -> *) where
   inj'  :: Proxy e -> f a :-> g a
@@ -164,19 +150,6 @@
             Inl y -> f1 y
             Inr y -> f2 y
 
--- Products
-
-infixr 8 :*:
-
-data (f :*: g) a = f a :*: g a
-
-
-fst :: (f :*: g) a -> f a
-fst (x :*: _) = x
-
-snd :: (f :*: g) a -> g a
-snd (_ :*: x) = x
-
 -- Constant Products
 
 infixr 7 :&:
@@ -184,7 +157,9 @@
 -- | This data type adds a constant product to a
 -- signature. Alternatively, this could have also been defined as
 --
--- @data (f :&: a) (g ::  * -> *) e = f g e :&: a e@
+-- @
+-- data (f :&: a) (g ::  * -> *) e = f g e :&: a e
+-- @
 --
 -- This is too general, however, for example for 'productHHom'.
 
diff --git a/src/Data/Comp/Multi/Projection.hs b/src/Data/Comp/Multi/Projection.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Multi/Projection.hs
@@ -0,0 +1,75 @@
+{-# LANGUAGE ConstraintKinds       #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE UndecidableInstances  #-}
+
+
+
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Multi.Projection
+-- Copyright   :  (c) 2014 Patrick Bahr
+-- License     :  BSD3
+-- Maintainer  :  Patrick Bahr <paba@di.ku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+--
+-- This module provides a generic projection function 'pr' for
+-- arbitrary nested binary products.
+--
+--------------------------------------------------------------------------------
+
+
+module Data.Comp.Multi.Projection (pr, (:<), (:*:)(..), ffst, fsnd) where
+
+import Data.Comp.SubsumeCommon
+import Data.Comp.Multi.Ops hiding (Elem)
+
+type family Elem (f :: * -> *)
+                 (g :: * -> *) :: Emb where
+    Elem f f = Found Here
+    Elem (f1 :*: f2) g =  Sum' (Elem f1 g) (Elem f2 g)
+    Elem f (g1 :*: g2) = Choose (Elem f g1) (Elem f g2)
+    Elem f g = NotFound
+
+class Proj (e :: Emb) (p :: * -> *)
+                      (q :: * -> *) where
+    pr'  :: Proxy e -> q a -> p a
+
+instance Proj (Found Here) f f where
+    pr' _ = id
+
+instance Proj (Found p) f g => Proj (Found (Le p)) f (g :*: g') where
+    pr' _ = pr' (P :: Proxy (Found p)) . ffst
+
+
+instance Proj (Found p) f g => Proj (Found (Ri p)) f (g' :*: g) where
+    pr' _ = pr' (P :: Proxy (Found p)) . fsnd
+
+
+instance (Proj (Found p1) f1 g, Proj (Found p2) f2 g)
+    => Proj (Found (Sum p1 p2)) (f1 :*: f2) g where
+    pr' _ x = (pr' (P :: Proxy (Found p1)) x :*: pr' (P :: Proxy (Found p2)) x)
+
+
+infixl 5 :<
+
+-- | The constraint @e :< p@ expresses that @e@ is a component of the
+-- type @p@. That is, @p@ is formed by binary products using the type
+-- @e@. The occurrence of @e@ must be unique. For example we have @Int
+-- :< (Bool,(Int,Bool))@ but not @Bool :< (Bool,(Int,Bool))@.
+
+type f :< g = (Proj (ComprEmb (Elem f g)) f g)
+
+
+-- | This function projects the component of type @e@ out or the
+-- compound value of type @p@.
+
+pr :: forall p q a . (p :< q) => q a -> p a
+pr = pr' (P :: Proxy (ComprEmb (Elem p q)))
diff --git a/src/Data/Comp/Multi/Variables.hs b/src/Data/Comp/Multi/Variables.hs
--- a/src/Data/Comp/Multi/Variables.hs
+++ b/src/Data/Comp/Multi/Variables.hs
@@ -81,17 +81,21 @@
     -- | Indicates the set of variables bound by the @f@ constructor
     -- for each argument of the constructor. For example for a
     -- non-recursive let binding:
+    -- 
     -- @
     -- data Let i e = Let Var (e i) (e i)
     -- instance HasVars Let Var where
     --   bindsVars (Let v x y) = y |-> Set.singleton v
     -- @
+    -- 
     -- If, instead, the let binding is recursive, the methods has to
     -- be implemented like this:
+    -- 
     -- @
     --   bindsVars (Let v x y) = x |-> Set.singleton v &
     --                           y |-> Set.singleton v
     -- @
+    -- 
     -- This indicates that the scope of the bound variable also
     -- extends to the right-hand side of the variable binding.
     --
diff --git a/src/Data/Comp/Ops.hs b/src/Data/Comp/Ops.hs
--- a/src/Data/Comp/Ops.hs
+++ b/src/Data/Comp/Ops.hs
@@ -98,25 +98,6 @@
     Elem f (g1 :+: g2) = Choose (Elem f g1) (Elem f g2)
     Elem f g = NotFound
 
-
-type family Choose (e1 :: Emb) (r :: Emb) :: Emb where
-    Choose (Found x) (Found y) = Ambiguous
-    Choose Ambiguous y = Ambiguous
-    Choose x Ambiguous = Ambiguous
-    Choose (Found x) y = Found (Le x)
-    Choose x (Found y) = Found (Ri y)
-    Choose x y = NotFound
-
-
-type family Sum' (e1 :: Emb) (r :: Emb) :: Emb where
-    Sum' (Found x) (Found y) = Found (Sum x y)
-    Sum' Ambiguous y = Ambiguous
-    Sum' x Ambiguous = Ambiguous
-    Sum' NotFound y = NotFound
-    Sum' x NotFound = NotFound
-
-data Proxy a = P
-
 class Subsume (e :: Emb) (f :: * -> *) (g :: * -> *) where
   inj'  :: Proxy e -> f a -> g a
   prj'  :: Proxy e -> g a -> Maybe (f a)
@@ -185,6 +166,21 @@
 
 fsnd :: (f :*: g) a -> g a
 fsnd (_ :*: x) = x
+
+instance (Functor f, Functor g) => Functor (f :*: g) where
+    fmap h (f :*: g) = (fmap h f :*: fmap h g)
+
+
+instance (Foldable f, Foldable g) => Foldable (f :*: g) where
+    foldr f e (x :*: y) = foldr f (foldr f e y) x
+    foldl f e (x :*: y) = foldl f (foldl f e x) y
+
+
+instance (Traversable f, Traversable g) => Traversable (f :*: g) where
+    traverse f (x :*: y) = liftA2 (:*:) (traverse f x) (traverse f y)
+    sequenceA (x :*: y) = liftA2 (:*:)(sequenceA x) (sequenceA y)
+    mapM f (x :*: y) = liftM2 (:*:) (mapM f x) (mapM f y)
+    sequence (x :*: y) = liftM2 (:*:) (sequence x) (sequence y)
 
 -- Constant Products
 
diff --git a/src/Data/Comp/Projection.hs b/src/Data/Comp/Projection.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Projection.hs
@@ -0,0 +1,74 @@
+{-# LANGUAGE ConstraintKinds       #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE UndecidableInstances  #-}
+
+
+
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Projection
+-- Copyright   :  (c) 2014 Patrick Bahr
+-- License     :  BSD3
+-- Maintainer  :  Patrick Bahr <paba@di.ku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+--
+-- This module provides a generic projection function 'pr' for
+-- arbitrary nested binary products.
+--
+--------------------------------------------------------------------------------
+
+
+module Data.Comp.Projection (pr, (:<)) where
+
+import Data.Comp.SubsumeCommon
+
+type family Elem (f :: *)
+                 (g :: *) :: Emb where
+    Elem f f = Found Here
+    Elem (f1, f2) g =  Sum' (Elem f1 g) (Elem f2 g)
+    Elem f (g1, g2) = Choose (Elem f g1) (Elem f g2)
+    Elem f g = NotFound
+
+class Proj (e :: Emb) (p :: *)
+                      (q :: *) where
+    pr'  :: Proxy e -> q -> p
+
+instance Proj (Found Here) f f where
+    pr' _ = id
+
+instance Proj (Found p) f g => Proj (Found (Le p)) f (g, g') where
+    pr' _ = pr' (P :: Proxy (Found p)) . fst
+
+
+instance Proj (Found p) f g => Proj (Found (Ri p)) f (g', g) where
+    pr' _ = pr' (P :: Proxy (Found p)) . snd
+
+
+instance (Proj (Found p1) f1 g, Proj (Found p2) f2 g)
+    => Proj (Found (Sum p1 p2)) (f1, f2) g where
+    pr' _ x = (pr' (P :: Proxy (Found p1)) x, pr' (P :: Proxy (Found p2)) x)
+
+
+infixl 5 :<
+
+-- | The constraint @e :< p@ expresses that @e@ is a component of the
+-- type @p@. That is, @p@ is formed by binary products using the type
+-- @e@. The occurrence of @e@ must be unique. For example we have @Int
+-- :< (Bool,(Int,Bool))@ but not @Bool :< (Bool,(Int,Bool))@.
+
+type f :< g = (Proj (ComprEmb (Elem f g)) f g)
+
+
+-- | This function projects the component of type @e@ out or the
+-- compound value of type @p@.
+
+pr :: forall p q . (p :< q) => q -> p
+pr = pr' (P :: Proxy (ComprEmb (Elem p q)))
diff --git a/src/Data/Comp/SubsumeCommon.hs b/src/Data/Comp/SubsumeCommon.hs
--- a/src/Data/Comp/SubsumeCommon.hs
+++ b/src/Data/Comp/SubsumeCommon.hs
@@ -2,6 +2,7 @@
 {-# LANGUAGE TypeFamilies         #-}
 {-# LANGUAGE TypeOperators        #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE PolyKinds            #-}
 
 --------------------------------------------------------------------------------
 -- |
@@ -21,6 +22,9 @@
     ( ComprEmb
     , Pos (..)
     , Emb (..)
+    , Choose
+    , Sum'
+    , Proxy (..)
     ) where
 
 -- | This type is used in its promoted form only. It represents
@@ -34,6 +38,26 @@
 -- found. 'Ambiguous' indicates that there are duplicates on the left-
 -- or the right-hand side.
 data Emb = Found Pos | NotFound | Ambiguous
+
+data Proxy a = P
+
+
+type family Choose (e1 :: Emb) (r :: Emb) :: Emb where
+    Choose (Found x) (Found y) = Ambiguous
+    Choose Ambiguous y = Ambiguous
+    Choose x Ambiguous = Ambiguous
+    Choose (Found x) y = Found (Le x)
+    Choose x (Found y) = Found (Ri y)
+    Choose x y = NotFound
+
+
+type family Sum' (e1 :: Emb) (r :: Emb) :: Emb where
+    Sum' (Found x) (Found y) = Found (Sum x y)
+    Sum' Ambiguous y = Ambiguous
+    Sum' x Ambiguous = Ambiguous
+    Sum' NotFound y = NotFound
+    Sum' x NotFound = NotFound
+
 
 -- | This type family takes a position type and compresses it. That
 -- means it replaces each nested occurrence of
diff --git a/src/Data/Comp/Sum.hs b/src/Data/Comp/Sum.hs
--- a/src/Data/Comp/Sum.hs
+++ b/src/Data/Comp/Sum.hs
@@ -26,7 +26,6 @@
      (:=:),
      (:+:),
      caseF,
-     Proxy (..),
 
      -- * Projections for Signatures and Terms
      proj,
diff --git a/src/Data/Comp/Unification.hs b/src/Data/Comp/Unification.hs
--- a/src/Data/Comp/Unification.hs
+++ b/src/Data/Comp/Unification.hs
@@ -20,7 +20,7 @@
 import Data.Comp.Term
 import Data.Comp.Variables
 
-import Control.Monad.Error
+import Control.Monad.Except
 import Control.Monad.State
 
 import Data.Traversable
@@ -42,10 +42,6 @@
 data UnifError f v = FailedOccursCheck v (Term f)
                    | HeadSymbolMismatch (Term f) (Term f)
                    | UnifError String
-
-instance Error (UnifError f v) where
-    strMsg = UnifError
-
 
 -- | This is used in order to signal a failed occurs check during
 -- unification.
diff --git a/src/Data/Comp/Variables.hs b/src/Data/Comp/Variables.hs
--- a/src/Data/Comp/Variables.hs
+++ b/src/Data/Comp/Variables.hs
@@ -43,6 +43,7 @@
 import Data.Comp.Derive
 import Data.Comp.Mapping
 import Data.Comp.Term
+import Data.Comp.Ops
 import Data.Foldable hiding (elem, notElem)
 import Data.Map (Map)
 import qualified Data.Map as Map
@@ -71,17 +72,21 @@
     -- | Indicates the set of variables bound by the @f@ constructor
     -- for each argument of the constructor. For example for a
     -- non-recursive let binding:
+    -- 
     -- @
     -- data Let e = Let Var e e
     -- instance HasVars Let Var where
     --   bindsVars (Let v x y) = y |-> Set.singleton v
     -- @
+    -- 
     -- If, instead, the let binding is recursive, the methods has to
     -- be implemented like this:
+    -- 
     -- @
     --   bindsVars (Let v x y) = x |-> Set.singleton v &
     --                           y |-> Set.singleton v
     -- @
+    -- 
     -- This indicates that the scope of the bound variable also
     -- extends to the right-hand side of the variable binding.
     --
@@ -91,6 +96,10 @@
 
 
 $(derive [liftSum] [''HasVars])
+
+instance HasVars f v => HasVars (f :&: a) v where
+  isVar (f :&: _)     = isVar f
+  bindsVars (f :&: _) = bindsVars f
 
 -- | Same as 'isVar' but it returns Nothing@ instead of @Just v@ if
 -- @v@ is contained in the given set of variables.