diff --git a/Data/Category.hs b/Data/Category.hs
--- a/Data/Category.hs
+++ b/Data/Category.hs
@@ -2,7 +2,6 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category
--- Copyright   :  (c) Sjoerd Visscher 2010
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  sjoerd@w3future.com
diff --git a/Data/Category/Adjunction.hs b/Data/Category/Adjunction.hs
--- a/Data/Category/Adjunction.hs
+++ b/Data/Category/Adjunction.hs
@@ -2,7 +2,6 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Adjunction
--- Copyright   :  (c) Sjoerd Visscher 2010
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  sjoerd@w3future.com
@@ -101,21 +100,9 @@
 
 
 
-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
+contAdj :: Adjunction (Op (->)) (->) (Opposite ((->) :-*: r) :.: OpOpInv (->)) ((->) :-*: r)
+contAdj = mkAdjunction
+  (Opposite (hom_X id) :.: OpOpInv)
+  (hom_X id)
+  (\_ -> flip ($))
+  (\_ -> Op (flip ($)))
diff --git a/Data/Category/Boolean.hs b/Data/Category/Boolean.hs
--- a/Data/Category/Boolean.hs
+++ b/Data/Category/Boolean.hs
@@ -2,7 +2,6 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Boolean
--- Copyright   :  (c) Sjoerd Visscher 2010
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  sjoerd@w3future.com
@@ -74,6 +73,7 @@
 type instance BinaryProduct Boolean Tru Fls = Fls
 type instance BinaryProduct Boolean Tru Tru = Tru
 
+-- | Conjunction is the binary product in the Boolean category.
 instance HasBinaryProducts Boolean where 
   
   proj1 Fls Fls = Fls
@@ -100,6 +100,7 @@
 type instance BinaryCoproduct Boolean Tru Fls = Tru
 type instance BinaryCoproduct Boolean Tru Tru = Tru
 
+-- | Disjunction is the binary coproduct in the Boolean category.
 instance HasBinaryCoproducts Boolean where 
   
   inj1 Fls Fls = Fls
@@ -126,6 +127,7 @@
 type instance Exponential Boolean Tru Fls = Fls
 type instance Exponential Boolean Tru Tru = Tru
 
+-- | Implication makes the Boolean category cartesian closed.
 instance CartesianClosed Boolean where
   
   apply Fls Fls = Fls
@@ -170,13 +172,15 @@
 falseProductComonoid = ComonoidObject F2T Fls
 
 
--- | 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)
+data NatAsFunctor f g where
+  NatAsFunctor :: (Functor f, Functor g, Category c, Category d, Dom f ~ c, Cod f ~ d, Dom g ~ c, Cod g ~ d)
+               => Nat (Dom f) (Cod f) f g -> NatAsFunctor 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
+-- | A natural transformation @Nat c d@ is isomorphic to a functor from @c :**: 2@ to @d@.
+instance (Category (Dom f), Category (Cod f)) => Functor (NatAsFunctor f g) where
   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
--- a/Data/Category/CartesianClosed.hs
+++ b/Data/Category/CartesianClosed.hs
@@ -2,7 +2,6 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.CartesianClosed
--- Copyright   :  (c) Sjoerd Visscher 2010
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  sjoerd@w3future.com
@@ -24,6 +23,7 @@
 
 type family Exponential (~>) y z :: *
 
+-- | A category is cartesian closed if it has all products and exponentials for all objects.
 class (HasTerminalObject (~>), HasBinaryProducts (~>)) => CartesianClosed (~>) where
   
   apply :: Obj (~>) y -> Obj (~>) z -> BinaryProduct (~>) (Exponential (~>) y z) y ~> z
@@ -35,6 +35,7 @@
 type instance Dom (ExpFunctor (~>)) = Op (~>) :**: (~>)
 type instance Cod (ExpFunctor (~>)) = (~>)
 type instance (ExpFunctor (~>)) :% (y, z) = Exponential (~>) y z
+-- | The exponential as a bifunctor.
 instance CartesianClosed (~>) => Functor (ExpFunctor (~>)) where
   ExpFunctor % (Op y :**: z) = z ^^^ y
 
@@ -42,6 +43,7 @@
 
 type instance Exponential (->) y z = y -> z
 
+-- | Exponentials in @Hask@ are functions.
 instance CartesianClosed (->) where
   
   apply _ _ (f, y) = f y
@@ -50,73 +52,59 @@
 
 
 
-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) = l ! r
+data Apply (y :: * -> * -> *) (z :: * -> * -> *) = Apply
+type instance Dom (Apply y z) = Nat y z :**: y
+type instance Cod (Apply y z) = z
+type instance Apply y z :% (f, a) = f :% a
+-- | 'Apply' is a bifunctor, @Apply :% (f, a)@ applies @f@ to @a@, i.e. @f :% a@.
+instance (Category y, Category z) => Functor (Apply y z) where
+  Apply % (l :**: r) = l ! r
 
-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
+data ToTuple1 (y :: * -> * -> *) (z :: * -> * -> *) = ToTuple1
+type instance Dom (ToTuple1 y z) = z
+type instance Cod (ToTuple1 y z) = Nat y (z :**: y)
+type instance ToTuple1 y z :% a = Tuple1 z y a
+-- | 'ToTuple1' converts an object @a@ to the functor 'Tuple1' @a@.
+instance (Category y, Category z) => Functor (ToTuple1 y z) where
+  ToTuple1 % f = Nat (Tuple1 (src f)) (Tuple1 (tgt f)) $ \z -> f :**: z
 
+data ToTuple2 (y :: * -> * -> *) (z :: * -> * -> *) = ToTuple2
+type instance Dom (ToTuple2 y z) = y
+type instance Cod (ToTuple2 y z) = Nat z (z :**: y)
+type instance ToTuple2 y z :% a = Tuple2 z y a
+-- | 'ToTuple2' converts an object @a@ to the functor 'Tuple2' @a@.
+instance (Category y, Category z) => Functor (ToTuple2 y z) where
+  ToTuple2 % f = Nat (Tuple2 (src f)) (Tuple2 (tgt f)) $ \y -> y :**: f
 
+
 type instance Exponential Cat (CatW c) (CatW d) = CatW (Nat c d)
 
+-- | Exponentials in @Cat@ are the functor categories.
 instance CartesianClosed Cat where
   
-  apply CatA{} CatA{}   = CatA CatApply
-  tuple CatA{} CatA{}   = CatA CatTuple
+  apply CatA{} CatA{}   = CatA Apply
+  tuple CatA{} CatA{}   = CatA ToTuple1
   (CatA f) ^^^ (CatA h) = CatA (Wrap f h)
 
 
