diff --git a/Data/Category.hs b/Data/Category.hs
--- a/Data/Category.hs
+++ b/Data/Category.hs
@@ -13,7 +13,7 @@
   
   -- * Category
     Category(..)
-  , Obj(..)
+  , Obj
   
   -- * Opposite category
   , Op(..)
@@ -23,41 +23,36 @@
 import Prelude (($))
 import qualified Prelude
 
+infixr 8 .
 
+
+-- | Whenever objects are required at value level, they are represented by their identity arrows.
+type Obj (~>) a = a ~> a
+
 -- | An instance of @Category (~>)@ declares the arrow @(~>)@ as a category.
 class Category (~>) where
   
-  data Obj (~>) :: * -> *
-
   src :: a ~> b -> Obj (~>) a
   tgt :: a ~> b -> Obj (~>) b
 
-  id  :: Obj (~>) a -> a ~> a
   (.) :: b ~> c -> a ~> b -> a ~> c
 
 
 -- | The category with Haskell types as objects and Haskell functions as arrows.
 instance Category (->) where
   
-  data Obj (->) a = HaskO
-  
-  src _ = HaskO
-  tgt _ = HaskO
+  src _ = Prelude.id
+  tgt _ = Prelude.id
   
-  id _  = Prelude.id  
   (.)   = (Prelude..)    
 
 
-data Op :: (* -> * -> *) -> * -> * -> * where
-  Op :: (a ~> b) -> Op (~>) b a
+data Op (~>) a b = Op { unOp :: b ~> a }
 
 -- | @Op (~>)@ is opposite category of the category @(~>)@.
 instance Category (~>) => Category (Op (~>)) where
   
-  data Obj (Op (~>)) a = OpObj (Obj (~>) a)
-  
-  src (Op a)      = OpObj $ tgt a
-  tgt (Op a)      = OpObj $ src a
+  src (Op a)      = Op $ tgt a
+  tgt (Op a)      = Op $ src a
   
-  id (OpObj x)    = Op $ id x
   (Op a) . (Op b) = Op $ b . a
diff --git a/Data/Category/Adjunction.hs b/Data/Category/Adjunction.hs
--- a/Data/Category/Adjunction.hs
+++ b/Data/Category/Adjunction.hs
@@ -9,19 +9,55 @@
 -- Stability   :  experimental
 -- Portability :  non-portable
 -----------------------------------------------------------------------------
-module Data.Category.Adjunction where
+module Data.Category.Adjunction (
+
+  -- * Adjunctions
+    Adjunction(..)
+  , mkAdjunction
+
+  , leftAdjunct
+  , rightAdjunct
   
-import Prelude hiding ((.), id, Functor)
-import Control.Monad.Instances()
+  -- * Adjunctions from universal morphisms
+  , initialPropAdjunction
+  , terminalPropAdjunction
+  
+  -- * Adjunctions to universal morphisms
+  , adjunctionInitialProp
+  , adjunctionTerminalProp
+  
+  -- * Adjunctions as a category
+  , AdjArrow(..)
+  
+  -- * (Co)limitfunctor adjunction
+  , limitAdj
+  , colimitAdj
+  
+  -- * (Co)monad of an adjunction
+  , adjunctionMonad
+  , adjunctionComonad
+  
+  -- * Examples
+  , contAdj
+  
+) where
+  
+import Prelude (($), id, flip)
+import Control.Monad.Instances ()
 
 import Data.Category
 import Data.Category.Functor
 import Data.Category.NaturalTransformation
 import Data.Category.Limit
+import qualified Data.Category.Monoidal as M
 
