diff --git a/Data/Category/Adjunction.hs b/Data/Category/Adjunction.hs
--- a/Data/Category/Adjunction.hs
+++ b/Data/Category/Adjunction.hs
@@ -18,25 +18,17 @@
   , leftAdjunct
   , rightAdjunct
   
+  -- * Adjunctions as a category
+  , AdjArrow(..)
+  
   -- * Adjunctions from universal morphisms
   , initialPropAdjunction
   , terminalPropAdjunction
   
-  -- * Adjunctions to universal morphisms
+  -- * Universal morphisms from adjunctions
   , adjunctionInitialProp
   , adjunctionTerminalProp
   
-  -- * Adjunctions as a category
-  , AdjArrow(..)
-  
-  -- * (Co)limitfunctor adjunction
-  , limitAdj
-  , colimitAdj
-  
-  -- * (Co)monad of an adjunction
-  , adjunctionMonad
-  , adjunctionComonad
-  
   -- * Examples
   , contAdj
   
@@ -48,8 +40,7 @@
 import Data.Category
 import Data.Category.Functor
 import Data.Category.NaturalTransformation
-import Data.Category.Limit
-import qualified Data.Category.Monoidal as M
+import Data.Category.RepresentableFunctor
 
 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
@@ -73,31 +64,25 @@
 
 -- 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 g un _) y = initialUniversal g (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 f g _ coun) x = terminalUniversal f (g % x) (coun ! x) (leftAdjunct adj)
 
 
 
 initialPropAdjunction :: forall f g c d. (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
   => 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 :: forall a. Obj c a -> c (f :% (g :% a)) a
-    coun a = initialFactorizer (univ (g % a)) a (g % a)
-    un   :: forall a. Obj d a -> d a (g :% (f :% a))
-    un   a = initialMorphism (univ a)
+initialPropAdjunction f g univ = mkAdjunction f g 
+  (universalElement . univ)
+  (\a -> represent (univ (g % a)) a (g % a))
    
 terminalPropAdjunction :: forall f g c d. (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   :: forall a. Obj d a -> d a (g :% (f :% a))
-    un   a = terminalFactorizer (univ (f % a)) a (f % a)
-    coun :: forall a. Obj c a -> c (f :% (g :% a)) a
-    coun a = terminalMorphism (univ a)
+terminalPropAdjunction f g univ = mkAdjunction f g 
+  (\a -> unOp $ represent (univ (f % a)) (Op a) (f % a)) 
+  (universalElement . univ)
     
 
 data AdjArrow c d where
@@ -110,27 +95,9 @@
   tgt (AdjArrow (Adjunction _ _ _ _)) = AdjArrow $ mkAdjunction Id Id id id
   
   AdjArrow (Adjunction f g u c) . AdjArrow (Adjunction f' g' u' c') = AdjArrow $ 
-    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.
-limitAdj :: forall j (~>). HasLimits j (~>) 
-  => LimitFunctor j (~>) 
-  -> Adjunction (Nat j (~>)) (~>) (Diag j (~>)) (LimitFunctor j (~>))
-limitAdj LimitFunctor = terminalPropAdjunction Diag LimitFunctor (\f @ Nat{} -> limitUniv f)
-
--- | The colimit functor is left adjoint to the diagonal functor.
-colimitAdj :: forall j (~>). HasColimits j (~>) 
-  => ColimitFunctor j (~>) 
-  -> Adjunction (~>) (Nat j (~>)) (ColimitFunctor j (~>)) (Diag j (~>))
-colimitAdj ColimitFunctor = initialPropAdjunction ColimitFunctor Diag (\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) !)
+    Adjunction (f' :.: f) (g :.: g') 
+      (compAssoc (g :.: g') f' f . Precompose f % (compAssocInv g g' f' . Postcompose g % u' . idPrecompInv g) . u)
+      (c' . Precompose g' % (idPrecomp f' . Postcompose f' % c . compAssoc f' f g) . compAssocInv (f' :.: f) g g')
 
 
 
diff --git a/Data/Category/Boolean.hs b/Data/Category/Boolean.hs
--- a/Data/Category/Boolean.hs
+++ b/Data/Category/Boolean.hs
@@ -172,7 +172,7 @@
 
 -- | 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 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
diff --git a/Data/Category/CartesianClosed.hs b/Data/Category/CartesianClosed.hs
--- a/Data/Category/CartesianClosed.hs
+++ b/Data/Category/CartesianClosed.hs
@@ -19,7 +19,7 @@
 import Data.Category.Product
 import Data.Category.Limit
 import Data.Category.Adjunction
-import qualified Data.Category.Monoidal as M
+import Data.Category.Monoidal as M
 
 
 type family Exponential (~>) y z :: *
@@ -74,21 +74,23 @@
   (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 (~>) ((YonedaEmbedding (~>) :% a) :*: 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)
+  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)
+  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)
@@ -113,7 +115,6 @@
 
 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
 
diff --git a/Data/Category/Coproduct.hs b/Data/Category/Coproduct.hs
--- a/Data/Category/Coproduct.hs
+++ b/Data/Category/Coproduct.hs
@@ -24,7 +24,7 @@
   I1 :: c1 a1 b1 -> (:++:) c1 c2 (I1 a1) (I1 b1)
   I2 :: c2 a2 b2 -> (:++:) c1 c2 (I2 a2) (I2 b2)
 
--- | The product category of category @c1@ and @c2@.
+-- | The coproduct category of category @c1@ and @c2@.
 instance (Category c1, Category c2) => Category (c1 :++: c2) where
   
   src (I1 a)      = I1 (src a)
diff --git a/Data/Category/Dialg.hs b/Data/Category/Dialg.hs
--- a/Data/Category/Dialg.hs
+++ b/Data/Category/Dialg.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleInstances, FlexibleContexts, ViewPatterns #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleInstances, FlexibleContexts, ViewPatterns, ScopedTypeVariables, UndecidableInstances #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Dialg
@@ -13,13 +13,16 @@
 -----------------------------------------------------------------------------
 module Data.Category.Dialg where
 
-import Prelude hiding ((.), Functor)
+import Prelude (($), id)
 import qualified Prelude
 
 import Data.Category
 import Data.Category.Functor
+import Data.Category.NaturalTransformation
 import Data.Category.Limit
 import Data.Category.Product
+import Data.Category.Monoidal
+import qualified Data.Category.Adjunction as A
 
 
 -- | Objects of Dialg(F,G) are (F,G)-dialgebras.
@@ -117,4 +120,28 @@
   initialObject = dialgId $ Dialgebra id (Z :**: S)
   
   initialize (dialgebra -> d@(Dialgebra _ (z :**: s))) = DialgA (dialgebra initialObject) d $ primRec z s
-    
+
+
+
+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
+    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
+
+eilenbergMooreAdj :: (Functor m, Dom m ~ (~>), Cod m ~ (~>)) 
+  => Monad m -> A.Adjunction (Alg m) (~>) (EMAdjF m) (EMAdjG m)
+eilenbergMooreAdj m = A.mkAdjunction (EMAdjF m) EMAdjG
+  (\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
@@ -19,9 +19,10 @@
   , Void
   , Unit
   , Pair
+  , magicZ
   
   -- * Functors
-  , Next(..)
+  , Succ(..)
   , DiscreteDiagram(..)
     
   -- * Natural Transformations
@@ -80,19 +81,13 @@
 type Pair = Discrete (S (S Z))
 
 
-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 f) = PredDiscrete (Dom f)
-type instance Cod (Next f) = Cod f
-type instance Next f :% a = f :% S 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)
+data Succ n = Succ
+type instance Dom (Succ n) = Discrete n
+type instance Cod (Succ n) = Discrete (S n)
+type instance Succ n :% a = S a
+instance (Category (Discrete n)) => Functor (Succ n) where
+  Succ % Z     = S Z
+  Succ % (S a) = S (S a)
 
 
 infixr 7 :::
diff --git a/Data/Category/Functor.hs b/Data/Category/Functor.hs
--- a/Data/Category/Functor.hs
+++ b/Data/Category/Functor.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, FlexibleContexts, UndecidableInstances, GADTs, RankNTypes #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, FlexibleContexts, FlexibleInstances, UndecidableInstances, GADTs, RankNTypes #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Functor
@@ -25,21 +25,31 @@
   , Id(..)
   , (:.:)(..)
   , Const(..), ConstF
-  , (:*-:)(..)
-  , (:-*:)(..)
   , Opposite(..)
   , EndoHask(..)
   
-  -- * Universal properties
-  , InitialUniversal(..)
-  , TerminalUniversal(..)
-
+  -- *** Related to the product category
+  , Proj1(..)
+  , Proj2(..)
+  , (:***:)(..)
+  , DiagProd(..)
+  , Tuple1(..)
+  , Tuple2(..)
+  
+  -- *** Hom functors
+  , Hom(..)
+  , (:*-:)
+  , homX_
+  , (:-*:)
+  , hom_X
+  
 ) where
   
-import Prelude hiding (id, (.), Functor)
+import Prelude hiding ((.), Functor)
 import qualified Prelude
   
 import Data.Category
+import Data.Category.Product
 
 infixr 9 %
 infixr 9 :%
@@ -112,31 +122,7 @@
 
 type ConstF f = Const (Dom f) (Cod f)
 
-  
--- | The covariant functor Hom(X,--)
-data (:*-:) :: * -> (* -> * -> *) -> * where
-  HomX_ :: Category (~>) => Obj (~>) x -> x :*-: (~>)
-  
-type instance Dom (x :*-: (~>)) = (~>)
-type instance Cod (x :*-: (~>)) = (->)
-type instance (x :*-: (~>)) :% a = x ~> a
 
-instance Category (~>) => Functor (x :*-: (~>)) where 
-  HomX_ _ % f = (f .)
-
-
--- | The contravariant functor Hom(--,X)
-data (:-*:) :: (* -> * -> *) -> * -> * where
-  Hom_X :: Category (~>) => Obj (~>) x -> (~>) :-*: x
-
-type instance Dom ((~>) :-*: x) = Op (~>)
-type instance Cod ((~>) :-*: x) = (->)
-type instance ((~>) :-*: x) :% a = a ~> x
-
-instance Category (~>) => Functor ((~>) :-*: x) where 
-  Hom_X _ % Op f = (. f)
-
-
 -- | The dual of a functor
 data Opposite f where
   Opposite :: Functor f => f -> Opposite f
@@ -161,14 +147,89 @@
   EndoHask % f = fmap f
 
 
--- | An initial universal property, a universal morphism from x to u.
-data InitialUniversal  x u a = InitialUniversal
-  { iuObject :: Obj (Dom u) a
-  , initialMorphism :: Cod u x (u :% a)
-  , initialFactorizer :: forall y. Obj (Dom u) y -> Cod u x (u :% y) -> Dom u a y }
+-- | '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
+
+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
+
+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)
+
+instance (Functor f1, Functor f2) => Functor (f1 :***: f2) where 
+  (g1 :***: g2) % (f1 :**: f2) = (g1 % f1) :**: (g2 % f2)
   
--- | A terminal universal property, a universal morphism from u to x.
-data TerminalUniversal x u a = TerminalUniversal 
-  { tuObject :: Obj (Dom u) a
-  , terminalMorphism :: Cod u (u :% a) x
-  , terminalFactorizer :: forall y. Obj (Dom u) y -> Cod u (u :% y) x -> Dom u y a }
+  
+-- | 'DiagProd' is the diagonal functor for products.
+data DiagProd ((~>) :: * -> * -> *) = DiagProd
+
+type instance Dom (DiagProd (~>)) = (~>)
+type instance Cod (DiagProd (~>)) = (~>) :**: (~>)
+type instance DiagProd (~>) :% a = (a, a)
+
+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)
+
+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)
+
+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
+
+instance Category (~>) => Functor (Hom (~>)) where 
+  Hom % (Op f1 :**: f2) = \g -> f2 . g . f1
+
+
+type x :*-: (~>) = Hom (~>) :.: Tuple1 (Op (~>)) (~>) 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)
+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
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, FlexibleInstances, FlexibleContexts, RankNTypes, ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, FlexibleInstances, FlexibleContexts, RankNTypes, ScopedTypeVariables, UndecidableInstances  #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Kleisli
@@ -23,14 +23,13 @@
 import qualified Data.Category.Adjunction as A
 
 