-type Presheaves (~>) = Nat (Op (~>)) (->)
-
-data PShExponential ((~>) :: * -> * -> *) p q = PShExponential
-type instance Dom (PShExponential (~>) p q) = Op (~>)
-type instance Cod (PShExponential (~>) p q) = (->)
-type instance PShExponential (~>) p q :% a = Presheaves (~>) (((~>) :-*: a) :*: p) q
-instance (Category (~>), Dom p ~ Op (~>), Dom q ~ Op (~>), Cod p ~ (->), Cod q ~ (->), Functor p, Functor q)
-  => Functor (PShExponential (~>) p q) where
-  PShExponential % Op f = \(Nat (_ :*: p) q n) -> Nat (hom_X (src f) :*: p) q $ \i (i2a, pi) -> n i (f . i2a, pi)
-
-type instance Exponential (Presheaves (~>)) y z = PShExponential (~>) y z
-
-instance Category (~>) => CartesianClosed (Presheaves (~>)) where
-  
-  apply (Nat y _ _) (Nat z _ _) = Nat (PShExponential :*: y) z $ \(Op i) (n, yi) -> (n ! Op i) (i, yi)
-  tuple (Nat y _ _) (Nat z _ _) = Nat z PShExponential $ \(Op i) zi -> (Nat (hom_X i) z $ \_ j2i -> (z % Op j2i) zi) *** natId y
-  zn@Nat{} ^^^ yn@Nat{} = Nat PShExponential PShExponential $ \(Op i) n -> zn . n . (natId (hom_X i) *** yn)
-
-    
-data ProductWith (~>) y = ProductWith (Obj (~>) y)
-type instance Dom (ProductWith (~>) y) = (~>)
-type instance Cod (ProductWith (~>) y) = (~>)
-type instance ProductWith (~>) y :% z = BinaryProduct (~>) 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)
+-- | The product functor is left adjoint the the exponential functor.
+curryAdj :: CartesianClosed (~>) 
+         => Obj (~>) y 
+         -> Adjunction (~>) (~>) 
+              (ProductFunctor (~>) :.: Tuple2 (~>) (~>) y) 
+              (ExpFunctor (~>) :.: Tuple1 (Op (~>)) (~>) y)
+curryAdj y = mkAdjunction (ProductFunctor :.: Tuple2 y) (ExpFunctor :.: Tuple1 (Op y)) (tuple y) (apply y)
 
-curry :: CartesianClosed (~>) => Obj (~>) x -> Obj (~>) y -> Obj (~>) z -> (ProductWith (~>) y :% x) ~> z -> x ~> (ExponentialWith (~>) y :% z)
+-- | From the adjunction between the product functor and the exponential functor we get the curry and uncurry functions,
+--   generalized to any cartesian closed category.
+curry :: CartesianClosed (~>) => Obj (~>) x -> Obj (~>) y -> Obj (~>) z -> BinaryProduct (~>) x y ~> z -> x ~> Exponential (~>) 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 :: CartesianClosed (~>) => Obj (~>) x -> Obj (~>) y -> Obj (~>) z -> x ~> Exponential (~>) y z -> BinaryProduct (~>) x y ~> z
 uncurry _ y z = rightAdjunct (curryAdj y) z
 
-type State (~>) s a = ExponentialWith (~>) s :% ProductWith (~>) s :% a
+-- | From every adjunction we get a monad, in this case the State monad.
+type State (~>) s a = Exponential (~>) s (BinaryProduct (~>) a s)
 
 stateMonadReturn :: CartesianClosed (~>) => Obj (~>) s -> Obj (~>) a -> a ~> State (~>) s a
 stateMonadReturn s a = M.unit (adjunctionMonad $ curryAdj s) ! a
@@ -124,7 +112,8 @@
 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
+-- ! From every adjunction we also get a comonad, the Context comonad in this case.
+type Context (~>) s a = BinaryProduct (~>) (Exponential (~>) s a) s
 
 contextComonadExtract :: CartesianClosed (~>) => Obj (~>) s -> Obj (~>) a -> Context (~>) s a ~> a
 contextComonadExtract s a = M.counit (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
@@ -2,7 +2,6 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Comma
--- Copyright   :  (c) Sjoerd Visscher 2010
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  sjoerd@w3future.com
@@ -31,6 +30,7 @@
     CommaO t s (a', b') ->
     (t :/\: s) (a, b) (a', b')
 
+-- | The comma category T \\downarrow S
 instance (Category (Dom t), Category (Dom s)) => Category (t :/\: s) where
     
   src (CommaA so@(CommaO a _ b) _ _ _)    = CommaA so a        b        so
diff --git a/Data/Category/Coproduct.hs b/Data/Category/Coproduct.hs
--- a/Data/Category/Coproduct.hs
+++ b/Data/Category/Coproduct.hs
@@ -1,8 +1,7 @@
 {-# LANGUAGE TypeFamilies, TypeOperators, GADTs, FlexibleContexts #-}
 -----------------------------------------------------------------------------
 -- |
--- Module      :  Data.Category.Product
--- Copyright   :  (c) Sjoerd Visscher 2010
+-- Module      :  Data.Category.Coproduct
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  sjoerd@w3future.com
@@ -43,6 +42,7 @@
 type instance Dom (Inj1 c1 c2) = c1
 type instance Cod (Inj1 c1 c2) = c1 :++: c2
 type instance Inj1 c1 c2 :% a = I1 a
+-- | 'Inj1' is a functor which injects into the left category.
 instance (Category c1, Category c2) => Functor (Inj1 c1 c2) where 
   Inj1 % f = I1 f
 
@@ -50,6 +50,7 @@
 type instance Dom (Inj2 c1 c2) = c2
 type instance Cod (Inj2 c1 c2) = c1 :++: c2
 type instance Inj2 c1 c2 :% a = I2 a
+-- | 'Inj2' is a functor which injects into the right category.
 instance (Category c1, Category c2) => Functor (Inj2 c1 c2) where 
   Inj2 % f = I2 f
 
@@ -58,6 +59,7 @@
 type instance Cod (f1 :+++: f2) = Cod f1 :++: Cod f2
 type instance (f1 :+++: f2) :% (I1 a) = I1 (f1 :% a)
 type instance (f1 :+++: f2) :% (I2 a) = I2 (f2 :% a)
+-- | @f1 :+++: f2@ is the coproduct of the functors @f1@ and @f2@.
 instance (Functor f1, Functor f2) => Functor (f1 :+++: f2) where 
   (g :+++: _) % I1 f = I1 (g % f)
   (_ :+++: g) % I2 f = I2 (g % f)
@@ -67,6 +69,7 @@
 type instance Cod (CodiagCoprod (~>)) = (~>)
 type instance CodiagCoprod (~>) :% I1 a = a
 type instance CodiagCoprod (~>) :% I2 a = a
+-- | 'CodiagCoprod' is the codiagonal functor for coproducts.
 instance Category (~>) => Functor (CodiagCoprod (~>)) where 
   CodiagCoprod % I1 f = f
   CodiagCoprod % I2 f = f
@@ -76,6 +79,7 @@
 type instance Cod (Cotuple1 c1 c2 a1) = c1
 type instance Cotuple1 c1 c2 _1 :% I1 a1 = a1
 type instance Cotuple1 c1 c2 a1 :% I2 a2 = a1
+-- | 'Cotuple1' projects out to the left category, replacing a value from the right category with a fixed object.
 instance (Category c1, Category c2) => Functor (Cotuple1 c1 c2 a1) where
   Cotuple1 _ % I1 f = f
   Cotuple1 a % I2 _ = a
@@ -85,6 +89,7 @@
 type instance Cod (Cotuple2 c1 c2 a2) = c2
 type instance Cotuple2 c1 c2 a2 :% I1 a1 = a2
 type instance Cotuple2 c1 c2 _2 :% I2 a2 = a2
+-- | 'Cotuple2' projects out to the right category, replacing a value from the left category with a fixed object.
 instance (Category c1, Category c2) => Functor (Cotuple2 c1 c2 a2) where
   Cotuple2 a % I1 _ = a
   Cotuple2 _ % I2 f = f
diff --git a/Data/Category/Dialg.hs b/Data/Category/Dialg.hs
--- a/Data/Category/Dialg.hs
+++ b/Data/Category/Dialg.hs
@@ -2,7 +2,6 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Dialg
--- Copyright   :  (c) Sjoerd Visscher 2010
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  sjoerd@w3future.com
@@ -41,6 +40,7 @@
 dialgebra :: Obj (Dialg f g) a -> Dialgebra f g a
 dialgebra (DialgA d _ _) = d
 
+-- | The category of (F,G)-dialgebras.
 instance Category (Dialg f g) where
   
   src (DialgA s _ _) = dialgId s
@@ -70,7 +70,6 @@
 
 
 
--- | 'FixF' provides the initial F-algebra for endofunctors in Hask.
 newtype FixF f = InF { outF :: f :% FixF f }
 
 -- | Catamorphisms for endofunctors in Hask.
@@ -82,6 +81,7 @@
 anaHask a@(Dialgebra _ f) = DialgA a (dialgebra terminalObject) $ ana_f where ana_f = InF . (EndoHask % ana_f) . f 
 
 
+-- | 'FixF' provides the initial F-algebra for endofunctors in Hask.
 instance Prelude.Functor f => HasInitialObject (Dialg (EndoHask f) (Id (->))) where
   
   type InitialObject (Dialg (EndoHask f) (Id (->))) = FixF (EndoHask f)
@@ -89,7 +89,8 @@
   initialObject = dialgId $ Dialgebra id InF
   initialize a = cataHask (dialgebra a)
   
-instance  Prelude.Functor f => HasTerminalObject (Dialg (Id (->)) (EndoHask f)) where
+-- | 'FixF' also provides the terminal F-coalgebra for endofunctors in Hask.
+instance Prelude.Functor f => HasTerminalObject (Dialg (Id (->)) (EndoHask f)) where
 
   type TerminalObject (Dialg (Id (->)) (EndoHask f)) = FixF (EndoHask f)
   
@@ -98,24 +99,16 @@
   
 
 
--- | 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 :: NatF (~>)
-type instance Dom (NatF (~>)) = (~>)
-type instance Cod (NatF (~>)) = (~>) :**: (~>)
-type instance NatF (~>) :% a = (TerminalObject (~>),  a)
-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)
 
-instance HasInitialObject (Dialg (NatF (->)) (DiagProd (->))) where
+-- | 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>@.
+instance HasInitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) where
   
