diff --git a/Data/Category.hs b/Data/Category.hs
--- a/Data/Category.hs
+++ b/Data/Category.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, RankNTypes #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category
@@ -11,144 +11,53 @@
 -----------------------------------------------------------------------------
 module Data.Category (
   
-  -- * Categories
-    CategoryO(..)
-  , CategoryA(..)
-  , Apply(..)
-  , Obj, obj
-  
-  -- * Functors
-  , F
-  , Dom
-  , Cod
-  , FunctorA(..)
-  , ContraFunctorA(..)
-  
-  -- ** Functor instances
-  , Id(..)
-  , (:.:)(..)
-  , Const(..)
-  , (:*-:)(..)
-  , (:-*:)(..)
-  
-  -- * Natural transformations
-  , Nat
-  , (:~>)
-  , Component
-  
-  -- * Universal arrows
-  , InitialUniversal(..)
-  , TerminalUniversal(..)
-  
-  -- * Adjunctions
-  , Adjunction(..)
+  -- * Category
+    Category(..)
+  , Obj(..)
   
-  ) where
-
-import Prelude hiding ((.), id, ($))
-
-
--- | An instance CategoryO (~>) a declares a as an object of the category (~>).
-class CategoryO (~>) a where
-  id  :: a ~> a
-  (!) :: Nat (~>) d f g -> Obj a -> Component f g a
-
--- | An instance CategoryA (~>) a b c defines composition of the arrows a ~> b and b ~> c.
-class (CategoryO (~>) a, CategoryO (~>) b, CategoryO (~>) c) => CategoryA (~>) a b c where
-  (.) :: b ~> c -> a ~> b -> a ~> c
-
-class (CategoryO (~>) a, CategoryO (~>) b) => Apply (~>) a b where
-  -- Would have liked to use ($) here, but that causes GHC to crash.
-  -- http://hackage.haskell.org/trac/ghc/ticket/3297
-  ($$) :: a ~> b -> a -> b
-
--- | The type synonym @Obj a@, when used as the type of a function argument,
--- is a promise that the value of the argument is not used, and only the type.
--- This is used to pass objects (which are types) to functions.
-type Obj a = a
--- | 'obj' is a synonym for 'undefined'. When you need to pass an object to
--- a function, you can use @(obj :: type)@.
-obj :: Obj a
-obj = undefined
+  -- * Opposite category
+  , Op(..)
+    
+) where
 
+import Prelude (($))
+import qualified Prelude
 
 
--- | Functors are represented by a type tag. The type family 'F' turns the tag into the actual functor.
-type family F ftag a :: *
--- | The domain, or source category, of the functor.
-type family Dom ftag :: * -> * -> *
--- | The codomain, or target category, of the funcor.
-type family Cod ftag :: * -> * -> *
+-- | An instance of @Category (~>)@ declares the arrow @(~>)@ as a category.
+class Category (~>) where
+  
+  data Obj (~>) :: * -> *
 
--- | The mapping of arrows by covariant functors.
--- To make this type check, we need to pass the type tag along.
-class (CategoryO (Dom ftag) a, CategoryO (Dom ftag) b) 
-  => FunctorA ftag a b where
-  (%) :: Obj ftag -> Dom ftag a b -> Cod ftag (F ftag a) (F ftag b)
+  src :: a ~> b -> Obj (~>) a
+  tgt :: a ~> b -> Obj (~>) b
 
--- | The mapping of arrows by contravariant functors.
-class (CategoryO (Dom ftag) a, CategoryO (Dom ftag) b) 
-  => ContraFunctorA ftag a b where
-  (-%) :: Obj ftag -> Dom ftag a b -> Cod ftag (F ftag b) (F ftag a)
+  id  :: Obj (~>) a -> a ~> a
+  (.) :: b ~> c -> a ~> b -> a ~> c
 
 
--- | The identity functor on (~>)
-data Id ((~>) :: * -> * -> *) = Id
-type instance F (Id (~>)) a = a
-type instance Dom (Id (~>)) = (~>)
-type instance Cod (Id (~>)) = (~>)
-instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Id (~>)) a b where
-  _ % f = f
-
--- | The composition of two functors.
-data (g :.: h) = g :.: h
-type instance F (g :.: h) a = F g (F h a)
-type instance Dom (g :.: h) = Dom h
-type instance Cod (g :.: h) = Cod g
-instance (FunctorA g (F h a) (F h b), FunctorA h a b, Cod h ~ Dom g) => FunctorA (g :.: h) a b where
-   _ % f = (obj :: g) % ((obj :: h) % f)
-
--- | The constant functor.
-data Const (c1 :: * -> * -> *) (c2 :: * -> * -> *) x = Const
-type instance F (Const c1 c2 x) a = x
-type instance Dom (Const c1 c2 x) = c1
-type instance Cod (Const c1 c2 x) = c2
-instance (CategoryO c1 a, CategoryO c1 b, CategoryO c2 x) => FunctorA (Const c1 c2 x) a b where
-  _ % _ = id
+-- | The category with Haskell types as objects and Haskell functions as arrows.
+instance Category (->) where
   
--- | The covariant functor Hom(X,--)
-data (x :*-: ((~>) :: * -> * -> *)) = HomX_
-type instance F (x :*-: (~>)) a = x ~> a
-type instance Dom (x :*-: (~>)) = (~>)
-type instance Cod (x :*-: (~>)) = (->)
-instance (CategoryO (~>) a, CategoryO (~>) b, CategoryA (~>) x a b) => FunctorA (x :*-: (~>)) a b where
-  _ % f = (f .)
-
--- | The contravariant functor Hom(--,X)
-data (((~>) :: * -> * -> *) :-*: x) = Hom_X
-type instance F ((~>) :-*: x) a = a ~> x
-type instance Dom ((~>) :-*: x) = (~>)
-type instance Cod ((~>) :-*: x) = (->)
-instance (CategoryO (~>) a, CategoryO (~>) b, CategoryA (~>) a b x) => ContraFunctorA ((~>) :-*: x) a b where
-  _ -% f = (. f)
+  data Obj (->) a = HaskO
   
+  src _ = HaskO
+  tgt _ = HaskO
   
-data family Nat (c :: * -> * -> *) (d :: * -> * -> *) (f :: *) (g :: *) :: *
+  id _  = Prelude.id  
+  (.)   = (Prelude..)    
 