-data Kleisli ((~>) :: * -> * -> *) m a b where
-  Kleisli :: Monad m -> Obj (~>) b -> a ~> (m :% b) -> Kleisli (~>) m a b
+data Kleisli m a b where
+  Kleisli :: (Functor m, Dom m ~ (~>), Cod m ~ (~>)) => 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 :: (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 (~>), Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Category (Kleisli (~>) m) where
+instance Category (Kleisli m) where
   
   src (Kleisli m _ f) = kleisliId m (src f)
   tgt (Kleisli m b _) = kleisliId m b
@@ -39,24 +38,22 @@
 
 
 
-data KleisliAdjF ((~>) :: * -> * -> *) m where
-  KleisliAdjF :: Monad m -> KleisliAdjF (~>) m
-type instance Dom (KleisliAdjF (~>) m) = (~>)
-type instance Cod (KleisliAdjF (~>) m) = Kleisli (~>) m
-type instance KleisliAdjF (~>) m :% a = a
-instance (Category (~>), Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Functor (KleisliAdjF (~>) m) where
+data KleisliAdjF m = KleisliAdjF (Monad m)
+type instance Dom (KleisliAdjF m) = Dom m
+type instance Cod (KleisliAdjF m) = Kleisli m
+type instance KleisliAdjF m :% a = a
+instance (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 :: Monad m -> KleisliAdjG (~>) m
-type instance Dom (KleisliAdjG (~>) m) = Kleisli (~>) m
-type instance Cod (KleisliAdjG (~>) m) = (~>)
-type instance KleisliAdjG (~>) m :% a = m :% a
-instance (Category (~>), Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Functor (KleisliAdjG (~>) m) where
+data KleisliAdjG m = KleisliAdjG (Monad m)
+type instance Dom (KleisliAdjG m) = Kleisli m
+type instance Cod (KleisliAdjG m) = Dom m
+type instance KleisliAdjG m :% a = m :% a
+instance (Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Functor (KleisliAdjG m) where
   KleisliAdjG m % Kleisli _ b f = (multiply m ! b) . (monadFunctor m % f)
 
-kleisliAdj :: (Functor m, Dom m ~ (~>), Cod m ~ (~>), Category (~>)) 
-  => Monad m -> A.Adjunction (Kleisli (~>) m) (~>) (KleisliAdjF (~>) m) (KleisliAdjG (~>) m)
+kleisliAdj :: (Functor m, Dom m ~ (~>), Cod m ~ (~>)) 
+  => 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
@@ -36,26 +36,16 @@
   -- * Limits
   , LimitFam
   , Limit
-  , LimitUniversal
-  , limitUniversal
-  , limit
-  , limitFactorizer
+  , HasLimits(..)
+  , LimitFunctor(..)
+  , limitAdj
   
   -- * Colimits
   , ColimitFam
   , Colimit
-  , ColimitUniversal
-  , colimitUniversal
-  , colimit
-  , colimitFactorizer
-  
-  -- * Limits of a certain type
-  , HasLimits(..)
   , HasColimits(..)
-  
-  -- ** As a functor
-  , LimitFunctor(..)
   , ColimitFunctor(..)
+  , colimitAdj
   
   -- ** Limits of type Void
   , HasTerminalObject(..)
@@ -72,21 +62,20 @@
   , CoproductFunctor(..)
   , (:+:)(..)
   
-  -- ** Limits of type Hask
-  , ForAll(..)
-  , endoHaskLimit
-  , Exists(..)
-  , endoHaskColimit
+  -- -- ** Limits of type Hask
+  -- , ForAll(..)
+  -- , Exists(..)
   
 ) where
 
 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.Adjunction
+
 import Data.Category.Product
 import Data.Category.Coproduct
 import Data.Category.Discrete
@@ -135,99 +124,57 @@
 
 type Limit f = LimitFam (Dom f) (Cod f) f
 
--- | A limit of @f@ is a universal morphism from the diagonal functor to @f@.
-type LimitUniversal f = TerminalUniversal f (DiagF f) (Limit f)
-
--- | @limitUniversal@ is a helper function to create the universal property from the limit and the limit factorizer.
-limitUniversal :: (Cod f ~ (~>)) 
-  => Cone f (Limit f)
-  -> (forall n. Cone f n -> n ~> Limit f)
-  -> LimitUniversal f
-limitUniversal l lf = TerminalUniversal
-  { tuObject           = coneVertex l
-  , terminalMorphism   = l
-  , terminalFactorizer = const lf
-  }
-
--- | A limit of the diagram @f@ is a cone of @f@.
-limit :: LimitUniversal f -> Cone f (Limit f)
-limit = terminalMorphism
-
--- | For any other cone of @f@ with vertex @n@ there exists a unique morphism from @n@ to the limit of @f@.
-limitFactorizer :: (Cod f ~ (~>)) => LimitUniversal f -> (forall n. Cone f n -> n ~> Limit f)
-limitFactorizer lu c = terminalFactorizer lu (coneVertex c) c
-
-
-
--- | Colimits in a category @(~>)@ by means of a diagram of type @j@, which is a functor from @j@ to @(~>)@.
-type family ColimitFam j (~>) f :: *
-
-type Colimit f = ColimitFam (Dom f) (Cod f) f
-
--- | A colimit of @f@ is a universal morphism from @f@ to the diagonal functor.
-type ColimitUniversal f = InitialUniversal f (DiagF f) (Colimit f)
-
--- | @colimitUniversal@ is a helper function to create the universal property from the colimit and the colimit factorizer.
-colimitUniversal :: (Cod f ~ (~>)) 
-  => Cocone f (Colimit f)
-  -> (forall n. Cocone f n -> Colimit f ~> n)
-  -> ColimitUniversal f
-colimitUniversal l lf = InitialUniversal
-  { iuObject          = coconeVertex l
-  , initialMorphism   = l
-  , initialFactorizer = const lf
-  }
-
--- | A colimit of the diagram @f@ is a co-cone of @f@.
-colimit :: ColimitUniversal f -> Cocone f (Colimit f)
-colimit = initialMorphism
-
--- | For any other co-cone of @f@ with vertex @n@ there exists a unique morphism from the colimit of @f@ to @n@.
-colimitFactorizer :: (Cod f ~ (~>)) => ColimitUniversal f -> (forall n. Cocone f n -> Colimit f ~> n)
-colimitFactorizer cu c = initialFactorizer cu (coconeVertex c) c
-
-
-
 -- | An instance of @HasLimits j (~>)@ says that @(~>)@ has all limits of type @j@.
 class (Category j, Category (~>)) => HasLimits j (~>) where
-  limitUniv :: Obj (Nat j (~>)) f -> LimitUniversal f
+  limit           :: Obj (Nat j (~>)) f -> Cone f (Limit f)
+  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 :: (* -> * -> *) -> (* -> * -> *) -> * where
-  LimitFunctor :: HasLimits j (~>) => LimitFunctor j (~>)
-
+data LimitFunctor (j :: * -> * -> *) ((~>)  :: * -> * -> *) = LimitFunctor
 type instance Dom (LimitFunctor j (~>)) = Nat j (~>)
 type instance Cod (LimitFunctor j (~>)) = (~>)
 type instance LimitFunctor j (~>) :% f = LimitFam j (~>) f
+instance HasLimits j (~>) => Functor (LimitFunctor j (~>)) where
+  LimitFunctor % n @ Nat{}  = limitFactorizer (tgt n) (n . limit (src n))
 
-instance (Category j, Category (~>)) => Functor (LimitFunctor j (~>)) where
-  LimitFunctor % n @ Nat{}  = limitFactorizer (limitUniv (tgt n)) (n . limit (limitUniv (src n)))
+-- | The limit functor is right adjoint to the diagonal functor.
+limitAdj :: HasLimits j (~>) => Adjunction (Nat j (~>)) (~>) (Diag j (~>)) (LimitFunctor j (~>))
+limitAdj = mkAdjunction diag LimitFunctor (\a -> limitFactorizer (diag % a) (diag % a)) (\f @ Nat{} -> limit f)
+  where diag = Diag -- Forces the type of all Diags to be the same.
 
 
 
+-- | Colimits in a category @(~>)@ by means of a diagram of type @j@, which is a functor from @j@ to @(~>)@.
+type family ColimitFam j (~>) f :: *
+
+type Colimit f = ColimitFam (Dom f) (Cod f) f
+
 -- | An instance of @HasColimits j (~>)@ says that @(~>)@ has all colimits of type @j@.
 class (Category j, Category (~>)) => HasColimits j (~>) where
-  colimitUniv :: Obj (Nat j (~>)) f -> ColimitUniversal f
+  colimit           :: Obj (Nat j (~>)) f -> Cocone f (Colimit f)
+  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 :: (* -> * -> *) -> (* -> * -> *) -> * where
-  ColimitFunctor :: HasColimits j (~>) => ColimitFunctor j (~>)
-  
+data ColimitFunctor (j :: * -> * -> *) ((~>)  :: * -> * -> *) = ColimitFunctor
 type instance Dom (ColimitFunctor j (~>)) = Nat j (~>)
 type instance Cod (ColimitFunctor j (~>)) = (~>)
 type instance ColimitFunctor j (~>) :% f = ColimitFam j (~>) f
-
-instance (Category j, Category (~>)) => Functor (ColimitFunctor j (~>)) where
-  ColimitFunctor % n @ Nat{}  = colimitFactorizer (colimitUniv (src n)) (colimit (colimitUniv (tgt n)) . n)
+instance HasColimits j (~>) => Functor (ColimitFunctor j (~>)) where
+  ColimitFunctor % n @ Nat{}  = colimitFactorizer (src n) (colimit (tgt n) . n)
 
+-- | The colimit functor is left adjoint to the diagonal functor.
+colimitAdj :: HasColimits j (~>) => Adjunction (~>) (Nat j (~>)) (ColimitFunctor j (~>)) (Diag j (~>))
+colimitAdj = mkAdjunction ColimitFunctor diag (\f @ Nat{} -> colimit f) (\a -> colimitFactorizer (diag % a) (diag % a)) 
+  where diag = Diag -- Forces the type of all Diags to be the same.
+  
 
 
 -- | A terminal object is the limit of the functor from /0/ to (~>).
@@ -244,9 +191,8 @@
 
 instance (HasTerminalObject (~>)) => HasLimits Void (~>) where
   
-  limitUniv (Nat f _ _) = limitUniversal
-    (voidNat (Const terminalObject) f)
-    (terminate . coneVertex)
+  limit (Nat f _ _) = voidNat (Const terminalObject) f
+  limitFactorizer Nat{} = terminate . coneVertex
 
 
 -- | @()@ is the terminal object in @Hask@.
@@ -301,9 +247,8 @@
 
 instance HasInitialObject (~>) => HasColimits Void (~>) where
   
-  colimitUniv (Nat f _ _) = colimitUniversal
-    (voidNat f (Const initialObject))
-    (initialize . coconeVertex)
+  colimit (Nat f _ _) = voidNat f (Const initialObject)
+  colimitFactorizer Nat{} = initialize . coconeVertex
 
 
 data Zero
@@ -358,30 +303,27 @@
   (&&&) :: (a ~> x) -> (a ~> y) -> (a ~> BinaryProduct (~>) x y)
 
   (***) :: (a1 ~> b1) -> (a2 ~> b2) -> (BinaryProduct (~>) a1 a2 ~> BinaryProduct (~>) b1 b2)
-  l *** r = (l . proj1 (src l) (src r)) &&& (r . proj2 (src l) (src r)) where
-
+  l *** r = (l . proj1 (src l) (src r)) &&& (r . proj2 (src l) (src r))
 
-type instance LimitFam (Discrete (S n)) (~>) f = BinaryProduct (~>) (f :% Z) (LimitFam (Discrete n) (~>) (Next f))
+type instance LimitFam (Discrete (S n)) (~>) f = BinaryProduct (~>) (f :% Z) (LimitFam (Discrete n) (~>) (f :.: Succ n))
 
 instance (HasLimits (Discrete n) (~>), HasBinaryProducts (~>)) => HasLimits (Discrete (S n)) (~>) where
   
-  limitUniv (Nat l _ _) = limitUniv' l
+  limit = limit'
     where
-      limitUniv' :: forall f. (Functor f, Dom f ~ Discrete (S n), Cod f ~ (~>), HasLimits (Discrete n) (~>), HasBinaryProducts (~>)) 
-                 => f -> LimitUniversal f
-      limitUniv' f = limitUniversal
-        (Nat (Const $ x *** y) f (\z -> unCom $ h z))
-        (\c -> c ! Z &&& limitFactorizer luNext (Nat (Const $ coneVertex c) (Next f) $ \n -> c ! S n))
+      limit' :: forall f. Obj (Nat (Discrete (S n)) (~>)) f -> Cone f (Limit f)
+      limit' l@Nat{} = Nat (Const $ x *** y) (srcF l) (\z -> unCom $ h z)
         where
-          x = f % Z
+          x = l ! Z
           y = coneVertex limNext
-          limNext = limit luNext
-          luNext = limitUniv (natId (Next f))
+          limNext = limit (l `o` natId Succ)
           h :: Obj (Discrete (S n)) z -> Com (ConstF f (LimitFam (Discrete (S n)) (~>) f)) f z
           h Z     = Com $               proj1 x y
           h (S n) = Com $ limNext ! n . proj2 x y
 
+  limitFactorizer l@Nat{} c = c ! Z &&& limitFactorizer (l `o` natId Succ) ((c `o` natId Succ) . constPostcompInv (srcF c) Succ)
 
+
 type instance BinaryProduct (->) x y = (x, y)
 
 instance HasBinaryProducts (->) where
@@ -453,28 +395,26 @@
   (|||) :: (x ~> a) -> (y ~> a) -> (BinaryCoproduct (~>) x y ~> a)
     
   (+++) :: (a1 ~> b1) -> (a2 ~> b2) -> (BinaryCoproduct (~>) a1 a2 ~> BinaryCoproduct (~>) b1 b2)
-  l +++ r = (inj1 (tgt l) (tgt r) . l) ||| (inj2 (tgt l) (tgt r) . r) where
+  l +++ r = (inj1 (tgt l) (tgt r) . l) ||| (inj2 (tgt l) (tgt r) . r)
     
 
-type instance ColimitFam (Discrete (S n)) (~>) f = BinaryCoproduct (~>) (f :% Z) (ColimitFam (Discrete n) (~>) (Next f))
+type instance ColimitFam (Discrete (S n)) (~>) f = BinaryCoproduct (~>) (f :% Z) (ColimitFam (Discrete n) (~>) (f :.: Succ n))
 
 instance (HasColimits (Discrete n) (~>), HasBinaryCoproducts (~>)) => HasColimits (Discrete (S n)) (~>) where
   
-  colimitUniv (Nat l _ _) = colimitUniv' l
+  colimit = colimit'
     where
-      colimitUniv' :: forall f. (Functor f, Dom f ~ Discrete (S n), Cod f ~ (~>), HasColimits (Discrete n) (~>), HasBinaryCoproducts (~>)) 
-                   => f -> ColimitUniversal f
-      colimitUniv' f = colimitUniversal
-        (Nat f (Const $ x +++ y) (\z -> unCom $ h z))
-        (\c -> c ! Z ||| colimitFactorizer cluNext (Nat (Next f) (Const $ coconeVertex c) $ \n -> c ! S n))
+      colimit' :: forall f. Obj (Nat (Discrete (S n)) (~>)) f -> Cocone f (Colimit f)
+      colimit' l@Nat{} = Nat (srcF l) (Const $ x +++ y) (\z -> unCom $ h z)
         where
-          x = f % Z
+          x = l ! Z
           y = coconeVertex colNext
-          colNext = colimit cluNext
-          cluNext = colimitUniv (natId (Next f))
+          colNext = colimit (l `o` natId Succ)
           h :: Obj (Discrete (S n)) z -> Com f (ConstF f (ColimitFam (Discrete (S n)) (~>) f)) z
           h Z     = Com $ inj1 x y
           h (S n) = Com $ inj2 x y . colNext ! n
+  
+  colimitFactorizer l@Nat{} c = c ! Z ||| colimitFactorizer (l `o` natId Succ) (constPostcomp (tgtF c) Succ . (c `o` natId Succ))
 
 
 type instance BinaryCoproduct (->) x y = Either x y
@@ -536,21 +476,21 @@
   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 id) EndoHask $ \_ -> unForAll)
-  (\c n -> ForAll ((c ! id) n)) -- ForAll . (c ! id)
-
-
-data Exists f = forall a. Exists (f a)
-
-type instance ColimitFam (->) (->) (EndoHask f) = Exists f
-
-endoHaskColimit :: Prelude.Functor f => ColimitUniversal (EndoHask f)
-endoHaskColimit = colimitUniversal
-  (Nat EndoHask (Const id) $ \_ -> Exists)
-  (\c (Exists fa) -> (c ! id) fa) -- (c ! id) . unExists
+-- newtype ForAll f = ForAll { unForAll :: forall a. f :% a }
+-- 
+-- type instance LimitFam (->) (->) f = ForAll f
+-- 
+-- instance HasLimits (->) (->) where
+--   
+--   limit (Nat f _ _) = Nat (Const id) f $ \_ -> unForAll
+--   limitFactorizer Nat{} c n = ForAll $ (c ! id) n -- ForAll . (c ! id)
+-- 
+-- 
+-- data Exists f = forall a. Exists (f :% a)
+-- 
+-- type instance ColimitFam (->) (->) f = Exists f
+-- 
+-- instance HasColimits (->) (->) where
+--   
+--   colimit (Nat f _ _) = Nat f (Const id) $ \_ -> Exists
+--   colimitFactorizer Nat{} 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
@@ -19,8 +19,8 @@
 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
+import Data.Category.Adjunction
+import Data.Category.Monoidal as M
 
 -- | The arrows are the values of the monoid.
 data MonoidA m a b where
@@ -71,13 +71,13 @@
 foldMap = unMonoidMorphism . rightAdjunct freeMonoidAdj (MonoidMorphism id)
 
 listMonadReturn :: a -> [a]
-listMonadReturn = unit (adjunctionMonad freeMonoidAdj) ! id
+listMonadReturn = M.unit (adjunctionMonad freeMonoidAdj) ! id
 
 listMonadJoin :: [[a]] -> [a]
-listMonadJoin = multiply (adjunctionMonad freeMonoidAdj) ! id
+listMonadJoin = M.multiply (adjunctionMonad freeMonoidAdj) ! id
 
 listComonadExtract :: Monoid m => [m] -> m
-listComonadExtract = let MonoidMorphism f = counit (adjunctionComonad freeMonoidAdj) ! MonoidMorphism id in f
+listComonadExtract = let MonoidMorphism f = M.counit (adjunctionComonad freeMonoidAdj) ! MonoidMorphism id in f
 
 listComonadDuplicate :: Monoid m => [m] -> [[m]]
-listComonadDuplicate = let MonoidMorphism f = comultiply (adjunctionComonad freeMonoidAdj) ! MonoidMorphism id in f
+listComonadDuplicate = let MonoidMorphism f = M.comultiply (adjunctionComonad freeMonoidAdj) ! MonoidMorphism id in f
diff --git a/Data/Category/Monoidal.hs b/Data/Category/Monoidal.hs
--- a/Data/Category/Monoidal.hs
+++ b/Data/Category/Monoidal.hs
@@ -18,9 +18,9 @@
 import Data.Category
 import Data.Category.Functor
 import Data.Category.NaturalTransformation
-import Data.Category.Product
+import Data.Category.Adjunction (Adjunction(Adjunction))
 import Data.Category.Limit
-
+import Data.Category.Product
 
 class Functor f => HasUnit f where
   
@@ -47,13 +47,13 @@
 
 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))