-  type InitialObject (Dialg (NatF (->)) (DiagProd (->))) = NatNum
+  type InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) = NatNum
     
   initialObject = dialgId $ Dialgebra id (Z :**: S)
   
@@ -123,25 +116,27 @@
 
 
 
-data EMAdjF m = EMAdjF (Monad m)
-type instance Dom (EMAdjF m) = Dom m
-type instance Cod (EMAdjF m) = Alg m
-type instance EMAdjF m :% a = m :% a
-instance (Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Functor (EMAdjF m) where
-  EMAdjF m % f = DialgA (alg (src f)) (alg (tgt f)) $ monadFunctor m % f
+data FreeAlg m = FreeAlg (Monad m)
+type instance Dom (FreeAlg m) = Dom m
+type instance Cod (FreeAlg m) = Alg m
+type instance FreeAlg m :% a = m :% a
+-- | @FreeAlg@ M takes @x@ to the free algebra @(M x, mu_x)@ of the monad @M@.
+instance (Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Functor (FreeAlg m) where
+  FreeAlg m % f = DialgA (alg (src f)) (alg (tgt f)) $ monadFunctor m % f
     where
       alg :: Obj (~>) x -> Algebra m (m :% x)
       alg x = Dialgebra (monadFunctor m % x) (multiply m ! x)
 
-data EMAdjG m = EMAdjG
-type instance Dom (EMAdjG m) = Alg m
-type instance Cod (EMAdjG m) = Dom m
-type instance EMAdjG m :% a = a
-instance (Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Functor (EMAdjG m) where
-  EMAdjG % DialgA _ _ f = f
+data ForgetAlg m = ForgetAlg
+type instance Dom (ForgetAlg m) = Alg m
+type instance Cod (ForgetAlg m) = Dom m
+type instance ForgetAlg m :% a = a
+-- | @ForgetAlg m@ is the forgetful functor for @Alg m@.
+instance (Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Functor (ForgetAlg m) where
+  ForgetAlg % DialgA _ _ f = f
 
 eilenbergMooreAdj :: (Functor m, Dom m ~ (~>), Cod m ~ (~>)) 
-  => Monad m -> A.Adjunction (Alg m) (~>) (EMAdjF m) (EMAdjG m)
-eilenbergMooreAdj m = A.mkAdjunction (EMAdjF m) EMAdjG
+  => Monad m -> A.Adjunction (Alg m) (~>) (FreeAlg m) (ForgetAlg m)
+eilenbergMooreAdj m = A.mkAdjunction (FreeAlg m) ForgetAlg
   (\x -> unit m ! x)
   (\(DialgA (Dialgebra _ h) _ _) -> DialgA (Dialgebra (src h) (monadFunctor m % h)) (Dialgebra (tgt h) h) h)
diff --git a/Data/Category/Discrete.hs b/Data/Category/Discrete.hs
--- a/Data/Category/Discrete.hs
+++ b/Data/Category/Discrete.hs
@@ -2,7 +2,6 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Discrete
--- Copyright   :  (c) Sjoerd Visscher 2010
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  sjoerd@w3future.com
@@ -73,11 +72,11 @@
   _   . _   = error "Other combinations should not type-check."
 
 
--- | @Void@ is the empty category.
+-- | 'Void' is the empty category.
 type Void = Discrete Z
--- | @Unit@ is the discrete category with one object.
+-- | 'Unit' is the discrete category with one object.
 type Unit = Discrete (S Z)
--- | @Pair@ is the discrete category with two objects.
+-- | 'Pair' is the discrete category with two objects.
 type Pair = Discrete (S (S Z))
 
 
@@ -85,6 +84,7 @@
 type instance Dom (Succ n) = Discrete n
 type instance Cod (Succ n) = Discrete (S n)
 type instance Succ n :% a = S a
+-- | 'Succ' maps each object in @Discrete n@ to its successor in @Discrete (S n)@.
 instance (Category (Discrete n)) => Functor (Succ n) where
   Succ % Z     = S Z
   Succ % (S a) = S (S a)
@@ -95,23 +95,25 @@
 -- | The functor from @Discrete n@ to @(~>)@, a diagram of @n@ objects in @(~>)@. 
 data DiscreteDiagram :: (* -> * -> *) -> * -> * -> * where
   Nil   :: DiscreteDiagram (~>) Z ()
-  (:::) :: Obj (~>) x -> DiscreteDiagram (~>) n xs -> DiscreteDiagram (~>) (S n) (x, xs)
+  (:::) :: (Category (~>), Category (Discrete n)) 
+        => 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 (Category (~>)) 
-  => Functor (DiscreteDiagram (~>) Z ()) where
+-- | The empty diagram.
+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
+-- | A diagram with one more object.
+instance Functor (DiscreteDiagram (~>) n xs) => Functor (DiscreteDiagram (~>) (S n) (x, xs)) where
   (x ::: _)  % Z   = x
   (_ ::: xs) % S n = xs % n
 
 
+-- | Natural transformations in 'Void' are trivial.
 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 = Nat f g magicZ
diff --git a/Data/Category/Functor.hs b/Data/Category/Functor.hs
--- a/Data/Category/Functor.hs
+++ b/Data/Category/Functor.hs
@@ -2,7 +2,6 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Functor
--- Copyright   :  (c) Sjoerd Visscher 2010
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  sjoerd@w3future.com
@@ -26,6 +25,8 @@
   , (:.:)(..)
   , Const(..), ConstF
   , Opposite(..)
+  , OpOp(..)
+  , OpOpInv(..)
   , EndoHask(..)
   
   -- *** Related to the product category
@@ -86,18 +87,17 @@
 
 
 
--- | The identity functor on (~>)
 data Id ((~>) :: * -> * -> *) = Id
 
 type instance Dom (Id (~>)) = (~>)
 type instance Cod (Id (~>)) = (~>)
 type instance Id (~>) :% a = a
 
+-- | The identity functor on (~>)
 instance Category (~>) => Functor (Id (~>)) where 
   _ % f = f
 
 
--- | The composition of two functors.
 data (g :.: h) where
   (:.:) :: (Functor g, Functor h, Cod h ~ Dom g) => g -> h -> g :.: h
   
@@ -105,11 +105,11 @@
 type instance Cod (g :.: h) = Cod g
 type instance (g :.: h) :% a = g :% (h :% a)
 
+-- | The composition of two functors.
 instance (Category (Cod g), Category (Dom h)) => Functor (g :.: h) where 
   (g :.: h) % f = g % (h % f)
 
 
--- | The constant functor.
 data Const (c1 :: * -> * -> *) (c2 :: * -> * -> *) x where
   Const :: Category c2 => Obj c2 x -> Const c1 c2 x
   
@@ -117,13 +117,14 @@
 type instance Cod (Const c1 c2 x) = c2
 type instance Const c1 c2 x :% a = x
 
+-- | The constant functor.
 instance (Category c1, Category c2) => Functor (Const c1 c2 x) where 
   Const x % _ = x
 
+-- | The constant functor with the same domain and codomain as f.
 type ConstF f = Const (Dom f) (Cod f)
 
 
--- | The dual of a functor
 data Opposite f where
   Opposite :: Functor f => f -> Opposite f
   
@@ -131,11 +132,33 @@
 type instance Cod (Opposite f) = Op (Cod f)
 type instance Opposite f :% a = f :% a
 
+-- | The dual of a functor
 instance (Category (Dom f), Category (Cod f)) => Functor (Opposite f) where
   Opposite f % Op a = Op $ f % a
 
 
--- | 'EndoHask' is a wrapper to turn instances of the 'Functor' class into categorical functors.
+data OpOp ((~>) :: * -> * -> *) = OpOp
+
+type instance Dom (OpOp (~>)) = Op (Op (~>))
+type instance Cod (OpOp (~>)) = (~>)
+type instance OpOp (~>) :% a = a
+
+-- | The @Op (Op x) = x@ functor.
+instance Category (~>) => Functor (OpOp (~>)) where
+  OpOp % Op (Op f) = f
+
+
+data OpOpInv ((~>) :: * -> * -> *) = OpOpInv
+
+type instance Dom (OpOpInv (~>)) = (~>)
+type instance Cod (OpOpInv (~>)) = Op (Op (~>))
+type instance OpOpInv (~>) :% a = a
+
+-- | The @x = Op (Op x)@ functor.
+instance Category (~>) => Functor (OpOpInv (~>)) where
+  OpOpInv % f = Op (Op f)
+
+
 data EndoHask :: (* -> *) -> * where
   EndoHask :: Prelude.Functor f => EndoHask f
   
@@ -143,93 +166,94 @@
 type instance Cod (EndoHask f) = (->)
 type instance EndoHask f :% r = f r
 
+-- | 'EndoHask' is a wrapper to turn instances of the 'Functor' class into categorical functors.
 instance Functor (EndoHask f) where
   EndoHask % f = fmap f
 
 
--- | 'Proj1' is a bifunctor that projects out the first component of a product.
 data Proj1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Proj1
 
 type instance Dom (Proj1 c1 c2) = c1 :**: c2
 type instance Cod (Proj1 c1 c2) = c1
 type instance Proj1 c1 c2 :% (a1, a2) = a1
 
+-- | 'Proj1' is a bifunctor that projects out the first component of a product.
 instance (Category c1, Category c2) => Functor (Proj1 c1 c2) where 
   Proj1 % (f1 :**: _) = f1
 
 
--- | 'Proj2' is a bifunctor that projects out the second component of a product.
 data Proj2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Proj2
 
 type instance Dom (Proj2 c1 c2) = c1 :**: c2
 type instance Cod (Proj2 c1 c2) = c2
 type instance Proj2 c1 c2 :% (a1, a2) = a2
 
+-- | 'Proj2' is a bifunctor that projects out the second component of a product.
 instance (Category c1, Category c2) => Functor (Proj2 c1 c2) where 
   Proj2 % (_ :**: f2) = f2
 
 
--- | @f1 :***: f2@ is the product of the functors @f1@ and @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)
 
+-- | @f1 :***: f2@ is the product of the functors @f1@ and @f2@.
 instance (Functor f1, Functor f2) => Functor (f1 :***: f2) where 
   (g1 :***: g2) % (f1 :**: f2) = (g1 % f1) :**: (g2 % f2)
   
   
--- | 'DiagProd' is the diagonal functor for products.
 data DiagProd ((~>) :: * -> * -> *) = DiagProd
 
 type instance Dom (DiagProd (~>)) = (~>)
 type instance Cod (DiagProd (~>)) = (~>) :**: (~>)
 type instance DiagProd (~>) :% a = (a, a)
 
+-- | 'DiagProd' is the diagonal functor for products.
 instance Category (~>) => Functor (DiagProd (~>)) where 
   DiagProd % f = f :**: f
 
 
--- | 'Tuple1' tuples with a fixed object on the left.
 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)
 
+-- | 'Tuple1' tuples with a fixed object on the left.
 instance (Category c1, Category c2) => Functor (Tuple1 c1 c2 a1) where
   Tuple1 a % f = a :**: f
 
 
--- | 'Tuple2' tuples with a fixed object on the right.
 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)
 
+-- | 'Tuple2' tuples with a fixed object on the right.
 instance (Category c1, Category c2) => Functor (Tuple2 c1 c2 a2) where
   Tuple2 a % f = f :**: a
 
 
--- | The Hom functor, Hom(–,–), a bifunctor contravariant in its first argument and covariant in its second argument.
 data Hom ((~>) :: * -> * -> *) = Hom  
 
 type instance Dom (Hom (~>)) = Op (~>) :**: (~>)
 type instance Cod (Hom (~>)) = (->)
 type instance (Hom (~>)) :% (a1, a2) = a1 ~> a2
 
+-- | The Hom functor, Hom(--,--), a bifunctor contravariant in its first argument and covariant in its second argument.
 instance Category (~>) => Functor (Hom (~>)) where 
   Hom % (Op f1 :**: f2) = \g -> f2 . g . f1
 
 
 type x :*-: (~>) = Hom (~>) :.: Tuple1 (Op (~>)) (~>) x
--- | The covariant functor Hom(X,–)
+-- | The covariant functor Hom(X,--)
 homX_ :: Category (~>) => Obj (~>) x -> x :*-: (~>)
 homX_ x = Hom :.: Tuple1 (Op x)
 
 type (~>) :-*: x = Hom (~>) :.: Tuple2 (Op (~>)) (~>) x
--- | The contravariant functor Hom(–,X)
+-- | The contravariant functor Hom(--,X)
 hom_X :: Category (~>) => Obj (~>) x -> (~>) :-*: x
 hom_X x = Hom :.: Tuple2 x
diff --git a/Data/Category/Kleisli.hs b/Data/Category/Kleisli.hs
--- a/Data/Category/Kleisli.hs
+++ b/Data/Category/Kleisli.hs
@@ -2,7 +2,6 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Kleisli
--- Copyright   :  (c) Sjoerd Visscher 2010
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  sjoerd@w3future.com
@@ -29,6 +28,7 @@
 kleisliId :: (Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Monad m -> Obj (~>) a -> Kleisli m a a
 kleisliId m a = Kleisli m a $ unit m ! a
 
+-- | The category of Kleisli arrows.
 instance Category (Kleisli m) where
   
   src (Kleisli m _ f) = kleisliId m (src f)
diff --git a/Data/Category/Limit.hs b/Data/Category/Limit.hs
--- a/Data/Category/Limit.hs
+++ b/Data/Category/Limit.hs
@@ -12,7 +12,6 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Limit
--- Copyright   :  (c) Sjoerd Visscher 2010
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  sjoerd@w3future.com
@@ -86,7 +85,6 @@
 infixl 2 |||
 
 
--- | The diagonal functor from (index-) category J to (~>).
 data Diag :: (* -> * -> *) -> (* -> * -> *) -> * where
   Diag :: Diag j (~>)
   
@@ -94,6 +92,7 @@
 type instance Cod (Diag j (~>)) = Nat j (~>)
 type instance Diag j (~>) :% a = Const j (~>) a
 
+-- | The diagonal functor from (index-) category J to (~>).
 instance (Category j, Category (~>)) => Functor (Diag j (~>)) where 
   Diag % f = Nat (Const $ src f) (Const $ tgt f) $ const f
 
@@ -126,18 +125,18 @@
 
 -- | An instance of @HasLimits j (~>)@ says that @(~>)@ has all limits of type @j@.
 class (Category j, Category (~>)) => HasLimits j (~>) where
+  -- | 'limit' returns the limiting cone for a functor @f@.
   limit           :: Obj (Nat j (~>)) f -> Cone f (Limit f)
+  -- | 'limitFactorizer' shows that the limiting cone is universal – i.e. any other cone of @f@ factors through it –
+  --   by returning the morphism between the vertices of the cones.
   limitFactorizer :: Obj (Nat j (~>)) f -> (forall n. Cone f n -> n ~> Limit f)
 
--- | If every diagram of type @j@ has a limit in @(~>)@ there exists a limit functor.
---
---   Applied to a natural transformation it is a generalisation of @(***)@:
---
---   @l@ '***' @r =@ 'LimitFunctor' '%' 'arrowPair' @l r@
 data LimitFunctor (j :: * -> * -> *) ((~>)  :: * -> * -> *) = LimitFunctor
 type instance Dom (LimitFunctor j (~>)) = Nat j (~>)
 type instance Cod (LimitFunctor j (~>)) = (~>)
 type instance LimitFunctor j (~>) :% f = LimitFam j (~>) f
+-- | If every diagram of type @j@ has a limit in @(~>)@ there exists a limit functor.
+--   It can be seen as a generalisation of @(***)@.
 instance HasLimits j (~>) => Functor (LimitFunctor j (~>)) where
   LimitFunctor % n @ Nat{}  = limitFactorizer (tgt n) (n . limit (src n))
 
@@ -155,18 +154,18 @@
 
 -- | An instance of @HasColimits j (~>)@ says that @(~>)@ has all colimits of type @j@.
 class (Category j, Category (~>)) => HasColimits j (~>) where
+  -- | 'colimit' returns the limiting co-cone for a functor @f@.
   colimit           :: Obj (Nat j (~>)) f -> Cocone f (Colimit f)
+  -- | 'colimitFactorizer' shows that the limiting co-cone is universal – i.e. any other co-cone of @f@ factors through it –
+  --   by returning the morphism between the vertices of the cones.
   colimitFactorizer :: Obj (Nat j (~>)) f -> (forall n. Cocone f n -> Colimit f ~> n)
 
--- | If every diagram of type @j@ has a colimit in @(~>)@ there exists a colimit functor.
---
---   Applied to a natural transformation it is a generalisation of @(+++)@:
---
---   @l@ '+++' @r =@ 'ColimitFunctor' '%' 'arrowPair' @l r@
 data ColimitFunctor (j :: * -> * -> *) ((~>)  :: * -> * -> *) = ColimitFunctor
 type instance Dom (ColimitFunctor j (~>)) = Nat j (~>)
 type instance Cod (ColimitFunctor j (~>)) = (~>)
 type instance ColimitFunctor j (~>) :% f = ColimitFam j (~>) f
+-- | If every diagram of type @j@ has a colimit in @(~>)@ there exists a colimit functor.
+--   It can be seen as a generalisation of @(+++)@.
 instance HasColimits j (~>) => Functor (ColimitFunctor j (~>)) where
   ColimitFunctor % n @ Nat{}  = colimitFactorizer (src n) (colimit (tgt n) . n)
 
@@ -177,7 +176,6 @@
   
 
 
--- | A terminal object is the limit of the functor from /0/ to (~>).
 class Category (~>) => HasTerminalObject (~>) where
   
   type TerminalObject (~>) :: *
@@ -189,6 +187,7 @@
 
 type instance LimitFam Void (~>) f = TerminalObject (~>)
 
+-- | A terminal object is the limit of the functor from /0/ to (~>).
 instance (HasTerminalObject (~>)) => HasLimits Void (~>) where
   
   limit (Nat f _ _) = voidNat (Const terminalObject) f
@@ -233,7 +232,6 @@
   
   
 
--- | An initial object is the colimit of the functor from /0/ to (~>).
 class Category (~>) => HasInitialObject (~>) where
   
   type InitialObject (~>) :: *
@@ -245,6 +243,7 @@
 
 type instance ColimitFam Void (~>) f = InitialObject (~>)
 
+-- | An initial object is the colimit of the functor from /0/ to (~>).
 instance HasInitialObject (~>) => HasColimits Void (~>) where
   
   colimit (Nat f _ _) = voidNat f (Const initialObject)
@@ -294,7 +293,6 @@
 
 type family BinaryProduct ((~>) :: * -> * -> *) x y :: *
 
--- | The product of 2 objects is the limit of the functor from Pair to (~>).
 class Category (~>) => HasBinaryProducts (~>) where
   
   proj1 :: Obj (~>) x -> Obj (~>) y -> BinaryProduct (~>) x y ~> x
@@ -307,6 +305,7 @@
 
 type instance LimitFam (Discrete (S n)) (~>) f = BinaryProduct (~>) (f :% Z) (LimitFam (Discrete n) (~>) (f :.: Succ n))
 
+-- | The product of @n@ objects is the limit of the functor from @Discrete n@ to @(~>)@.
 instance (HasLimits (Discrete n) (~>), HasBinaryProducts (~>)) => HasLimits (Discrete (S n)) (~>) where
   
   limit = limit'
@@ -326,6 +325,7 @@
 
 type instance BinaryProduct (->) x y = (x, y)
 
+-- | The tuple is the binary product in @Hask@.
 instance HasBinaryProducts (->) where
   
   proj1 _ _ = fst
@@ -336,6 +336,7 @@
 
 type instance BinaryProduct Cat (CatW c1) (CatW c2) = CatW (c1 :**: c2)
 
+-- | The product of categories '(:**:)' is the binary product in 'Cat'.
 instance HasBinaryProducts Cat where
   
   proj1 (CatA _) (CatA _) = CatA Proj1
@@ -346,6 +347,7 @@
 
 type instance BinaryProduct (c1 :**: c2) (x1, x2) (y1, y2) = (BinaryProduct c1 x1 y1, BinaryProduct c2 x2 y2)
 
+-- | The binary product of the product of 2 categories is the product of their binary products.
 instance (HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts (c1 :**: c2) where
   
   proj1 (x1 :**: x2) (y1 :**: y2) = proj1 x1 y1 :**: proj1 x2 y2
@@ -355,25 +357,26 @@
   (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
+-- | Binary product as a bifunctor.
 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)
+-- | The product of two functors, passing the same object to both functors and taking the product of the results.
 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
 
+-- | The functor product '(:*:)' is the binary product in functor categories.
 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)
@@ -386,7 +389,6 @@
 
 type family BinaryCoproduct ((~>) :: * -> * -> *) x y :: *
 
--- | The coproduct of 2 objects is the colimit of the functor from Pair to (~>).
 class Category (~>) => HasBinaryCoproducts (~>) where
 
   inj1 :: Obj (~>) x -> Obj (~>) y -> x ~> BinaryCoproduct (~>) x y
@@ -400,6 +402,7 @@
 
 type instance ColimitFam (Discrete (S n)) (~>) f = BinaryCoproduct (~>) (f :% Z) (ColimitFam (Discrete n) (~>) (f :.: Succ n))
 
+-- | The coproduct of @n@ objects is the colimit of the functor from @Discrete n@ to @(~>)@.
 instance (HasColimits (Discrete n) (~>), HasBinaryCoproducts (~>)) => HasColimits (Discrete (S n)) (~>) where
   
   colimit = colimit'
@@ -419,6 +422,7 @@
 
 type instance BinaryCoproduct (->) x y = Either x y
 
+-- | 'Either' is the coproduct in @Hask@.
 instance HasBinaryCoproducts (->) where
   
   inj1 _ _ = Left
@@ -429,6 +433,7 @@
 
 type instance BinaryCoproduct Cat (CatW c1) (CatW c2) = CatW (c1 :++: c2)
 
+-- | The coproduct of categories '(:++:)' is the binary coproduct in 'Cat'.
 instance HasBinaryCoproducts Cat where
   
   inj1 (CatA _) (CatA _) = CatA Inj1
@@ -439,6 +444,7 @@
 
 type instance BinaryCoproduct (c1 :**: c2) (x1, x2) (y1, y2) = (BinaryCoproduct c1 x1 y1, BinaryCoproduct c2 x2 y2)
 
+-- | The binary coproduct of the product of 2 categories is the product of their binary coproducts.
 instance (HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts (c1 :**: c2) where
   
   inj1 (x1 :**: x2) (y1 :**: y2) = inj1 x1 y1 :**: inj1 x2 y2
@@ -448,25 +454,26 @@
   (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
+-- | Binary coproduct as a bifunctor.
 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)
+-- | The coproduct of two functors, passing the same object to both functors and taking the coproduct of the results.
 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
 
+-- | The functor coproduct '(:+:)' is the binary coproduct in functor categories.
 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)
diff --git a/Data/Category/Monoid.hs b/Data/Category/Monoid.hs
--- a/Data/Category/Monoid.hs
+++ b/Data/Category/Monoid.hs
@@ -2,7 +2,6 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Monoid
--- Copyright   :  (c) Sjoerd Visscher 2010
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  sjoerd@w3future.com
@@ -26,7 +25,7 @@
 data MonoidA m a b where
   MonoidA :: Monoid m => m -> MonoidA m m m
 
--- | A monoid as a category with one object.
+-- | A (prelude) monoid as a category with one object.
 instance Monoid m => Category (MonoidA m) where
   
   src (MonoidA _) = MonoidA mempty
@@ -38,9 +37,6 @@
 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
   
@@ -54,6 +50,7 @@
 type instance Dom ForgetMonoid = Mon
 type instance Cod ForgetMonoid = (->)
 type instance ForgetMonoid :% a = a
+-- | The 'ForgetMonoid' functor forgets the monoid structure.
 instance Functor ForgetMonoid where
   ForgetMonoid % MonoidMorphism f = f
   
@@ -61,14 +58,16 @@
 type instance Dom FreeMonoid = (->)
 type instance Cod FreeMonoid = Mon
 type instance FreeMonoid :% a = [a]
+-- | The 'FreeMonoid' functor is the list functor.
 instance Functor FreeMonoid where
   FreeMonoid % f = MonoidMorphism $ map f
 
+-- | The free monoid functor is left adjoint to the forgetful functor.
 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)
+foldMap = (ForgetMonoid %) . rightAdjunct freeMonoidAdj (MonoidMorphism id)
 
 listMonadReturn :: a -> [a]
 listMonadReturn = M.unit (adjunctionMonad freeMonoidAdj) ! id
@@ -77,7 +76,7 @@
 listMonadJoin = M.multiply (adjunctionMonad freeMonoidAdj) ! id
 
 listComonadExtract :: Monoid m => [m] -> m
-listComonadExtract = let MonoidMorphism f = M.counit (adjunctionComonad freeMonoidAdj) ! MonoidMorphism id in f
+listComonadExtract = ForgetMonoid % (M.counit (adjunctionComonad freeMonoidAdj) ! MonoidMorphism id)
 
 listComonadDuplicate :: Monoid m => [m] -> [[m]]
-listComonadDuplicate = let MonoidMorphism f = M.comultiply (adjunctionComonad freeMonoidAdj) ! MonoidMorphism id in f
+listComonadDuplicate = ForgetMonoid % (M.comultiply (adjunctionComonad freeMonoidAdj) ! MonoidMorphism id)
diff --git a/Data/Category/Monoidal.hs b/Data/Category/Monoidal.hs
--- a/Data/Category/Monoidal.hs
+++ b/Data/Category/Monoidal.hs
@@ -2,7 +2,6 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Monoidal
--- Copyright   :  (c) Sjoerd Visscher 2010
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  sjoerd@w3future.com
@@ -22,31 +21,14 @@
 import Data.Category.Limit
 import Data.Category.Product
 
-class Functor f => HasUnit f where
+
+-- | A monoidal category is a category with some kind of tensor product.
+--   A tensor product is a bifunctor, with a unit object.
+class Functor f => TensorProduct f where
   
   type Unit f :: *
   unitObject :: f -> 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 (~>) a -> (f :% (Unit f, a)) ~> a
   leftUnitorInv  :: Cod f ~ (~>) => f -> Obj (~>) a -> a ~> (f :% (Unit f, a))
   rightUnitor    :: Cod f ~ (~>) => f -> Obj (~>) a -> (f :% (a, Unit f)) ~> a
@@ -56,8 +38,13 @@
   associatorInv  :: Cod f ~ (~>) => f -> Obj (~>) a -> Obj (~>) b -> Obj (~>) c -> (f :% (a, f :% (b, c))) ~> (f :% (f :% (a, b), c))
 
 
+-- | If a category has all products, then the product functor makes it a monoidal category,
+--   with the terminal object as unit.
 instance (HasTerminalObject (~>), HasBinaryProducts (~>)) => TensorProduct (ProductFunctor (~>)) where
   
+  type Unit (ProductFunctor (~>)) = TerminalObject (~>)
+  unitObject _ = terminalObject
+
   leftUnitor     _ a = proj2 terminalObject a
   leftUnitorInv  _ a = terminate a &&& a
   rightUnitor    _ a = proj1 a terminalObject
@@ -66,8 +53,13 @@
   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))
 