-data Adjunction c d f g where
-  Adjunction :: (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) =>
-    f -> g -> Nat d d (Id d) (g :.: f) -> Nat c c (f :.: g) (Id c) -> Adjunction c d f g
+data Adjunction c d f g = (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
+  => Adjunction
+  { leftAdjoint  :: f
+  , rightAdjoint :: g
+  , unit         :: Nat d d (Id d) (g :.: f)
+  , counit       :: Nat c c (f :.: g) (Id c)
+  }
 
 mkAdjunction :: (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
   => f -> g 
@@ -30,11 +66,6 @@
   -> Adjunction c d f g
 mkAdjunction f g un coun = Adjunction f g (Nat Id (g :.: f) un) (Nat (f :.: g) Id coun)
 
-unit :: Adjunction c d f g -> Id d :~> (g :.: f)
-unit (Adjunction _ _ u _) = u
-counit :: Adjunction c d f g -> (f :.: g) :~> Id c
-counit (Adjunction _ _ _ c) = c
-
 leftAdjunct :: Adjunction c d f g -> Obj d a -> c (f :% a) b -> d a (g :% b)
 leftAdjunct (Adjunction _ g un _) i h = (g % h) . (un ! i)
 rightAdjunct :: Adjunction c d f g -> Obj c b -> d a (g :% b) -> c (f :% a) b
@@ -42,11 +73,11 @@
 
 -- Each pair (FY, unit_Y) is an initial morphism from Y to G.
 adjunctionInitialProp :: Adjunction c d f g -> Obj d y -> InitialUniversal y g (f :% y)
-adjunctionInitialProp adj@(Adjunction f _ un _) y = InitialUniversal (f %% y) (un ! y) (rightAdjunct adj)
+adjunctionInitialProp adj@(Adjunction f _ un _) y = InitialUniversal (f % y) (un ! y) (rightAdjunct adj)
 
 -- Each pair (GX, counit_X) is a terminal morphism from F to X.
 adjunctionTerminalProp :: Adjunction c d f g -> Obj c x -> TerminalUniversal x f (g :% x)
-adjunctionTerminalProp adj@(Adjunction _ g _ coun) x = TerminalUniversal (g %% x) (coun ! x) (leftAdjunct adj)
+adjunctionTerminalProp adj@(Adjunction _ g _ coun) x = TerminalUniversal (g % x) (coun ! x) (leftAdjunct adj)
 
 
 
@@ -54,45 +85,28 @@
   => f -> g -> (forall y. Obj d y -> InitialUniversal y g (f :% y)) -> Adjunction c d f g
 initialPropAdjunction f g univ = mkAdjunction f g un coun
   where
-    coun a = let ga = g %% a in initialFactorizer (univ ga) a (id ga)
+    coun a = initialFactorizer (univ (g % a)) a (g % a)
     un   a = initialMorphism (univ a)
     
 terminalPropAdjunction :: (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
   => f -> g -> (forall x. Obj c x -> TerminalUniversal x f (g :% x)) -> Adjunction c d f g
 terminalPropAdjunction f g univ = mkAdjunction f g un coun
   where
-    un   a = let fa = f %% a in terminalFactorizer (univ fa) a (id fa)
+    un   a = terminalFactorizer (univ (f % a)) a (f % a)
     coun a = terminalMorphism (univ a)
     
 
 data AdjArrow c d where
   AdjArrow :: (Category c, Category d) => Adjunction c d f g -> AdjArrow (CatW c) (CatW d)
 
+-- | The category with categories as objects and adjunctions as arrows.
 instance Category AdjArrow where
   
-  data Obj AdjArrow a where
-    AdjCategory :: Category (~>) => Obj AdjArrow (CatW (~>))
-  
-  src (AdjArrow _) = AdjCategory
-  tgt (AdjArrow _) = AdjCategory
-  
-  id AdjCategory = AdjArrow $ mkAdjunction Id Id id id
+  src (AdjArrow (Adjunction _ _ _ _)) = AdjArrow $ mkAdjunction Id Id id id
+  tgt (AdjArrow (Adjunction _ _ _ _)) = AdjArrow $ mkAdjunction Id Id id id
   
   AdjArrow (Adjunction f g u c) . AdjArrow (Adjunction f' g' u' c') = AdjArrow $ 
-    Adjunction (f' :.: f) (g :.: g') (wrap g f u' . u) (c' . cowrap f' g' c)
-
-
-wrap :: (Functor g, Functor f, Dom g ~ Dom f', Dom g ~ Cod f) 
-  => g -> f -> Nat (Dom f') (Dom f') (Id (Dom f')) (g' :.: f') -> (g :.: f) :~> ((g :.: g') :.: (f' :.: f))
-wrap g f (Nat Id (g' :.: f') n) = Nat (g :.: f) ((g :.: g') :.: (f' :.: f)) $ (g %) . n . (f %%)
-
-cowrap :: (Functor f', Functor g', Dom f' ~ Dom g, Dom f' ~ Cod g') 
-  => f' -> g' -> Nat (Dom g) (Dom g) (f :.: g) (Id (Dom g)) -> ((f' :.: f) :.: (g :.: g')) :~> (f' :.: g')
-cowrap f' g' (Nat (f :.: g) Id n) = Nat ((f' :.: f) :.: (g :.: g')) (f' :.: g') $ (f' %) . n . (g' %%)
-
-
-curryAdj :: Adjunction (->) (->) (EndoHask ((,) e)) (EndoHask ((->) e))
-curryAdj = mkAdjunction EndoHask EndoHask (\HaskO -> \a e -> (e, a)) (\HaskO -> \(e, f) -> f e)
+    mkAdjunction (f' :.: f) (g :.: g') (\i -> ((Wrap g f % u') ! i) . (u ! i)) (\i -> (c' ! i) . ((Wrap f' g' % c) ! i))
 
 
 -- | The limit functor is right adjoint to the diagonal functor.
@@ -102,7 +116,7 @@
 limitAdj LimitFunctor = terminalPropAdjunction Diag LimitFunctor univ
   where
     univ :: Obj (Nat j (~>)) f -> TerminalUniversal f (Diag j (~>)) (LimitFam j (~>) f)
-    univ f @ NatO{} = limitUniv f
+    univ f@Nat{} = limitUniv f
 
 -- | The colimit functor is left adjoint to the diagonal functor.
 colimitAdj :: forall j (~>). HasColimits j (~>) 
@@ -111,4 +125,32 @@
 colimitAdj ColimitFunctor = initialPropAdjunction ColimitFunctor Diag univ
   where
     univ :: Obj (Nat j (~>)) f -> InitialUniversal f (Diag j (~>)) (ColimitFam j (~>) f)
-    univ f @ NatO{} = colimitUniv f
+    univ f@Nat{} = colimitUniv f
+
+
+adjunctionMonad :: Adjunction c d f g -> M.Monad (g :.: f)
+adjunctionMonad (Adjunction f g un coun) = M.mkMonad (g :.: f) (un !) ((Wrap g f % coun) !)
+
+adjunctionComonad :: Adjunction c d f g -> M.Comonad (f :.: g)
+adjunctionComonad (Adjunction f g un coun) = M.mkComonad (f :.: g) (coun !) ((Wrap f g % un) !)
+
+
+
+data Cont1 r = Cont1
+type instance Dom (Cont1 r) = (->)
+type instance Cod (Cont1 r) = Op (->)
+type instance (Cont1 r) :% a = a -> r
+instance Functor (Cont1 r) where 
+  Cont1 % f = Op (. f)
+
+data Cont2 r = Cont2
+type instance Dom (Cont2 r) = Op (->)
+type instance Cod (Cont2 r) = (->)
+type instance (Cont2 r) :% a = a -> r
+instance Functor (Cont2 r) where 
+  Cont2 % (Op f) = (. f)
+
+contAdj :: Adjunction (Op (->)) (->) (Cont1 r) (Cont2 r)
+contAdj = mkAdjunction Cont1 Cont2 (\_ -> flip ($)) (\_ -> Op (flip ($)))
+
+-- leftAdjunct contAdj id . Op === unOp . rightAdjunct contAdj (Op id) === flip
diff --git a/Data/Category/Boolean.hs b/Data/Category/Boolean.hs
--- a/Data/Category/Boolean.hs
+++ b/Data/Category/Boolean.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, GADTs, EmptyDataDecls, FlexibleInstances #-}
+{-# LANGUAGE TypeFamilies, GADTs, EmptyDataDecls, TypeOperators, ScopedTypeVariables, UndecidableInstances #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Boolean
@@ -18,106 +18,118 @@
 import Prelude hiding ((.), id, Functor)
 
 import Data.Category
+import Data.Category.Functor
+import Data.Category.NaturalTransformation
+import Data.Category.Product
 import Data.Category.Limit
 
 
-data BF
-data BT
+data Fls
+data Tru
   
 data Boolean a b where
-  IdFls  :: Boolean BF BF
-  FlsTru :: Boolean BF BT
-  IdTru  :: Boolean BT BT
+  Fls :: Boolean Fls Fls
+  F2T :: Boolean Fls Tru
+  Tru :: Boolean Tru Tru
 
 -- | @Boolean@ is the category with true and false as objects, and an arrow from false to true.
 instance Category Boolean where
-  data Obj Boolean a where
-    Fls :: Obj Boolean BF
-    Tru :: Obj Boolean BT
   
-  src IdFls  = Fls
-  src FlsTru = Fls
-  src IdTru  = Tru
-  
-  tgt IdFls  = Fls
-  tgt FlsTru = Tru
-  tgt IdTru  = Tru
+  src Fls   = Fls
+  src F2T   = Fls
+  src Tru   = Tru
   
-  id Fls     = IdFls
-  id Tru     = IdTru
+  tgt Fls   = Fls
+  tgt F2T   = Tru
+  tgt Tru   = Tru
   
-  IdFls  . IdFls  = IdFls
-  FlsTru . IdFls  = FlsTru
-  IdTru  . FlsTru = FlsTru
-  IdTru  . IdTru  = IdTru
+  Fls . Fls = Fls
+  F2T . Fls = F2T
+  Tru . F2T = F2T
+  Tru . Tru = Tru
   _      . _      = error "Other combinations should not type check"
 
 
 -- | False is the initial object in the Boolean category.
 instance HasInitialObject Boolean where
-  type InitialObject Boolean = BF
+  type InitialObject Boolean = Fls
   initialObject = Fls
-  initialize Fls = IdFls
-  initialize Tru = FlsTru
+  initialize Fls = Fls
+  initialize Tru = F2T
+  initialize _   = error "Other values should not type check"
   
 -- | True is the terminal object in the Boolean category.
 instance HasTerminalObject Boolean where
-  type TerminalObject Boolean = BT
+  type TerminalObject Boolean = Tru
   terminalObject = Tru
-  terminate Fls = FlsTru
-  terminate Tru = IdTru
+  terminate Fls = F2T
+  terminate Tru = Tru
+  terminate _   = error "Other values should not type check"
 
 
-type instance BinaryProduct Boolean BF BF = BF
-type instance BinaryProduct Boolean BF BT = BF
-type instance BinaryProduct Boolean BT BF = BF
-type instance BinaryProduct Boolean BT BT = BT
+type instance BinaryProduct Boolean Fls Fls = Fls
+type instance BinaryProduct Boolean Fls Tru = Fls
+type instance BinaryProduct Boolean Tru Fls = Fls
+type instance BinaryProduct Boolean Tru Tru = Tru
 
 instance HasBinaryProducts Boolean where 
   
-  product Fls Fls = Fls
-  product Fls Tru = Fls
-  product Tru Fls = Fls
-  product Tru Tru = Tru
-  
-  proj Fls Fls = (IdFls , IdFls)
-  proj Fls Tru = (IdFls , FlsTru)
-  proj Tru Fls = (FlsTru, IdFls)
-  proj Tru Tru = (IdTru , IdTru)
-  
-  IdFls  &&& IdFls  = IdFls
-  IdFls  &&& FlsTru = IdFls
-  FlsTru &&& IdFls  = IdFls
-  FlsTru &&& FlsTru = FlsTru
-  IdTru  &&& IdTru  = IdTru
-  _      &&& _      = error "Other combinations should not type check"
+  proj1 Fls Fls = Fls
+  proj1 Fls Tru = Fls
+  proj1 Tru Fls = F2T
+  proj1 Tru Tru = Tru
+  proj1 _   _   = error "Other combinations should not type check"
+  proj2 Fls Fls = Fls
+  proj2 Fls Tru = F2T
+  proj2 Tru Fls = Fls
+  proj2 Tru Tru = Tru
+  proj2 _   _   = error "Other combinations should not type check"
+    
+  Fls &&& Fls = Fls
+  Fls &&& F2T = Fls
+  F2T &&& Fls = Fls
+  F2T &&& F2T = F2T
+  Tru &&& Tru = Tru
+  _   &&& _   = error "Other combinations should not type check"
 
 
-type instance BinaryCoproduct Boolean BF BF = BF
-type instance BinaryCoproduct Boolean BF BT = BT
-type instance BinaryCoproduct Boolean BT BF = BT
-type instance BinaryCoproduct Boolean BT BT = BT
+type instance BinaryCoproduct Boolean Fls Fls = Fls
+type instance BinaryCoproduct Boolean Fls Tru = Tru
+type instance BinaryCoproduct Boolean Tru Fls = Tru
+type instance BinaryCoproduct Boolean Tru Tru = Tru
 
 instance HasBinaryCoproducts Boolean where 
   
-  coproduct Fls Fls = Fls
-  coproduct Fls Tru = Tru
-  coproduct Tru Fls = Tru
-  coproduct Tru Tru = Tru
-  
-  inj Fls Fls = (IdFls , IdFls)
-  inj Fls Tru = (FlsTru, IdTru)
-  inj Tru Fls = (IdTru , FlsTru)
-  inj Tru Tru = (IdTru , IdTru)
-  
-  IdFls  ||| IdFls  = IdFls
-  FlsTru ||| FlsTru = FlsTru
-  FlsTru ||| IdTru  = IdTru
-  IdTru  ||| FlsTru = IdTru
-  IdTru  ||| IdTru  = IdTru
-  _      ||| _      = error "Other combinations should not type check"
+  inj1 Fls Fls = Fls
+  inj1 Fls Tru = F2T
+  inj1 Tru Fls = Tru
+  inj1 Tru Tru = Tru
+  inj1 _   _   = error "Other combinations should not type check"
+  inj2 Fls Fls = Fls
+  inj2 Fls Tru = Tru
+  inj2 Tru Fls = F2T
+  inj2 Tru Tru = Tru
+  inj2 _   _   = error "Other combinations should not type check"
+    
+  Fls ||| Fls = Fls
+  F2T ||| F2T = F2T
+  F2T ||| Tru = Tru
+  Tru ||| F2T = Tru
+  Tru ||| Tru = Tru
+  _   ||| _   = error "Other combinations should not type check"
 
 
-instance Show (Obj Boolean a) where
-  show Fls = "Fls"
-  show Tru = "Tru"
+
+-- | A natural transformation @Nat c d@ is isomorphic to a functor from @c :**: 2@ to @d@.
+data NatAsFunctor f g = NatAsFunctor (Nat (Dom f) (Cod f) f g)
+type instance Dom (NatAsFunctor f g) = (Dom f) :**: Boolean
+type instance Cod (NatAsFunctor f g) = Cod f
+type instance NatAsFunctor f g :% (a, Fls) = f :% a
+type instance NatAsFunctor f g :% (a, Tru) = g :% a
+instance (Functor f, Functor g, Category c, Category d, Dom f ~ c, Cod f ~ d, Dom g ~ c, Cod g ~ d) => Functor (NatAsFunctor f g) where
+  NatAsFunctor n % (a :**: b) = natAsFunctor n a b
+    where
+      natAsFunctor :: Nat c d f g -> c a1 a2 -> Boolean b1 b2 -> d (NatAsFunctor f g :% (a1, b1)) (NatAsFunctor f g :% (a2, b2))
+      natAsFunctor (Nat f _ _) a Fls = f % a
+      natAsFunctor (Nat _ g _) a Tru = g % a
+      natAsFunctor n           a F2T = n ! a
diff --git a/Data/Category/CartesianClosed.hs b/Data/Category/CartesianClosed.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/CartesianClosed.hs
@@ -0,0 +1,119 @@
+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, Rank2Types, ScopedTypeVariables, UndecidableInstances #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Category.CartesianClosed
+-- Copyright   :  (c) Sjoerd Visscher 2010
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  sjoerd@w3future.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+-----------------------------------------------------------------------------
+module Data.Category.CartesianClosed where
+  
+import Prelude (($))
+
+import Data.Category
+import Data.Category.Functor
+import Data.Category.NaturalTransformation
+import Data.Category.Product
+import Data.Category.Limit
+import Data.Category.Adjunction
+import qualified Data.Category.Monoidal as M
+
+
+type family Exponential (~>) y z :: *
+
+class (HasTerminalObject (~>), HasBinaryProducts (~>)) => CartesianClosed (~>) where
+  
+  apply :: Obj (~>) y -> Obj (~>) z -> BinaryProduct (~>) (Exponential (~>) y z) y ~> z
+  tuple :: Obj (~>) y -> Obj (~>) z -> z ~> Exponential (~>) y (BinaryProduct (~>) z y)
+  (^^^) :: (z1 ~> z2) -> (y2 ~> y1) -> (Exponential (~>) y1 z1 ~> Exponential (~>) y2 z2)
+
+
+data ExpFunctor ((~>) :: * -> * -> *) = ExpFunctor
+type instance Dom (ExpFunctor (~>)) = Op (~>) :**: (~>)
+type instance Cod (ExpFunctor (~>)) = (~>)
+type instance (ExpFunctor (~>)) :% (y, z) = Exponential (~>) y z
+instance CartesianClosed (~>) => Functor (ExpFunctor (~>)) where
+  ExpFunctor % (Op y :**: z) = z ^^^ y
+
+
+
+type instance Exponential (->) y z = y -> z
+
+instance (CartesianClosed (->)) where
+  
+  apply _ _ (f, y) = f y
+  tuple _ _ z      = \y -> (z, y)
+  f ^^^ h          = \g -> f . g . h
+
+
+
+data CatApply (y :: * -> * -> *) (z :: * -> * -> *) = CatApply
+type instance Dom (CatApply y z) = Nat y z :**: y
+type instance Cod (CatApply y z) = z
+type instance CatApply y z :% (f, a) = f :% a
+instance (Category y, Category z) => Functor (CatApply y z) where
+  CatApply % (l :**: r) = catApply l r
+    where
+      catApply :: Nat y z f g -> y a b -> z (f :% a) (g :% b)
+      catApply n@Nat{} h = n ! h
+
+data CatTuple (y :: * -> * -> *) (z :: * -> * -> *) = CatTuple
+type instance Dom (CatTuple y z) = z
+type instance Cod (CatTuple y z) = Nat y (z :**: y)
+type instance CatTuple y z :% a = Tuple1 z y a
+instance (Category y, Category z) => Functor (CatTuple y z) where
+  CatTuple % f = Nat (Tuple1 (src f)) (Tuple1 (tgt f)) $ \z -> f :**: z
+
+
+type instance Exponential Cat (CatW c) (CatW d) = CatW (Nat c d)
+
+instance (CartesianClosed Cat) where
+  
+  apply CatA{} CatA{}   = CatA CatApply
+  tuple CatA{} CatA{}   = CatA CatTuple
+  (CatA f) ^^^ (CatA h) = CatA (Wrap f h)
+
+
+
+data ProductWith (~>) y = ProductWith (Obj (~>) y)
+type instance Dom (ProductWith (~>) y) = (~>)
+type instance Cod (ProductWith (~>) y) = (~>)
+type instance ProductWith (~>) y :% z = ProductFunctor (~>) :% (z, y)
+instance HasBinaryProducts (~>) => Functor (ProductWith (~>) y) where
+  ProductWith y % f = f *** y
+  
+data ExponentialWith (~>) y = ExponentialWith (Obj (~>) y)
+type instance Dom (ExponentialWith (~>) y) = (~>)
+type instance Cod (ExponentialWith (~>) y) = (~>)
+type instance ExponentialWith (~>) y :% z = Exponential (~>) y z
+instance CartesianClosed (~>) => Functor (ExponentialWith (~>) y) where
+  ExponentialWith y % f = f ^^^ y
+
+curryAdj :: CartesianClosed (~>) => Obj (~>) y -> Adjunction (~>) (~>) (ProductWith (~>) y) (ExponentialWith (~>) y)
+curryAdj y = mkAdjunction (ProductWith y) (ExponentialWith y) (tuple y) (apply y)
+
+curry :: CartesianClosed (~>) => Obj (~>) x -> Obj (~>) y -> Obj (~>) z -> (ProductWith (~>) y :% x) ~> z -> x ~> (ExponentialWith (~>) y :% z)
+curry x y _ = leftAdjunct (curryAdj y) x
+
+uncurry :: CartesianClosed (~>) => Obj (~>) x -> Obj (~>) y -> Obj (~>) z -> x ~> (ExponentialWith (~>) y :% z) -> (ProductWith (~>) y :% x) ~> z
+uncurry _ y z = rightAdjunct (curryAdj y) z
+
+
+type State (~>) s a = ExponentialWith (~>) s :% ProductWith (~>) s :% a
+
+stateMonadReturn :: CartesianClosed (~>) => Obj (~>) s -> Obj (~>) a -> a ~> State (~>) s a
+stateMonadReturn s a = M.unit (adjunctionMonad $ curryAdj s) ! a
+
+stateMonadJoin :: CartesianClosed (~>) => Obj (~>) s -> Obj (~>) a -> State (~>) s (State (~>) s a) ~> State (~>) s a
+stateMonadJoin s a = M.multiply (adjunctionMonad $ curryAdj s) ! a
+
+type Context (~>) s a = ProductWith (~>) s :% ExponentialWith (~>) s :% a
+
+contextComonadExtract :: CartesianClosed (~>) => Obj (~>) s -> Obj (~>) a -> Context (~>) s a ~> a
+contextComonadExtract s a = M.counit (adjunctionComonad $ curryAdj s) ! a
+
+contextComonadDuplicate :: CartesianClosed (~>) => Obj (~>) s -> Obj (~>) a -> Context (~>) s a ~> Context (~>) s (Context (~>) s a)
+contextComonadDuplicate s a = M.comultiply (adjunctionComonad $ curryAdj s) ! a
diff --git a/Data/Category/Comma.hs b/Data/Category/Comma.hs
--- a/Data/Category/Comma.hs
+++ b/Data/Category/Comma.hs
@@ -17,27 +17,25 @@
 
 import Data.Category
 import Data.Category.Functor
-import Data.Category.NaturalTransformation
 
 
+data CommaO :: * -> * -> * -> * where
+  CommaO :: (Cod t ~ (~>), Cod s ~ (~>))
+    => Obj (Dom t) a -> (t :% a ~> s :% b) -> Obj (Dom s) b -> CommaO t s (a, b)
+    
 data (:/\:) :: * -> * -> * -> * -> * where 
   CommaA :: 
-    Obj (t :/\: s) (a, b) ->
+    CommaO t s (a, b) ->
     Dom t a a' -> 
     Dom s b b' -> 
-    Obj (t :/\: s) (a', b') ->
+    CommaO t s (a', b') ->
     (t :/\: s) (a, b) (a', b')
 
 instance (Category (Dom t), Category (Dom s)) => Category (t :/\: s) where
     
-  data Obj (t :/\: s) x where
-    CommaO :: (Cod t ~ (~>), Cod s ~ (~>))
-      => Obj (Dom t) a -> (t :% a ~> s :% b) -> Obj (Dom s) b -> Obj (t :/\: s) (a, b)
-    
-  src (CommaA so _ _ _) = so
-  tgt (CommaA _ _ _ to) = to
+  src (CommaA so@(CommaO a _ b) _ _ _)    = CommaA so a        b        so
+  tgt (CommaA _ _ _ to@(CommaO a _ b))    = CommaA to a        b        to
   
-  id x@(CommaO a _ b)                     = CommaA x  (id a)   (id b)   x
   (CommaA _ g h to) . (CommaA so g' h' _) = CommaA so (g . g') (h . h') to
 
 
diff --git a/Data/Category/Dialg.hs b/Data/Category/Dialg.hs
--- a/Data/Category/Dialg.hs
+++ b/Data/Category/Dialg.hs
@@ -13,7 +13,7 @@
 -----------------------------------------------------------------------------
 module Data.Category.Dialg where
 
-import Prelude hiding ((.), id, Functor)
+import Prelude hiding ((.), Functor)
 import qualified Prelude
 
 import Data.Category
@@ -23,24 +23,26 @@
 
 
 -- | Objects of Dialg(F,G) are (F,G)-dialgebras.
-type Dialgebra f g a = Obj (Dialg f g) a
+data Dialgebra f g a where
+  Dialgebra :: (Category c, Category d, Dom f ~ c, Dom g ~ c, Cod f ~ d, Cod g ~ d, Functor f, Functor g) 
+    => Obj c a -> d (f :% a) (g :% a) -> Dialgebra f g a
 
 -- | Arrows of Dialg(F,G) are (F,G)-homomorphisms.
 data Dialg f g a b where
   DialgA :: (Category c, Category d, Dom f ~ c, Dom g ~ c, Cod f ~ d, Cod g ~ d, Functor f, Functor g) 
     => Dialgebra f g a -> Dialgebra f g b -> c a b -> Dialg f g a b
 
+dialgId :: Dialgebra f g a -> Obj (Dialg f g) a
+dialgId d@(Dialgebra a _) = DialgA d d a
 
+dialgebra :: Obj (Dialg f g) a -> Dialgebra f g a
+dialgebra (DialgA d _ _) = d
+
 instance Category (Dialg f g) where
   
-  data Obj (Dialg f g) a where
-    Dialgebra :: (Category c, Category d, Dom f ~ c, Dom g ~ c, Cod f ~ d, Cod g ~ d, Functor f, Functor g) 
-      => Obj c a -> d (f :% a) (g :% a) -> Obj (Dialg f g) a
-      
-  src (DialgA s _ _) = s
-  tgt (DialgA _ t _) = t
+  src (DialgA s _ _) = dialgId s
+  tgt (DialgA _ t _) = dialgId t
   
-  id x@(Dialgebra a _)        = DialgA x x $ id a
   DialgA _ t f . DialgA s _ g = DialgA s t $ f . g
 
 
@@ -66,56 +68,55 @@
 
 
 -- | 'FixF' provides the initial F-algebra for endofunctors in Hask.
-newtype FixF f = InF { outF :: f (FixF f) }
+newtype FixF f = InF { outF :: f :% FixF f }
 
 -- | Catamorphisms for endofunctors in Hask.
 cataHask :: Prelude.Functor f => Cata (EndoHask f) a
-cataHask a@(Dialgebra HaskO f) = DialgA initialObject a $ cata f where cata f = f . fmap (cata f) . outF 
+cataHask a@(Dialgebra _ f) = DialgA (dialgebra initialObject) a $ cata_f where cata_f = f . (EndoHask % cata_f) . outF 
 
--- -- | Anamorphisms for endofunctors in Hask.
+-- | Anamorphisms for endofunctors in Hask.
 anaHask :: Prelude.Functor f => Ana (EndoHask f) a
-anaHask a@(Dialgebra HaskO f) = DialgA a terminalObject $ ana f where ana f = InF . fmap (ana f) . f 
+anaHask a@(Dialgebra _ f) = DialgA a (dialgebra terminalObject) $ ana_f where ana_f = InF . (EndoHask % ana_f) . f 
 
 
 instance Prelude.Functor f => HasInitialObject (Dialg (EndoHask f) (Id (->))) where
   
-  type InitialObject (Dialg (EndoHask f) (Id (->))) = FixF f
+  type InitialObject (Dialg (EndoHask f) (Id (->))) = FixF (EndoHask f)
   
-  initialObject = Dialgebra HaskO InF
-  initialize = cataHask
+  initialObject = dialgId $ Dialgebra id InF
+  initialize a = cataHask (dialgebra a)
   
 instance  Prelude.Functor f => HasTerminalObject (Dialg (Id (->)) (EndoHask f)) where
 
-  type TerminalObject (Dialg (Id (->)) (EndoHask f)) = FixF f
+  type TerminalObject (Dialg (Id (->)) (EndoHask f)) = FixF (EndoHask f)
   
-  terminalObject = Dialgebra HaskO outF
-  terminate = anaHask
+  terminalObject = dialgId $ Dialgebra id outF
+  terminate a = anaHask (dialgebra a)
   
 
 
 -- | The category for defining the natural numbers and primitive recursion can be described as
 -- @Dialg(F,G)@, with @F(A)=\<1,A>@ and @G(A)=\<A,A>@.
 data NatF ((~>) :: * -> * -> *) where
-  NatF :: HasTerminalObject (~>) => NatF (~>)
+  NatF :: NatF (~>)
 type instance Dom (NatF (~>)) = (~>)
-type instance Cod (NatF (~>)) = (~>) :*: (~>)
+type instance Cod (NatF (~>)) = (~>) :**: (~>)
 type instance NatF (~>) :% a = (TerminalObject (~>),  a)
-instance Functor (NatF (~>)) where
-  NatF %% x = ProdO terminalObject x
-  NatF %  f = id terminalObject :**: f
+instance HasTerminalObject (~>) => Functor (NatF (~>)) where
+  NatF % f = terminalObject :**: f
 
-data NatNum = Z | S NatNum
-primRec :: t -> (t -> t) -> NatNum -> t
-primRec z _ Z     = z
-primRec z s (S n) = s (primRec z s n)
+data NatNum = Z () | S NatNum
+primRec :: (() -> t) -> (t -> t) -> NatNum -> t
+primRec z _ (Z ()) = z ()
+primRec z s (S  n) = s (primRec z s n)
 
 instance HasInitialObject (Dialg (NatF (->)) (DiagProd (->))) where
   
   type InitialObject (Dialg (NatF (->)) (DiagProd (->))) = NatNum
     
-  initialObject = Dialgebra HaskO (const Z :**: S)
+  initialObject = dialgId $ Dialgebra id (Z :**: S)
   
-  initialize o@(Dialgebra HaskO p) = DialgA initialObject o $ f p where
-    f :: ((->) :*: (->)) ((), t) (t, t) -> NatNum -> t
-    f (z :**: s) = primRec (z ()) s
+  initialize a = DialgA (dialgebra initialObject) (dialgebra a) $ f undefined where
+    f :: ((->) :**: (->)) ((), t) (t, t) -> NatNum -> t
+    f (z :**: s) = primRec z s
     
diff --git a/Data/Category/Discrete.hs b/Data/Category/Discrete.hs
--- a/Data/Category/Discrete.hs
+++ b/Data/Category/Discrete.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, EmptyDataDecls, FlexibleContexts, FlexibleInstances, UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, RankNTypes, EmptyDataDecls, ScopedTypeVariables, FlexibleContexts, FlexibleInstances, UndecidableInstances #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Discrete
@@ -11,95 +11,151 @@
 --
 -- Discrete n, the category with n objects, and as the only arrows their identities.
 -----------------------------------------------------------------------------
-module Data.Category.Discrete where
+module Data.Category.Discrete (
 
+  -- * Discrete Categories
+    Discrete(..)
+  , Z, S
+  , Void
+  , Unit
+  , Pair
+  
+  -- * Diagrams
+  , DiscreteDiagram(..)
+  , PairDiagram
+  , arrowPair
+    
+  -- * Natural Transformations
+  , discreteNat
+  , ComList(..)
+  , voidNat
+  , pairNat
+    
+) where
+
 import Prelude hiding ((.), id, Functor, product)
 
 import Data.Category
 import Data.Category.Functor
 import Data.Category.NaturalTransformation
-import Data.Category.Void
-import Data.Category.Pair
 
+
 data Z
-data S n = S n
+data S n
 
 -- | The arrows in Discrete n, a finite set of identity arrows.
 data Discrete :: * -> * -> * -> * where
-  IdZ   :: Discrete (S n) Z Z
-  StepS :: Discrete n a a -> Discrete (S n) (S a) (S a)
-
-
-instance Category (Discrete n) => Category (Discrete (S n)) where
-  
-  data Obj (Discrete (S n)) a where
-    OZ :: Obj (Discrete (S n)) Z
-    OS :: Obj (Discrete n) o -> Obj (Discrete (S n)) (S o)
-    
-  src IdZ       = OZ
-  src (StepS a) = OS $ src a
-  
-  tgt IdZ       = OZ
-  tgt (StepS a) = OS $ tgt a
-  
-  id OZ             = IdZ
-  id (OS n)         = StepS $ id n
-  
-  IdZ     . IdZ     = IdZ
-  StepS a . StepS b = StepS (a . b)
-  _       . _       = error "Other combinations should not type-check."
+  Z :: Discrete (S n) Z Z
+  S :: Discrete n a a -> Discrete (S n) (S a) (S a)
 
 
 magicZ :: Discrete Z a b -> x
 magicZ x = x `seq` error "we never get this far"
 
-magicZO :: Obj (Discrete Z) a -> x
-magicZO x = x `seq` error "we never get this far"
 
+-- | @Discrete Z@ is the discrete category with no objects.
+instance Category (Discrete Z) where
+  
+  src   = magicZ
+  tgt   = magicZ
+  
+  a . b = magicZ (a `seq` b)
 
 
-instance Category (Discrete Z) where
+-- | @Discrete (S n)@ is the discrete category with one object more than @Discrete n@.
+instance Category (Discrete n) => Category (Discrete (S n)) where
   
-  data Obj (Discrete Z) a
+  src Z     = Z
+  src (S a) = S $ src a
   
-  src = magicZ
-  tgt = magicZ
+  tgt Z     = Z
+  tgt (S a) = S $ tgt a
   
-  id    = magicZO
-  a . b = magicZ (a `seq` b)
+  Z   . Z   = Z
+  S a . S b = S (a . b)
+  _   . _   = error "Other combinations should not type-check."
 
 
+-- | @Void@ is the empty category.
+type Void = Discrete Z
+-- | @Unit@ is the discrete category with one object.
+type Unit = Discrete (S Z)
+-- | @Pair@ is the discrete category with two objects.
+type Pair = Discrete (S (S Z))
 
-data Next :: * -> * -> * where
-  Next :: (Functor f, Dom f ~ Discrete (S n)) => f -> Next n f
+
+type family PredDiscrete (c :: * -> * -> *) :: * -> * -> *
+type instance PredDiscrete (Discrete (S n)) = Discrete n
+
+data Next :: * -> * where
+  Next :: (Functor f, Dom f ~ Discrete (S n)) => f -> Next f
   
-type instance Dom (Next n f) = Discrete n
-type instance Cod (Next n f) = Cod f
-type instance Next n f :% a = f :% S a
+type instance Dom (Next f) = PredDiscrete (Dom f)
+type instance Cod (Next f) = Cod f
+type instance Next f :% a = f :% S a
 
-instance Functor (Next n f) where
-  Next f %% n = f %% OS n
-  Next f % IdZ       = f % StepS IdZ
-  Next f % (StepS a) = f % StepS (StepS a)
-    
+instance (Functor f, Category (PredDiscrete (Dom f))) => Functor (Next f) where
+  Next f % Z     = f % S Z
+  Next f % (S a) = f % S (S a)
 
+
 infixr 7 :::
 
+-- | The functor from @Discrete n@ to @(~>)@, a diagram of @n@ objects in @(~>)@. 
 data DiscreteDiagram :: (* -> * -> *) -> * -> * -> * where
   Nil   :: DiscreteDiagram (~>) Z ()
-  (:::) :: Category (~>) => Obj (~>) x -> DiscreteDiagram (~>) n xs -> DiscreteDiagram (~>) (S n) (x, xs)
+  (:::) :: Obj (~>) x -> DiscreteDiagram (~>) n xs -> DiscreteDiagram (~>) (S n) (x, xs)
   
 type instance Dom (DiscreteDiagram (~>) n xs) = Discrete n
 type instance Cod (DiscreteDiagram (~>) n xs) = (~>)
 type instance DiscreteDiagram (~>) (S n) (x, xs) :% Z = x
 type instance DiscreteDiagram (~>) (S n) (x, xs) :% (S a) = DiscreteDiagram (~>) n xs :% a
 
-instance Functor (DiscreteDiagram (~>) n xs) where
-  
-  Nil        %% x  = magicZO x
-  (x ::: _)  %% OZ = x
-  (_ ::: xs) %% OS n = xs %% n
+instance (Category (~>)) 
+  => Functor (DiscreteDiagram (~>) Z ()) where
+  Nil        % f = magicZ f
+
+instance (Category (~>), Category (Discrete n), Functor (DiscreteDiagram (~>) n xs)) 
+  => Functor (DiscreteDiagram (~>) (S n) (x, xs)) where
+  (x ::: _)  % Z   = x
+  (_ ::: xs) % S n = xs % n
+
+
+infixr 7 ::::
+
+data ComList f g n z where
+  ComNil :: ComList f g Z z
+  (::::) :: Com f g z -> ComList f g n (S z) -> ComList f g (S n) z
+
+class DiscreteNat n where
+  discreteNat :: (Functor f, Functor g, Category d, Dom f ~ Discrete n, Dom g ~ Discrete n, Cod f ~ d, Cod g ~ d)
+    => f -> g -> ComList f g n Z -> Nat (Discrete n) d f g
+  shiftComList :: ComList f g n (S z) -> ComList (Next f) (Next g) n z
   
-  Nil        %  f = magicZ f
-  (x ::: _)  %  IdZ = id x
-  (_ ::: xs) %  StepS n = xs % n
+instance DiscreteNat Z where
+  discreteNat f g ComNil = Nat f g magicZ
+  shiftComList ComNil = ComNil
+
+instance (Category (Discrete n), DiscreteNat n) => DiscreteNat (S n) where
+  discreteNat f g comlist = Nat f g (\x -> unCom $ h f g comlist x) where
+    h :: (Functor f, Functor g, Category d, Dom f ~ Discrete (S n), Dom g ~ Discrete (S n), Cod f ~ d, Cod g ~ d)
+      => f -> g -> ComList f g (S n) Z -> Obj (Discrete (S n)) a -> Com f g a
+    h _  _  (c :::: _ ) Z     = c
+    h f' g' (_ :::: cs) (S n) = Com $ (discreteNat (Next f') (Next g') (shiftComList cs)) ! n
+  shiftComList (Com c :::: cs) = Com c :::: shiftComList cs
+
+voidNat :: (Functor f, Functor g, Category d, Dom f ~ Void, Dom g ~ Void, Cod f ~ d, Cod g ~ d)
+  => f -> g -> Nat Void d f g
+voidNat f g       = discreteNat f g ComNil
+
+pairNat :: (Functor f, Functor g, Category d, Dom f ~ Pair, Cod f ~ d, Dom g ~ Pair, Cod g ~ d) 
+  => f -> g -> Com f g Z -> Com f g (S Z) -> Nat Pair d f g
+pairNat f g c1 c2 = discreteNat f g (c1 :::: c2 :::: ComNil)
+
+
+-- | The functor from @Pair@ to @(~>)@, a diagram of 2 objects in @(~>)@. 
+type PairDiagram (~>) x y = DiscreteDiagram (~>) (S (S Z)) (x, (y, ()))
+
+arrowPair :: Category (~>) => (x1 ~> x2) -> (y1 ~> y2) -> Nat Pair (~>) (PairDiagram (~>) x1 y1) (PairDiagram (~>) x2 y2)
+arrowPair l r = pairNat (src l ::: src r ::: Nil) (tgt l ::: tgt r ::: Nil) (Com l) (Com r)
+
diff --git a/Data/Category/Functor.hs b/Data/Category/Functor.hs
--- a/Data/Category/Functor.hs
+++ b/Data/Category/Functor.hs
@@ -13,7 +13,6 @@
 
   -- * Cat
     Cat(..)
-  , Obj(..)
   , CatW
 
   -- * Functors
@@ -42,20 +41,20 @@
   
 import Data.Category
 
+infixr 9 %
+infixr 9 :%
 
 -- | The domain, or source category, of the functor.
 type family Dom ftag :: * -> * -> *
 -- | The codomain, or target category, of the functor.
 type family Cod ftag :: * -> * -> *
 
--- | Functors map objects and arrows. As objects are represented at both the type and value level, we need 3 maps in total.
-class Functor ftag where
-  -- | @%%@ maps objects at the value level.
-  (%%) :: ftag -> Obj (Dom ftag) a -> Obj (Cod ftag) (ftag :% a)
+-- | Functors map objects and arrows.
+class (Category (Dom ftag), Category (Cod ftag)) => Functor ftag where
   -- | @%@ maps arrows.
   (%)  :: ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
 
--- | @:%@ maps objects at the type level.
+-- | @:%@ maps objects.
 type family ftag :% a :: *
 
 
@@ -70,14 +69,9 @@
 -- | @Cat@ is the category with categories as objects and funtors as arrows.
 instance Category Cat where
   
-  -- | The objects in the category Cat are the categories themselves.
-  data Obj Cat a where
-    CatO :: Category (~>) => Obj Cat (CatW (~>))
-    
-  src (CatA _) = CatO
-  tgt (CatA _) = CatO
+  src (CatA _)      = CatA Id
+  tgt (CatA _)      = CatA Id
   
-  id CatO           = CatA Id
   CatA f1 . CatA f2 = CatA (f1 :.: f2)
 
 
@@ -89,9 +83,8 @@
 type instance Cod (Id (~>)) = (~>)
 type instance Id (~>) :% a = a
 
-instance Functor (Id (~>)) where 
-  _ %% x = x
-  _ %  f = f
+instance Category (~>) => Functor (Id (~>)) where 
+  _ % f = f
 
 
 -- | The composition of two functors.
@@ -102,9 +95,8 @@
 type instance Cod (g :.: h) = Cod g
 type instance (g :.: h) :% a = g :% (h :% a)
 
-instance Functor (g :.: h) where 
-  (g :.: h) %% x = g %% (h %% x)
-  (g :.: h) %  f = g %  (h %  f)
+instance (Category (Cod g), Category (Dom h)) => Functor (g :.: h) where 
+  (g :.: h) % f = g % (h % f)
 
 
 -- | The constant functor.
@@ -115,9 +107,8 @@
 type instance Cod (Const c1 c2 x) = c2
 type instance Const c1 c2 x :% a = x
 
-instance Functor (Const c1 c2 x) where 
-  Const x %% _ = x
-  Const x %  _ = id x
+instance (Category c1, Category c2) => Functor (Const c1 c2 x) where 
+  Const x % _ = x
 
 type ConstF f = Const (Dom f) (Cod f)
 
@@ -130,9 +121,8 @@
 type instance Cod (x :*-: (~>)) = (->)
 type instance (x :*-: (~>)) :% a = x ~> a
 
-instance Functor (x :*-: (~>)) where 
-  HomX_ _ %% _ = HaskO
-  HomX_ _ %  f = (f .)
+instance Category (~>) => Functor (x :*-: (~>)) where 
+  HomX_ _ % f = (f .)
 
 
 -- | The contravariant functor Hom(--,X)
@@ -143,8 +133,7 @@
 type instance Cod ((~>) :-*: x) = (->)
 type instance ((~>) :-*: x) :% a = a ~> x
 
-instance Functor ((~>) :-*: x) where 
-  Hom_X _ %% _   = HaskO
+instance Category (~>) => Functor ((~>) :-*: x) where 
   Hom_X _ % Op f = (. f)
 
 
@@ -156,8 +145,7 @@
 type instance Cod (Opposite f) = Op (Cod f)
 type instance Opposite f :% a = f :% a
 
-instance Functor (Opposite f) where
-  Opposite f %% OpObj x = OpObj $ f %% x
+instance (Category (Dom f), Category (Cod f)) => Functor (Opposite f) where
   Opposite f % Op a = Op $ f % a
 
 
@@ -170,7 +158,6 @@
 type instance EndoHask f :% r = f r
 
 instance Functor (EndoHask f) where
-  EndoHask %% HaskO = HaskO
   EndoHask % f = fmap f
 
 
diff --git a/Data/Category/Kleisli.hs b/Data/Category/Kleisli.hs
--- a/Data/Category/Kleisli.hs
+++ b/Data/Category/Kleisli.hs
@@ -19,52 +19,44 @@
 import Data.Category
 import Data.Category.Functor
 import Data.Category.NaturalTransformation
-import Data.Category.Adjunction
+import Data.Category.Monoidal
+import qualified Data.Category.Adjunction as A
 
 
-class Functor m => Pointed m where
-  point :: m -> Id (Dom m) :~> m
-  
-class Pointed m => Monad m where
-  join :: m -> (m :.: m) :~> m
-
-  
 data Kleisli ((~>) :: * -> * -> *) m a b where
-  Kleisli :: m -> Obj (~>) b -> a ~> (m :% b) -> Kleisli (~>) m a b
+  Kleisli :: Monad m -> Obj (~>) b -> a ~> (m :% b) -> Kleisli (~>) m a b
 
+kleisliId :: (Category (~>), Functor m, Dom m ~ (~>), Cod m ~ (~>)) 
+  => Monad m -> Obj (~>) a -> Kleisli (~>) m a a
+kleisliId m a = Kleisli m a $ unit m ! a
 
-instance (Category (~>), Monad m, Dom m ~ (~>), Cod m ~ (~>)) => Category (Kleisli (~>) m) where
-  
-  data Obj (Kleisli (~>) m) a = KleisliO m (Obj (~>) a)
+instance (Category (~>), Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Category (Kleisli (~>) m) where
   
-  src (Kleisli m _ f) = KleisliO m (src f)
-  tgt (Kleisli m b _) = KleisliO m b
+  src (Kleisli m _ f) = kleisliId m (src f)
+  tgt (Kleisli m b _) = kleisliId m b
   
-  id (KleisliO m o)                 = Kleisli m o $ point m ! o
-  (Kleisli m c f) . (Kleisli _ _ g) = Kleisli m c $ (join m ! c) . (m % f) . g
+  (Kleisli m c f) . (Kleisli _ _ g) = Kleisli m c $ (multiply m ! c) . (monadFunctor m % f) . g
 
 
 
 data KleisliAdjF ((~>) :: * -> * -> *) m where
-  KleisliAdjF :: (Category (~>), Monad m, Dom m ~ (~>), Cod m ~ (~>)) => m -> KleisliAdjF (~>) m
+  KleisliAdjF :: Monad m -> KleisliAdjF (~>) m
 type instance Dom (KleisliAdjF (~>) m) = (~>)
 type instance Cod (KleisliAdjF (~>) m) = Kleisli (~>) m
 type instance KleisliAdjF (~>) m :% a = a
-instance Functor (KleisliAdjF (~>) m) where
-  KleisliAdjF m %% x = KleisliO m x
-  KleisliAdjF m %  f = Kleisli m (tgt f) $ (point m ! tgt f) . f
+instance (Category (~>), Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Functor (KleisliAdjF (~>) m) where
+  KleisliAdjF m % f = Kleisli m (tgt f) $ (unit m ! tgt f) . f
    
 data KleisliAdjG ((~>) :: * -> * -> *) m where
-  KleisliAdjG :: (Category (~>), Monad m, Dom m ~ (~>), Cod m ~ (~>)) => m -> KleisliAdjG (~>) m
+  KleisliAdjG :: Monad m -> KleisliAdjG (~>) m
 type instance Dom (KleisliAdjG (~>) m) = Kleisli (~>) m
 type instance Cod (KleisliAdjG (~>) m) = (~>)
 type instance KleisliAdjG (~>) m :% a = m :% a
-instance Functor (KleisliAdjG (~>) m) where
-  KleisliAdjG m %% KleisliO _ x = m %% x
-  KleisliAdjG m % Kleisli _ b f = (join m ! b) . (m % f)
+instance (Category (~>), Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Functor (KleisliAdjG (~>) m) where
+  KleisliAdjG m % Kleisli _ b f = (multiply m ! b) . (monadFunctor m % f)
 
-kleisliAdj :: (Monad m, Dom m ~ (~>), Cod m ~ (~>), Category (~>)) 
-  => m -> Adjunction (Kleisli (~>) m) (~>) (KleisliAdjF (~>) m) (KleisliAdjG (~>) m)
-kleisliAdj m = mkAdjunction (KleisliAdjF m) (KleisliAdjG m)
-  (\x -> point m ! x)
-  (\(KleisliO _ x) -> Kleisli m x $ m % id x)
+kleisliAdj :: (Functor m, Dom m ~ (~>), Cod m ~ (~>), Category (~>)) 
+  => Monad m -> A.Adjunction (Kleisli (~>) m) (~>) (KleisliAdjF (~>) m) (KleisliAdjG (~>) m)
+kleisliAdj m = A.mkAdjunction (KleisliAdjF m) (KleisliAdjG m)
+  (\x -> unit m ! x)
+  (\(Kleisli _ x _) -> Kleisli m x $ monadFunctor m % x)
diff --git a/Data/Category/Limit.hs b/Data/Category/Limit.hs
--- a/Data/Category/Limit.hs
+++ b/Data/Category/Limit.hs
@@ -8,6 +8,7 @@
   ScopedTypeVariables,
   TypeOperators, 
   TypeFamilies,
+  TypeSynonymInstances,
   UndecidableInstances  #-}
 -----------------------------------------------------------------------------
 -- |
@@ -65,8 +66,12 @@
   -- ** Limits of type Pair
   , BinaryProduct
   , HasBinaryProducts(..)
+  , ProductFunctor(..)
+  , (:*:)
   , BinaryCoproduct
   , HasBinaryCoproducts(..)
+  , CoproductFunctor(..)
+  , (:+:)
   
   -- ** Limits of type Hask
   , ForAll(..)
@@ -76,36 +81,32 @@
   
 ) where
 
-import Prelude hiding ((.), id, Functor, product)
+import Prelude hiding ((.), Functor, product)
 import qualified Prelude (Functor)
 import qualified Control.Arrow as A ((&&&), (***), (|||), (+++))
 
 import Data.Category
 import Data.Category.Functor
 import Data.Category.NaturalTransformation
-import Data.Category.Void
-import Data.Category.Pair
-import Data.Category.Unit
 import Data.Category.Product
 import Data.Category.Discrete
 
-infixr 3 ***
-infixr 3 &&&
-infixr 2 +++
-infixr 2 |||
+infixl 3 ***
+infixl 3 &&&
+infixl 2 +++
+infixl 2 |||
 
 
 -- | The diagonal functor from (index-) category J to (~>).
 data Diag :: (* -> * -> *) -> (* -> * -> *) -> * where
-  Diag :: (Category j, Category (~>)) => Diag j (~>)
+  Diag :: Diag j (~>)
   
 type instance Dom (Diag j (~>)) = (~>)
 type instance Cod (Diag j (~>)) = Nat j (~>)
 type instance Diag j (~>) :% a = Const j (~>) a
 
-instance Functor (Diag j (~>)) where 
-  Diag %% x = NatO $ Const x
-  Diag %  f = Nat (Const $ src f) (Const $ tgt f) $ const f
+instance (Category j, Category (~>)) => Functor (Diag j (~>)) where 
+  Diag % f = Nat (Const $ src f) (Const $ tgt f) $ const f
 
 -- | The diagonal functor with the same domain and codomain as @f@.
 type DiagF f = Diag (Dom f) (Cod f)
@@ -203,9 +204,8 @@
 type instance Cod (LimitFunctor j (~>)) = (~>)
 type instance LimitFunctor j (~>) :% f = LimitFam j (~>) f
 
-instance Functor (LimitFunctor j (~>)) where
-  LimitFunctor %% f @ NatO{} = tuObject (limitUniv f)
-  LimitFunctor %  n @ Nat{}  = limitFactorizer (limitUniv (tgt n)) (n . limit (limitUniv (src n)))
+instance (Category j, Category (~>)) => Functor (LimitFunctor j (~>)) where
+  LimitFunctor % n @ Nat{}  = limitFactorizer (limitUniv (tgt n)) (n . limit (limitUniv (src n)))
 
 
 
@@ -225,9 +225,8 @@
 type instance Cod (ColimitFunctor j (~>)) = (~>)
 type instance ColimitFunctor j (~>) :% f = ColimitFam j (~>) f
 
-instance Functor (ColimitFunctor j (~>)) where
-  ColimitFunctor %% f @ NatO{} = iuObject (colimitUniv f)
-  ColimitFunctor %  n @ Nat{}  = colimitFactorizer (colimitUniv (src n)) (colimit (colimitUniv (tgt n)) . n)
+instance (Category j, Category (~>)) => Functor (ColimitFunctor j (~>)) where
+  ColimitFunctor % n @ Nat{}  = colimitFactorizer (colimitUniv (src n)) (colimit (colimitUniv (tgt n)) . n)
 
 
 
@@ -245,7 +244,7 @@
 
 instance (HasTerminalObject (~>)) => HasLimits Void (~>) where
   
-  limitUniv (NatO f) = limitUniversal
+  limitUniv (Nat f _ _) = limitUniversal
     (voidNat (Const terminalObject) f)
     (terminate . coneVertex)
 
@@ -255,18 +254,18 @@
   
   type TerminalObject (->) = ()
   
-  terminalObject = HaskO
+  terminalObject = id
   
-  terminate HaskO _ = ()
+  terminate _ _ = ()
 
 -- | @Unit@ is the terminal category.
 instance HasTerminalObject Cat where
   
   type TerminalObject Cat = CatW Unit
   
-  terminalObject = CatO
+  terminalObject = CatA Id
   
-  terminate CatO = CatA $ Const UnitO
+  terminate (CatA _) = CatA $ Const Z
 
 
 -- | An initial object is the colimit of the functor from /0/ to (~>).
@@ -283,7 +282,7 @@
 
 instance HasInitialObject (~>) => HasColimits Void (~>) where
   
-  colimitUniv (NatO f) = colimitUniversal
+  colimitUniv (Nat f _ _) = colimitUniversal
     (voidNat f (Const initialObject))
     (initialize . coconeVertex)
 
@@ -295,18 +294,18 @@
   
   type InitialObject (->) = Zero
   
-  initialObject = HaskO
+  initialObject = id
   
   -- With thanks to Conor McBride
-  initialize HaskO x = x `seq` error "we never get this far"
+  initialize _ x = x `seq` error "we never get this far"
 
 instance HasInitialObject Cat where
   
   type InitialObject Cat = CatW Void
   
-  initialObject = CatO
+  initialObject = CatA Id
   
-  initialize CatO = CatA VoidDiagram
+  initialize (CatA _) = CatA Nil
 
 
 
@@ -315,106 +314,173 @@
 -- | The product of 2 objects is the limit of the functor from Pair to (~>).
 class Category (~>) => HasBinaryProducts (~>) where
   
-  product :: Obj (~>) x -> Obj (~>) y -> Obj (~>) (BinaryProduct (~>) x y)
-  
-  proj :: Obj (~>) x -> Obj (~>) y -> (BinaryProduct (~>) x y ~> x, BinaryProduct (~>) x y ~> y)
+  proj1 :: Obj (~>) x -> Obj (~>) y -> BinaryProduct (~>) x y ~> x
+  proj2 :: Obj (~>) x -> Obj (~>) y -> BinaryProduct (~>) x y ~> y
 
   (&&&) :: (a ~> x) -> (a ~> y) -> (a ~> BinaryProduct (~>) x y)
 
   (***) :: (a1 ~> b1) -> (a2 ~> b2) -> (BinaryProduct (~>) a1 a2 ~> BinaryProduct (~>) b1 b2)
-  l *** r = (l . proj1) &&& (r . proj2) where
-    (proj1, proj2) = proj (src l) (src r)
+  l *** r = (l . proj1 (src l) (src r)) &&& (r . proj2 (src l) (src r)) where
 
 
-type instance LimitFam Pair (~>) f = BinaryProduct (~>) (f :% P1) (f :% P2)
+type instance LimitFam Pair (~>) f = BinaryProduct (~>) (f :% Z) (f :% S Z)
 
 instance HasBinaryProducts (~>) => HasLimits Pair (~>) where
 
-  limitUniv (NatO f) = limitUniversal
-    (pairNat (Const prod) f (Com $ fst prj) (Com $ snd prj))
-    (\c -> c ! Fst &&& c ! Snd)
+  limitUniv (Nat f _ _) = limitUniversal
+    (pairNat (Const $ x *** y) f (Com $ proj1 x y) (Com $ proj2 x y))
+    (\c -> c ! Z &&& c ! S Z)
     where
-      x = f %% Fst
-      y = f %% Snd
-      prod = product x y
-      prj = proj x y
+      x = f % Z
+      y = f % S Z
 
 
 type instance BinaryProduct (->) x y = (x, y)
 
 instance HasBinaryProducts (->) where
   
-  product HaskO HaskO = HaskO
-  
-  proj _ _ = (fst, snd)
+  proj1 _ _ = fst
+  proj2 _ _ = snd
   
   (&&&) = (A.&&&)
   (***) = (A.***)
 
-type instance BinaryProduct Cat (CatW c1) (CatW c2) = CatW (c1 :*: c2)
+type instance BinaryProduct Cat (CatW c1) (CatW c2) = CatW (c1 :**: c2)
 
 instance HasBinaryProducts Cat where
   
-  product CatO CatO = CatO
-  
-  proj CatO CatO = (CatA Proj1, CatA Proj2)
+  proj1 (CatA _) (CatA _) = CatA Proj1
+  proj2 (CatA _) (CatA _) = CatA Proj2
   
   CatA f1 &&& CatA f2 = CatA ((f1 :***: f2) :.: DiagProd)
   CatA f1 *** CatA f2 = CatA (f1 :***: f2)
 
 
+type instance BinaryProduct (c1 :**: c2) (x1, x2) (y1, y2) = (BinaryProduct c1 x1 y1, BinaryProduct c2 x2 y2)
 
+instance (HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts (c1 :**: c2) where
+  
+  proj1 (x1 :**: x2) (y1 :**: y2) = proj1 x1 y1 :**: proj1 x2 y2
+  proj2 (x1 :**: x2) (y1 :**: y2) = proj2 x1 y1 :**: proj2 x2 y2
+  
+  (f1 :**: f2) &&& (g1 :**: g2) = (f1 &&& g1) :**: (f2 &&& g2)
+  (f1 :**: f2) *** (g1 :**: g2) = (f1 *** g1) :**: (f2 *** g2)
+
+
+-- | Binary product as a bifunctor.
+data ProductFunctor ((~>) :: * -> * -> *) = ProductFunctor
+type instance Dom (ProductFunctor (~>)) = (~>) :**: (~>)
+type instance Cod (ProductFunctor (~>)) = (~>)
+type instance ProductFunctor (~>) :% (a, b) = BinaryProduct (~>) a b
+instance HasBinaryProducts (~>) => Functor (ProductFunctor (~>)) where
+  ProductFunctor % (a1 :**: a2) = a1 *** a2
+
+-- | The product of two functors.
+data p :*: q where 
+  (:*:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ (~>), Cod q ~ (~>), HasBinaryProducts (~>)) => p -> q -> p :*: q
+type instance Dom (p :*: q) = Dom p
+type instance Cod (p :*: q) = Cod p
+type instance (p :*: q) :% a = BinaryProduct (Cod p) (p :% a) (q :% a)
+instance (Category (Dom p), Category (Cod p)) => Functor (p :*: q) where
+  (p :*: q) % f = (p % f) *** (q % f)
+
+type instance BinaryProduct (Nat c d) x y = x :*: y
+
+instance (Category c, HasBinaryProducts d) => HasBinaryProducts (Nat c d) where
+  
+  proj1 (Nat f _ _) (Nat g _ _) = Nat (f :*: g) f $ \z -> proj1 (f % z) (g % z)
+  proj2 (Nat f _ _) (Nat g _ _) = Nat (f :*: g) g $ \z -> proj2 (f % z) (g % z)
+  
+  Nat a f af &&& Nat _ g ag = Nat a (f :*: g) $ \z -> af z &&& ag z
+  Nat f1 f2 f *** Nat g1 g2 g = Nat (f1 :*: g1) (f2 :*: g2) $ \z -> f z *** g z
+  
+  
+
 type family BinaryCoproduct ((~>) :: * -> * -> *) x y :: *
 
 -- | The coproduct of 2 objects is the colimit of the functor from Pair to (~>).
 class Category (~>) => HasBinaryCoproducts (~>) where
 
-  coproduct :: Obj (~>) x -> Obj (~>) y -> Obj (~>) (BinaryCoproduct (~>) x y)
-  
-  inj :: Obj (~>) x -> Obj (~>) y -> (x ~> BinaryCoproduct (~>) x y, y ~> BinaryCoproduct (~>) x y)
+  inj1 :: Obj (~>) x -> Obj (~>) y -> x ~> BinaryCoproduct (~>) x y
+  inj2 :: Obj (~>) x -> Obj (~>) y -> y ~> BinaryCoproduct (~>) x y
 
   (|||) :: (x ~> a) -> (y ~> a) -> (BinaryCoproduct (~>) x y ~> a)
     
   (+++) :: (a1 ~> b1) -> (a2 ~> b2) -> (BinaryCoproduct (~>) a1 a2 ~> BinaryCoproduct (~>) b1 b2)
-  l +++ r = (inj1 . l) ||| (inj2 . r) where
-    (inj1, inj2) = inj (tgt l) (tgt r)
+  l +++ r = (inj1 (tgt l) (tgt r) . l) ||| (inj2 (tgt l) (tgt r) . r) where
     
 
-type instance ColimitFam Pair (~>) f = BinaryCoproduct (~>) (f :% P1) (f :% P2)
+type instance ColimitFam Pair (~>) f = BinaryCoproduct (~>) (f :% Z) (f :% S Z)
 
 instance HasBinaryCoproducts (~>) => HasColimits Pair (~>) where
   
-  colimitUniv (NatO f) = colimitUniversal
-    (pairNat f (Const cop) (Com $ fst i) (Com $ snd i))
-    (\c -> c ! Fst ||| c ! Snd)
+  colimitUniv (Nat f _ _) = colimitUniversal
+    (pairNat f (Const $ x +++ y) (Com $ inj1 x y) (Com $ inj2 x y))
+    (\c -> c ! Z ||| c ! S Z)
     where
-      x = f %% Fst
-      y = f %% Snd
-      cop = coproduct x y
-      i = inj x y
+      x = f % Z
+      y = f % S Z
 
 
 type instance BinaryCoproduct (->) x y = Either x y
 
 instance HasBinaryCoproducts (->) where
   
-  coproduct HaskO HaskO = HaskO
-  
-  inj _ _ = (Left, Right)
+  inj1 _ _ = Left
+  inj2 _ _ = Right
   
   (|||) = (A.|||)
   (+++) = (A.+++)
+  
+  
+type instance BinaryCoproduct (c1 :**: c2) (x1, x2) (y1, y2) = (BinaryCoproduct c1 x1 y1, BinaryCoproduct c2 x2 y2)
 
+instance (HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts (c1 :**: c2) where
+  
+  inj1 (x1 :**: x2) (y1 :**: y2) = inj1 x1 y1 :**: inj1 x2 y2
+  inj2 (x1 :**: x2) (y1 :**: y2) = inj2 x1 y1 :**: inj2 x2 y2
+  
+  (f1 :**: f2) ||| (g1 :**: g2) = (f1 ||| g1) :**: (f2 ||| g2)
+  (f1 :**: f2) +++ (g1 :**: g2) = (f1 +++ g1) :**: (f2 +++ g2)
 
 
+-- | Binary coproduct as a bifunctor.
+data CoproductFunctor ((~>) :: * -> * -> *) = CoproductFunctor
+type instance Dom (CoproductFunctor (~>)) = (~>) :**: (~>)
+type instance Cod (CoproductFunctor (~>)) = (~>)
+type instance CoproductFunctor (~>) :% (a, b) = BinaryCoproduct (~>) a b
+instance HasBinaryCoproducts (~>) => Functor (CoproductFunctor (~>)) where
+  CoproductFunctor % (a1 :**: a2) = a1 +++ a2
+
+-- | The coproduct of two functors.
+data p :+: q where 
+  (:+:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ (~>), Cod q ~ (~>), HasBinaryCoproducts (~>)) => p -> q -> p :+: q
+type instance Dom (p :+: q) = Dom p
+type instance Cod (p :+: q) = Cod p
+type instance (p :+: q) :% a = BinaryCoproduct (Cod p) (p :% a) (q :% a)
+instance (Category (Dom p), Category (Cod p)) => Functor (p :+: q) where
+  (p :+: q) % f = (p % f) +++ (q % f)
+
+type instance BinaryCoproduct (Nat c d) x y = x :+: y
+
+instance (Category c, HasBinaryCoproducts d) => HasBinaryCoproducts (Nat c d) where
+  
+  inj1 (Nat f _ _) (Nat g _ _) = Nat f (f :+: g) $ \z -> inj1 (f % z) (g % z)
+  inj2 (Nat f _ _) (Nat g _ _) = Nat g (f :+: g) $ \z -> inj2 (f % z) (g % z)
+  
+  Nat f a fa ||| Nat g _ ga = Nat (f :+: g) a $ \z -> fa z ||| ga z
+  Nat f1 f2 f +++ Nat g1 g2 g = Nat (f1 :+: g1) (f2 :+: g2) $ \z -> f z +++ g z
+
+
+
 newtype ForAll f = ForAll { unForAll :: forall a. f a }
 
 type instance LimitFam (->) (->) (EndoHask f) = ForAll f
 
 endoHaskLimit :: Prelude.Functor f => LimitUniversal (EndoHask f)
 endoHaskLimit = limitUniversal
-  (Nat (Const HaskO) EndoHask $ \HaskO -> unForAll)
-  (\c n -> ForAll ((c ! HaskO) n)) -- ForAll . (c ! Hask)
+  (Nat (Const id) EndoHask $ \_ -> unForAll)
+  (\c n -> ForAll ((c ! id) n)) -- ForAll . (c ! id)
 
 
 data Exists f = forall a. Exists (f a)
@@ -423,5 +489,5 @@
 
 endoHaskColimit :: Prelude.Functor f => ColimitUniversal (EndoHask f)
 endoHaskColimit = colimitUniversal
-  (Nat EndoHask (Const HaskO) $ \HaskO -> Exists)
-  (\c (Exists fa) -> (c ! HaskO) fa) -- (c ! HaskO) . unExists
+  (Nat EndoHask (Const id) $ \_ -> Exists)
+  (\c (Exists fa) -> (c ! id) fa) -- (c ! id) . unExists
diff --git a/Data/Category/Monoid.hs b/Data/Category/Monoid.hs
--- a/Data/Category/Monoid.hs
+++ b/Data/Category/Monoid.hs
@@ -13,23 +13,71 @@
 -----------------------------------------------------------------------------
 module Data.Category.Monoid where
 
-import Prelude hiding ((.), id)
+import Prelude hiding ((.), Functor)
 import Data.Monoid
 
 import Data.Category
-
+import Data.Category.Functor
+import Data.Category.NaturalTransformation
+import Data.Category.Adjunction (Adjunction, mkAdjunction, adjunctionMonad, adjunctionComonad, leftAdjunct, rightAdjunct)
+import Data.Category.Monoidal
 
 -- | The arrows are the values of the monoid.
 data MonoidA m a b where
   MonoidA :: Monoid m => m -> MonoidA m m m
 
+-- | A monoid as a category with one object.
 instance Monoid m => Category (MonoidA m) where
   
-  data Obj (MonoidA m) a where
-     MonoidO :: Obj (MonoidA m) m
-  
-  src (MonoidA _) = MonoidO
-  tgt (MonoidA _) = MonoidO
+  src (MonoidA _) = MonoidA mempty
+  tgt (MonoidA _) = MonoidA mempty
   
-  id MonoidO            = MonoidA mempty
   MonoidA a . MonoidA b = MonoidA $ a `mappend` b
+
+
+data Mon :: * -> * -> * where
+  MonoidMorphism :: (Monoid m1, Monoid m2) => (m1 -> m2) -> Mon m1 m2
+
+unMonoidMorphism :: (Monoid m1, Monoid m2) => Mon m1 m2 -> m1 -> m2
+unMonoidMorphism (MonoidMorphism f) = f
+
+-- | The category of all monoids, with monoid morphisms as arrows.
+instance Category Mon where
+  
+  src (MonoidMorphism _) = MonoidMorphism id
+  tgt (MonoidMorphism _) = MonoidMorphism id
+  
+  MonoidMorphism f . MonoidMorphism g = MonoidMorphism $ f . g
+
+
+data ForgetMonoid = ForgetMonoid
+type instance Dom ForgetMonoid = Mon
+type instance Cod ForgetMonoid = (->)
+type instance ForgetMonoid :% a = a
+instance Functor ForgetMonoid where
+  ForgetMonoid % MonoidMorphism f = f
+  
+data FreeMonoid = FreeMonoid
+type instance Dom FreeMonoid = (->)
+type instance Cod FreeMonoid = Mon
+type instance FreeMonoid :% a = [a]
+instance Functor FreeMonoid where
+  FreeMonoid % f = MonoidMorphism $ map f
+
+freeMonoidAdj :: Adjunction Mon (->) FreeMonoid ForgetMonoid
+freeMonoidAdj = mkAdjunction FreeMonoid ForgetMonoid (\_ -> (:[])) (\(MonoidMorphism _) -> MonoidMorphism mconcat)
+
+foldMap :: Monoid m => (a -> m) -> [a] -> m
+foldMap = unMonoidMorphism . rightAdjunct freeMonoidAdj (MonoidMorphism id)
+
+listMonadReturn :: a -> [a]
+listMonadReturn = unit (adjunctionMonad freeMonoidAdj) ! id
+
+listMonadJoin :: [[a]] -> [a]
+listMonadJoin = multiply (adjunctionMonad freeMonoidAdj) ! id
+
+listComonadExtract :: Monoid m => [m] -> m
+listComonadExtract = let MonoidMorphism f = counit (adjunctionComonad freeMonoidAdj) ! MonoidMorphism id in f
+
+listComonadDuplicate :: Monoid m => [m] -> [[m]]
+listComonadDuplicate = let MonoidMorphism f = comultiply (adjunctionComonad freeMonoidAdj) ! MonoidMorphism id in f
diff --git a/Data/Category/Monoidal.hs b/Data/Category/Monoidal.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/Monoidal.hs
@@ -0,0 +1,133 @@
+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, Rank2Types, ScopedTypeVariables #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Category.Monoidal
+-- Copyright   :  (c) Sjoerd Visscher 2010
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  sjoerd@w3future.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+-----------------------------------------------------------------------------
+module Data.Category.Monoidal where
+
+import Prelude (($))
+import qualified Control.Monad as M
+
+import Data.Category
+import Data.Category.Functor
+import Data.Category.NaturalTransformation
+import Data.Category.Limit
+
+
+class Functor f => HasUnit f where
+  
+  type Unit f :: *
+  unitObject :: Obj (Cod f) (Unit f)
+
+
+instance (HasTerminalObject (~>), HasBinaryProducts (~>)) => HasUnit (ProductFunctor (~>)) where
+  
+  type Unit (ProductFunctor (~>)) = TerminalObject (~>)
+  unitObject = terminalObject
+
+instance (HasInitialObject (~>), HasBinaryCoproducts (~>)) => HasUnit (CoproductFunctor (~>)) where
+  
+  type Unit (CoproductFunctor (~>)) = InitialObject (~>)
+  unitObject = initialObject
+
+instance Category (~>) => HasUnit (FunctorCompose (~>)) where
+  
+  type Unit (FunctorCompose (~>)) = Id (~>)
+  unitObject = natId Id
+  
+
+
+class HasUnit f => TensorProduct f where
+  
+  leftUnitor     :: Cod f ~ (~>) => f -> Obj (Cod f) a -> (f :% (Unit f, a)) ~> a
+  leftUnitorInv  :: Cod f ~ (~>) => f -> Obj (Cod f) a -> a ~> (f :% (Unit f, a))
+  rightUnitor    :: Cod f ~ (~>) => f -> Obj (Cod f) a -> (f :% (a, Unit f)) ~> a
+  rightUnitorInv :: Cod f ~ (~>) => f -> Obj (Cod f) a -> a ~> (f :% (a, Unit f))
+  
+  associator     :: Cod f ~ (~>) => f -> Obj (Cod f) a -> Obj (Cod f) b -> Obj (Cod f) c -> (f :% (f :% (a, b), c)) ~> (f :% (a, f :% (b, c)))
+  associatorInv  :: Cod f ~ (~>) => f -> Obj (Cod f) a -> Obj (Cod f) b -> Obj (Cod f) c -> (f :% (a, f :% (b, c))) ~> (f :% (f :% (a, b), c))
+
+
+instance (HasTerminalObject (~>), HasBinaryProducts (~>)) => TensorProduct (ProductFunctor (~>)) where
+  
+  leftUnitor     _ a = proj2 terminalObject a
+  leftUnitorInv  _ a = terminate a &&& a
+  rightUnitor    _ a = proj1 a terminalObject
+  rightUnitorInv _ a = a &&& terminate a
+
+  associator    _ a b c = (proj1 a b . proj1 (a *** b) c) &&& (proj2 a b *** c)
+  associatorInv _ a b c = (a *** proj1 b c) &&& (proj2 b c . proj2 a (b *** c))
+
+instance (HasInitialObject (~>), HasBinaryCoproducts (~>)) => TensorProduct (CoproductFunctor (~>)) where
+  
+  leftUnitor     _ a = initialize a ||| a
+  leftUnitorInv  _ a = inj2 initialObject a
+  rightUnitor    _ a = a ||| initialize a
+  rightUnitorInv _ a = inj1 a initialObject
+  
+  associator    _ a b c = (a +++ inj1 b c) ||| (inj2 a (b +++ c) . inj2 b c)
+  associatorInv _ a b c = (inj1 (a +++ b) c . inj1 a b) ||| (inj2 a b +++ c)
+  
+instance Category (~>) => TensorProduct (FunctorCompose (~>)) where
+  
+  leftUnitor     _ (Nat g _ _) = Nat (Id :.: g) g $ \i -> g % i
+  leftUnitorInv  _ (Nat g _ _) = Nat g (Id :.: g) $ \i -> g % i
+  rightUnitor    _ (Nat g _ _) = Nat (g :.: Id) g $ \i -> g % i
+  rightUnitorInv _ (Nat g _ _) = Nat g (g :.: Id) $ \i -> g % i
+
+  associator    _ (Nat f _ _) (Nat g _ _) (Nat h _ _) = Nat ((f :.: g) :.: h) (f :.: (g :.: h)) $ \i -> f % g % h % i
+  associatorInv _ (Nat f _ _) (Nat g _ _) (Nat h _ _) = Nat (f :.: (g :.: h)) ((f :.: g) :.: h) $ \i -> f % g % h % i
+
+
+
+data MonoidObject f a = MonoidObject
+  { unit     :: (Cod f ~ (~>)) => Unit f        ~> a
+  , multiply :: (Cod f ~ (~>)) => (f :% (a, a)) ~> a
+  }
+  
+data ComonoidObject f a = ComonoidObject
+  { counit     :: (Cod f ~ (~>)) => a ~> Unit f
+  , comultiply :: (Cod f ~ (~>)) => a ~> (f :% (a, a))
+  }
+
+
+type Monad f = MonoidObject (FunctorCompose (Dom f)) f
+
+mkMonad :: (Functor f, Dom f ~ (~>), Cod f ~ (~>), Category (~>)) 
+  => f 
+  -> (forall a. Obj (~>) a -> Component (Id (~>)) f a) 
+  -> (forall a. Obj (~>) a -> Component (f :.: f) f a)
+  -> Monad f
+mkMonad f ret join = MonoidObject
+  { unit     = Nat Id        f ret
+  , multiply = Nat (f :.: f) f join
+  }
+
+preludeMonad :: (M.Functor f, M.Monad f) => Monad (EndoHask f)
+preludeMonad = mkMonad EndoHask (\_ -> M.return) (\_ -> M.join)
+
+monadFunctor :: forall f. Monad f -> f
+monadFunctor m = f
+  where
+    u :: Nat (Dom f) (Dom f) (Id (Dom f)) f
+    u@(Nat _ f _) = unit m
+
+
+type Comonad f = ComonoidObject (FunctorCompose (Dom f)) f
+
+mkComonad :: (Functor f, Dom f ~ (~>), Cod f ~ (~>), Category (~>)) 
+  => f 
+  -> (forall a. Obj (~>) a -> Component f (Id (~>)) a) 
+  -> (forall a. Obj (~>) a -> Component f (f :.: f) a)
+  -> Comonad f
+mkComonad f extr dupl = ComonoidObject
+  { counit     = Nat f Id        extr
+  , comultiply = Nat f (f :.: f) dupl
+  }
+
diff --git a/Data/Category/NaturalTransformation.hs b/Data/Category/NaturalTransformation.hs
--- a/Data/Category/NaturalTransformation.hs
+++ b/Data/Category/NaturalTransformation.hs
@@ -13,17 +13,27 @@
 
   -- * Natural transformations
     (:~>)
-  , Nat(..)
-  , Obj(..)
   , Component
   , Com(..)
-  , o
   , (!)
-  
+  , o
+  , natId
+
+  -- * Functor category
+  , Nat(..)
+  , Endo
+    
   -- * Related functors
+  , FunctorCompose(..)
   , Precompose(..)
   , Postcompose(..)
+  , Wrap(..)
+  
+  -- ** Yoneda
   , YonedaEmbedding(..)
+  , Yoneda(..)
+  , fromYoneda
+  , toYoneda
   
 ) where
   
@@ -31,6 +41,7 @@
 
 import Data.Category
 import Data.Category.Functor
+import Data.Category.Product
 
 infixl 9 !
 
@@ -43,69 +54,94 @@
   Nat :: (Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) 
     => f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
 
+
 -- | A component for an object @z@ is an arrow from @F z@ to @G z@.
 type Component f g z = Cod f (f :% z) (g :% z)
 
+-- | A newtype wrapper for components,
+--   which can be useful for helper functions dealing with components.
+newtype Com f g z = Com { unCom :: Component f g z }
 
+-- | 'n ! a' returns the component for the object @a@ of a natural transformation @n@.
+--   This can be generalized to any arrow (instead of just identity arrows).
+(!) :: (Category c, Category d) => Nat c d f g -> c a b -> d (f :% a) (g :% b)
+Nat f _ n ! h = n (tgt h) . f % h -- or g % h . n (src h), or n h when h is an identity arrow
+
+
+-- | Horizontal composition of natural transformations.
+o :: (Category c, Category d, Category e) => Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
+njk@(Nat j k _) `o` nfg@(Nat f g _) = Nat (j :.: f) (k :.: g) $ (njk !) . (nfg !)
+-- Nat j k njk `o` Nat f g nfg = Nat (j :.: f) (k :.: g) $ \x -> njk (g % x) . j % nfg x -- or k % nfg x . njk (f % x)
+
+-- | The identity natural transformation of a functor.
+natId :: Functor f => f -> Nat (Dom f) (Cod f) f f
+natId f = Nat f f $ \i -> f % i
+
+
 -- | Functor category D^C.
 -- Objects of D^C are functors from C to D.
 -- Arrows of D^C are natural transformations.
 instance (Category c, Category d) => Category (Nat c d) where
   
-  data Obj (Nat c d) a where
-    NatO :: (Functor f, Dom f ~ c, Cod f ~ d) => f -> Obj (Nat c d) f
-    
-  src (Nat f _ _) = NatO f
-  tgt (Nat _ g _) = NatO g
+  src (Nat f _ _)           = natId f
+  tgt (Nat _ g _)           = natId g
   
-  id (NatO f)               = Nat f f $ \i -> id $ f %% i
   Nat _ h ngh . Nat f _ nfg = Nat f h $ \i -> ngh i . nfg i
 
 
--- | Horizontal composition of natural transformations.
-o :: Category e => Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
-Nat j k njk `o` Nat f g nfg = Nat (j :.: f) (k :.: g) $ \x -> k % nfg x . njk (f %% x)
+-- | The category of endofunctors.
+type Endo (~>) = Nat (~>) (~>)
 
 
--- | A newtype wrapper for components,
---   which can be useful for helper functions dealing with components.
-newtype Com f g z = Com { unCom :: Component f g z }
-
+-- | Composition of endofunctors is a functor.
+data FunctorCompose ((~>) :: * -> * -> *) = FunctorCompose
 
+type instance Dom (FunctorCompose (~>)) = Endo (~>) :**: Endo (~>)
+type instance Cod (FunctorCompose (~>)) = Endo (~>)
+type instance FunctorCompose (~>) :% (f, g) = f :.: g
 
--- | 'n ! a' returns the component for the object @a@ of a natural transformation @n@.
-(!) :: (Cod f ~ d, Cod g ~ d) => Nat (~>) d f g -> Obj (~>) a -> d (f :% a) (g :% a)
-Nat _ _ n ! x = n x
+instance Category (~>) => Functor (FunctorCompose (~>)) where
+  FunctorCompose % (n1 :**: n2) = n1 `o` n2
 
 
 -- | @Precompose f d@ is the functor such that @Precompose f d :% g = g :.: f@, 
 --   for functors @g@ that compose with @f@ and with codomain @d@.
 data Precompose :: * -> (* -> * -> *) -> * where
-  Precompose :: (Functor f, Category d) => f -> Precompose f d
+  Precompose :: f -> Precompose f d
 
 type instance Dom (Precompose f d) = Nat (Cod f) d
 type instance Cod (Precompose f d) = Nat (Dom f) d
 type instance Precompose f d :% g = g :.: f
 
-instance Functor (Precompose f d) where
-  Precompose f %% NatO g = NatO $ g :.: f
-  Precompose f % (Nat g h n) = Nat (g :.: f) (h :.: f) $ n . (f %%)
+instance (Functor f, Category d) => Functor (Precompose f d) where
+  Precompose f % (Nat g h n) = Nat (g :.: f) (h :.: f) $ n . (f %)
 
 
 -- | @Postcompose f c@ is the functor such that @Postcompose f c :% g = f :.: g@, 
 --   for functors @g@ that compose with @f@ and with domain @c@.
 data Postcompose :: * -> (* -> * -> *) -> * where
-  Postcompose :: (Functor f, Category c) => f -> Postcompose f c
+  Postcompose :: f -> Postcompose f c
 
 type instance Dom (Postcompose f c) = Nat c (Dom f)
 type instance Cod (Postcompose f c) = Nat c (Cod f)
 type instance Postcompose f c :% g = f :.: g
 
-instance Functor (Postcompose f c) where
-  Postcompose f %% NatO g = NatO $ f :.: g
+instance (Functor f, Category c) => Functor (Postcompose f c) where
   Postcompose f % (Nat g h n) = Nat (f :.: g) (f :.: h) $ (f %) . n
 
 
+-- | @Wrap f h@ is the functor such that @Wrap f h :% g = f :.: g :.: h@, 
+--   for functors @g@ that compose with @f@ and @h@.
+data Wrap f h = Wrap f h
+
+type instance Dom (Wrap f h) = Nat (Cod h) (Dom f)
+type instance Cod (Wrap f h) = Nat (Dom h) (Cod f)
+type instance Wrap f h :% g = f :.: g :.: h
+
+instance (Functor f, Functor h) => Functor (Wrap f h) where
+  Wrap f h % (Nat g1 g2 n) = Nat (f :.: g1 :.: h) (f :.: g2 :.: h) $ (f %) . n . (h %)
+
+
 -- | A functor F: Op(C) -> Set is representable if it is naturally isomorphic to the contravariant hom-functor.
 class Functor f => Representable f where
   type RepresentingObject f :: *
@@ -114,18 +150,38 @@
 
 instance Category (~>) => Representable ((~>) :-*: x) where
   type RepresentingObject ((~>) :-*: x) = x
-  represent   f = id $ NatO f
-  unrepresent f = id $ NatO f
+  represent   f = natId f
+  unrepresent f = natId f
 
 
 -- | The Yoneda embedding functor.
 data YonedaEmbedding :: (* -> * -> *) -> * where
   YonedaEmbedding :: Category (~>) => YonedaEmbedding (~>)
   
-type instance Dom (YonedaEmbedding (~>)) = (~>)
-type instance Cod (YonedaEmbedding (~>)) = Nat (Op (~>)) (->)
-type instance YonedaEmbedding (~>) :% a = (~>) :-*: a
+type instance Dom (YonedaEmbedding (~>)) = Op (~>)
+type instance Cod (YonedaEmbedding (~>)) = Nat (~>) (->)
+type instance YonedaEmbedding (~>) :% a = a :*-: (~>)
 
-instance Functor (YonedaEmbedding (~>)) where
-  YonedaEmbedding %% x = NatO $ Hom_X x
-  YonedaEmbedding % f = Nat (Hom_X $ src f) (Hom_X $ tgt f) $ \_ -> (f .)
+instance Category (~>) => Functor (YonedaEmbedding (~>)) where
+  YonedaEmbedding % (Op f) = Nat (HomX_ $ tgt f) (HomX_ $ src f) $ \_ -> (. f)
+
+
+data Yoneda f = Yoneda
+type instance Dom (Yoneda f) = Dom f
+type instance Cod (Yoneda f) = (->)
+type instance Yoneda f :% a = Nat (Dom f) (->) (a :*-: Dom f) f
+instance Functor f => Functor (Yoneda f) where
+  Yoneda % g = h g
+    where
+      h :: Dom f a b -> Yoneda f :% a -> Yoneda f :% b
+      h ab (Nat _ f n) = Nat (HomX_ $ tgt ab) f $ \z bz -> n z (bz . ab)
+      
+  
+fromYoneda :: (Functor f, Cod f ~ (->)) => f -> Nat (Dom f) (->) (Yoneda f) f
+fromYoneda f = Nat Yoneda f $ \a n -> (n ! a) a
+
+toYoneda :: (Functor f, Cod f ~ (->)) => f -> Nat (Dom f) (->) f (Yoneda f)
+toYoneda f = Nat f Yoneda $ \a fa -> Nat (HomX_ a) f $ \_ h -> (f % h) fa
+
+-- Contravariant Yoneda:
+-- type instance Yoneda f :% a = Nat (Op (Dom f)) (->) (Dom f :-*: a) f
diff --git a/Data/Category/Omega.hs b/Data/Category/Omega.hs
--- a/Data/Category/Omega.hs
+++ b/Data/Category/Omega.hs
@@ -25,43 +25,38 @@
 
 -- | The arrows of omega, there's an arrow from a to b iff a <= b.
 data Omega :: * -> * -> * where
-  IdZ :: Omega Z Z
-  GTZ :: Omega Z n -> Omega Z (S n)
-  StS :: Omega a b -> Omega (S a) (S b)
+  Z   :: Omega Z Z
+  Z2S :: Omega Z n -> Omega Z (S n)
+  S   :: Omega a b -> Omega (S a) (S b)
   
 instance Category Omega where
   
-  data Obj Omega a where
-    OZ :: Obj Omega Z
-    OS :: Obj Omega n -> Obj Omega (S n)
-  
-  src IdZ     = OZ
-  src (GTZ _) = OZ
-  src (StS a) = OS (src a)
-  
-  tgt IdZ     = OZ
-  tgt (GTZ a) = OS (tgt a)
-  tgt (StS a) = OS (tgt a)
+  src Z       = Z
+  src (Z2S _) = Z
+  src (S   a) = S (src a)
   
-  id OZ             = IdZ
-  id (OS n)         = StS (id n)
+  tgt Z       = Z
+  tgt (Z2S a) = S (tgt a)
+  tgt (S   a) = S (tgt a)
   
-  a       . IdZ     = a
-  (StS a) . (GTZ n) = GTZ (a . n)
-  (StS a) . (StS b) = StS (a . b)
-  _       . _       = error "Other combinations should not type check"
+  a     . Z       = a
+  (S a) . (Z2S n) = Z2S (a . n)
+  (S a) . (S   b) = S   (a . b)
+  _       . _     = error "Other combinations should not type check"
 
 
 instance HasInitialObject Omega where
   
   type InitialObject Omega = Z
   
-  initialObject     = OZ
+  initialObject    = Z
   
-  initialize OZ     = IdZ
-  initialize (OS n) = GTZ $ initialize n
+  initialize Z     = Z
+  initialize (S n) = Z2S $ initialize n
+  initialize _     = error "Other combinations should not type check"
 
 
+
 type instance BinaryProduct Omega Z     n = Z
 type instance BinaryProduct Omega n     Z = Z
 type instance BinaryProduct Omega (S a) (S b) = S (BinaryProduct Omega a b)
@@ -69,19 +64,22 @@
 -- The product in omega is the minimum.
 instance HasBinaryProducts Omega where 
 
-  product OZ     _      = OZ
-  product _      OZ     = OZ
-  product (OS a) (OS b) = OS (product a b)
-  
-  proj OZ     OZ     = (IdZ, IdZ)
-  proj OZ     (OS n) = (IdZ, GTZ . snd $ proj OZ n)
-  proj (OS n) OZ     = (GTZ . fst $ proj n OZ, IdZ)
-  proj (OS a) (OS b) = (StS proj1, StS proj2) where (proj1, proj2) = proj a b
+  proj1 Z     Z     = Z
+  proj1 Z     (S _) = Z
+  proj1 (S n) Z     = Z2S $ proj1 n Z
+  proj1 (S a) (S b) = S $ proj1 a b
+  proj1 _     _     = error "Other combinations should not type check"
+
+  proj2 Z     Z     = Z
+  proj2 Z     (S n) = Z2S $ proj2 Z n
+  proj2 (S _) Z     = Z
+  proj2 (S a) (S b) = S $ proj2 a b
+  proj2 _     _     = error "Other combinations should not type check"
   
-  IdZ   &&& _     = IdZ
-  _     &&& IdZ   = IdZ
-  GTZ a &&& GTZ b = GTZ (a &&& b)
-  StS a &&& StS b = StS (a &&& b)
+  Z   &&& _     = Z
+  _     &&& Z   = Z
+  Z2S a &&& Z2S b = Z2S (a &&& b)
+  S a &&& S b = S (a &&& b)
   _     &&& _      = error "Other combinations should not type check"
 
 
@@ -92,22 +90,19 @@
 -- -- The coproduct in omega is the maximum.
 instance HasBinaryCoproducts Omega where 
   
-  coproduct OZ     n      = n
-  coproduct n      OZ     = n
-  coproduct (OS a) (OS b) = OS (coproduct a b)
-  
-  inj OZ OZ = (IdZ, IdZ)
-  inj OZ (OS n) = (GTZ inj1, StS inj2) where (inj1, inj2) = inj OZ n
-  inj (OS n) OZ = (StS inj1, GTZ inj2) where (inj1, inj2) = inj n OZ
-  inj (OS a) (OS b) = (StS inj1, StS inj2) where (inj1, inj2) = inj a b
+  inj1 Z     Z     = Z
+  inj1 Z     (S n) = Z2S $ inj1 Z n
+  inj1 (S n) Z     = S $ inj1 n Z
+  inj1 (S a) (S b) = S $ inj1 a b
+  inj1 _     _     = error "Other combinations should not type check"
+  inj2 Z     Z     = Z
+  inj2 Z     (S n) = S $ inj2 Z n
+  inj2 (S n) Z     = Z2S $ inj2 n Z
+  inj2 (S a) (S b) = S $ inj2 a b
+  inj2 _     _     = error "Other combinations should not type check"
   
-  IdZ   ||| IdZ   = IdZ
-  GTZ _ ||| a     = a
-  a     ||| GTZ _ = a
-  StS a ||| StS b = StS (a ||| b)
+  Z   ||| Z   = Z
+  Z2S _ ||| a     = a
+  a     ||| Z2S _ = a
+  S a ||| S b = S (a ||| b)
   _     ||| _      = error "Other combinations should not type check"
-  
-  
-instance Show (Obj Omega a) where
-  show OZ = "OZ"
-  show (OS n) = "OS " ++ show n
diff --git a/Data/Category/Pair.hs b/Data/Category/Pair.hs
deleted file mode 100644
--- a/Data/Category/Pair.hs
+++ /dev/null
@@ -1,76 +0,0 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, EmptyDataDecls #-}
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Category.Pair
--- Copyright   :  (c) Sjoerd Visscher 2010
--- License     :  BSD-style (see the file LICENSE)
---
--- Maintainer  :  sjoerd@w3future.com
--- Stability   :  experimental
--- Portability :  non-portable
---
--- Pair, the category with just 2 objects and their identity arrows.
--- The limit and colimit of the functor from Pair to some category provide 
--- products and coproducts in that category.
------------------------------------------------------------------------------
-module Data.Category.Pair where
-
-import Prelude (($), undefined)
-
-import Data.Category
-import Data.Category.Functor
-import Data.Category.NaturalTransformation
-
-
-data P1
-data P2
-
--- | The arrows of Pair.
-data Pair :: * -> * -> * where
-  IdFst :: Pair P1 P1
-  IdSnd :: Pair P2 P2
-
-instance Category Pair where
-  
-  data Obj Pair a where
-    Fst :: Obj Pair P1
-    Snd :: Obj Pair P2
-  
-  src IdFst = Fst
-  src IdSnd = Snd
-  
-  tgt IdFst = Fst
-  tgt IdSnd = Snd
-  
-  id  Fst       = IdFst
-  id  Snd       = IdSnd
-  
-  IdFst . IdFst = IdFst
-  IdSnd . IdSnd = IdSnd
-  _     . _     = undefined -- this can't happen
-
-
--- | The functor from Pair to (~>), a diagram of 2 objects in (~>).
-data PairDiagram :: (* -> * -> *) -> * -> * -> * where
-  PairDiagram :: Category (~>) => Obj (~>) x -> Obj (~>) y -> PairDiagram (~>) x y
-type instance Dom (PairDiagram (~>) x y) = Pair
-type instance Cod (PairDiagram (~>) x y) = (~>)
-type instance PairDiagram (~>) x y :% P1 = x
-type instance PairDiagram (~>) x y :% P2 = y
-instance Functor (PairDiagram (~>) x y) where
-  PairDiagram x _ %% Fst = x
-  PairDiagram _ y %% Snd = y
-  PairDiagram x _ % IdFst = id x
-  PairDiagram _ y % IdSnd = id y
-
-
-pairNat :: (Functor f, Functor g, Dom f ~ Pair, Cod f ~ d, Dom g ~ Pair, Cod g ~ d) 
-  => f -> g -> Com f g P1 -> Com f g P2 -> Nat Pair d f g
-pairNat f g c1 c2 = Nat f g (\x -> unCom $ n c1 c2 x) where
-  n :: (Functor f, Functor g, Dom f ~ Pair, Cod f ~ d, Dom g ~ Pair, Cod g ~ d) 
-    => Com f g P1 -> Com f g P2 -> Obj Pair a -> Com f g a
-  n c _ Fst = c
-  n _ c Snd = c
-
-arrowPair :: Category (~>) => (x1 ~> x2) -> (y1 ~> y2) -> Nat Pair (~>) (PairDiagram (~>) x1 y1) (PairDiagram (~>) x2 y2)
-arrowPair l r = pairNat (PairDiagram (src l) (src r)) (PairDiagram (tgt l) (tgt r)) (Com l) (Com r)
diff --git a/Data/Category/Peano.hs b/Data/Category/Peano.hs
--- a/Data/Category/Peano.hs
+++ b/Data/Category/Peano.hs
@@ -20,33 +20,40 @@
 import Data.Category.Limit
 
 
+data PeanoO (~>) a where
+  PeanoO :: (TerminalObject (~>) ~> x) -> (x ~> x) -> PeanoO (~>) x
+    
 data Peano :: (* -> * -> *) -> * -> * -> * where
-  PeanoA :: Obj (Peano (~>)) a -> Obj (Peano (~>)) b -> (a ~> b) -> Peano (~>) a b
+  PeanoA :: PeanoO (~>) a -> PeanoO (~>) b -> (a ~> b) -> Peano (~>) a b
 
-instance Category (~>) => Category (Peano (~>)) where
+peanoId :: Category (~>) => PeanoO (~>) a -> Obj (Peano (~>)) a
+peanoId o@(PeanoO z _) = PeanoA o o $ tgt z
+
+peanoO :: Category (~>) => Obj (Peano (~>)) a -> PeanoO (~>) a
+peanoO (PeanoA o _ _) = o
+
+instance HasTerminalObject (~>) => Category (Peano (~>)) where
   
-  data Obj (Peano (~>)) a where
-    PeanoO :: Obj (~>) x -> x -> (x ~> x) -> Obj (Peano (~>)) x
-    
-  src (PeanoA s _ _) = s
-  tgt (PeanoA _ t _) = t
+  src (PeanoA s _ _) = peanoId s
+  tgt (PeanoA _ t _) = peanoId t
   
-  id p@(PeanoO x _ _)             = PeanoA p p $ id x
   (PeanoA _ t f) . (PeanoA s _ g) = PeanoA s t $ f . g
   
   
 -- | The natural numbers are the initial object for the 'Peano' category.
-data NatNum = Z | S NatNum
+data NatNum = Z () | S NatNum
 
 -- | Primitive recursion is the factorizer from the natural numbers.
-primRec :: t -> (t -> t) -> NatNum -> t
-primRec z _ Z     = z
-primRec z s (S n) = s (primRec z s n)
+primRec :: (() -> t) -> (t -> t) -> NatNum -> t
+primRec z _ (Z ()) = z ()
+primRec z s (S  n) = s (primRec z s n)
   
 instance HasInitialObject (Peano (->)) where
   
   type InitialObject (Peano (->)) = NatNum
   
-  initialObject = PeanoO HaskO Z S
+  initialObject = peanoId $ PeanoO Z S
   
-  initialize o@(PeanoO HaskO z s) = PeanoA initialObject o $ primRec z s
+  initialize a = PeanoA (peanoO initialObject) o $ primRec z s
+    where
+      o@(PeanoO z s) = peanoO a
diff --git a/Data/Category/Product.hs b/Data/Category/Product.hs
--- a/Data/Category/Product.hs
+++ b/Data/Category/Product.hs
@@ -11,25 +11,20 @@
 -----------------------------------------------------------------------------
 module Data.Category.Product where
 
-import Prelude hiding ((.), id, Functor)
+import Prelude ()
 
 import Data.Category
 import Data.Category.Functor
 
 
-data (:*:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where
-  (:**:) :: c1 a1 b1 -> c2 a2 b2 -> (:*:) c1 c2 (a1, a2) (b1, b2)
+data (:**:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where
+  (:**:) :: c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
 
 -- | The product category of category @c1@ and @c2@.
-instance (Category c1, Category c2) => Category (c1 :*: c2) where
-  
-  data Obj (c1 :*: c2) a where
-    ProdO :: Obj c1 a1 -> Obj c2 a2 -> Obj (c1 :*: c2) (a1, a2)
-    
-  src (a1 :**: a2)            = ProdO (src a1) (src a2)
-  tgt (a1 :**: a2)            = ProdO (tgt a1) (tgt a2)
+instance (Category c1, Category c2) => Category (c1 :**: c2) where
   
-  id (ProdO x1 x2)            = id x1 :**: id x2
+  src (a1 :**: a2)            = src a1 :**: src a2
+  tgt (a1 :**: a2)            = tgt a1 :**: tgt a2
   
   (a1 :**: a2) . (b1 :**: b2) = (a1 . b1) :**: (a2 . b2)
 
@@ -38,44 +33,44 @@
   
     
 data Proj1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Proj1
-type instance Dom (Proj1 c1 c2) = c1 :*: c2
+type instance Dom (Proj1 c1 c2) = c1 :**: c2
 type instance Cod (Proj1 c1 c2) = c1
 type instance Proj1 c1 c2 :% (a1, a2) = a1
-instance Functor (Proj1 c1 c2) where 
-  Proj1 %% ProdO x1 _ = x1
+instance (Category c1, Category c2) => Functor (Proj1 c1 c2) where 
   Proj1 % (f1 :**: _) = f1
 
 data Proj2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Proj2
-type instance Dom (Proj2 c1 c2) = c1 :*: c2
+type instance Dom (Proj2 c1 c2) = c1 :**: c2
 type instance Cod (Proj2 c1 c2) = c2
 type instance Proj2 c1 c2 :% (a1, a2) = a2
-instance Functor (Proj2 c1 c2) where 
-  Proj2 %% ProdO _ x2 = x2
+instance (Category c1, Category c2) => Functor (Proj2 c1 c2) where 
   Proj2 % (_ :**: f2) = f2
 
-data f1 :***: f2 where 
-  (:***:) :: (Functor f1, Functor f2, Category (Cod f1), Category (Cod f2)) => f1 -> f2 -> f1 :***: f2
-type instance Dom (f1 :***: f2) = Dom f1 :*: Dom f2
-type instance Cod (f1 :***: f2) = Cod f1 :*: Cod f2
+data f1 :***: f2 = f1 :***: f2
+type instance Dom (f1 :***: f2) = Dom f1 :**: Dom f2
+type instance Cod (f1 :***: f2) = Cod f1 :**: Cod f2
 type instance (f1 :***: f2) :% (a1, a2) = (f1 :% a1, f2 :% a2)
-instance Functor (f1 :***: f2) where 
-  (g1 :***: g2) %% ProdO x1 x2 = ProdO (g1 %% x1) (g2 %% x2)
+instance (Functor f1, Functor f2) => Functor (f1 :***: f2) where 
   (g1 :***: g2) % (f1 :**: f2) = (g1 % f1) :**: (g2 % f2)
   
-data Hom (~>) where
-  Hom :: Category (~>) => Hom (~>)
-type instance Dom (Hom (~>)) = Op (~>) :*: (~>)
-type instance Cod (Hom (~>)) = (->)
-type instance Hom (~>) :% (a, b) = a ~> b
-instance Functor (Hom (~>)) where 
-  (%%) = undefined
-  Hom % (Op g1 :**: g2) = \f -> g2 . f . g1
-  
-data DiagProd :: (* -> * -> *) -> * where 
-  DiagProd :: Category (~>) => DiagProd (~>)
+data DiagProd ((~>) :: * -> * -> *) = DiagProd
 type instance Dom (DiagProd (~>)) = (~>)
-type instance Cod (DiagProd (~>)) = (~>) :*: (~>)
+type instance Cod (DiagProd (~>)) = (~>) :**: (~>)
 type instance DiagProd (~>) :% a = (a, a)
-instance Functor (DiagProd (~>)) where 
-  DiagProd %% x = ProdO x x
+instance Category (~>) => Functor (DiagProd (~>)) where 
   DiagProd % f = f :**: f
+
+data Tuple1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Tuple1 (Obj c1 a)
+type instance Dom (Tuple1 c1 c2 a1) = c2
+type instance Cod (Tuple1 c1 c2 a1) = c1 :**: c2
+type instance Tuple1 c1 c2 a1 :% a2 = (a1, a2)
+instance (Category c1, Category c2) => Functor (Tuple1 c1 c2 a1) where
+  Tuple1 a % f = a :**: f
+
+data Tuple2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Tuple2 (Obj c2 a)
+type instance Dom (Tuple2 c1 c2 a2) = c1
+type instance Cod (Tuple2 c1 c2 a2) = c1 :**: c2
+type instance Tuple2 c1 c2 a2 :% a1 = (a1, a2)
+instance (Category c1, Category c2) => Functor (Tuple2 c1 c2 a2) where
+  Tuple2 a % f = f :**: a
+
diff --git a/Data/Category/Unit.hs b/Data/Category/Unit.hs
deleted file mode 100644
--- a/Data/Category/Unit.hs
+++ /dev/null
@@ -1,33 +0,0 @@
-{-# LANGUAGE TypeFamilies, GADTs, EmptyDataDecls #-}
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Category.Unit
--- Copyright   :  (c) Sjoerd Visscher 2010
--- License     :  BSD-style (see the file LICENSE)
---
--- Maintainer  :  sjoerd@w3future.com
--- Stability   :  experimental
--- Portability :  non-portable
---
--- /1/, The singleton category with just one object with only its identity arrow.
------------------------------------------------------------------------------
-module Data.Category.Unit where
-
-import Data.Category
-
-data UnitO
-
--- | The arrows of Unit.
-data Unit a b where
-  UnitId :: Unit UnitO UnitO
-
-instance Category Unit where
-  
-  data Obj Unit a where
-    UnitO :: Obj Unit UnitO
-  
-  src UnitId = UnitO
-  tgt UnitId = UnitO
-  
-  id UnitO        = UnitId
-  UnitId . UnitId = UnitId
diff --git a/Data/Category/Void.hs b/Data/Category/Void.hs
deleted file mode 100644
--- a/Data/Category/Void.hs
+++ /dev/null
@@ -1,59 +0,0 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, EmptyDataDecls #-}
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Category.Void
--- Copyright   :  (c) Sjoerd Visscher 2010
--- License     :  BSD-style (see the file LICENSE)
---
--- Maintainer  :  sjoerd@w3future.com
--- Stability   :  experimental
--- Portability :  non-portable
---
--- /0/, the empty category. 
--- The limit and colimit of the functor from /0/ to some category provide 
--- terminal and initial objects in that category.
------------------------------------------------------------------------------
-module Data.Category.Void where
-
-import Prelude hiding ((.), id, Functor)
-import Data.Category
-import Data.Category.Functor
-import Data.Category.NaturalTransformation
-
-
--- | The (empty) data type of the arrows in /0/. 
-data Void a b
-
-magicVoid :: Void a b -> x
-magicVoid x = x `seq` error "we never get this far"
-
-magicVoidO :: Obj Void a -> x
-magicVoidO x = x `seq` error "we never get this far"
-
-
-instance Category Void where
-  
-  -- | The (empty) data type of the objects in /0/. 
-  data Obj Void a
-  
-  src = magicVoid
-  tgt = magicVoid
-  
-  id    = magicVoidO
-  a . b = magicVoid (a `seq` b)
-
-
--- | The functor from /0/ to (~>), the empty diagram in (~>).
-data VoidDiagram ((~>) :: * -> * -> *) = VoidDiagram
-
-type instance Dom (VoidDiagram (~>)) = Void
-type instance Cod (VoidDiagram (~>)) = (~>)
-
-instance Functor (VoidDiagram (~>)) where 
-  VoidDiagram %% x = magicVoidO x
-  VoidDiagram %  f = magicVoid f
-
-
-voidNat :: (Functor f, Functor g, Dom f ~ Void, Dom g ~ Void, Cod f ~ d, Cod g ~ d)
-  => f -> g -> Nat Void d f g
-voidNat f g = Nat f g magicVoidO
diff --git a/data-category.cabal b/data-category.cabal
--- a/data-category.cabal
+++ b/data-category.cabal
@@ -1,14 +1,18 @@
 name:                data-category
-version:             0.2.0
+version:             0.3.0
 synopsis:            Restricted categories
 
 description:         Data-category is a collection of categories, and some categorical constructions on them.
                      .
                      You can restrict the types of the objects of your category by using a GADT for the arrow type.
                      To be able to proof to the compiler that a type is an object in some category, objects also need to be represented at the value level.
-                     Therefore the 'Category' class has an associated data type 'Obj'. This which will often also be a GADT.
+                     The corresponding identity arrow of the object is used for that.
                      .
                      See the 'Monoid', 'Boolean' and 'Product' categories for some examples.
+                     .
+                     Note: Strictly speaking this package defines Hask-enriched categories, not ordinary categories (which are Set-enriched.)
+                     In practice this means we are allowed to ignore 'undefined' (f.e. when talking about uniqueness of morphisms),
+                     and we can treat the categories as normal categories.
 
 category:            Data
 license:             BSD3
@@ -26,14 +30,13 @@
   exposed-modules:     
     Data.Category,
     Data.Category.Functor,
+    Data.Category.Product,
     Data.Category.NaturalTransformation,
     Data.Category.Limit,
     Data.Category.Adjunction,
-    Data.Category.Void,
-    Data.Category.Unit,
-    Data.Category.Pair,
+    Data.Category.Monoidal,
+    Data.Category.CartesianClosed,
     Data.Category.Discrete,
-    Data.Category.Product,
     Data.Category.Monoid,
     Data.Category.Boolean,
     Data.Category.Omega,