+  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
+  rightUnitorInv :: Cod f ~ (~>) => f -> Obj (~>) 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))
+  associator     :: Cod f ~ (~>) => f -> Obj (~>) a -> Obj (~>) b -> Obj (~>) c -> (f :% (f :% (a, b), c)) ~> (f :% (a, f :% (b, c)))
+  associatorInv  :: Cod f ~ (~>) => f -> Obj (~>) a -> Obj (~>) b -> Obj (~>) c -> (f :% (a, f :% (b, c))) ~> (f :% (f :% (a, b), c))
 
 
 instance (HasTerminalObject (~>), HasBinaryProducts (~>)) => TensorProduct (ProductFunctor (~>)) where
@@ -78,13 +78,13 @@
   
 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
+  leftUnitor     _ (Nat g _ _) = idPostcomp g
+  leftUnitorInv  _ (Nat g _ _) = idPostcompInv g
+  rightUnitor    _ (Nat g _ _) = idPrecomp g
+  rightUnitorInv _ (Nat g _ _) = idPrecompInv g
 
-  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
+  associator    _ (Nat f _ _) (Nat g _ _) (Nat h _ _) = compAssoc f g h
+  associatorInv _ (Nat f _ _) (Nat g _ _) (Nat h _ _) = compAssocInv f g h
 
 
 