--- | @f :~> g@ is a natural transformation from functor f to functor g.
-type f :~> g = (c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => Nat c d f g
 
--- | Natural transformations are built up of components, 
--- one for each object @z@ in the domain category of @f@ and @g@.
--- This type synonym can be used when creating data instances of @Nat@.
-type Component f g z = Cod f (F f z) (F g z)
-  
-type InitMorF x u = (x :*-: Cod u) :.: u
-type TermMorF x u = (Cod u :-*: x) :.: u
-data InitialUniversal  x u a = InitialUniversal  (F (InitMorF x u) a) (InitMorF x u :~> (a :*-: Dom u))
-data TerminalUniversal x u a = TerminalUniversal (F (TermMorF x u) a) (TermMorF x u :~> (Dom u :-*: a))
+data Op :: (* -> * -> *) -> * -> * -> * where
+  Op :: (a ~> b) -> Op (~>) b a
 
-data Adjunction f g = Adjunction 
-  { unit :: Id (Dom f) :~> (g :.: f)
-  , counit :: (f :.: g) :~> Id (Dom g)
-  }
+-- | @Op (~>)@ is opposite category of the category @(~>)@.
+instance Category (~>) => Category (Op (~>)) where
+  
+  data Obj (Op (~>)) a = OpObj (Obj (~>) a)
+  
+  src (Op a)      = OpObj $ tgt a
+  tgt (Op a)      = OpObj $ src a
+  
+  id (OpObj x)    = Op $ id x
+  (Op a) . (Op b) = Op $ b . a
diff --git a/Data/Category/Adjunction.hs b/Data/Category/Adjunction.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/Adjunction.hs
@@ -0,0 +1,114 @@
+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleContexts, ScopedTypeVariables, RankNTypes #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Category.Adjunction
+-- Copyright   :  (c) Sjoerd Visscher 2010
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  sjoerd@w3future.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+-----------------------------------------------------------------------------
+module Data.Category.Adjunction where
+  
+import Prelude hiding ((.), id, Functor)
+import Control.Monad.Instances()
+
+import Data.Category
+import Data.Category.Functor
+import Data.Category.NaturalTransformation
+import Data.Category.Limit
+
+data Adjunction c d f g where
+  Adjunction :: (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) =>
+    f -> g -> Nat d d (Id d) (g :.: f) -> Nat c c (f :.: g) (Id c) -> Adjunction c d f g
+
+mkAdjunction :: (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
+  => f -> g 
+  -> (forall a. Obj d a -> Component (Id d) (g :.: f) a) 
+  -> (forall a. Obj c a -> Component (f :.: g) (Id c) a)
+  -> Adjunction c d f g
+mkAdjunction f g un coun = Adjunction f g (Nat Id (g :.: f) un) (Nat (f :.: g) Id coun)
+
+unit :: Adjunction c d f g -> Id d :~> (g :.: f)
+unit (Adjunction _ _ u _) = u
+counit :: Adjunction c d f g -> (f :.: g) :~> Id c
+counit (Adjunction _ _ _ c) = c
+
+leftAdjunct :: Adjunction c d f g -> Obj d a -> c (f :% a) b -> d a (g :% b)
+leftAdjunct (Adjunction _ g un _) i h = (g % h) . (un ! i)
+rightAdjunct :: Adjunction c d f g -> Obj c b -> d a (g :% b) -> c (f :% a) b
+rightAdjunct (Adjunction f _ _ coun) i h = (coun ! i) . (f % h)
+
+-- 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)
+
+-- 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)
+
+
+
+initialPropAdjunction :: (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 a = let ga = g %% a in initialFactorizer (univ ga) a (id ga)
+    un   a = initialMorphism (univ a)
+    
+terminalPropAdjunction :: (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
+  => f -> g -> (forall x. Obj c x -> TerminalUniversal x f (g :% x)) -> Adjunction c d f g
+terminalPropAdjunction f g univ = mkAdjunction f g un coun
+  where
+    un   a = let fa = f %% a in terminalFactorizer (univ fa) a (id fa)
+    coun a = terminalMorphism (univ a)
+    
+
+data AdjArrow c d where
+  AdjArrow :: (Category c, Category d) => Adjunction c d f g -> AdjArrow (CatW c) (CatW d)
+
+instance Category AdjArrow where
+  
+  data Obj AdjArrow a where
+    AdjCategory :: Category (~>) => Obj AdjArrow (CatW (~>))
+  
+  src (AdjArrow _) = AdjCategory
+  tgt (AdjArrow _) = AdjCategory
+  
+  id AdjCategory = AdjArrow $ mkAdjunction Id Id id id
+  
+  AdjArrow (Adjunction f g u c) . AdjArrow (Adjunction f' g' u' c') = AdjArrow $ 
+    Adjunction (f' :.: f) (g :.: g') (wrap g f u' . u) (c' . cowrap f' g' c)
+
+
+wrap :: (Functor g, Functor f, Dom g ~ Dom f', Dom g ~ Cod f) 
+  => g -> f -> Nat (Dom f') (Dom f') (Id (Dom f')) (g' :.: f') -> (g :.: f) :~> ((g :.: g') :.: (f' :.: f))
+wrap g f (Nat Id (g' :.: f') n) = Nat (g :.: f) ((g :.: g') :.: (f' :.: f)) $ (g %) . n . (f %%)
+
+cowrap :: (Functor f', Functor g', Dom f' ~ Dom g, Dom f' ~ Cod g') 
+  => f' -> g' -> Nat (Dom g) (Dom g) (f :.: g) (Id (Dom g)) -> ((f' :.: f) :.: (g :.: g')) :~> (f' :.: g')
+cowrap f' g' (Nat (f :.: g) Id n) = Nat ((f' :.: f) :.: (g :.: g')) (f' :.: g') $ (f' %) . n . (g' %%)
+
+
+curryAdj :: Adjunction (->) (->) (EndoHask ((,) e)) (EndoHask ((->) e))
+curryAdj = mkAdjunction EndoHask EndoHask (\HaskO -> \a e -> (e, a)) (\HaskO -> \(e, f) -> f e)
+
+
+-- | 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 univ
+  where
+    univ :: Obj (Nat j (~>)) f -> TerminalUniversal f (Diag j (~>)) (LimitFam j (~>) f)
+    univ f @ NatO{} = 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 univ
+  where
+    univ :: Obj (Nat j (~>)) f -> InitialUniversal f (Diag j (~>)) (ColimitFam j (~>) f)
+    univ f @ NatO{} = colimitUniv f
diff --git a/Data/Category/Alg.hs b/Data/Category/Alg.hs
deleted file mode 100644
--- a/Data/Category/Alg.hs
+++ /dev/null
@@ -1,53 +0,0 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, RankNTypes #-}
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Category.Alg
--- Copyright   :  (c) Sjoerd Visscher 2010
--- License     :  BSD-style (see the file LICENSE)
---
--- Maintainer  :  sjoerd@w3future.com
--- Stability   :  experimental
--- Portability :  non-portable
---
--- Alg(F), the category of F-algebras and F-homomorphisms.
------------------------------------------------------------------------------
-module Data.Category.Alg where
-
-import Prelude hiding ((.), id)
-
-import Data.Category
-import Data.Category.Void
-import Data.Category.Hask
-
--- | Objects of Alg(F) are F-algebras.
-newtype Algebra f a = Algebra (Dom f (F f a) a)
-
--- | Arrows of Alg(F) are F-homomorphisms.
-data family Alg f a b :: *
-data instance Alg f (Algebra f a) (Algebra f b) = AlgA (Dom f a b)
-
-newtype instance Nat (Alg f) d g h = 
-  AlgNat { unAlgNat :: forall a. Obj (Algebra f a) -> Component g h (Algebra f a) }
-
-instance (Dom f ~ (~>), Cod f ~ (~>), CategoryO (~>) a) => CategoryO (Alg f) (Algebra f a) where
-  id = AlgA id
-  (!) = unAlgNat
-instance (Dom f ~ (~>), Cod f ~ (~>), CategoryA (~>) a b c) => CategoryA (Alg f) (Algebra f a) (Algebra f b) (Algebra f c) where
-  AlgA f . AlgA g = AlgA (f . g)
-
--- | The initial F-algebra is the initial object in the category of F-algebras.
-type InitialFAlgebra f = InitialObject (Alg f)
-
--- | A catamorphism of an F-algebra is the arrow to it from the initial F-algebra.
-type Cata f a = Algebra f a -> Alg f (InitialFAlgebra f) (Algebra f a)
-
--- | FixF provides the initial F-algebra for endofunctors in Hask.
-newtype FixF f = InF { outF :: f (FixF f) }
-
--- | Catamorphisms for endofunctors in Hask.
-cataHask :: Functor f => Cata (EndoHask f) a
-cataHask (Algebra f) = AlgA $ cata f where cata f = f . fmap (cata f) . outF 
-
-instance Functor f => VoidColimit (Alg (EndoHask f)) where
-  type InitialObject (Alg (EndoHask f)) = Algebra (EndoHask f) (FixF f)
-  voidColimit = InitialUniversal VoidNat (AlgNat $ \f VoidNat -> cataHask f)
diff --git a/Data/Category/Boolean.hs b/Data/Category/Boolean.hs
--- a/Data/Category/Boolean.hs
+++ b/Data/Category/Boolean.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, GADTs, EmptyDataDecls, FlexibleInstances #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Boolean
@@ -15,80 +15,109 @@
 -----------------------------------------------------------------------------
 module Data.Category.Boolean where
 
-import Prelude hiding ((.), id)
+import Prelude hiding ((.), id, Functor)
 
 import Data.Category
-import Data.Category.Void
-import Data.Category.Pair
+import Data.Category.Limit
 
--- | 'Fls', the object representing false.
-data Fls = Fls deriving Show
--- | 'Tru', the object representing true.
-data Tru = Tru deriving Show
 
--- | The arrows of the boolean category.
-data family Boolean a b :: *
-data instance Boolean Fls Fls = IdFls
-data instance Boolean Tru Tru = IdTru
-data instance Boolean Fls Tru = FlsTru
+data BF
+data BT
+  
+data Boolean a b where
+  IdFls  :: Boolean BF BF
+  FlsTru :: Boolean BF BT
+  IdTru  :: Boolean BT BT
 
-data instance Nat Boolean d f g = 
-  BooleanNat (Component f g Fls) (Component f g Tru)
+-- | @Boolean@ is the category with true and false as objects, and an arrow from false to true.
+instance Category Boolean where
+  data Obj Boolean a where
+    Fls :: Obj Boolean BF
+    Tru :: Obj Boolean BT
+  
+  src IdFls  = Fls
+  src FlsTru = Fls
+  src IdTru  = Tru
+  
+  tgt IdFls  = Fls
+  tgt FlsTru = Tru
+  tgt IdTru  = Tru
+  
+  id Fls     = IdFls
+  id Tru     = IdTru
+  
+  IdFls  . IdFls  = IdFls
+  FlsTru . IdFls  = FlsTru
+  IdTru  . FlsTru = FlsTru
+  IdTru  . IdTru  = IdTru
+  _      . _      = error "Other combinations should not type check"
 
-instance CategoryO Boolean Fls where
-  id = IdFls
-  BooleanNat f _ ! Fls = f
-instance CategoryO Boolean Tru where
-  id = IdTru
-  BooleanNat _ t ! Tru = t
 
-instance CategoryA Boolean Fls Fls Fls where
-  IdFls . IdFls = IdFls
-instance CategoryA Boolean Fls Fls Tru where
-  FlsTru . IdFls = FlsTru  
-instance CategoryA Boolean Fls Tru Tru where
-  IdTru . FlsTru = FlsTru  
-instance CategoryA Boolean Tru Tru Tru where
-  IdTru . IdTru = IdTru
-    
-instance Apply Boolean Fls Fls where
-  IdFls $$ Fls = Fls
-instance Apply Boolean Fls Tru where
-  FlsTru $$ Fls = Tru
-instance Apply Boolean Tru Tru where
-  IdTru $$ Tru = Tru
+-- | False is the initial object in the Boolean category.
+instance HasInitialObject Boolean where
+  type InitialObject Boolean = BF
+  initialObject = Fls
+  initialize Fls = IdFls
+  initialize Tru = FlsTru
   
+-- | True is the terminal object in the Boolean category.
+instance HasTerminalObject Boolean where
+  type TerminalObject Boolean = BT
+  terminalObject = Tru
+  terminate Fls = FlsTru
+  terminate Tru = IdTru
 
 
-instance VoidColimit Boolean where
-  type InitialObject Boolean = Fls
-  voidColimit = InitialUniversal VoidNat (BooleanNat (\VoidNat -> IdFls) (\VoidNat -> FlsTru))
-instance VoidLimit Boolean where
-  type TerminalObject Boolean = Tru
-  voidLimit = TerminalUniversal VoidNat (BooleanNat (\VoidNat -> FlsTru) (\VoidNat -> IdTru))
+type instance BinaryProduct Boolean BF BF = BF
+type instance BinaryProduct Boolean BF BT = BF
+type instance BinaryProduct Boolean BT BF = BF
+type instance BinaryProduct Boolean BT BT = BT
 
-instance PairLimit Boolean Fls Fls where 
-  type Product Fls Fls = Fls
-  pairLimit = TerminalUniversal (IdFls :***: IdFls) (BooleanNat (! Fst) (! Snd))
-instance PairLimit Boolean Fls Tru where 
-  type Product Fls Tru = Fls
-  pairLimit = TerminalUniversal (IdFls :***: FlsTru) (BooleanNat (! Fst) (! Fst))
-instance PairLimit Boolean Tru Fls where 
-  type Product Tru Fls = Fls
-  pairLimit = TerminalUniversal (FlsTru :***: IdFls) (BooleanNat (! Snd) (! Snd))
-instance PairLimit Boolean Tru Tru where 
-  type Product Tru Tru = Tru
-  pairLimit = TerminalUniversal (IdTru :***: IdTru) (BooleanNat (! Fst) (! Snd))
+instance HasBinaryProducts Boolean where 
+  
+  product Fls Fls = Fls
+  product Fls Tru = Fls
+  product Tru Fls = Fls
+  product Tru Tru = Tru
+  
+  proj Fls Fls = (IdFls , IdFls)
+  proj Fls Tru = (IdFls , FlsTru)
+  proj Tru Fls = (FlsTru, IdFls)
+  proj Tru Tru = (IdTru , IdTru)
+  
+  IdFls  &&& IdFls  = IdFls
+  IdFls  &&& FlsTru = IdFls
+  FlsTru &&& IdFls  = IdFls
+  FlsTru &&& FlsTru = FlsTru
+  IdTru  &&& IdTru  = IdTru
+  _      &&& _      = error "Other combinations should not type check"
 
-instance PairColimit Boolean Fls Fls where 
-  type Coproduct Fls Fls = Fls
-  pairColimit = InitialUniversal (IdFls :***: IdFls) (BooleanNat (! Fst) (! Snd))
-instance PairColimit Boolean Fls Tru where 
-  type Coproduct Fls Tru = Tru
-  pairColimit = InitialUniversal (FlsTru :***: IdTru) (BooleanNat (! Snd) (! Snd))
-instance PairColimit Boolean Tru Fls where 
-  type Coproduct Tru Fls = Tru
-  pairColimit = InitialUniversal (IdTru :***: FlsTru) (BooleanNat (! Fst) (! Fst))
-instance PairColimit Boolean Tru Tru where 
-  type Coproduct Tru Tru = Tru
-  pairColimit = InitialUniversal (IdTru :***: IdTru) (BooleanNat (! Fst) (! Snd))
+
+type instance BinaryCoproduct Boolean BF BF = BF
+type instance BinaryCoproduct Boolean BF BT = BT
+type instance BinaryCoproduct Boolean BT BF = BT
+type instance BinaryCoproduct Boolean BT BT = BT
+
+instance HasBinaryCoproducts Boolean where 
+  
+  coproduct Fls Fls = Fls
+  coproduct Fls Tru = Tru
+  coproduct Tru Fls = Tru
+  coproduct Tru Tru = Tru
+  
+  inj Fls Fls = (IdFls , IdFls)
+  inj Fls Tru = (FlsTru, IdTru)
+  inj Tru Fls = (IdTru , FlsTru)
+  inj Tru Tru = (IdTru , IdTru)
+  
+  IdFls  ||| IdFls  = IdFls
+  FlsTru ||| FlsTru = FlsTru
+  FlsTru ||| IdTru  = IdTru
+  IdTru  ||| FlsTru = IdTru
+  IdTru  ||| IdTru  = IdTru
+  _      ||| _      = error "Other combinations should not type check"
+
+
+instance Show (Obj Boolean a) where
+  show Fls = "Fls"
+  show Tru = "Tru"
diff --git a/Data/Category/Comma.hs b/Data/Category/Comma.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/Comma.hs
@@ -0,0 +1,48 @@
+{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, GADTs, FlexibleContexts, FlexibleInstances #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Category.Comma
+-- Copyright   :  (c) Sjoerd Visscher 2010
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  sjoerd@w3future.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Comma categories.
+-----------------------------------------------------------------------------
+module Data.Category.Comma where
+
+import Prelude()
+
+import Data.Category
+import Data.Category.Functor
+import Data.Category.NaturalTransformation
+
+
+data (:/\:) :: * -> * -> * -> * -> * where 
+  CommaA :: 
+    Obj (t :/\: s) (a, b) ->
+    Dom t a a' -> 
+    Dom s b b' -> 
+    Obj (t :/\: s) (a', b') ->
+    (t :/\: s) (a, b) (a', b')
+
+instance (Category (Dom t), Category (Dom s)) => Category (t :/\: s) where
+    
+  data Obj (t :/\: s) x where
+    CommaO :: (Cod t ~ (~>), Cod s ~ (~>))
+      => Obj (Dom t) a -> (t :% a ~> s :% b) -> Obj (Dom s) b -> Obj (t :/\: s) (a, b)
+    
+  src (CommaA so _ _ _) = so
+  tgt (CommaA _ _ _ to) = to
+  
+  id x@(CommaO a _ b)                     = CommaA x  (id a)   (id b)   x
+  (CommaA _ g h to) . (CommaA so g' h' _) = CommaA so (g . g') (h . h') to
+
+
+type (f `ObjectsFUnder` a) = ConstF f a :/\: f
+type (f `ObjectsFOver`  a) = f :/\: ConstF f a
+
+type (c `ObjectsUnder` a) = Id c `ObjectsFUnder` a
+type (c `ObjectsOver`  a) = Id c `ObjectsFOver`  a
diff --git a/Data/Category/Dialg.hs b/Data/Category/Dialg.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/Dialg.hs
@@ -0,0 +1,121 @@
+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleInstances, FlexibleContexts #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Category.Dialg
+-- Copyright   :  (c) Sjoerd Visscher 2010
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  sjoerd@w3future.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Dialg(F,G), the category of (F,G)-dialgebras and (F,G)-homomorphisms.
+-----------------------------------------------------------------------------
+module Data.Category.Dialg where
+
+import Prelude hiding ((.), id, Functor)
+import qualified Prelude
+
+import Data.Category
+import Data.Category.Functor
+import Data.Category.Limit
+import Data.Category.Product
+
+
+-- | Objects of Dialg(F,G) are (F,G)-dialgebras.
+type Dialgebra f g a = Obj (Dialg f g) a
+
+-- | Arrows of Dialg(F,G) are (F,G)-homomorphisms.
+data Dialg f g a b where
+  DialgA :: (Category c, Category d, Dom f ~ c, Dom g ~ c, Cod f ~ d, Cod g ~ d, Functor f, Functor g) 
+    => Dialgebra f g a -> Dialgebra f g b -> c a b -> Dialg f g a b
+
+
+instance Category (Dialg f g) where
+  
+  data Obj (Dialg f g) a where
+    Dialgebra :: (Category c, Category d, Dom f ~ c, Dom g ~ c, Cod f ~ d, Cod g ~ d, Functor f, Functor g) 
+      => Obj c a -> d (f :% a) (g :% a) -> Obj (Dialg f g) a
+      
+  src (DialgA s _ _) = s
+  tgt (DialgA _ t _) = t
+  
+  id x@(Dialgebra a _)        = DialgA x x $ id a
+  DialgA _ t f . DialgA s _ g = DialgA s t $ f . g
+
+
+
+type Alg f = Dialg f (Id (Dom f))
+type Algebra f a = Dialgebra f (Id (Dom f)) a
+type Coalg f = Dialg (Id (Dom f)) f
+type Coalgebra f a = Dialgebra (Id (Dom f)) f a
+
+-- | The initial F-algebra is the initial object in the category of F-algebras.
+type InitialFAlgebra f = InitialObject (Alg f)
+
+-- | The terminal F-coalgebra is the terminal object in the category of F-coalgebras.
+type TerminalFAlgebra f = TerminalObject (Coalg f)
+
+-- | A catamorphism of an F-algebra is the arrow to it from the initial F-algebra.
+type Cata f a = Algebra f a -> Alg f (InitialFAlgebra f) a
+
+-- | A anamorphism of an F-coalgebra is the arrow from it to the terminal F-coalgebra.
+type Ana f a = Coalgebra f a -> Coalg f a (TerminalFAlgebra f)
+
+
+
+
+-- | 'FixF' provides the initial F-algebra for endofunctors in Hask.
+newtype FixF f = InF { outF :: f (FixF f) }
+
+-- | Catamorphisms for endofunctors in Hask.
+cataHask :: Prelude.Functor f => Cata (EndoHask f) a
+cataHask a@(Dialgebra HaskO f) = DialgA initialObject a $ cata f where cata f = f . fmap (cata f) . outF 
+
+-- -- | Anamorphisms for endofunctors in Hask.
+anaHask :: Prelude.Functor f => Ana (EndoHask f) a
+anaHask a@(Dialgebra HaskO f) = DialgA a terminalObject $ ana f where ana f = InF . fmap (ana f) . f 
+
+
+instance Prelude.Functor f => HasInitialObject (Dialg (EndoHask f) (Id (->))) where
+  
+  type InitialObject (Dialg (EndoHask f) (Id (->))) = FixF f
+  
+  initialObject = Dialgebra HaskO InF
+  initialize = cataHask
+  
+instance  Prelude.Functor f => HasTerminalObject (Dialg (Id (->)) (EndoHask f)) where
+
+  type TerminalObject (Dialg (Id (->)) (EndoHask f)) = FixF f
+  
+  terminalObject = Dialgebra HaskO outF
+  terminate = anaHask
+  
+
+
+-- | The category for defining the natural numbers and primitive recursion can be described as
+-- @Dialg(F,G)@, with @F(A)=\<1,A>@ and @G(A)=\<A,A>@.
+data NatF ((~>) :: * -> * -> *) where
+  NatF :: HasTerminalObject (~>) => NatF (~>)
+type instance Dom (NatF (~>)) = (~>)
+type instance Cod (NatF (~>)) = (~>) :*: (~>)
+type instance NatF (~>) :% a = (TerminalObject (~>),  a)
+instance Functor (NatF (~>)) where
+  NatF %% x = ProdO terminalObject x
+  NatF %  f = id terminalObject :**: f
+
+data NatNum = Z | S NatNum
+primRec :: t -> (t -> t) -> NatNum -> t
+primRec z _ Z     = z
+primRec z s (S n) = s (primRec z s n)
+
+instance HasInitialObject (Dialg (NatF (->)) (DiagProd (->))) where
+  
+  type InitialObject (Dialg (NatF (->)) (DiagProd (->))) = NatNum
+    
+  initialObject = Dialgebra HaskO (const Z :**: S)
+  
+  initialize o@(Dialgebra HaskO p) = DialgA initialObject o $ f p where
+    f :: ((->) :*: (->)) ((), t) (t, t) -> NatNum -> t
+    f (z :**: s) = primRec (z ()) s
+    
diff --git a/Data/Category/Discrete.hs b/Data/Category/Discrete.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/Discrete.hs
@@ -0,0 +1,105 @@
+{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, EmptyDataDecls, FlexibleContexts, FlexibleInstances, UndecidableInstances #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Category.Discrete
+-- Copyright   :  (c) Sjoerd Visscher 2010
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  sjoerd@w3future.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Discrete n, the category with n objects, and as the only arrows their identities.
+-----------------------------------------------------------------------------
+module Data.Category.Discrete where
+
+import Prelude hiding ((.), id, Functor, product)
+
+import Data.Category
+import Data.Category.Functor
+import Data.Category.NaturalTransformation
+import Data.Category.Void
+import Data.Category.Pair
+
+data Z
+data S n = S n
+
+-- | The arrows in Discrete n, a finite set of identity arrows.
+data Discrete :: * -> * -> * -> * where
+  IdZ   :: Discrete (S n) Z Z
+  StepS :: Discrete n a a -> Discrete (S n) (S a) (S a)
+
+
+instance Category (Discrete n) => Category (Discrete (S n)) where
+  
+  data Obj (Discrete (S n)) a where
+    OZ :: Obj (Discrete (S n)) Z
+    OS :: Obj (Discrete n) o -> Obj (Discrete (S n)) (S o)
+    
+  src IdZ       = OZ
+  src (StepS a) = OS $ src a
+  
+  tgt IdZ       = OZ
+  tgt (StepS a) = OS $ tgt a
+  
+  id OZ             = IdZ
+  id (OS n)         = StepS $ id n
+  
+  IdZ     . IdZ     = IdZ
+  StepS a . StepS b = StepS (a . b)
+  _       . _       = error "Other combinations should not type-check."
+
+
+magicZ :: Discrete Z a b -> x
+magicZ x = x `seq` error "we never get this far"
+
+magicZO :: Obj (Discrete Z) a -> x
+magicZO x = x `seq` error "we never get this far"
+
+
+
+instance Category (Discrete Z) where
+  
+  data Obj (Discrete Z) a
+  
+  src = magicZ
+  tgt = magicZ
+  
+  id    = magicZO
+  a . b = magicZ (a `seq` b)
+
+
+
+data Next :: * -> * -> * where
+  Next :: (Functor f, Dom f ~ Discrete (S n)) => f -> Next n f
+  
+type instance Dom (Next n f) = Discrete n
+type instance Cod (Next n f) = Cod f
+type instance Next n f :% a = f :% S a
+
+instance Functor (Next n f) where
+  Next f %% n = f %% OS n
+  Next f % IdZ       = f % StepS IdZ
+  Next f % (StepS a) = f % StepS (StepS a)
+    
+
+infixr 7 :::
+
+data DiscreteDiagram :: (* -> * -> *) -> * -> * -> * where
+  Nil   :: DiscreteDiagram (~>) Z ()
+  (:::) :: Category (~>) => Obj (~>) x -> DiscreteDiagram (~>) n xs -> DiscreteDiagram (~>) (S n) (x, xs)
+  
+type instance Dom (DiscreteDiagram (~>) n xs) = Discrete n
+type instance Cod (DiscreteDiagram (~>) n xs) = (~>)
+type instance DiscreteDiagram (~>) (S n) (x, xs) :% Z = x
+type instance DiscreteDiagram (~>) (S n) (x, xs) :% (S a) = DiscreteDiagram (~>) n xs :% a
+
+instance Functor (DiscreteDiagram (~>) n xs) where
+  
+  Nil        %% x  = magicZO x
+  (x ::: _)  %% OZ = x
+  (_ ::: xs) %% OS n = xs %% n
+  
+  Nil        %  f = magicZ f
+  (x ::: _)  %  IdZ = id x
+  (_ ::: xs) %  StepS n = xs % n
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, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, GADTs #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, EmptyDataDecls, FlexibleContexts, UndecidableInstances, GADTs, RankNTypes #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Functor
@@ -9,35 +9,179 @@
 -- Stability   :  experimental
 -- Portability :  non-portable
 -----------------------------------------------------------------------------
-module Data.Category.Functor where
+module Data.Category.Functor (
+
+  -- * Cat
+    Cat(..)
+  , Obj(..)
+  , CatW
+
+  -- * Functors
+  , Dom
+  , Cod
+  , Functor(..)
+  , (:%)
   
+  -- ** Functor instances
+  , Id(..)
+  , (:.:)(..)
+  , Const(..), ConstF
+  , (:*-:)(..)
+  , (:-*:)(..)
+  , Opposite(..)
+  , EndoHask(..)
+  
+  -- * Universal properties
+  , InitialUniversal(..)
+  , TerminalUniversal(..)
+
+) where
+  
+import Prelude hiding (id, (.), Functor)
+import qualified Prelude
+  
 import Data.Category
 
 
--- | Functor category Funct(C, D), or D^C.
--- Objects of Funct(C, D) are functors from C to D.
--- Arrows of Funct(C, D) are natural transformations.
--- Each category C needs its own data instance.
+-- | The domain, or source category, of the functor.
+type family Dom ftag :: * -> * -> *
+-- | The codomain, or target category, of the functor.
+type family Cod ftag :: * -> * -> *
 
+-- | Functors map objects and arrows. As objects are represented at both the type and value level, we need 3 maps in total.
+class Functor ftag where
+  -- | @%%@ maps objects at the value level.
+  (%%) :: ftag -> Obj (Dom ftag) a -> Obj (Cod ftag) (ftag :% a)
+  -- | @%@ maps arrows.
+  (%)  :: ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
 
+-- | @:%@ maps objects at the type level.
+type family ftag :% a :: *
 
--- | Arrows of the category Funct(Funct(C, D), E)
--- I.e. natural transformations between functors of type D^C -> E
-data instance Nat (Nat c d) e f g = 
-  FunctNat { unFunctNat :: forall h. (Dom h ~ c, Cod h ~ d) => Obj h -> Component f g h }
 
+-- | Functors are arrows in the category Cat.
+data Cat :: * -> * -> * where
+  CatA :: (Functor ftag, Category (Dom ftag), Category (Cod ftag)) => ftag -> Cat (CatW (Dom ftag)) (CatW (Cod ftag))
 
+-- | We need a wrapper here because objects need to be of kind *, and categories are of kind * -> * -> *.
+data CatW :: (* -> * -> *) -> *
 
--- | The diagonal functor from (index-) category J to (~>).
-data Diag (j :: * -> * -> *) ((~>) :: * -> * -> *) = Diag
-type instance Dom (Diag j (~>)) = (~>)
-type instance Cod (Diag j (~>)) = Nat j (~>)
-type instance F (Diag j (~>)) a = Const j (~>) a
 
--- | A cone from N to F is a natural transformation from the constant functor to N to F.
-type Cone   f n = Const (Dom f) (Cod f) n :~> f
--- | A co-cone from F to N is a natural transformation from F to the constant functor to N.
-type Cocone f n = f :~> Const (Dom f) (Cod f) n
+-- | @Cat@ is the category with categories as objects and funtors as arrows.
+instance Category Cat where
+  
+  -- | The objects in the category Cat are the categories themselves.
+  data Obj Cat a where
+    CatO :: Category (~>) => Obj Cat (CatW (~>))
+    
+  src (CatA _) = CatO
+  tgt (CatA _) = CatO
+  
+  id CatO           = CatA Id
+  CatA f1 . CatA f2 = CatA (f1 :.: f2)
 
-type Limit   f l = TerminalUniversal f (Diag (Dom f) (Cod f)) l
-type Colimit f l = InitialUniversal  f (Diag (Dom f) (Cod f)) l
+
+
+-- | The identity functor on (~>)
+data Id ((~>) :: * -> * -> *) = Id
+
+type instance Dom (Id (~>)) = (~>)
+type instance Cod (Id (~>)) = (~>)
+type instance Id (~>) :% a = a
+
+instance Functor (Id (~>)) where 
+  _ %% x = x
+  _ %  f = f
+
+
+-- | The composition of two functors.
+data (g :.: h) where
+  (:.:) :: (Functor g, Functor h, Cod h ~ Dom g) => g -> h -> g :.: h
+  
+type instance Dom (g :.: h) = Dom h
+type instance Cod (g :.: h) = Cod g
+type instance (g :.: h) :% a = g :% (h :% a)
+
+instance Functor (g :.: h) where 
+  (g :.: h) %% x = g %% (h %% x)
+  (g :.: h) %  f = g %  (h %  f)
+
+
+-- | The constant functor.
+data Const (c1 :: * -> * -> *) (c2 :: * -> * -> *) x where
+  Const :: Category c2 => Obj c2 x -> Const c1 c2 x
+  
+type instance Dom (Const c1 c2 x) = c1
+type instance Cod (Const c1 c2 x) = c2
+type instance Const c1 c2 x :% a = x
+
+instance Functor (Const c1 c2 x) where 
+  Const x %% _ = x
+  Const x %  _ = id x
+
+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 Functor (x :*-: (~>)) where 
+  HomX_ _ %% _ = HaskO
+  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 Functor ((~>) :-*: x) where 
+  Hom_X _ %% _   = HaskO
+  Hom_X _ % Op f = (. f)
+
+
+-- | The dual of a functor
+data Opposite f where
+  Opposite :: Functor f => f -> Opposite f
+  
+type instance Dom (Opposite f) = Op (Dom f)
+type instance Cod (Opposite f) = Op (Cod f)
+type instance Opposite f :% a = f :% a
+
+instance Functor (Opposite f) where
+  Opposite f %% OpObj x = OpObj $ f %% x
+  Opposite f % Op a = Op $ f % a
+
+
+-- | 'EndoHask' is a wrapper to turn instances of the 'Functor' class into categorical functors.
+data EndoHask :: (* -> *) -> * where
+  EndoHask :: Prelude.Functor f => EndoHask f
+  
+type instance Dom (EndoHask f) = (->)
+type instance Cod (EndoHask f) = (->)
+type instance EndoHask f :% r = f r
+
+instance Functor (EndoHask f) where
+  EndoHask %% HaskO = HaskO
+  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 }
+  
+-- | 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 }
diff --git a/Data/Category/Hask.hs b/Data/Category/Hask.hs
deleted file mode 100644
--- a/Data/Category/Hask.hs
+++ /dev/null
@@ -1,107 +0,0 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, GADTs, EmptyDataDecls, ScopedTypeVariables #-}
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Category.Hask
--- Copyright   :  (c) Sjoerd Visscher 2010
--- License     :  BSD-style (see the file LICENSE)
---
--- Maintainer  :  sjoerd@w3future.com
--- Stability   :  experimental
--- Portability :  non-portable
------------------------------------------------------------------------------
-module Data.Category.Hask where
-
-import Prelude hiding ((.), id)
-import qualified Prelude
-import Control.Arrow ((&&&), (***), (+++))
-
-import Data.Category
-import Data.Category.Functor
-import Data.Category.Void
-import Data.Category.Pair
--- import Data.Category.Discrete
-
-type Hask = (->)
-
-instance Apply (->) a b where
-  ($$) = ($)
-
-instance CategoryO (->) a where
-  id = Prelude.id
-  (!) = unHaskNat
-  
-instance CategoryA (->) a b c where
-  (.) = (Prelude..)
-
-newtype instance Nat (->) d f g = 
-  HaskNat { unHaskNat :: forall a. Obj a -> Component f g a }
-  
--- | 'EndoHask' is a wrapper to turn instances of the 'Functor' class into categorical functors.
-data EndoHask (f :: * -> *) = EndoHask
-type instance Dom (EndoHask f) = (->)
-type instance Cod (EndoHask f) = (->)
-type instance F (EndoHask f) r = f r
-instance Functor f => FunctorA (EndoHask f) a b where
-  _ % f = fmap f
-
-instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Diag (->) (~>)) a b where
-  Diag % f = HaskNat $ const f
-
--- | Any empty data type is an initial object in Hask.
-data Zero
--- With thanks to Conor McBride
-magic :: Zero -> a
-magic x = x `seq` error "we never get this far"
-
-instance VoidColimit (->) where
-  type InitialObject (->) = Zero
-  voidColimit = InitialUniversal VoidNat (HaskNat $ \_ VoidNat -> magic)
-instance VoidLimit (->) where
-  type TerminalObject (->) = ()
-  voidLimit = TerminalUniversal VoidNat (HaskNat $ \_ VoidNat -> const ())
-
--- | An alternative way to define the initial object.
-initObjInHask :: Limit (Id (->)) Zero
-initObjInHask = TerminalUniversal (HaskNat $ const magic) (HaskNat $ const (! (obj :: Zero)))
--- | An alternative way to define the terminal object.
-termObjInHask :: Colimit (Id (->)) ()
-termObjInHask = InitialUniversal (HaskNat $ \_ _ -> ()) (HaskNat $ const (! ()))
-
-instance PairColimit (->) x y where
-  type Coproduct x y = Either x y
-  pairColimit = InitialUniversal (Left :***: Right) (HaskNat $ \_ (l :***: r) -> either l r)
-instance PairLimit (->) x y where
-  type Product x y = (x, y)
-  pairLimit = TerminalUniversal (fst :***: snd) (HaskNat $ \_ (f :***: s) -> f &&& s)
-
--- type instance F (z, zs) Z = z
--- type instance F (z, zs) (S a) = F zs a
--- type instance ProductN (S n) f = (F f n, ProductN n f)
--- type instance ProductN Z f = ()
--- 
--- instance DiscreteLimit (S n) (->) f where
---   discreteLimit = TerminalUniversal (DiscreteNat fst (\_ _ c p -> snd c p in undefined)) undefined
-
--- | The product functor, Hask^2 -> Hask
-data ProdInHask = ProdInHask
-type instance Dom ProdInHask = Nat Pair (->)
-type instance Cod ProdInHask = (->)
-type instance F ProdInHask f = (F f Fst, F f Snd)
-instance (Dom f ~ Pair, Cod f ~ (->), Dom g ~ Pair, Cod g ~ (->)) => FunctorA ProdInHask f g where
-  ProdInHask % (f :***: g) = f *** g
-
--- | The product functor is right adjoint to the diagonal functor.
-prodInHaskAdj :: Adjunction (Diag Pair (->)) ProdInHask
-prodInHaskAdj = Adjunction { unit = HaskNat $ const (id &&& id), counit = FunctNat $ const (fst :***: snd) }
-
--- | The coproduct functor, Hask^2 -> Hask
-data CoprodInHask = CoprodInHask
-type instance Dom CoprodInHask = Nat Pair (->)
-type instance Cod CoprodInHask = (->)
-type instance F CoprodInHask f = Either (F f Fst) (F f Snd)
-instance (Dom f ~ Pair, Cod f ~ (->), Dom g ~ Pair, Cod g ~ (->)) => FunctorA CoprodInHask f g where
-  CoprodInHask % (f :***: g) = f +++ g
-
--- | The coproduct functor is left adjoint to the diagonal functor.
-coprodInHaskAdj :: Adjunction CoprodInHask (Diag Pair (->))
-coprodInHaskAdj = Adjunction { unit = FunctNat $ const (Left :***: Right), counit = HaskNat $ const (either id id) }
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, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, FlexibleInstances, FlexibleContexts, RankNTypes, ScopedTypeVariables #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Kleisli
@@ -14,48 +14,57 @@
 -----------------------------------------------------------------------------
 module Data.Category.Kleisli where
   
-import Prelude hiding ((.), id, Monad(..))
+import Prelude hiding ((.), id, Functor(..), Monad(..))
 
 import Data.Category
-import Data.Category.Hask
+import Data.Category.Functor
+import Data.Category.NaturalTransformation
+import Data.Category.Adjunction
 
-class Pointed m where
-  point :: m -> Id (Cod m) :~> m
+
+class Functor m => Pointed m where
+  point :: m -> Id (Dom m) :~> m
   
 class Pointed m => Monad m where
   join :: m -> (m :.: m) :~> m
+
   
-data Kleisli ((~>) :: * -> * -> *) m a b = Kleisli (m -> a ~> F m b)
+data Kleisli ((~>) :: * -> * -> *) m a b where
+  Kleisli :: m -> Obj (~>) b -> a ~> (m :% b) -> Kleisli (~>) m a b
 
-newtype instance Nat (Kleisli (->) m) d f g = 
-  KleisliNat { unKleisliNat :: forall a. Obj a -> Component f g a }
 
-instance (Monad m, Dom m ~ (->), Cod m ~ (->)) => CategoryO (Kleisli (->) m) o where
-  id = Kleisli $ \m -> point m ! (obj :: o)
-  (!) = unKleisliNat
-instance (Monad m, Dom m ~ (->), Cod m ~ (->), FunctorA m b (F m c)) => CategoryA (Kleisli (->) m) a b c where
-  (Kleisli f) . (Kleisli g) = Kleisli $ \m -> join m ! (obj :: c) . (m % f m) . g m
+instance (Category (~>), Monad m, Dom m ~ (~>), Cod m ~ (~>)) => Category (Kleisli (~>) m) where
+  
+  data Obj (Kleisli (~>) m) a = KleisliO m (Obj (~>) a)
+  
+  src (Kleisli m _ f) = KleisliO m (src f)
+  tgt (Kleisli m b _) = KleisliO m b
+  
+  id (KleisliO m o)                 = Kleisli m o $ point m ! o
+  (Kleisli m c f) . (Kleisli _ _ g) = Kleisli m c $ (join m ! c) . (m % f) . g
 
 
 
-data KleisliAdjF ((~>) :: * -> * -> *) m = KleisliAdjF m
+data KleisliAdjF ((~>) :: * -> * -> *) m where
+  KleisliAdjF :: (Category (~>), Monad m, Dom m ~ (~>), Cod m ~ (~>)) => m -> KleisliAdjF (~>) m
 type instance Dom (KleisliAdjF (~>) m) = (~>)
 type instance Cod (KleisliAdjF (~>) m) = Kleisli (~>) m
-type instance F (KleisliAdjF (~>) m) a = a
-instance (Monad m, Dom m ~ (->), Cod m ~ (->)) => FunctorA (KleisliAdjF (->) m) a b where
-  KleisliAdjF _ % f = Kleisli $ \m -> point m ! (obj :: b) . f
-  
-data KleisliAdjG ((~>) :: * -> * -> *) m = KleisliAdjG m
+type instance KleisliAdjF (~>) m :% a = a
+instance Functor (KleisliAdjF (~>) m) where
+  KleisliAdjF m %% x = KleisliO m x
+  KleisliAdjF m %  f = Kleisli m (tgt f) $ (point m ! tgt f) . f
+   
+data KleisliAdjG ((~>) :: * -> * -> *) m where
+  KleisliAdjG :: (Category (~>), Monad m, Dom m ~ (~>), Cod m ~ (~>)) => m -> KleisliAdjG (~>) m
 type instance Dom (KleisliAdjG (~>) m) = Kleisli (~>) m
 type instance Cod (KleisliAdjG (~>) m) = (~>)
-type instance F (KleisliAdjG (~>) m) a = F m a
-instance (Monad m, Dom m ~ (->), Cod m ~ (->), FunctorA m a (F m b)) => FunctorA (KleisliAdjG (->) m) a b where
-  KleisliAdjG m % Kleisli f = join m ! (obj :: b) . (m % f m)
+type instance KleisliAdjG (~>) m :% a = m :% a
+instance Functor (KleisliAdjG (~>) m) where
+  KleisliAdjG m %% KleisliO _ x = m %% x
+  KleisliAdjG m % Kleisli _ b f = (join m ! b) . (m % f)
 
-instance (Pointed m, Dom m ~ (->), Cod m ~ (->)) => Pointed (KleisliAdjG (->) m :.: KleisliAdjF (->) m) where
-  point (KleisliAdjG m :.: _) = HaskNat (point m !)
-   
-kleisliAdj :: (Monad m, Dom m ~ (->), Cod m ~ (->)) => m -> Adjunction (KleisliAdjF (->) m) (KleisliAdjG (->) m)
-kleisliAdj m = Adjunction 
-  { unit = point (KleisliAdjG m :.: KleisliAdjF m)
-  , counit = KleisliNat (\obja -> Kleisli $ \_ -> undefined) }
+kleisliAdj :: (Monad m, Dom m ~ (~>), Cod m ~ (~>), Category (~>)) 
+  => m -> Adjunction (Kleisli (~>) m) (~>) (KleisliAdjF (~>) m) (KleisliAdjG (~>) m)
+kleisliAdj m = mkAdjunction (KleisliAdjF m) (KleisliAdjG m)
+  (\x -> point m ! x)
+  (\(KleisliO _ x) -> Kleisli m x $ m % id x)
diff --git a/Data/Category/Limit.hs b/Data/Category/Limit.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/Limit.hs
@@ -0,0 +1,427 @@
+{-# LANGUAGE 
+  EmptyDataDecls, 
+  FlexibleContexts, 
+  FlexibleInstances, 
+  GADTs, 
+  MultiParamTypeClasses,
+  RankNTypes, 
+  ScopedTypeVariables,
+  TypeOperators, 
+  TypeFamilies,
+  UndecidableInstances  #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Category.Limit
+-- Copyright   :  (c) Sjoerd Visscher 2010
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  sjoerd@w3future.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+-----------------------------------------------------------------------------
+module Data.Category.Limit (
+
+  -- * Prelimiairies
+  
+  -- ** Diagonal Functor
+    Diag(..)
+  , DiagF
+  
+  -- ** Cones
+  , Cone
+  , Cocone
+  , coneVertex
+  , coconeVertex
+  
+  -- * Limits
+  , LimitFam
+  , Limit
+  , LimitUniversal
+  , limitUniversal
+  , limit
+  , limitFactorizer
+  
+  -- * Colimits
+  , ColimitFam
+  , Colimit
+  , ColimitUniversal
+  , colimitUniversal
+  , colimit
+  , colimitFactorizer
+  
+  -- * Limits of a certain type
+  , HasLimits(..)
+  , HasColimits(..)
+  
+  -- ** As a functor
+  , LimitFunctor(..)
+  , ColimitFunctor(..)
+  
+  -- ** Limits of type Void
+  , HasTerminalObject(..)
+  , HasInitialObject(..)
+  , Zero
+  
+  -- ** Limits of type Pair
+  , BinaryProduct
+  , HasBinaryProducts(..)
+  , BinaryCoproduct
+  , HasBinaryCoproducts(..)
+  
+  -- ** Limits of type Hask
+  , ForAll(..)
+  , endoHaskLimit
+  , Exists(..)
+  , endoHaskColimit
+  
+) where
+
+import Prelude hiding ((.), id, Functor, product)
+import qualified Prelude (Functor)
+import qualified Control.Arrow as A ((&&&), (***), (|||), (+++))
+
+import Data.Category
+import Data.Category.Functor
+import Data.Category.NaturalTransformation
+import Data.Category.Void
+import Data.Category.Pair
+import Data.Category.Unit
+import Data.Category.Product
+import Data.Category.Discrete
+
+infixr 3 ***
+infixr 3 &&&
+infixr 2 +++
+infixr 2 |||
+
+
+-- | The diagonal functor from (index-) category J to (~>).
+data Diag :: (* -> * -> *) -> (* -> * -> *) -> * where
+  Diag :: (Category j, Category (~>)) => Diag j (~>)
+  
+type instance Dom (Diag j (~>)) = (~>)
+type instance Cod (Diag j (~>)) = Nat j (~>)
+type instance Diag j (~>) :% a = Const j (~>) a
+
+instance Functor (Diag j (~>)) where 
+  Diag %% x = NatO $ Const x
+  Diag %  f = Nat (Const $ src f) (Const $ tgt f) $ const f
+
+-- | The diagonal functor with the same domain and codomain as @f@.
+type DiagF f = Diag (Dom f) (Cod f)
+
+
+
+-- | A cone from N to F is a natural transformation from the constant functor to N to F.
+type Cone   f n = Nat (Dom f) (Cod f) (ConstF f n) f
+
+-- | A co-cone from F to N is a natural transformation from F to the constant functor to N.
+type Cocone f n = Nat (Dom f) (Cod f) f (ConstF f n)
+
+
+-- | The vertex (or apex) of a cone.
+coneVertex :: Cone f n -> Obj (Cod f) n
+coneVertex (Nat (Const x) _ _) = x
+
+-- | The vertex (or apex) of a co-cone.
+coconeVertex :: Cocone f n -> Obj (Cod f) n
+coconeVertex (Nat _ (Const x) _) = x
+
+
+
+-- | Limits in a category @(~>)@ by means of a diagram of type @j@, which is a functor from @j@ to @(~>)@.
+type family LimitFam j (~>) f :: *
+
+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
+
+-- | 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 (~>)
+
+type instance Dom (LimitFunctor j (~>)) = Nat j (~>)
+type instance Cod (LimitFunctor j (~>)) = (~>)
+type instance LimitFunctor j (~>) :% f = LimitFam j (~>) f
+
+instance Functor (LimitFunctor j (~>)) where
+  LimitFunctor %% f @ NatO{} = tuObject (limitUniv f)
+  LimitFunctor %  n @ Nat{}  = limitFactorizer (limitUniv (tgt n)) (n . limit (limitUniv (src n)))
+
+
+
+-- | 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
+
+-- | 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 (~>)
+  
+type instance Dom (ColimitFunctor j (~>)) = Nat j (~>)
+type instance Cod (ColimitFunctor j (~>)) = (~>)
+type instance ColimitFunctor j (~>) :% f = ColimitFam j (~>) f
+
+instance Functor (ColimitFunctor j (~>)) where
+  ColimitFunctor %% f @ NatO{} = iuObject (colimitUniv f)
+  ColimitFunctor %  n @ Nat{}  = colimitFactorizer (colimitUniv (src n)) (colimit (colimitUniv (tgt n)) . n)
+
+
+
+-- | A terminal object is the limit of the functor from /0/ to (~>).
+class Category (~>) => HasTerminalObject (~>) where
+  
+  type TerminalObject (~>) :: *
+  
+  terminalObject :: Obj (~>) (TerminalObject (~>))
+  
+  terminate :: Obj (~>) a -> a ~> TerminalObject (~>)
+
+
+type instance LimitFam Void (~>) f = TerminalObject (~>)
+
+instance (HasTerminalObject (~>)) => HasLimits Void (~>) where
+  
+  limitUniv (NatO f) = limitUniversal
+    (voidNat (Const terminalObject) f)
+    (terminate . coneVertex)
+
+
+-- | @()@ is the terminal object in @Hask@.
+instance HasTerminalObject (->) where
+  
+  type TerminalObject (->) = ()
+  
+  terminalObject = HaskO
+  
+  terminate HaskO _ = ()
+
+-- | @Unit@ is the terminal category.
+instance HasTerminalObject Cat where
+  
+  type TerminalObject Cat = CatW Unit
+  
+  terminalObject = CatO
+  
+  terminate CatO = CatA $ Const UnitO
+
+
+-- | An initial object is the colimit of the functor from /0/ to (~>).
+class Category (~>) => HasInitialObject (~>) where
+  
+  type InitialObject (~>) :: *
+  
+  initialObject :: Obj (~>) (InitialObject (~>))
+
+  initialize :: Obj (~>) a -> InitialObject (~>) ~> a
+
+
+type instance ColimitFam Void (~>) f = InitialObject (~>)
+
+instance HasInitialObject (~>) => HasColimits Void (~>) where
+  
+  colimitUniv (NatO f) = colimitUniversal
+    (voidNat f (Const initialObject))
+    (initialize . coconeVertex)
+
+
+-- | Any empty data type is an initial object in Hask.
+data Zero
+
+instance HasInitialObject (->) where
+  
+  type InitialObject (->) = Zero
+  
+  initialObject = HaskO
+  
+  -- With thanks to Conor McBride
+  initialize HaskO x = x `seq` error "we never get this far"
+
+instance HasInitialObject Cat where
+  
+  type InitialObject Cat = CatW Void
+  
+  initialObject = CatO
+  
+  initialize CatO = CatA VoidDiagram
+
+
+
+type family BinaryProduct ((~>) :: * -> * -> *) x y :: *
+
+-- | The product of 2 objects is the limit of the functor from Pair to (~>).
+class Category (~>) => HasBinaryProducts (~>) where
+  
+  product :: Obj (~>) x -> Obj (~>) y -> Obj (~>) (BinaryProduct (~>) x y)
+  
+  proj :: Obj (~>) x -> Obj (~>) y -> (BinaryProduct (~>) x y ~> x, BinaryProduct (~>) x y ~> y)
+
+  (&&&) :: (a ~> x) -> (a ~> y) -> (a ~> BinaryProduct (~>) x y)
+
+  (***) :: (a1 ~> b1) -> (a2 ~> b2) -> (BinaryProduct (~>) a1 a2 ~> BinaryProduct (~>) b1 b2)
+  l *** r = (l . proj1) &&& (r . proj2) where
+    (proj1, proj2) = proj (src l) (src r)
+
+
+type instance LimitFam Pair (~>) f = BinaryProduct (~>) (f :% P1) (f :% P2)
+
+instance HasBinaryProducts (~>) => HasLimits Pair (~>) where
+
+  limitUniv (NatO f) = limitUniversal
+    (pairNat (Const prod) f (Com $ fst prj) (Com $ snd prj))
+    (\c -> c ! Fst &&& c ! Snd)
+    where
+      x = f %% Fst
+      y = f %% Snd
+      prod = product x y
+      prj = proj x y
+
+
+type instance BinaryProduct (->) x y = (x, y)
+
+instance HasBinaryProducts (->) where
+  
+  product HaskO HaskO = HaskO
+  
+  proj _ _ = (fst, snd)
+  
+  (&&&) = (A.&&&)
+  (***) = (A.***)
+
+type instance BinaryProduct Cat (CatW c1) (CatW c2) = CatW (c1 :*: c2)
+
+instance HasBinaryProducts Cat where
+  
+  product CatO CatO = CatO
+  
+  proj CatO CatO = (CatA Proj1, CatA Proj2)
+  
+  CatA f1 &&& CatA f2 = CatA ((f1 :***: f2) :.: DiagProd)
+  CatA f1 *** CatA f2 = CatA (f1 :***: f2)
+
+
+
+type family BinaryCoproduct ((~>) :: * -> * -> *) x y :: *
+
+-- | The coproduct of 2 objects is the colimit of the functor from Pair to (~>).
+class Category (~>) => HasBinaryCoproducts (~>) where
+
+  coproduct :: Obj (~>) x -> Obj (~>) y -> Obj (~>) (BinaryCoproduct (~>) x y)
+  
+  inj :: Obj (~>) x -> Obj (~>) y -> (x ~> BinaryCoproduct (~>) x y, y ~> BinaryCoproduct (~>) x y)
+
+  (|||) :: (x ~> a) -> (y ~> a) -> (BinaryCoproduct (~>) x y ~> a)
+    
+  (+++) :: (a1 ~> b1) -> (a2 ~> b2) -> (BinaryCoproduct (~>) a1 a2 ~> BinaryCoproduct (~>) b1 b2)
+  l +++ r = (inj1 . l) ||| (inj2 . r) where
+    (inj1, inj2) = inj (tgt l) (tgt r)
+    
+
+type instance ColimitFam Pair (~>) f = BinaryCoproduct (~>) (f :% P1) (f :% P2)
+
+instance HasBinaryCoproducts (~>) => HasColimits Pair (~>) where
+  
+  colimitUniv (NatO f) = colimitUniversal
+    (pairNat f (Const cop) (Com $ fst i) (Com $ snd i))
+    (\c -> c ! Fst ||| c ! Snd)
+    where
+      x = f %% Fst
+      y = f %% Snd
+      cop = coproduct x y
+      i = inj x y
+
+
+type instance BinaryCoproduct (->) x y = Either x y
+
+instance HasBinaryCoproducts (->) where
+  
+  coproduct HaskO HaskO = HaskO
+  
+  inj _ _ = (Left, Right)
+  
+  (|||) = (A.|||)
+  (+++) = (A.+++)
+
+
+
+newtype ForAll f = ForAll { unForAll :: forall a. f a }
+
+type instance LimitFam (->) (->) (EndoHask f) = ForAll f
+
+endoHaskLimit :: Prelude.Functor f => LimitUniversal (EndoHask f)
+endoHaskLimit = limitUniversal
+  (Nat (Const HaskO) EndoHask $ \HaskO -> unForAll)
+  (\c n -> ForAll ((c ! HaskO) n)) -- ForAll . (c ! Hask)
+
+
+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 HaskO) $ \HaskO -> Exists)
+  (\c (Exists fa) -> (c ! HaskO) fa) -- (c ! HaskO) . unExists
diff --git a/Data/Category/Monoid.hs b/Data/Category/Monoid.hs
--- a/Data/Category/Monoid.hs
+++ b/Data/Category/Monoid.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances #-}
+{-# LANGUAGE TypeFamilies, GADTs, FlexibleInstances #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Monoid
@@ -18,16 +18,18 @@
 
 import Data.Category
 
--- | The arrows are the values of the monoid.
-newtype MonoidA m a b = MonoidA m
 
-newtype instance Nat (MonoidA m) d f g =
-  MonoidNat (Component f g m)
+-- | The arrows are the values of the monoid.
+data MonoidA m a b where
+  MonoidA :: Monoid m => m -> MonoidA m m m
 
-instance Monoid m => CategoryO (MonoidA m) m where
-  id = MonoidA mempty
-  MonoidNat c ! _ = c  
-instance Monoid m => CategoryA (MonoidA m) m m m where
+instance Monoid m => Category (MonoidA m) where
+  
+  data Obj (MonoidA m) a where
+     MonoidO :: Obj (MonoidA m) m
+  
+  src (MonoidA _) = MonoidO
+  tgt (MonoidA _) = MonoidO
+  
+  id MonoidO            = MonoidA mempty
   MonoidA a . MonoidA b = MonoidA $ a `mappend` b
-instance Monoid m => Apply (MonoidA m) m m where
-  MonoidA a $$ b = a `mappend` b
diff --git a/Data/Category/NaturalTransformation.hs b/Data/Category/NaturalTransformation.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/NaturalTransformation.hs
@@ -0,0 +1,131 @@
+{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, ScopedTypeVariables, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, GADTs #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Category.NaturalTransformation
+-- Copyright   :  (c) Sjoerd Visscher 2010
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  sjoerd@w3future.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+-----------------------------------------------------------------------------
+module Data.Category.NaturalTransformation (
+
+  -- * Natural transformations
+    (:~>)
+  , Nat(..)
+  , Obj(..)
+  , Component
+  , Com(..)
+  , o
+  , (!)
+  
+  -- * Related functors
+  , Precompose(..)
+  , Postcompose(..)
+  , YonedaEmbedding(..)
+  
+) where
+  
+import Prelude hiding ((.), id, Functor)
+
+import Data.Category
+import Data.Category.Functor
+
+infixl 9 !
+
+-- | @f :~> g@ is a natural transformation from functor f to functor g.
+type f :~> g = (c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => Nat c d f g
+
+-- | Natural transformations are built up of components, 
+-- one for each object @z@ in the domain category of @f@ and @g@.
+data Nat :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where
+  Nat :: (Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) 
+    => f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
+
+-- | A component for an object @z@ is an arrow from @F z@ to @G z@.
+type Component f g z = Cod f (f :% z) (g :% z)
+
+
+-- | Functor category D^C.
+-- Objects of D^C are functors from C to D.
+-- Arrows of D^C are natural transformations.
+instance (Category c, Category d) => Category (Nat c d) where
+  
+  data Obj (Nat c d) a where
+    NatO :: (Functor f, Dom f ~ c, Cod f ~ d) => f -> Obj (Nat c d) f
+    
+  src (Nat f _ _) = NatO f
+  tgt (Nat _ g _) = NatO g
+  
+  id (NatO f)               = Nat f f $ \i -> id $ f %% i
+  Nat _ h ngh . Nat f _ nfg = Nat f h $ \i -> ngh i . nfg i
+
+
+-- | Horizontal composition of natural transformations.
+o :: Category e => Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
+Nat j k njk `o` Nat f g nfg = Nat (j :.: f) (k :.: g) $ \x -> k % nfg x . njk (f %% x)
+
+
+-- | A newtype wrapper for components,
+--   which can be useful for helper functions dealing with components.
+newtype Com f g z = Com { unCom :: Component f g z }
+
+
+
+-- | 'n ! a' returns the component for the object @a@ of a natural transformation @n@.
+(!) :: (Cod f ~ d, Cod g ~ d) => Nat (~>) d f g -> Obj (~>) a -> d (f :% a) (g :% a)
+Nat _ _ n ! x = n x
+
+
+-- | @Precompose f d@ is the functor such that @Precompose f d :% g = g :.: f@, 
+--   for functors @g@ that compose with @f@ and with codomain @d@.
+data Precompose :: * -> (* -> * -> *) -> * where
+  Precompose :: (Functor f, Category d) => f -> Precompose f d
+
+type instance Dom (Precompose f d) = Nat (Cod f) d
+type instance Cod (Precompose f d) = Nat (Dom f) d
+type instance Precompose f d :% g = g :.: f
+
+instance Functor (Precompose f d) where
+  Precompose f %% NatO g = NatO $ g :.: f
+  Precompose f % (Nat g h n) = Nat (g :.: f) (h :.: f) $ n . (f %%)
+
+
+-- | @Postcompose f c@ is the functor such that @Postcompose f c :% g = f :.: g@, 
+--   for functors @g@ that compose with @f@ and with domain @c@.
+data Postcompose :: * -> (* -> * -> *) -> * where
+  Postcompose :: (Functor f, Category c) => f -> Postcompose f c
+
+type instance Dom (Postcompose f c) = Nat c (Dom f)
+type instance Cod (Postcompose f c) = Nat c (Cod f)
+type instance Postcompose f c :% g = f :.: g
+
+instance Functor (Postcompose f c) where
+  Postcompose f %% NatO g = NatO $ f :.: g
+  Postcompose f % (Nat g h n) = Nat (f :.: g) (f :.: h) $ (f %) . n
+
+
+-- | 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 = id $ NatO f
+  unrepresent f = id $ NatO 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 Functor (YonedaEmbedding (~>)) where
+  YonedaEmbedding %% x = NatO $ Hom_X x
+  YonedaEmbedding % f = Nat (Hom_X $ src f) (Hom_X $ tgt f) $ \_ -> (f .)
diff --git a/Data/Category/Omega.hs b/Data/Category/Omega.hs
--- a/Data/Category/Omega.hs
+++ b/Data/Category/Omega.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, EmptyDataDecls, FlexibleInstances #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Omega
@@ -14,100 +14,100 @@
 -----------------------------------------------------------------------------
 module Data.Category.Omega where
 
-import Prelude hiding ((.), id)
+import Prelude hiding ((.), id, Functor, product)
 
 import Data.Category
-import Data.Category.Functor
-import Data.Category.Void
-import Data.Category.Pair
+import Data.Category.Limit
 
 
--- | The object Z represents zero.
-data Z = Z deriving Show
--- | The object S n represents the successor of n.
-newtype S n = S n deriving Show
-
-instance CategoryO Omega Z where
-  id = IdZ
-  OmegaNat z _ ! Z = z  
-instance (CategoryO Omega n) => CategoryO Omega (S n) where
-  id = StepS id
-  on@(OmegaNat _ s) ! (S n) = s n (on ! n)
+data Z
+data S n
 
 -- | The arrows of omega, there's an arrow from a to b iff a <= b.
-data family Omega a b :: *
-data instance Omega Z Z = IdZ
-newtype instance Omega Z (S n) = GTZ (Omega Z n)
-newtype instance Omega (S a) (S b) = StepS (Omega a b)
+data Omega :: * -> * -> * where
+  IdZ :: Omega Z Z
+  GTZ :: Omega Z n -> Omega Z (S n)
+  StS :: Omega a b -> Omega (S a) (S b)
+  
+instance Category Omega where
+  
+  data Obj Omega a where
+    OZ :: Obj Omega Z
+    OS :: Obj Omega n -> Obj Omega (S n)
+  
+  src IdZ     = OZ
+  src (GTZ _) = OZ
+  src (StS a) = OS (src a)
+  
+  tgt IdZ     = OZ
+  tgt (GTZ a) = OS (tgt a)
+  tgt (StS a) = OS (tgt a)
+  
+  id OZ             = IdZ
+  id (OS n)         = StS (id n)
+  
+  a       . IdZ     = a
+  (StS a) . (GTZ n) = GTZ (a . n)
+  (StS a) . (StS b) = StS (a . b)
+  _       . _       = error "Other combinations should not type check"
 
-instance (CategoryO Omega n) => CategoryA Omega Z Z n where
-  a . IdZ = a
-instance (CategoryA Omega Z n p) => CategoryA Omega Z (S n) (S p) where
-  (StepS a) . (GTZ n) = GTZ (a . n)
-instance (CategoryA Omega n p q) => CategoryA Omega (S n) (S p) (S q) where
-  (StepS a) . (StepS b) = StepS (a . b)
 
-instance Apply Omega Z Z where
-  IdZ $$ Z = Z
-instance Apply Omega Z n => Apply Omega Z (S n) where
-  GTZ d $$ Z = S (d $$ Z)
-instance Apply Omega a b => Apply Omega (S a) (S b) where
-  StepS d $$ S a = S (d $$ a)
+instance HasInitialObject Omega where
+  
+  type InitialObject Omega = Z
+  
+  initialObject     = OZ
+  
+  initialize OZ     = IdZ
+  initialize (OS n) = GTZ $ initialize n
 
-data instance Nat Omega d f g = 
-  OmegaNat (Component f g Z) (forall n. Obj n -> Component f g n -> Component f g (S n))
 
+type instance BinaryProduct Omega Z     n = Z
+type instance BinaryProduct Omega n     Z = Z
+type instance BinaryProduct Omega (S a) (S b) = S (BinaryProduct Omega a b)
 
-data OmegaF ((~>) :: * -> * -> *) z f = OmegaF
-type instance Dom (OmegaF (~>) z f) = Omega
-type instance Cod (OmegaF (~>) z f) = (~>)
-type instance F (OmegaF (~>) z f) Z = z
-type instance F (OmegaF (~>) z f) (S n) = F f (F (OmegaF (~>) z f) n)
-instance CategoryO (~>) z => FunctorA (OmegaF (~>) z f) Z Z where
-  OmegaF % IdZ = id
+-- The product in omega is the minimum.
+instance HasBinaryProducts Omega where 
 
-class CategoryO (~>) z => OmegaLimit (~>) z f where
-  type OmegaL (~>) z f :: *
-  omegaLimit :: Limit (OmegaF (~>) z f) (OmegaL (~>) z f)
-class CategoryO (~>) z => OmegaColimit (~>) z f where
-  type OmegaC (~>) z f :: *
-  omegaColimit :: Colimit (OmegaF (~>) z f) (OmegaC (~>) z f)
+  product OZ     _      = OZ
+  product _      OZ     = OZ
+  product (OS a) (OS b) = OS (product a b)
   
+  proj OZ     OZ     = (IdZ, IdZ)
+  proj OZ     (OS n) = (IdZ, GTZ . snd $ proj OZ n)
+  proj (OS n) OZ     = (GTZ . fst $ proj n OZ, IdZ)
+  proj (OS a) (OS b) = (StS proj1, StS proj2) where (proj1, proj2) = proj a b
+  
+  IdZ   &&& _     = IdZ
+  _     &&& IdZ   = IdZ
+  GTZ a &&& GTZ b = GTZ (a &&& b)
+  StS a &&& StS b = StS (a &&& b)
+  _     &&& _      = error "Other combinations should not type check"
 
-instance VoidColimit Omega where
-  type InitialObject Omega = Z
-  voidColimit = InitialUniversal VoidNat (OmegaNat (\VoidNat -> IdZ) (\_ cpt VoidNat -> GTZ (cpt VoidNat)))
 
--- The product in omega is the minimum.
-instance PairLimit Omega Z Z where 
-  type Product Z Z = Z
-  pairLimit = TerminalUniversal (IdZ :***: IdZ) undefined
-instance (PairLimit Omega Z n, Product Z n ~ Z) => PairLimit Omega Z (S n) where 
-  type Product Z (S n) = Z
-  pairLimit = TerminalUniversal (IdZ :***: GTZ p) undefined where
-    TerminalUniversal (_ :***: p) _ = pairLimit :: Limit (PairF Omega Z n) (Product Z n)
-instance (PairLimit Omega n Z, Product n Z ~ Z) => PairLimit Omega (S n) Z where 
-  type Product (S n) Z = Z
-  pairLimit = TerminalUniversal (GTZ p :***: IdZ) undefined where
-    TerminalUniversal (p :***: _) _ = pairLimit :: Limit (PairF Omega n Z) (Product n Z)
-instance (PairLimit Omega a b) => PairLimit Omega (S a) (S b) where 
-  type Product (S a) (S b) = S (Product a b)
-  pairLimit = TerminalUniversal (StepS p1 :***: StepS p2) undefined where
-    TerminalUniversal (p1 :***: p2) _ = pairLimit :: Limit (PairF Omega a b) (Product a b)
+type instance BinaryCoproduct Omega Z     n     = n
+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.
-instance PairColimit Omega Z Z where 
-  type Coproduct Z Z = Z
-  pairColimit = InitialUniversal (IdZ :***: IdZ) undefined
-instance (PairColimit Omega Z n, Coproduct Z n ~ n) => PairColimit Omega Z (S n) where 
-  type Coproduct Z (S n) = S n
-  pairColimit = InitialUniversal (GTZ p1 :***: StepS p2) undefined where
-    InitialUniversal (p1 :***: p2) _ = pairColimit :: Colimit (PairF Omega Z n) (Coproduct Z n)
-instance (PairColimit Omega n Z, Coproduct n Z ~ n) => PairColimit Omega (S n) Z where 
-  type Coproduct (S n) Z = S n
-  pairColimit = InitialUniversal (StepS p1 :***: GTZ p2) undefined where
-    InitialUniversal (p1 :***: p2) _ = pairColimit :: Colimit (PairF Omega n Z) (Coproduct n Z)
-instance (PairColimit Omega a b) => PairColimit Omega (S a) (S b) where 
-  type Coproduct (S a) (S b) = S (Coproduct a b)
-  pairColimit = InitialUniversal (StepS p1 :***: StepS p2) undefined where
-    InitialUniversal (p1 :***: p2) _ = pairColimit :: Colimit (PairF Omega a b) (Coproduct a b)
+-- -- The coproduct in omega is the maximum.
+instance HasBinaryCoproducts Omega where 
+  
+  coproduct OZ     n      = n
+  coproduct n      OZ     = n
+  coproduct (OS a) (OS b) = OS (coproduct a b)
+  
+  inj OZ OZ = (IdZ, IdZ)
+  inj OZ (OS n) = (GTZ inj1, StS inj2) where (inj1, inj2) = inj OZ n
+  inj (OS n) OZ = (StS inj1, GTZ inj2) where (inj1, inj2) = inj n OZ
+  inj (OS a) (OS b) = (StS inj1, StS inj2) where (inj1, inj2) = inj a b
+  
+  IdZ   ||| IdZ   = IdZ
+  GTZ _ ||| a     = a
+  a     ||| GTZ _ = a
+  StS a ||| StS b = StS (a ||| b)
+  _     ||| _      = error "Other combinations should not type check"
+  
+  
+instance Show (Obj Omega a) where
+  show OZ = "OZ"
+  show (OS n) = "OS " ++ show n
diff --git a/Data/Category/Pair.hs b/Data/Category/Pair.hs
--- a/Data/Category/Pair.hs
+++ b/Data/Category/Pair.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies, TypeOperators, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, EmptyDataDecls #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Pair
@@ -15,71 +15,62 @@
 -----------------------------------------------------------------------------
 module Data.Category.Pair where
 
-import Prelude hiding ((.), id)
+import Prelude (($), undefined)
 
 import Data.Category
 import Data.Category.Functor
+import Data.Category.NaturalTransformation
 
--- | One object of Pair
-data Fst = Fst deriving Show
--- | The other object of Pair
-data Snd = Snd deriving Show
 
-instance CategoryO Pair Fst where
-  id = IdFst
-  (f :***: _) ! Fst = f  
-instance CategoryO Pair Snd where
-  id = IdSnd
-  (_ :***: s) ! Snd = s  
+data P1
+data P2
 
 -- | The arrows of Pair.
-data family Pair a b :: *
-data instance Pair Fst Fst = IdFst
-data instance Pair Snd Snd = IdSnd
+data Pair :: * -> * -> * where
+  IdFst :: Pair P1 P1
+  IdSnd :: Pair P2 P2
 
-instance CategoryA Pair Fst Fst Fst where
+instance Category Pair where
+  
+  data Obj Pair a where
+    Fst :: Obj Pair P1
+    Snd :: Obj Pair P2
+  
+  src IdFst = Fst
+  src IdSnd = Snd
+  
+  tgt IdFst = Fst
+  tgt IdSnd = Snd
+  
+  id  Fst       = IdFst
+  id  Snd       = IdSnd
+  
   IdFst . IdFst = IdFst
-instance CategoryA Pair Snd Snd Snd where
   IdSnd . IdSnd = IdSnd
+  _     . _     = undefined -- this can't happen
 
-instance Apply Pair Fst Fst where
-  IdFst $$ Fst = Fst
-instance Apply Pair Snd Snd where
-  IdSnd $$ Snd = Snd
 
-  
-data instance Nat Pair d f g = Component f g Fst :***: Component f g Snd
-instance (Dom f ~ Pair, Cod f ~ (~>), CategoryO (~>) (F f Fst), CategoryO (~>) (F f Snd)) => CategoryO (Nat Pair (~>)) f where
-  id = id :***: id
-  FunctNat n ! f = n f
-instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Diag Pair (~>)) a b where
-  Diag % f = f :***: f
-
 -- | The functor from Pair to (~>), a diagram of 2 objects in (~>).
-data PairF ((~>) :: * -> * -> *) x y = PairF
-type instance Dom (PairF (~>) x y) = Pair
-type instance Cod (PairF (~>) x y) = (~>)
-type instance F (PairF (~>) x y) Fst = x
-type instance F (PairF (~>) x y) Snd = y
-instance (CategoryO (~>) x) => FunctorA (PairF (~>) x y) Fst Fst where
-  PairF % IdFst = id
-instance (CategoryO (~>) y) => FunctorA (PairF (~>) x y) Snd Snd where
-  PairF % IdSnd = id
+data PairDiagram :: (* -> * -> *) -> * -> * -> * where
+  PairDiagram :: Category (~>) => Obj (~>) x -> Obj (~>) y -> PairDiagram (~>) x y
+type instance Dom (PairDiagram (~>) x y) = Pair
+type instance Cod (PairDiagram (~>) x y) = (~>)
+type instance PairDiagram (~>) x y :% P1 = x
+type instance PairDiagram (~>) x y :% P2 = y
+instance Functor (PairDiagram (~>) x y) where
+  PairDiagram x _ %% Fst = x
+  PairDiagram _ y %% Snd = y
+  PairDiagram x _ % IdFst = id x
+  PairDiagram _ y % IdSnd = id y
 
--- | The product of 2 objects is the limit of the functor from Pair to (~>).
-class (CategoryO (~>) x, CategoryO (~>) y) => PairLimit (~>) x y where
-  type Product x y :: *
-  pairLimit :: Limit (PairF (~>) x y) (Product x y)
-  proj1 :: Product x y ~> x
-  proj2 :: Product x y ~> y
-  proj1 = p where TerminalUniversal (p :***: _) _ = pairLimit :: Limit (PairF (~>) x y) (Product x y)
-  proj2 = p where TerminalUniversal (_ :***: p) _ = pairLimit :: Limit (PairF (~>) x y) (Product x y)
--- | The coproduct of 2 objects is the colimit of the functor from Pair to (~>).
-class (CategoryO (~>) x, CategoryO (~>) y) => PairColimit (~>) x y where
-  type Coproduct x y :: *
-  pairColimit :: Colimit (PairF (~>) x y) (Coproduct x y)
-  inj1 :: x ~> Coproduct x y
-  inj2 :: y ~> Coproduct x y
-  inj1 = i where InitialUniversal (i :***: _) _ = pairColimit :: Colimit (PairF (~>) x y) (Coproduct x y)
-  inj2 = i where InitialUniversal (_ :***: i) _ = pairColimit :: Colimit (PairF (~>) x y) (Coproduct x y)
-  
+
+pairNat :: (Functor f, Functor g, Dom f ~ Pair, Cod f ~ d, Dom g ~ Pair, Cod g ~ d) 
+  => f -> g -> Com f g P1 -> Com f g P2 -> Nat Pair d f g
+pairNat f g c1 c2 = Nat f g (\x -> unCom $ n c1 c2 x) where
+  n :: (Functor f, Functor g, Dom f ~ Pair, Cod f ~ d, Dom g ~ Pair, Cod g ~ d) 
+    => Com f g P1 -> Com f g P2 -> Obj Pair a -> Com f g a
+  n c _ Fst = c
+  n _ c Snd = c
+
+arrowPair :: Category (~>) => (x1 ~> x2) -> (y1 ~> y2) -> Nat Pair (~>) (PairDiagram (~>) x1 y1) (PairDiagram (~>) x2 y2)
+arrowPair l r = pairNat (PairDiagram (src l) (src r)) (PairDiagram (tgt l) (tgt r)) (Com l) (Com r)
diff --git a/Data/Category/Peano.hs b/Data/Category/Peano.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/Peano.hs
@@ -0,0 +1,52 @@
+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleInstances #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Category.Peano
+-- Copyright   :  (c) Sjoerd Visscher 2010
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  sjoerd@w3future.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+-- 
+-- A Peano category as in @When is one thing equal to some other thing?@
+-- Barry Mazur, 2007
+-----------------------------------------------------------------------------
+module Data.Category.Peano where
+
+import Prelude(($))
+
+import Data.Category
+import Data.Category.Limit
+
+
+data Peano :: (* -> * -> *) -> * -> * -> * where
+  PeanoA :: Obj (Peano (~>)) a -> Obj (Peano (~>)) b -> (a ~> b) -> Peano (~>) a b
+
+instance Category (~>) => Category (Peano (~>)) where
+  
+  data Obj (Peano (~>)) a where
+    PeanoO :: Obj (~>) x -> x -> (x ~> x) -> Obj (Peano (~>)) x
+    
+  src (PeanoA s _ _) = s
+  tgt (PeanoA _ t _) = t
+  
+  id p@(PeanoO x _ _)             = PeanoA p p $ id x
+  (PeanoA _ t f) . (PeanoA s _ g) = PeanoA s t $ f . g
+  
+  
+-- | The natural numbers are the initial object for the 'Peano' category.
+data NatNum = Z | S NatNum
+
+-- | Primitive recursion is the factorizer from the natural numbers.
+primRec :: t -> (t -> t) -> NatNum -> t
+primRec z _ Z     = z
+primRec z s (S n) = s (primRec z s n)
+  
+instance HasInitialObject (Peano (->)) where
+  
+  type InitialObject (Peano (->)) = NatNum
+  
+  initialObject = PeanoO HaskO Z S
+  
+  initialize o@(PeanoO HaskO z s) = PeanoA initialObject o $ primRec z s
diff --git a/Data/Category/Product.hs b/Data/Category/Product.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/Product.hs
@@ -0,0 +1,81 @@
+{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, FlexibleContexts #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Category.Product
+-- Copyright   :  (c) Sjoerd Visscher 2010
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  sjoerd@w3future.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+-----------------------------------------------------------------------------
+module Data.Category.Product where
+
+import Prelude hiding ((.), id, Functor)
+
+import Data.Category
+import Data.Category.Functor
+
+
+data (:*:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where
+  (:**:) :: c1 a1 b1 -> c2 a2 b2 -> (:*:) c1 c2 (a1, a2) (b1, b2)
+
+-- | The product category of category @c1@ and @c2@.
+instance (Category c1, Category c2) => Category (c1 :*: c2) where
+  
+  data Obj (c1 :*: c2) a where
+    ProdO :: Obj c1 a1 -> Obj c2 a2 -> Obj (c1 :*: c2) (a1, a2)
+    
+  src (a1 :**: a2)            = ProdO (src a1) (src a2)
+  tgt (a1 :**: a2)            = ProdO (tgt a1) (tgt a2)
+  
+  id (ProdO x1 x2)            = id x1 :**: id x2
+  
+  (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 Functor (Proj1 c1 c2) where 
+  Proj1 %% ProdO x1 _ = x1
+  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 Functor (Proj2 c1 c2) where 
+  Proj2 %% ProdO _ x2 = x2
+  Proj2 % (_ :**: f2) = f2
+
+data f1 :***: f2 where 
+  (:***:) :: (Functor f1, Functor f2, Category (Cod f1), Category (Cod f2)) => f1 -> f2 -> f1 :***: f2
+type instance Dom (f1 :***: f2) = Dom f1 :*: Dom f2
+type instance Cod (f1 :***: f2) = Cod f1 :*: Cod f2
+type instance (f1 :***: f2) :% (a1, a2) = (f1 :% a1, f2 :% a2)
+instance Functor (f1 :***: f2) where 
+  (g1 :***: g2) %% ProdO x1 x2 = ProdO (g1 %% x1) (g2 %% x2)
+  (g1 :***: g2) % (f1 :**: f2) = (g1 % f1) :**: (g2 % f2)
+  
+data Hom (~>) where
+  Hom :: Category (~>) => Hom (~>)
+type instance Dom (Hom (~>)) = Op (~>) :*: (~>)
+type instance Cod (Hom (~>)) = (->)
+type instance Hom (~>) :% (a, b) = a ~> b
+instance Functor (Hom (~>)) where 
+  (%%) = undefined
+  Hom % (Op g1 :**: g2) = \f -> g2 . f . g1
+  
+data DiagProd :: (* -> * -> *) -> * where 
+  DiagProd :: Category (~>) => DiagProd (~>)
+type instance Dom (DiagProd (~>)) = (~>)
+type instance Cod (DiagProd (~>)) = (~>) :*: (~>)
+type instance DiagProd (~>) :% a = (a, a)
+instance Functor (DiagProd (~>)) where 
+  DiagProd %% x = ProdO x x
+  DiagProd % f = f :**: f
diff --git a/Data/Category/Unit.hs b/Data/Category/Unit.hs
--- a/Data/Category/Unit.hs
+++ b/Data/Category/Unit.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies, MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies, GADTs, EmptyDataDecls #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Unit
@@ -15,20 +15,19 @@
 
 import Data.Category
 
--- | The one object of /1/.
-data UnitO = UnitO
+data UnitO
 
 -- | The arrows of Unit.
-data family Unit a b :: *
-data instance Unit UnitO UnitO = UnitId
+data Unit a b where
+  UnitId :: Unit UnitO UnitO
 
-newtype instance Nat Unit d f g =
-  UnitNat (Component f g UnitO)
+instance Category Unit where
   
-instance CategoryO Unit UnitO where
-  id = UnitId
-  UnitNat c ! UnitO = c
-instance CategoryA Unit UnitO UnitO UnitO where
+  data Obj Unit a where
+    UnitO :: Obj Unit UnitO
+  
+  src UnitId = UnitO
+  tgt UnitId = UnitO
+  
+  id UnitO        = UnitId
   UnitId . UnitId = UnitId
-instance Apply Unit UnitO UnitO where
-  UnitId $$ UnitO = UnitO
diff --git a/Data/Category/Void.hs b/Data/Category/Void.hs
--- a/Data/Category/Void.hs
+++ b/Data/Category/Void.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, FlexibleInstances, FlexibleContexts, MultiParamTypeClasses, EmptyDataDecls, ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, EmptyDataDecls #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Void
@@ -15,34 +15,45 @@
 -----------------------------------------------------------------------------
 module Data.Category.Void where
 
+import Prelude hiding ((.), id, Functor)
 import Data.Category
 import Data.Category.Functor
+import Data.Category.NaturalTransformation
 
+
 -- | The (empty) data type of the arrows in /0/. 
 data Void a b
 
-data instance Nat Void d f g = 
-  VoidNat
-instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Diag Void (~>)) a b where
-  Diag % _ = VoidNat
+magicVoid :: Void a b -> x
+magicVoid x = x `seq` error "we never get this far"
 
--- | The functor from /0/ to (~>), the empty diagram in (~>).
-data VoidF ((~>) :: * -> * -> *) = VoidF
-type instance Dom (VoidF (~>)) = Void
-type instance Cod (VoidF (~>)) = (~>)
+magicVoidO :: Obj Void a -> x
+magicVoidO x = x `seq` error "we never get this far"
 
--- | An initial object is the colimit of the functor from /0/ to (~>).
-class VoidColimit (~>) where
-  type InitialObject (~>) :: *
-  voidColimit :: Colimit (VoidF (~>)) (InitialObject (~>))
-  initialize :: CategoryO (~>) a => InitialObject (~>) ~> a
-  initialize = (n ! (obj :: a)) VoidNat where 
-    InitialUniversal VoidNat n = voidColimit
+
+instance Category Void where
   
--- | A terminal object is the limit of the functor from /0/ to (~>).
-class VoidLimit (~>) where
-  type TerminalObject (~>) :: *
-  voidLimit :: Limit (VoidF (~>)) (TerminalObject (~>))
-  terminate :: CategoryO (~>) a => a ~> TerminalObject (~>)
-  terminate = (n ! (obj :: a)) VoidNat where
-    TerminalUniversal VoidNat n = voidLimit
+  -- | The (empty) data type of the objects in /0/. 
+  data Obj Void a
+  
+  src = magicVoid
+  tgt = magicVoid
+  
+  id    = magicVoidO
+  a . b = magicVoid (a `seq` b)
+
+
+-- | The functor from /0/ to (~>), the empty diagram in (~>).
+data VoidDiagram ((~>) :: * -> * -> *) = VoidDiagram
+
+type instance Dom (VoidDiagram (~>)) = Void
+type instance Cod (VoidDiagram (~>)) = (~>)
+
+instance Functor (VoidDiagram (~>)) where 
+  VoidDiagram %% x = magicVoidO x
+  VoidDiagram %  f = magicVoid f
+
+
+voidNat :: (Functor f, Functor g, Dom f ~ Void, Dom g ~ Void, Cod f ~ d, Cod g ~ d)
+  => f -> g -> Nat Void d f g
+voidNat f g = Nat f g magicVoidO
diff --git a/data-category.cabal b/data-category.cabal
--- a/data-category.cabal
+++ b/data-category.cabal
@@ -1,8 +1,15 @@
 name:                data-category
-version:             0.1.0
+version:             0.2.0
 synopsis:            Restricted categories
-description:         
-  Data-category is a collection of categories, and some categorical constructions on them.
+
+description:         Data-category is a collection of categories, and some categorical constructions on them.
+                     .
+                     You can restrict the types of the objects of your category by using a GADT for the arrow type.
+                     To be able to proof to the compiler that a type is an object in some category, objects also need to be represented at the value level.
+                     Therefore the 'Category' class has an associated data type 'Obj'. This which will often also be a GADT.
+                     .
+                     See the 'Monoid', 'Boolean' and 'Product' categories for some examples.
+
 category:            Data
 license:             BSD3
 license-file:        LICENSE
@@ -10,21 +17,34 @@
 maintainer:          sjoerd@w3future.com
 stability:           experimental
 homepage:            http://github.com/sjoerdvisscher/data-category
+bug-reports:         http://github.com/sjoerdvisscher/data-category/issues
+
 build-type:          Simple
-cabal-version:       >= 1.2
+cabal-version:       >= 1.6
 
 Library
   exposed-modules:     
     Data.Category,
     Data.Category.Functor,
+    Data.Category.NaturalTransformation,
+    Data.Category.Limit,
+    Data.Category.Adjunction,
     Data.Category.Void,
     Data.Category.Unit,
-    Data.Category.Monoid,
     Data.Category.Pair,
+    Data.Category.Discrete,
+    Data.Category.Product,
+    Data.Category.Monoid,
     Data.Category.Boolean,
     Data.Category.Omega,
-    Data.Category.Hask,
     Data.Category.Kleisli,
-    Data.Category.Alg
+    Data.Category.Dialg,
+    Data.Category.Peano,
+    Data.Category.Comma
     
   build-depends:       base >= 3 && < 5
+  
+
+source-repository head
+  type:     git
+  location: git://github.com/sjoerdvisscher/data-category.git