+-- | If a category has all coproducts, then the coproduct functor makes it a monoidal category,
+--   with the initial object as unit.
 instance (HasInitialObject (~>), HasBinaryCoproducts (~>)) => TensorProduct (CoproductFunctor (~>)) where
   
+  type Unit (CoproductFunctor (~>)) = InitialObject (~>)
+  unitObject _ = initialObject
+
   leftUnitor     _ a = initialize a ||| a
   leftUnitorInv  _ a = inj2 initialObject a
   rightUnitor    _ a = a ||| initialize a
@@ -76,8 +68,12 @@
   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)
   
+-- | Functor composition makes the category of endofunctors monoidal, with the identity functor as unit.
 instance Category (~>) => TensorProduct (FunctorCompose (~>)) where
   
+  type Unit (FunctorCompose (~>)) = Id (~>)
+  unitObject _ = natId Id
+  
   leftUnitor     _ (Nat g _ _) = idPostcomp g
   leftUnitorInv  _ (Nat g _ _) = idPostcompInv g
   rightUnitor    _ (Nat g _ _) = idPrecomp g
@@ -87,26 +83,28 @@
   associatorInv _ (Nat f _ _) (Nat g _ _) (Nat h _ _) = compAssocInv f g h
 
 
-
+-- | @MonoidObject f a@ defines a monoid @a@ in a monoidal category with tensor product @f@.
 data MonoidObject f a = MonoidObject
   { unit     :: (Cod f ~ (~>)) => Unit f        ~> a
   , multiply :: (Cod f ~ (~>)) => (f :% (a, a)) ~> a
   }
   