@@ -147,3 +147,9 @@
   , comultiply = Nat f (f :.: f) dupl
   }
 
+
+adjunctionMonad :: Adjunction c d f g -> Monad (g :.: f)
+adjunctionMonad (Adjunction f g un coun) = mkMonad (g :.: f) (un !) ((Wrap g f % coun) !)
+
+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
@@ -18,10 +18,24 @@
   , (!)
   , o
   , natId
+  , srcF
+  , tgtF
 
   -- * Functor category
   , Nat(..)
   , Endo
+  
+  -- * Functor isomorphisms
+  , compAssoc
+  , compAssocInv
+  , idPrecomp
+  , idPrecompInv
+  , idPostcomp
+  , idPostcompInv
+  , constPrecomp
+  , constPrecompInv
+  , constPostcomp
+  , constPostcompInv
     
   -- * Related functors
   , FunctorCompose(..)
@@ -29,19 +43,9 @@
   , Postcompose(..)
   , Wrap(..)
   
-  -- ** Presheaves
-  , Presheaves
-  , Representable(..)
-  
-  -- ** Yoneda
-  , YonedaEmbedding(..)
-  , Yoneda(..)
-  , fromYoneda
-  , toYoneda
-  
 ) where
   
-import Prelude hiding ((.), id, Functor)
+import Prelude hiding ((.), Functor)
 
 import Data.Category
 import Data.Category.Functor