+-- | @ComonoidObject f a@ defines a comonoid @a@ in a comonoidal category with tensor product @f@.
 data ComonoidObject f a = ComonoidObject
   { counit     :: (Cod f ~ (~>)) => a ~> Unit f
   , comultiply :: (Cod f ~ (~>)) => a ~> (f :% (a, a))
   }
 
-
+-- | Monoids as defined in the prelude are monoids in @Hask@ with the product functor as tensor product.
 preludeMonoid :: M.Monoid m => MonoidObject (ProductFunctor (->)) m
 preludeMonoid = MonoidObject M.mempty (uncurry M.mappend)
 
 
 data MonoidAsCategory f m a b where
-  MonoidValue :: (TensorProduct f , Dom f ~ ((~>) :**: (~>)), Cod f ~ (~>))
+  MonoidValue :: (TensorProduct f, Dom f ~ ((~>) :**: (~>)), Cod f ~ (~>))
               => f -> MonoidObject f m -> Unit f ~> m -> MonoidAsCategory f m m m
 
+-- | A monoid as a category with one object.
 instance Category (MonoidAsCategory f m) where
   
   src (MonoidValue f m _) = MonoidValue f m $ unit m
@@ -115,7 +113,7 @@
   MonoidValue f m a . MonoidValue _ _ b = MonoidValue f m $ multiply m . f % (a :**: b) . leftUnitorInv f (unitObject f)
 
 