@@ -81,7 +85,12 @@
 natId :: Functor f => f -> Nat (Dom f) (Cod f) f f
 natId f = Nat f f $ \i -> f % i
 
+srcF :: Nat c d f g -> f
+srcF (Nat f _ _) = f
 
+tgtF :: Nat c d f g -> g
+tgtF (Nat _ g _) = g
+
 -- | Functor category D^C.
 -- Objects of D^C are functors from C to D.
 -- Arrows of D^C are natural transformations.
@@ -93,6 +102,41 @@
   Nat _ h ngh . Nat f _ nfg = Nat f h $ \i -> ngh i . nfg i
 
 
+compAssoc :: (Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h) 
+          => f -> g -> h -> Nat (Dom h) (Cod f) ((f :.: g) :.: h) (f :.: (g :.: h))
+compAssoc f g h = Nat ((f :.: g) :.: h) (f :.: (g :.: h)) $ \i -> f % g % h % i
+
+compAssocInv :: (Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h) 
+             => f -> g -> h -> Nat (Dom h) (Cod f) (f :.: (g :.: h)) ((f :.: g) :.: h)
+compAssocInv f g h = Nat (f :.: (g :.: h)) ((f :.: g) :.: h) $ \i -> f % g % h % i
+
+idPrecomp :: Functor f => f -> Nat (Dom f) (Cod f) (f :.: Id (Dom f)) f
+idPrecomp f = Nat (f :.: Id) f (f %)
+
+idPrecompInv :: Functor f => f -> Nat (Dom f) (Cod f) f (f :.: Id (Dom f))
+idPrecompInv f = Nat f (f :.: Id) (f %)
+
+idPostcomp :: Functor f => f -> Nat (Dom f) (Cod f) (Id (Cod f) :.: f) f
+idPostcomp f = Nat (Id :.: f) f (f %)
+
+idPostcompInv :: Functor f => f -> Nat (Dom f) (Cod f) f (Id (Cod f) :.: f)
+idPostcompInv f = Nat f (Id :.: f) (f %)
+
+
+constPrecomp :: (Category c1, Functor f) => Const c1 (Dom f) x -> f -> Nat c1 (Cod f) (f :.: Const c1 (Dom f) x) (Const c1 (Cod f) (f :% x))
+constPrecomp (Const x) f = let fx = f % x in Nat (f :.: Const x) (Const fx) $ const fx
+
+constPrecompInv :: (Category c1, Functor f) => Const c1 (Dom f) x -> f -> Nat c1 (Cod f) (Const c1 (Cod f) (f :% x)) (f :.: Const c1 (Dom f) x)
+constPrecompInv (Const x) f = let fx = f % x in Nat (Const fx) (f :.: Const x) $ const fx
+
+constPostcomp :: Functor f => Const (Cod f) c2 x -> f -> Nat (Dom f) c2 (Const (Cod f) c2 x :.: f) (Const (Dom f) c2 x)
+constPostcomp (Const x) f = Nat (Const x :.: f) (Const x) $ const x
+
+constPostcompInv :: Functor f => Const (Cod f) c2 x -> f -> Nat (Dom f) c2 (Const (Dom f) c2 x) (Const (Cod f) c2 x :.: f)
+constPostcompInv (Const x) f = Nat (Const x) (Const x :.: f) $ const x
+
+
+
 -- | The category of endofunctors.
 type Endo (~>) = Nat (~>) (~>)
 