-
+-- | A monad is a monoid in the category of endofunctors.
 type Monad f = MonoidObject (FunctorCompose (Dom f)) f
 
 mkMonad :: (Functor f, Dom f ~ (~>), Cod f ~ (~>), Category (~>)) 
@@ -131,10 +129,11 @@
 preludeMonad :: (M.Functor f, M.Monad f) => Monad (EndoHask f)
 preludeMonad = mkMonad EndoHask (\_ -> M.return) (\_ -> M.join)
 
-monadFunctor :: forall f. Monad f -> f
+monadFunctor :: Monad f -> f
 monadFunctor (unit -> Nat _ f _) = f
 
 
+-- | A comonad is a comonoid in the category of endofunctors.
 type Comonad f = ComonoidObject (FunctorCompose (Dom f)) f
 
 mkComonad :: (Functor f, Dom f ~ (~>), Cod f ~ (~>), Category (~>)) 
@@ -148,8 +147,10 @@
   }
 
 
+-- | Every adjunction gives rise to an associated monad.
 adjunctionMonad :: Adjunction c d f g -> Monad (g :.: f)
 adjunctionMonad (Adjunction f g un coun) = mkMonad (g :.: f) (un !) ((Wrap g f % coun) !)
 
+-- | Every adjunction gives rise to an associated comonad.
 adjunctionComonad :: Adjunction c d f g -> Comonad (f :.: g)
 adjunctionComonad (Adjunction f g un coun) = mkComonad (f :.: g) (coun !) ((Wrap f g % un) !)
diff --git a/Data/Category/NaturalTransformation.hs b/Data/Category/NaturalTransformation.hs
--- a/Data/Category/NaturalTransformation.hs
+++ b/Data/Category/NaturalTransformation.hs
@@ -2,7 +2,6 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.NaturalTransformation
--- Copyright   :  (c) Sjoerd Visscher 2010
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  sjoerd@w3future.com
@@ -141,19 +140,17 @@
 type Endo (~>) = Nat (~>) (~>)
 
 
--- | 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
 
+-- | Composition of endofunctors is a functor.
 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 :: f -> Precompose f d
 
@@ -161,12 +158,12 @@
 type instance Cod (Precompose f d) = Nat (Dom f) d
 type instance Precompose f d :% g = g :.: f
 
+-- | @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@.
 instance (Functor f, Category d) => Functor (Precompose f d) where
   Precompose f % n = n `o` natId 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 :: f -> Postcompose f c
 
@@ -174,17 +171,19 @@
 type instance Cod (Postcompose f c) = Nat c (Cod f)
 type instance Postcompose f c :% g = f :.: g
 
+-- | @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@.
 instance (Functor f, Category c) => Functor (Postcompose f c) where
   Postcompose f % n = natId f `o` 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
 
+-- | @Wrap f h@ is the functor such that @Wrap f h :% g = f :.: g :.: h@, 
+--   for functors @g@ that compose with @f@ and @h@.
 instance (Functor f, Functor h) => Functor (Wrap f h) where
   Wrap f h % n = natId f `o` n `o` natId h
diff --git a/Data/Category/Omega.hs b/Data/Category/Omega.hs
--- a/Data/Category/Omega.hs
+++ b/Data/Category/Omega.hs
@@ -2,7 +2,6 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Omega
--- Copyright   :  (c) Sjoerd Visscher 2010
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  sjoerd@w3future.com
@@ -30,6 +29,7 @@
   Z2S :: Omega Z n -> Omega Z (S n)
   S   :: Omega a b -> Omega (S a) (S b)
   
+-- | The objects of omega are the natural numbers, and there's an arrow from a to b iff a <= b.
 instance Category Omega where
   
   src Z       = Z
@@ -46,6 +46,7 @@
   _       . _     = error "Other combinations should not type check"
 
 
+-- | 'Z' (zero) is the initial object of omega.
 instance HasInitialObject Omega where
   
   type InitialObject Omega = Z
@@ -62,7 +63,7 @@
 type instance BinaryProduct Omega n     Z = Z
 type instance BinaryProduct Omega (S a) (S b) = S (BinaryProduct Omega a b)
 
--- The product in omega is the minimum.
+-- | The product in omega is the minimum.
 instance HasBinaryProducts Omega where 
 
   proj1 Z     Z     = Z
@@ -88,7 +89,7 @@
 type instance BinaryCoproduct Omega n     Z     = n
 type instance BinaryCoproduct Omega (S a) (S b) = S (BinaryCoproduct Omega a b)
 
--- The coproduct in omega is the maximum.
+-- | The coproduct in omega is the maximum.
 instance HasBinaryCoproducts Omega where 
   
   inj1 Z     Z     = Z
@@ -109,10 +110,10 @@
   _     ||| _     = error "Other combinations should not type check"
 
 
--- Zero is a monoid object wrt the maximum.
+-- | Zero is a monoid object wrt the maximum.
 zeroMonoid :: MonoidObject (CoproductFunctor Omega) Z
 zeroMonoid = MonoidObject Z Z
 
--- Zero is also a comonoid object wrt the maximum.
+-- | Zero is also a comonoid object wrt the maximum.
 zeroComonoid :: ComonoidObject (CoproductFunctor Omega) Z
 zeroComonoid = ComonoidObject Z Z
diff --git a/Data/Category/Peano.hs b/Data/Category/Peano.hs
--- a/Data/Category/Peano.hs
+++ b/Data/Category/Peano.hs
@@ -2,7 +2,6 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Peano
--- Copyright   :  (c) Sjoerd Visscher 2010
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  sjoerd@w3future.com
@@ -32,6 +31,7 @@
 peanoO :: Category (~>) => Obj (Peano (~>)) a -> PeanoO (~>) a
 peanoO (PeanoA o _ _) = o
 
+-- | The 'Peano' category.
 instance HasTerminalObject (~>) => Category (Peano (~>)) where
   
   src (PeanoA s _ _) = peanoId s