@@ -144,47 +188,3 @@
 
 instance (Functor f, Functor h) => Functor (Wrap f h) where
   Wrap f h % n = natId f `o` n `o` natId h
-
-
-type Presheaves (~>) = Nat (Op (~>)) (->)
-
--- | 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 :: *
-  represent   :: (Dom f ~ Op c) => f -> (c :-*: RepresentingObject f) :~> f
-  unrepresent :: (Dom f ~ Op c) => f -> f :~> (c :-*: RepresentingObject f)
-
-instance Category (~>) => Representable ((~>) :-*: x) where
-  type RepresentingObject ((~>) :-*: x) = x
-  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
-
-instance Category (~>) => Functor (YonedaEmbedding (~>)) where
-  YonedaEmbedding % f = Nat (Hom_X $ src f) (Hom_X $ tgt 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 % 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/Product.hs b/Data/Category/Product.hs
--- a/Data/Category/Product.hs
+++ b/Data/Category/Product.hs
@@ -14,7 +14,6 @@
 import Prelude ()
 
 import Data.Category
-import Data.Category.Functor
 
 
 data (:**:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where
@@ -27,50 +26,3 @@
   tgt (a1 :**: a2)            = tgt a1 :**: tgt a2
   
   (a1 :**: a2) . (b1 :**: b2) = (a1 . b1) :**: (a2 . b2)
-
-
-  
-  
-    
-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
-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 Cod (Proj2 c1 c2) = c2
-type instance Proj2 c1 c2 :% (a1, a2) = a2
-instance (Category c1, Category c2) => Functor (Proj2 c1 c2) where 
-  Proj2 % (_ :**: f2) = 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, Functor f2) => Functor (f1 :***: f2) where 
-  (g1 :***: g2) % (f1 :**: f2) = (g1 % f1) :**: (g2 % f2)
-  
-data DiagProd ((~>) :: * -> * -> *) = DiagProd
-type instance Dom (DiagProd (~>)) = (~>)
-type instance Cod (DiagProd (~>)) = (~>) :**: (~>)
-type instance DiagProd (~>) :% a = (a, a)
-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/RepresentableFunctor.hs b/Data/Category/RepresentableFunctor.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/RepresentableFunctor.hs
@@ -0,0 +1,74 @@
+{-# LANGUAGE TypeOperators, TypeFamilies, RankNTypes #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Category.RepresentableFunctor
+-- Copyright   :  (c) Sjoerd Visscher 2010
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  sjoerd@w3future.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+-----------------------------------------------------------------------------
+module Data.Category.RepresentableFunctor where
+
+import Prelude (($), id)
+
+import Data.Category
+import Data.Category.Functor
+
+
+data Representable f repObj = Representable
+  { representedFunctor :: f
+  , representingObject :: Obj (Dom f) repObj
+  , represent          :: (Dom f ~ (~>), Cod f ~ (->)) => Obj (~>) z -> f :% z -> repObj ~> z
+  , universalElement   :: (Dom f ~ (~>), Cod f ~ (->)) => f :% repObj
+  }
+
+unrepresent :: (Functor f, Dom f ~ (~>), Cod f ~ (->)) => Representable f repObj -> repObj ~> z -> f :% z
+unrepresent rep h = representedFunctor rep % h $ universalElement rep
+
+covariantHomRepr :: Category (~>) => Obj (~>) x -> Representable (x :*-: (~>)) x
+covariantHomRepr x = Representable
+  { representedFunctor = homX_ x
+  , representingObject = x
+  , represent          = \_ -> id
+  , universalElement   = x
+  }
+
+contravariantHomRepr :: Category (~>) => Obj (~>) x -> Representable ((~>) :-*: x) x
+contravariantHomRepr x = Representable
+  { representedFunctor = hom_X x
+  , representingObject = Op x
+  , represent          = \_ h -> Op h
+  , universalElement   = x
+  }
+
+type InitialUniversal x u a = Representable ((x :*-: Cod u) :.: u) a
+-- | An initial universal property, a universal morphism from x to u.
+initialUniversal :: Functor u
+                 => u 
+                 -> Obj (Dom u) a 
+                 -> Cod u x (u :% a) 
+                 -> (forall y. Obj (Dom u) y -> Cod u x (u :% y) -> Dom u a y) 
+                 -> InitialUniversal x u a
+initialUniversal u obj mor factorizer = Representable
+  { representedFunctor = homX_ (src mor) :.: u
+  , representingObject = obj
+  , represent          = factorizer
+  , universalElement   = mor
+  }
+  
+type TerminalUniversal x u a = Representable ((Cod u :-*: x) :.: Opposite u) a
+-- | A terminal universal property, a universal morphism from u to x.
+terminalUniversal :: Functor u
+                  => u 
+                  -> Obj (Dom u) a
+                  -> Cod u (u :% a) x
+                  -> (forall y. Obj (Dom u) y -> Cod u (u :% y) x -> Dom u y a) 
+                  -> TerminalUniversal x u a
+terminalUniversal u obj mor factorizer = Representable
+  { representedFunctor = hom_X (tgt mor) :.: Opposite u
+  , representingObject = Op obj
+  , represent          = \(Op y) f -> Op (factorizer y f)
+  , universalElement   = mor
+  }
diff --git a/Data/Category/Yoneda.hs b/Data/Category/Yoneda.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/Yoneda.hs
@@ -0,0 +1,48 @@
+{-# LANGUAGE TypeOperators, TypeFamilies #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Category.Yoneda
+-- Copyright   :  (c) Sjoerd Visscher 2010
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  sjoerd@w3future.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+-----------------------------------------------------------------------------
+module Data.Category.Yoneda where
+
+import Prelude (($))
+
+import Data.Category
+import Data.Category.Functor
+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)
+
+-- | The Yoneda embedding functor.
+yonedaEmbedding :: Category (~>) => Postcompose (Hom (~>)) (~>) :.: CatTuple (~>) (Op (~>))
+yonedaEmbedding = Postcompose Hom :.: CatTuple
+
+
+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
+      
+  
+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
+
+-- Contravariant Yoneda:
+-- type instance Yoneda f :% a = Nat (Op (Dom f)) (->) (Dom f :-*: a) f
diff --git a/data-category.cabal b/data-category.cabal
--- a/data-category.cabal
+++ b/data-category.cabal
@@ -1,5 +1,5 @@
 name:                data-category
-version:             0.3.1.1
+version:             0.4
 synopsis:            Restricted categories
 
 description:         Data-category is a collection of categories, and some categorical constructions on them.
@@ -31,6 +31,7 @@
     Data.Category,
     Data.Category.Functor,
     Data.Category.NaturalTransformation,
+    Data.Category.RepresentableFunctor,
     Data.Category.Adjunction,
     Data.Category.Limit,
     Data.Category.Monoidal,
@@ -38,6 +39,7 @@
     Data.Category.Product,
     Data.Category.Coproduct,
     Data.Category.Discrete,
+    Data.Category.Yoneda,
     Data.Category.Monoid,
     Data.Category.Boolean,
     Data.Category.Omega,