@@ -40,7 +40,6 @@
   (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
 
 -- | Primitive recursion is the factorizer from the natural numbers.
@@ -48,6 +47,7 @@
 primRec z _ (Z ()) = z ()
 primRec z s (S  n) = s (primRec z s n)
   
+-- | The natural numbers are the initial object for the 'Peano' category.
 instance HasInitialObject (Peano (->)) where
   
   type InitialObject (Peano (->)) = NatNum
diff --git a/Data/Category/Presheaf.hs b/Data/Category/Presheaf.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/Presheaf.hs
@@ -0,0 +1,42 @@
+{-# LANGUAGE TypeOperators, TypeFamilies, TypeSynonymInstances, GADTs #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Category.Presheaf
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  sjoerd@w3future.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+-----------------------------------------------------------------------------
+module Data.Category.Presheaf where
+
+import Prelude (($))
+
+import Data.Category
+import Data.Category.Functor
+import Data.Category.NaturalTransformation
+import Data.Category.Limit
+import Data.Category.CartesianClosed
+import Data.Category.Yoneda
+
+
+type Presheaves (~>) = Nat (Op (~>)) (->)
+
+type PShExponential (~>) y z = (Presheaves (~>) :-*: z) :.: Opposite 
+  (   ProductFunctor (Presheaves (~>))
+  :.: Tuple2 (Presheaves (~>)) (Presheaves (~>)) y
+  :.: YonedaEmbedding (~>)
+  )
+pshExponential :: Category (~>) => Obj (Presheaves (~>)) y -> Obj (Presheaves (~>)) z -> PShExponential (~>) y z
+pshExponential y z = hom_X z :.: Opposite (ProductFunctor :.: Tuple2 y :.: yonedaEmbedding)
+
+type instance Exponential (Presheaves (~>)) y z = PShExponential (~>) y z
+
+-- | The category of presheaves on a category @C@ is cartesian closed for any @C@.
+instance Category (~>) => CartesianClosed (Presheaves (~>)) where
+  
+  apply yn@(Nat y _ _) zn@(Nat z _ _) = Nat (pshExponential yn zn :*: y) z $ \(Op i) (n, yi) -> (n ! Op i) (i, yi)
+  tuple yn zn@(Nat z _ _) = Nat z (pshExponential yn (zn *** yn)) $ \(Op i) zi -> (Nat (hom_X i) z $ \_ j2i -> (z % Op j2i) zi) *** yn
+  zn ^^^ yn = Nat (pshExponential (tgt yn) (src zn)) (pshExponential (src yn) (tgt zn)) $ \(Op i) n -> zn . n . (natId (hom_X i) *** yn)
+
+    
diff --git a/Data/Category/Product.hs b/Data/Category/Product.hs
--- a/Data/Category/Product.hs
+++ b/Data/Category/Product.hs
@@ -2,7 +2,6 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Product
--- Copyright   :  (c) Sjoerd Visscher 2010
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  sjoerd@w3future.com
diff --git a/Data/Category/RepresentableFunctor.hs b/Data/Category/RepresentableFunctor.hs
--- a/Data/Category/RepresentableFunctor.hs
+++ b/Data/Category/RepresentableFunctor.hs
@@ -2,7 +2,6 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.RepresentableFunctor
--- Copyright   :  (c) Sjoerd Visscher 2010
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  sjoerd@w3future.com
diff --git a/Data/Category/Yoneda.hs b/Data/Category/Yoneda.hs
--- a/Data/Category/Yoneda.hs
+++ b/Data/Category/Yoneda.hs
@@ -2,7 +2,6 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Yoneda
--- Copyright   :  (c) Sjoerd Visscher 2010
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  sjoerd@w3future.com
@@ -18,31 +17,25 @@
 import Data.Category.NaturalTransformation
 import Data.Category.CartesianClosed
 
--- The Yoneda emedding is just the Hom functor in curried form:
--- curry (CatA Id) (CatA Id) (CatA Id) (CatA Hom)
--- leftAdjunct (curryAdj (CatA Id)) (CatA Id) (CatA Hom)
--- (ExponentialWith (CatA Id) % (CatA Hom)) . (tuple (CatA Id) (CatA Id))
--- CatA (Wrap Hom Id) . CatA CatTuple
--- CatA (Postcompose Hom :.: CatTuple)
+type YonedaEmbedding (~>) = Postcompose (Hom (~>)) (Op (~>)) :.: ToTuple2 (~>) (Op (~>)) 
 
--- | The Yoneda embedding functor.
-yonedaEmbedding :: Category (~>) => Postcompose (Hom (~>)) (~>) :.: CatTuple (~>) (Op (~>))
-yonedaEmbedding = Postcompose Hom :.: CatTuple
+-- | The Yoneda embedding functor, @C -> Set^(C^op)@.
+yonedaEmbedding :: Category (~>) => YonedaEmbedding (~>)
+yonedaEmbedding = Postcompose Hom :.: ToTuple2
 
 
-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 % ab = \n -> n . yonedaEmbedding % Op ab
+data Yoneda ((~>) :: * -> * -> *) f = Yoneda
+type instance Dom (Yoneda (~>) f) = Op (~>)
+type instance Cod (Yoneda (~>) f) = (->)
+type instance Yoneda (~>) f :% a = Nat (Op (~>)) (->) ((~>) :-*: a) f
+-- | 'Yoneda' converts a functor @f@ into a natural transformation from the hom functor to f.
+instance (Category (~>), Functor f, Dom f ~ Op (~>), Cod f ~ (->)) => Functor (Yoneda (~>) f) where
+  Yoneda % Op ab = \n -> n . yonedaEmbedding % ab
       
   
-fromYoneda :: (Functor f, Cod f ~ (->)) => f -> Yoneda f :~> f
-fromYoneda f = Nat Yoneda f $ \a n -> (n ! a) a
-
-toYoneda :: (Functor f, Cod f ~ (->)) => f -> f :~> Yoneda f
-toYoneda f = Nat f Yoneda $ \a fa -> Nat (homX_ a) f $ \_ h -> (f % h) fa
+-- | 'fromYoneda' and 'toYoneda' are together the isomophism from the Yoneda lemma.
+fromYoneda :: (Category (~>), Functor f, Dom f ~ Op (~>), Cod f ~ (->)) => f -> Yoneda (~>) f :~> f
+fromYoneda f = Nat Yoneda f $ \(Op a) n -> (n ! Op a) a
 
--- Contravariant Yoneda:
--- type instance Yoneda f :% a = Nat (Op (Dom f)) (->) (Dom f :-*: a) f
+toYoneda   :: (Category (~>), Functor f, Dom f ~ Op (~>), Cod f ~ (->)) => f -> f :~> Yoneda (~>) f
+toYoneda   f = Nat f Yoneda $ \(Op a) fa -> Nat (hom_X a) f $ \_ h -> (f % Op h) fa
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright Sjoerd Visscher 2010
+Copyright Sjoerd Visscher 2011
 
 All rights reserved.
 
diff --git a/data-category.cabal b/data-category.cabal
--- a/data-category.cabal
+++ b/data-category.cabal
@@ -1,6 +1,6 @@
 name:                data-category
-version:             0.4
-synopsis:            Restricted categories
+version:             0.4.1
+synopsis:            Category theory
 
 description:         Data-category is a collection of categories, and some categorical constructions on them.
                      .
@@ -8,13 +8,13 @@
                      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.
                      The corresponding identity arrow of the object is used for that.
                      .
-                     See the 'Monoid', 'Boolean' and 'Product' categories for some examples.
+                     See the '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
+category:            Math
 license:             BSD3
 license-file:        LICENSE
 author:              Sjoerd Visscher
@@ -40,6 +40,7 @@
     Data.Category.Coproduct,
     Data.Category.Discrete,
     Data.Category.Yoneda,
+    Data.Category.Presheaf,
     Data.Category.Monoid,
     Data.Category.Boolean,
     Data.Category.Omega,