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, GADTs, RankNTypes #-}
+{-# LANGUAGE TypeFamilies, GADTs, RankNTypes, NoImplicitPrelude #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category
@@ -19,39 +19,36 @@
     
 ) where
 
-import Prelude (($))
-import qualified Prelude
-
 infixr 8 .
 
 
 -- | Whenever objects are required at value level, they are represented by their identity arrows.
-type Obj (~>) a = a ~> a
+type Obj k a = k a a
 
--- | An instance of @Category (~>)@ declares the arrow @(~>)@ as a category.
-class Category (~>) where
+-- | An instance of @Category k@ declares the arrow @k@ as a category.
+class Category k where
   
-  src :: a ~> b -> Obj (~>) a
-  tgt :: a ~> b -> Obj (~>) b
+  src :: k a b -> Obj k a
+  tgt :: k a b -> Obj k b
 
-  (.) :: b ~> c -> a ~> b -> a ~> c
+  (.) :: k b c -> k a b -> k a c
 
 
 -- | The category with Haskell types as objects and Haskell functions as arrows.
 instance Category (->) where
   
-  src _ = Prelude.id
-  tgt _ = Prelude.id
+  src _ = \x -> x
+  tgt _ = \x -> x
   
-  (.)   = (Prelude..)    
+  f . g = \x -> f (g x)
 
 
-data Op (~>) a b = Op { unOp :: b ~> a }
+data Op k a b = Op { unOp :: k b a }
 
--- | @Op (~>)@ is opposite category of the category @(~>)@.
-instance Category (~>) => Category (Op (~>)) where
+-- | @Op k@ is opposite category of the category @k@.
+instance Category k => Category (Op k) where
   
-  src (Op a)      = Op $ tgt a
-  tgt (Op a)      = Op $ src a
+  src (Op a)      = Op (tgt a)
+  tgt (Op a)      = Op (src a)
   
-  (Op a) . (Op b) = Op $ b . a
+  (Op a) . (Op b) = Op (b . a)
diff --git a/Data/Category/Adjunction.hs b/Data/Category/Adjunction.hs
--- a/Data/Category/Adjunction.hs
+++ b/Data/Category/Adjunction.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleContexts, ScopedTypeVariables, RankNTypes #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleContexts, ScopedTypeVariables, RankNTypes, NoImplicitPrelude #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Adjunction
@@ -18,6 +18,8 @@
   , rightAdjunct
   
   -- * Adjunctions as a category
+  , idAdj
+  , composeAdj
   , AdjArrow(..)
   
   -- * Adjunctions from universal morphisms
@@ -33,9 +35,6 @@
   
 ) where
   
-import Prelude (($), id, flip)
-import Control.Monad.Instances ()
-
 import Data.Category
 import Data.Category.Functor
 import Data.Category.NaturalTransformation
@@ -61,6 +60,8 @@
 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 g un _) y = initialUniversal g (f % y) (un ! y) (rightAdjunct adj)
@@ -80,29 +81,49 @@
 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 
-  (\a -> unOp $ represent (univ (f % a)) (Op a) (f % a)) 
+  (\a -> unOp (represent (univ (f % a)) (Op a) (f % a)))
   (universalElement . univ)
     
 
+idAdj :: Category k => Adjunction k k (Id k) (Id k)
+idAdj = mkAdjunction Id Id (\x -> x) (\x -> x)
+
+composeAdj :: Adjunction d e f g -> Adjunction c d f' g' -> Adjunction c e (f' :.: f) (g :.: g')
+composeAdj (Adjunction f g u c) (Adjunction f' g' u' c') = 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')
+
+
 data AdjArrow c d where
   AdjArrow :: (Category c, Category d) => Adjunction c d f g -> AdjArrow (CatW c) (CatW d)
 
 -- | The category with categories as objects and adjunctions as arrows.
 instance Category AdjArrow where
   
-  src (AdjArrow (Adjunction _ _ _ _)) = AdjArrow $ mkAdjunction Id Id id id
-  tgt (AdjArrow (Adjunction _ _ _ _)) = AdjArrow $ mkAdjunction Id Id id id
+  src (AdjArrow (Adjunction _ _ _ _)) = AdjArrow idAdj
+  tgt (AdjArrow (Adjunction _ _ _ _)) = AdjArrow idAdj
   
-  AdjArrow (Adjunction f g u c) . AdjArrow (Adjunction f' g' u' c') = AdjArrow $ 
-    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')
+  AdjArrow x . AdjArrow y = AdjArrow (composeAdj x y)
 
 
 
+precomposeAdj :: Category e => Adjunction c d f g -> Adjunction (Nat c e) (Nat d e) (Precompose g e) (Precompose f e)
+precomposeAdj (Adjunction f g un coun) = mkAdjunction 
+  (Precompose g)
+  (Precompose f)
+  (\nh@(Nat h _ _) -> compAssocInv h g f . (nh `o` un) . idPrecompInv h)
+  (\nh@(Nat h _ _) -> idPrecomp h . (nh `o` coun) . compAssoc h f g)
+
+postcomposeAdj :: Category e => Adjunction c d f g -> Adjunction (Nat e c) (Nat e d) (Postcompose f e) (Postcompose g e)
+postcomposeAdj (Adjunction f g un coun) = mkAdjunction 
+  (Postcompose f)
+  (Postcompose g)
+  (\nh@(Nat h _ _) -> compAssoc g f h . (un `o` nh) . idPostcompInv h)
+  (\nh@(Nat h _ _) -> idPostcomp h . (coun `o` nh) . compAssocInv f g h)
+
 contAdj :: Adjunction (Op (->)) (->) (Opposite ((->) :-*: r) :.: OpOpInv (->)) ((->) :-*: r)
 contAdj = mkAdjunction
-  (Opposite (hom_X id) :.: OpOpInv)
-  (hom_X id)
-  (\_ -> flip ($))
-  (\_ -> Op (flip ($)))
+  (Opposite (hom_X (\x -> x)) :.: OpOpInv)
+  (hom_X (\x -> x))
+  (\_ x f -> f x)
+  (\_ -> Op (\x f -> f x))
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, GADTs, TypeOperators, ScopedTypeVariables, UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies, GADTs, TypeOperators, ScopedTypeVariables, UndecidableInstances, NoImplicitPrelude #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Boolean
@@ -14,8 +14,6 @@
 -----------------------------------------------------------------------------
 module Data.Category.Boolean where
 
-import Prelude hiding ((.), id, Functor)
-
 import Data.Category
 import Data.Category.Functor
 import Data.Category.NaturalTransformation
@@ -48,7 +46,6 @@
   F2T . Fls = F2T
   Tru . F2T = F2T
   Tru . Tru = Tru
-  _      . _      = error "Other combinations should not type check"
 
 
 -- | False is the initial object in the Boolean category.
@@ -57,7 +54,6 @@
   initialObject = Fls
   initialize Fls = Fls
   initialize Tru = F2T
-  initialize _   = error "Other values should not type check"
   
 -- | True is the terminal object in the Boolean category.
 instance HasTerminalObject Boolean where
@@ -65,7 +61,6 @@
   terminalObject = Tru
   terminate Fls = F2T
   terminate Tru = Tru
-  terminate _   = error "Other values should not type check"
 
 
 type instance BinaryProduct Boolean Fls Fls = Fls
@@ -80,19 +75,16 @@
   proj1 Fls Tru = Fls
   proj1 Tru Fls = F2T
   proj1 Tru Tru = Tru
-  proj1 _   _   = error "Other combinations should not type check"
   proj2 Fls Fls = Fls
   proj2 Fls Tru = F2T
   proj2 Tru Fls = Fls
   proj2 Tru Tru = Tru
-  proj2 _   _   = error "Other combinations should not type check"
     
   Fls &&& Fls = Fls
   Fls &&& F2T = Fls
   F2T &&& Fls = Fls
   F2T &&& F2T = F2T
   Tru &&& Tru = Tru
-  _   &&& _   = error "Other combinations should not type check"
 
 
 type instance BinaryCoproduct Boolean Fls Fls = Fls
@@ -107,19 +99,16 @@
   inj1 Fls Tru = F2T
   inj1 Tru Fls = Tru
   inj1 Tru Tru = Tru
-  inj1 _   _   = error "Other combinations should not type check"
   inj2 Fls Fls = Fls
   inj2 Fls Tru = Tru
   inj2 Tru Fls = F2T
   inj2 Tru Tru = Tru
-  inj2 _   _   = error "Other combinations should not type check"
     
   Fls ||| Fls = Fls
   F2T ||| F2T = F2T
   F2T ||| Tru = Tru
   Tru ||| F2T = Tru
   Tru ||| Tru = Tru
-  _   ||| _   = error "Other combinations should not type check"
 
 
 type instance Exponential Boolean Fls Fls = Tru
@@ -134,13 +123,11 @@
   apply Fls Tru = F2T
   apply Tru Fls = Fls
   apply Tru Tru = Tru
-  apply _   _   = error "Other combinations should not type check"
   
   tuple Fls Fls = F2T
   tuple Fls Tru = Tru
   tuple Tru Fls = Fls
   tuple Tru Tru = Tru
-  tuple _   _   = error "Other combinations should not type check"
   
   Fls ^^^ Fls = Tru
   Fls ^^^ F2T = F2T
@@ -171,16 +158,3 @@
 falseProductComonoid :: ComonoidObject (ProductFunctor Boolean) Fls
 falseProductComonoid = ComonoidObject F2T Fls
 
-
-data NatAsFunctor f g where
-  NatAsFunctor :: (Functor f, Functor g, Category c, Category d, Dom f ~ c, Cod f ~ d, Dom g ~ c, Cod g ~ d)
-               => Nat (Dom f) (Cod f) f g -> NatAsFunctor f g
-type instance Dom (NatAsFunctor f g) = Dom f :**: Boolean
-type instance Cod (NatAsFunctor f g) = Cod f
-type instance NatAsFunctor f g :% (a, Fls) = f :% a
-type instance NatAsFunctor f g :% (a, Tru) = g :% a
--- | A natural transformation @Nat c d@ is isomorphic to a functor from @c :**: 2@ to @d@.
-instance (Category (Dom f), Category (Cod f)) => Functor (NatAsFunctor f g) where
-  NatAsFunctor (Nat f _ _) % (a :**: Fls) = f % a
-  NatAsFunctor (Nat _ g _) % (a :**: Tru) = g % a
-  NatAsFunctor n           % (a :**: F2T) = n ! a
diff --git a/Data/Category/CartesianClosed.hs b/Data/Category/CartesianClosed.hs
--- a/Data/Category/CartesianClosed.hs
+++ b/Data/Category/CartesianClosed.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, Rank2Types, ScopedTypeVariables, UndecidableInstances, TypeSynonymInstances #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, Rank2Types, ScopedTypeVariables, UndecidableInstances, TypeSynonymInstances, NoImplicitPrelude #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.CartesianClosed
@@ -10,8 +10,6 @@
 -----------------------------------------------------------------------------
 module Data.Category.CartesianClosed where
   
-import Prelude (($))
-
 import Data.Category
 import Data.Category.Functor
 import Data.Category.NaturalTransformation
@@ -21,22 +19,22 @@
 import Data.Category.Monoidal as M
 
 
-type family Exponential (~>) y z :: *
+type family Exponential (k :: * -> * -> *) y z :: *
 
 -- | A category is cartesian closed if it has all products and exponentials for all objects.
-class (HasTerminalObject (~>), HasBinaryProducts (~>)) => CartesianClosed (~>) where
+class (HasTerminalObject k, HasBinaryProducts k) => CartesianClosed k where
   
-  apply :: Obj (~>) y -> Obj (~>) z -> BinaryProduct (~>) (Exponential (~>) y z) y ~> z
-  tuple :: Obj (~>) y -> Obj (~>) z -> z ~> Exponential (~>) y (BinaryProduct (~>) z y)
-  (^^^) :: (z1 ~> z2) -> (y2 ~> y1) -> (Exponential (~>) y1 z1 ~> Exponential (~>) y2 z2)
+  apply :: Obj k y -> Obj k z -> k (BinaryProduct k (Exponential k y z) y) z
+  tuple :: Obj k y -> Obj k z -> k z (Exponential k y (BinaryProduct k z y))
+  (^^^) :: k z1 z2 -> k y2 y1 -> k (Exponential k y1 z1) (Exponential k y2 z2)
 
 
-data ExpFunctor ((~>) :: * -> * -> *) = ExpFunctor
-type instance Dom (ExpFunctor (~>)) = Op (~>) :**: (~>)
-type instance Cod (ExpFunctor (~>)) = (~>)
-type instance (ExpFunctor (~>)) :% (y, z) = Exponential (~>) y z
+data ExpFunctor (k :: * -> * -> *) = ExpFunctor
+type instance Dom (ExpFunctor k) = Op k :**: k
+type instance Cod (ExpFunctor k) = k
+type instance (ExpFunctor k) :% (y, z) = Exponential k y z
 -- | The exponential as a bifunctor.
-instance CartesianClosed (~>) => Functor (ExpFunctor (~>)) where
+instance CartesianClosed k => Functor (ExpFunctor k) where
   ExpFunctor % (Op y :**: z) = z ^^^ y
 
 
@@ -66,7 +64,7 @@
 type instance ToTuple1 y z :% a = Tuple1 z y a
 -- | 'ToTuple1' converts an object @a@ to the functor 'Tuple1' @a@.
 instance (Category y, Category z) => Functor (ToTuple1 y z) where
-  ToTuple1 % f = Nat (Tuple1 (src f)) (Tuple1 (tgt f)) $ \z -> f :**: z
+  ToTuple1 % f = Nat (Tuple1 (src f)) (Tuple1 (tgt f)) (\z -> f :**: z)
 
 data ToTuple2 (y :: * -> * -> *) (z :: * -> * -> *) = ToTuple2
 type instance Dom (ToTuple2 y z) = y
@@ -74,7 +72,7 @@
 type instance ToTuple2 y z :% a = Tuple2 z y a
 -- | 'ToTuple2' converts an object @a@ to the functor 'Tuple2' @a@.
 instance (Category y, Category z) => Functor (ToTuple2 y z) where
-  ToTuple2 % f = Nat (Tuple2 (src f)) (Tuple2 (tgt f)) $ \y -> y :**: f
+  ToTuple2 % f = Nat (Tuple2 (src f)) (Tuple2 (tgt f)) (\y -> y :**: f)
 
 
 type instance Exponential Cat (CatW c) (CatW d) = CatW (Nat c d)
@@ -88,36 +86,36 @@
 
 
 -- | The product functor is left adjoint the the exponential functor.
-curryAdj :: CartesianClosed (~>) 
-         => Obj (~>) y 
-         -> Adjunction (~>) (~>) 
-              (ProductFunctor (~>) :.: Tuple2 (~>) (~>) y) 
-              (ExpFunctor (~>) :.: Tuple1 (Op (~>)) (~>) y)
+curryAdj :: CartesianClosed k 
+         => Obj k y 
+         -> Adjunction k k 
+              (ProductFunctor k :.: Tuple2 k k y) 
+              (ExpFunctor k :.: Tuple1 (Op k) k y)
 curryAdj y = mkAdjunction (ProductFunctor :.: Tuple2 y) (ExpFunctor :.: Tuple1 (Op y)) (tuple y) (apply y)
 
 -- | From the adjunction between the product functor and the exponential functor we get the curry and uncurry functions,
 --   generalized to any cartesian closed category.
-curry :: CartesianClosed (~>) => Obj (~>) x -> Obj (~>) y -> Obj (~>) z -> BinaryProduct (~>) x y ~> z -> x ~> Exponential (~>) y z
+curry :: CartesianClosed k => Obj k x -> Obj k y -> Obj k z -> k (BinaryProduct k x y) z -> k x (Exponential k y z)
 curry x y _ = leftAdjunct (curryAdj y) x
 
-uncurry :: CartesianClosed (~>) => Obj (~>) x -> Obj (~>) y -> Obj (~>) z -> x ~> Exponential (~>) y z -> BinaryProduct (~>) x y ~> z
+uncurry :: CartesianClosed k => Obj k x -> Obj k y -> Obj k z -> k x (Exponential k y z) -> k (BinaryProduct k x y) z
 uncurry _ y z = rightAdjunct (curryAdj y) z
 
 -- | From every adjunction we get a monad, in this case the State monad.
-type State (~>) s a = Exponential (~>) s (BinaryProduct (~>) a s)
+type State k s a = Exponential k s (BinaryProduct k a s)
 
-stateMonadReturn :: CartesianClosed (~>) => Obj (~>) s -> Obj (~>) a -> a ~> State (~>) s a
-stateMonadReturn s a = M.unit (adjunctionMonad $ curryAdj s) ! a
+stateMonadReturn :: CartesianClosed k => Obj k s -> Obj k a -> k a (State k s a)
+stateMonadReturn s a = M.unit (adjunctionMonad (curryAdj s)) ! a
 
-stateMonadJoin :: CartesianClosed (~>) => Obj (~>) s -> Obj (~>) a -> State (~>) s (State (~>) s a) ~> State (~>) s a
-stateMonadJoin s a = M.multiply (adjunctionMonad $ curryAdj s) ! a
+stateMonadJoin :: CartesianClosed k => Obj k s -> Obj k a -> k (State k s (State k s a)) (State k s a)
+stateMonadJoin s a = M.multiply (adjunctionMonad (curryAdj s)) ! a
 
 -- ! From every adjunction we also get a comonad, the Context comonad in this case.
-type Context (~>) s a = BinaryProduct (~>) (Exponential (~>) s a) s
+type Context k s a = BinaryProduct k (Exponential k s a) s
 
-contextComonadExtract :: CartesianClosed (~>) => Obj (~>) s -> Obj (~>) a -> Context (~>) s a ~> a
-contextComonadExtract s a = M.counit (adjunctionComonad $ curryAdj s) ! a
+contextComonadExtract :: CartesianClosed k => Obj k s -> Obj k a -> k (Context k s a) a
+contextComonadExtract s a = M.counit (adjunctionComonad (curryAdj s)) ! a
 
-contextComonadDuplicate :: CartesianClosed (~>) => Obj (~>) s -> Obj (~>) a -> Context (~>) s a ~> Context (~>) s (Context (~>) s a)
-contextComonadDuplicate s a = M.comultiply (adjunctionComonad $ curryAdj s) ! a
+contextComonadDuplicate :: CartesianClosed k => Obj k s -> Obj k a -> k (Context k s a) (Context k s (Context k s a))
+contextComonadDuplicate s a = M.comultiply (adjunctionComonad (curryAdj s)) ! a
 
diff --git a/Data/Category/Comma.hs b/Data/Category/Comma.hs
--- a/Data/Category/Comma.hs
+++ b/Data/Category/Comma.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, GADTs, FlexibleContexts, FlexibleInstances #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, GADTs, FlexibleContexts, FlexibleInstances, ScopedTypeVariables, NoImplicitPrelude #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Comma
@@ -12,15 +12,15 @@
 -----------------------------------------------------------------------------
 module Data.Category.Comma where
 
-import Prelude()
-
 import Data.Category
 import Data.Category.Functor
+import Data.Category.Limit
+import Data.Category.RepresentableFunctor
 
 
 data CommaO :: * -> * -> * -> * where
-  CommaO :: (Cod t ~ (~>), Cod s ~ (~>))
-    => Obj (Dom t) a -> ((t :% a) ~> (s :% b)) -> Obj (Dom s) b -> CommaO t s (a, b)
+  CommaO :: (Cod t ~ k, Cod s ~ k)
+    => Obj (Dom t) a -> k (t :% a) (s :% b) -> Obj (Dom s) b -> CommaO t s (a, b)
     
 data (:/\:) :: * -> * -> * -> * -> * where 
   CommaA :: 
@@ -30,11 +30,14 @@
     CommaO t s (a', b') ->
     (t :/\: s) (a, b) (a', b')
 
+commaId :: CommaO t s (a, b) -> Obj (t :/\: s) (a, b)
+commaId o@(CommaO a _ b) = CommaA o a b o
+
 -- | The comma category T \\downarrow S
 instance (Category (Dom t), Category (Dom s)) => Category (t :/\: s) where
     
-  src (CommaA so@(CommaO a _ b) _ _ _)    = CommaA so a        b        so
-  tgt (CommaA _ _ _ to@(CommaO a _ b))    = CommaA to a        b        to
+  src (CommaA so _ _ _) = commaId so
+  tgt (CommaA _ _ _ to) = commaId to
   
   (CommaA _ g h to) . (CommaA so g' h' _) = CommaA so (g . g') (h . h') to
 
@@ -44,3 +47,30 @@
 
 type (c `ObjectsUnder` a) = Id c `ObjectsFUnder` a
 type (c `ObjectsOver`  a) = Id c `ObjectsFOver`  a
+
+
+initialUniversalComma :: forall u x c a a_
+                       . (Functor u, c ~ (u `ObjectsFUnder` x), HasInitialObject c, (a_, a) ~ InitialObject c)
+                      => u -> InitialUniversal x u a
+initialUniversalComma u = case initialObject :: Obj c (a_, a) of
+  CommaA (CommaO _ mor a) _ _ _ -> 
+    initialUniversal u a mor factorizer
+      where
+        factorizer :: forall y. Obj (Dom u) y -> Cod u x (u :% y) -> Dom u a y
+        factorizer y arr = case (init (commaId (CommaO y arr y))) of CommaA _ _ f _ -> f
+          where
+            init :: Obj c (y, y) -> c (a_, a) (y, y)
+            init = initialize
+
+terminalUniversalComma :: forall u x c a a_
+                        . (Functor u, c ~ (u `ObjectsFOver` x), HasTerminalObject c, (a, a_) ~ TerminalObject c)
+                       => u -> TerminalUniversal x u a
+terminalUniversalComma u = case terminalObject :: Obj c (a, a_) of
+  CommaA (CommaO a mor _) _ _ _ ->
+    terminalUniversal u a mor factorizer
+      where
+        factorizer :: forall y. Obj (Dom u) y -> Cod u (u :% y) x -> Dom u y a
+        factorizer y arr = case (term (commaId (CommaO y arr y))) of CommaA _ f _ _ -> f
+          where
+            term :: Obj c (y, y) -> c (y, y) (a, a_)
+            term = terminate
diff --git a/Data/Category/Coproduct.hs b/Data/Category/Coproduct.hs
--- a/Data/Category/Coproduct.hs
+++ b/Data/Category/Coproduct.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, FlexibleContexts #-}
+{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, FlexibleContexts, NoImplicitPrelude #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Coproduct
@@ -10,12 +10,14 @@
 -----------------------------------------------------------------------------
 module Data.Category.Coproduct where
 
-import Prelude (error)
-
 import Data.Category
 import Data.Category.Functor
 
+import Data.Category.NaturalTransformation
+import Data.Category.Product
+import Data.Category.Unit
 
+
 data I1 a
 data I2 a
 
@@ -23,7 +25,7 @@
   I1 :: c1 a1 b1 -> (:++:) c1 c2 (I1 a1) (I1 b1)
   I2 :: c2 a2 b2 -> (:++:) c1 c2 (I2 a2) (I2 b2)
 
--- | The coproduct category of category @c1@ and @c2@.
+-- | The coproduct category of categories @c1@ and @c2@.
 instance (Category c1, Category c2) => Category (c1 :++: c2) where
   
   src (I1 a)      = I1 (src a)
@@ -33,7 +35,6 @@
 
   (I1 a) . (I1 b) = I1 (a . b)
   (I2 a) . (I2 b) = I2 (a . b)
-  _      . _      = error "Other combinations should not type check"
 
   
   
@@ -64,13 +65,13 @@
   (g :+++: _) % I1 f = I1 (g % f)
   (_ :+++: g) % I2 f = I2 (g % f)
   
-data CodiagCoprod ((~>) :: * -> * -> *) = CodiagCoprod
-type instance Dom (CodiagCoprod (~>)) = (~>) :++: (~>)
-type instance Cod (CodiagCoprod (~>)) = (~>)
-type instance CodiagCoprod (~>) :% I1 a = a
-type instance CodiagCoprod (~>) :% I2 a = a
+data CodiagCoprod (k :: * -> * -> *) = CodiagCoprod
+type instance Dom (CodiagCoprod k) = k :++: k
+type instance Cod (CodiagCoprod k) = k
+type instance CodiagCoprod k :% I1 a = a
+type instance CodiagCoprod k :% I2 a = a
 -- | 'CodiagCoprod' is the codiagonal functor for coproducts.
-instance Category (~>) => Functor (CodiagCoprod (~>)) where 
+instance Category k => Functor (CodiagCoprod k) where 
   CodiagCoprod % I1 f = f
   CodiagCoprod % I2 f = f
 
@@ -94,3 +95,37 @@
   Cotuple2 a % I1 _ = a
   Cotuple2 _ % I2 f = f
 
+
+data (:>>:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where
+  I1A :: c1 a1 b1 -> (:>>:) c1 c2 (I1 a1) (I1 b1)
+  I12 :: Obj c1 a -> Obj c2 b -> (:>>:) c1 c2 (I1 a) (I2 b)
+  I2A :: c2 a2 b2 -> (:>>:) c1 c2 (I2 a2) (I2 b2)
+
+-- | The directed coproduct category of categories @c1@ and @c2@.
+instance (Category c1, Category c2) => Category (c1 :>>: c2) where
+
+  src (I1A a)   = I1A (src a)
+  src (I12 a _) = I1A a
+  src (I2A a)   = I2A (src a)
+  tgt (I1A a)   = I1A (tgt a)
+  tgt (I12 _ b) = I2A b
+  tgt (I2A a)   = I2A (tgt a)
+
+  (I1A a) . (I1A b) = I1A (a . b)
+  (I12 _ a) . (I1A b) = I12 (src b) a
+  (I2A a) . (I12 b _) = I12 b (tgt a)
+  (I2A a) . (I2A b) = I2A (a . b)
+
+
+
+
+data NatAsFunctor f g = NatAsFunctor (Nat (Dom f) (Cod f) f g)
+type instance Dom (NatAsFunctor f g) = Dom f :**: (Unit :>>: Unit)
+type instance Cod (NatAsFunctor f g) = Cod f
+type instance NatAsFunctor f g :% (a, I1 ()) = f :% a
+type instance NatAsFunctor f g :% (a, I2 ()) = g :% a
+-- | A natural transformation @Nat c d@ is isomorphic to a functor from @c :**: 2@ to @d@.
+instance (Functor f, Functor g, Dom f ~ Dom g, Cod f ~ Cod g) => Functor (NatAsFunctor f g) where
+  NatAsFunctor (Nat f _ _) % (a :**: I1A Unit) = f % a
+  NatAsFunctor (Nat _ g _) % (a :**: I2A Unit) = g % a
+  NatAsFunctor n           % (a :**: I12 Unit Unit) = n ! 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, ScopedTypeVariables, UndecidableInstances #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleInstances, FlexibleContexts, ViewPatterns, ScopedTypeVariables, UndecidableInstances, NoImplicitPrelude #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Dialg
@@ -12,9 +12,6 @@
 -----------------------------------------------------------------------------
 module Data.Category.Dialg where
 
-import Prelude (($), id)
-import qualified Prelude
-
 import Data.Category
 import Data.Category.Functor
 import Data.Category.NaturalTransformation
@@ -46,7 +43,7 @@
   src (DialgA s _ _) = dialgId s
   tgt (DialgA _ t _) = dialgId t
   
-  DialgA _ t f . DialgA s _ g = DialgA s t $ f . g
+  DialgA _ t f . DialgA s _ g = DialgA s t (f . g)
 
 
 
@@ -70,35 +67,7 @@
 
 
 
-newtype FixF f = InF { outF :: f :% FixF f }
 
--- | Catamorphisms for endofunctors in Hask.
-cataHask :: Prelude.Functor f => Cata (EndoHask f) a
-cataHask a@(Dialgebra _ f) = DialgA (dialgebra initialObject) a $ cata_f where cata_f = f . (EndoHask % cata_f) . outF 
-
--- | Anamorphisms for endofunctors in Hask.
-anaHask :: Prelude.Functor f => Ana (EndoHask f) a
-anaHask a@(Dialgebra _ f) = DialgA a (dialgebra terminalObject) $ ana_f where ana_f = InF . (EndoHask % ana_f) . f 
-
-
--- | 'FixF' provides the initial F-algebra for endofunctors in Hask.
-instance Prelude.Functor f => HasInitialObject (Dialg (EndoHask f) (Id (->))) where
-  
-  type InitialObject (Dialg (EndoHask f) (Id (->))) = FixF (EndoHask f)
-  
-  initialObject = dialgId $ Dialgebra id InF
-  initialize a = cataHask (dialgebra a)
-  
--- | 'FixF' also provides the terminal F-coalgebra for endofunctors in Hask.
-instance Prelude.Functor f => HasTerminalObject (Dialg (Id (->)) (EndoHask f)) where
-
-  type TerminalObject (Dialg (Id (->)) (EndoHask f)) = FixF (EndoHask f)
-  
-  terminalObject = dialgId $ Dialgebra id outF
-  terminate a = anaHask (dialgebra a)
-  
-
-
 data NatNum = Z () | S NatNum
 primRec :: (() -> t) -> (t -> t) -> NatNum -> t
 primRec z _ (Z ()) = z ()
@@ -110,9 +79,9 @@
   
   type InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) = NatNum
     
-  initialObject = dialgId $ Dialgebra id (Z :**: S)
+  initialObject = dialgId (Dialgebra (\x -> x) (Z :**: S))
   
-  initialize (dialgebra -> d@(Dialgebra _ (z :**: s))) = DialgA (dialgebra initialObject) d $ primRec z s
+  initialize (dialgebra -> d@(Dialgebra _ (z :**: s))) = DialgA (dialgebra initialObject) d (primRec z s)
 
 
 
@@ -121,10 +90,10 @@
 type instance Cod (FreeAlg m) = Alg m
 type instance FreeAlg m :% a = m :% a
 -- | @FreeAlg@ M takes @x@ to the free algebra @(M x, mu_x)@ of the monad @M@.
-instance (Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Functor (FreeAlg m) where
-  FreeAlg m % f = DialgA (alg (src f)) (alg (tgt f)) $ monadFunctor m % f
+instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (FreeAlg m) where
+  FreeAlg m % f = DialgA (alg (src f)) (alg (tgt f)) (monadFunctor m % f)
     where
-      alg :: Obj (~>) x -> Algebra m (m :% x)
+      alg :: Obj k x -> Algebra m (m :% x)
       alg x = Dialgebra (monadFunctor m % x) (multiply m ! x)
 
 data ForgetAlg m = ForgetAlg
@@ -132,11 +101,11 @@
 type instance Cod (ForgetAlg m) = Dom m
 type instance ForgetAlg m :% a = a
 -- | @ForgetAlg m@ is the forgetful functor for @Alg m@.
-instance (Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Functor (ForgetAlg m) where
+instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (ForgetAlg m) where
   ForgetAlg % DialgA _ _ f = f
 
-eilenbergMooreAdj :: (Functor m, Dom m ~ (~>), Cod m ~ (~>)) 
-  => Monad m -> A.Adjunction (Alg m) (~>) (FreeAlg m) (ForgetAlg m)
+eilenbergMooreAdj :: (Functor m, Dom m ~ k, Cod m ~ k) 
+  => Monad m -> A.Adjunction (Alg m) k (FreeAlg m) (ForgetAlg m)
 eilenbergMooreAdj m = A.mkAdjunction (FreeAlg m) ForgetAlg
   (\x -> unit m ! x)
   (\(DialgA (Dialgebra _ h) _ _) -> DialgA (Dialgebra (src h) (monadFunctor m % h)) (Dialgebra (tgt h) h) h)
diff --git a/Data/Category/Discrete.hs b/Data/Category/Discrete.hs
deleted file mode 100644
--- a/Data/Category/Discrete.hs
+++ /dev/null
@@ -1,119 +0,0 @@
-{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, RankNTypes, ScopedTypeVariables, FlexibleContexts, FlexibleInstances, UndecidableInstances #-}
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Category.Discrete
--- 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 (
-
-  -- * Discrete Categories
-    Discrete(..)
-  , Z, S
-  , Void
-  , Unit
-  , Pair
-  , magicZ
-  
-  -- * Functors
-  , Succ(..)
-  , DiscreteDiagram(..)
-    
-  -- * Natural Transformations
-  , voidNat
-    
-) where
-
-import Prelude hiding ((.), id, Functor, product)
-
-import Data.Category
-import Data.Category.Functor
-import Data.Category.NaturalTransformation
-
-
-data Z
-data S n
-
--- | The arrows in Discrete n, a finite set of identity arrows.
-data Discrete :: * -> * -> * -> * where
-  Z :: Discrete (S n) Z Z
-  S :: Discrete n a a -> Discrete (S n) (S a) (S a)
-
-
-magicZ :: Discrete Z a b -> x
-magicZ x = x `seq` error "we never get this far"
-
-
--- | @Discrete Z@ is the discrete category with no objects.
-instance Category (Discrete Z) where
-  
-  src   = magicZ
-  tgt   = magicZ
-  
-  a . b = magicZ (a `seq` b)
-
-
--- | @Discrete (S n)@ is the discrete category with one object more than @Discrete n@.
-instance Category (Discrete n) => Category (Discrete (S n)) where
-  
-  src Z     = Z
-  src (S a) = S $ src a
-  
-  tgt Z     = Z
-  tgt (S a) = S $ tgt a
-  
-  Z   . Z   = Z
-  S a . S b = S (a . b)
-  _   . _   = error "Other combinations should not type-check."
-
-
--- | 'Void' is the empty category.
-type Void = Discrete Z
--- | 'Unit' is the discrete category with one object.
-type Unit = Discrete (S Z)
--- | 'Pair' is the discrete category with two objects.
-type Pair = Discrete (S (S Z))
-
-
-data 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
--- | 'Succ' maps each object in @Discrete n@ to its successor in @Discrete (S n)@.
-instance (Category (Discrete n)) => Functor (Succ n) where
-  Succ % Z     = S Z
-  Succ % (S a) = S (S a)
-
-
-infixr 7 :::
-
--- | The functor from @Discrete n@ to @(~>)@, a diagram of @n@ objects in @(~>)@. 
-data DiscreteDiagram :: (* -> * -> *) -> * -> * -> * where
-  Nil   :: DiscreteDiagram (~>) Z ()
-  (:::) :: (Category (~>), Category (Discrete n)) 
-        => Obj (~>) x -> DiscreteDiagram (~>) n xs -> DiscreteDiagram (~>) (S n) (x, xs)
-  
-type instance Dom (DiscreteDiagram (~>) n xs) = Discrete n
-type instance Cod (DiscreteDiagram (~>) n xs) = (~>)
-type instance DiscreteDiagram (~>) (S n) (x, xs) :% Z = x
-type instance DiscreteDiagram (~>) (S n) (x, xs) :% (S a) = DiscreteDiagram (~>) n xs :% a
-
--- | The empty diagram.
-instance Category (~>) => Functor (DiscreteDiagram (~>) Z ()) where
-  Nil        % f = magicZ f
-
--- | A diagram with one more object.
-instance Functor (DiscreteDiagram (~>) n xs) => Functor (DiscreteDiagram (~>) (S n) (x, xs)) where
-  (x ::: _)  % Z   = x
-  (_ ::: xs) % S n = xs % n
-
-
--- | Natural transformations in 'Void' are trivial.
-voidNat :: (Functor f, Functor g, Category d, Dom f ~ Void, Dom g ~ Void, Cod f ~ d, Cod g ~ d)
-  => f -> g -> Nat Void d f g
-voidNat f g = Nat f g magicZ
diff --git a/Data/Category/Fix.hs b/Data/Category/Fix.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/Fix.hs
@@ -0,0 +1,65 @@
+{-# LANGUAGE TypeOperators, TypeFamilies, UndecidableInstances, NoImplicitPrelude #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Category.AddObject
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  sjoerd@w3future.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+-----------------------------------------------------------------------------
+module Data.Category.Fix where
+  
+import Data.Category
+import Data.Category.Functor
+import Data.Category.Limit
+
+import Data.Category.Unit
+import Data.Category.Coproduct
+
+
+newtype Fix f a b = Fix (f (Fix f) a b)
+
+-- | @`Fix` f@ is the fixed point category for a category combinator `f`.
+instance Category (f (Fix f)) => Category (Fix f) where
+  src (Fix a) = Fix (src a)
+  tgt (Fix a) = Fix (tgt a)
+  Fix a . Fix b = Fix (a . b)
+
+-- | @Fix f@ inherits its (co)limits from @f (Fix f)@.
+instance HasInitialObject (f (Fix f)) => HasInitialObject (Fix f) where
+  type InitialObject (Fix f) = InitialObject (f (Fix f))
+  initialObject = Fix initialObject
+  initialize (Fix o) = Fix (initialize o)
+
+-- | @Fix f@ inherits its (co)limits from @f (Fix f)@.
+instance HasTerminalObject (f (Fix f)) => HasTerminalObject (Fix f) where
+  type TerminalObject (Fix f) = TerminalObject (f (Fix f))
+  terminalObject = Fix terminalObject
+  terminate (Fix o) = Fix (terminate o)
+
+type instance BinaryProduct (Fix f) a b = BinaryProduct (f (Fix f)) a b
+-- | @Fix f@ inherits its (co)limits from @f (Fix f)@.
+instance HasBinaryProducts (f (Fix f)) => HasBinaryProducts (Fix f) where
+  proj1 (Fix a) (Fix b) = Fix (proj1 a b)
+  proj2 (Fix a) (Fix b) = Fix (proj2 a b)
+  Fix a &&& Fix b = Fix (a &&& b)
+  
+type instance BinaryCoproduct (Fix f) a b = BinaryCoproduct (f (Fix f)) a b
+-- | @Fix f@ inherits its (co)limits from @f (Fix f)@.
+instance HasBinaryCoproducts (f (Fix f)) => HasBinaryCoproducts (Fix f) where
+  inj1 (Fix a) (Fix b) = Fix (inj1 a b)
+  inj2 (Fix a) (Fix b) = Fix (inj2 a b)
+  Fix a ||| Fix b = Fix (a ||| b)
+
+data Wrap (f :: (* -> * -> *) -> * -> * -> *) = Wrap
+type instance Dom (Wrap f) = f (Fix f)
+type instance Cod (Wrap f) = Fix f
+type instance Wrap f :% a = a
+-- | The `Wrap` functor wraps `Fix` around @f (Fix f)@.
+instance Category (f (Fix f)) => Functor (Wrap f) where
+  Wrap % f = Fix f
+
+-- | Take the `Omega` category, add a new disctinct object, and an arrow from that object to every object in `Omega`,
+--   and you get `Omega` again.
+type Omega = Fix ((:>>:) Unit)
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, FlexibleInstances, UndecidableInstances, GADTs, RankNTypes #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, FlexibleContexts, FlexibleInstances, UndecidableInstances, GADTs, RankNTypes, NoImplicitPrelude #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Functor
@@ -27,7 +27,6 @@
   , Opposite(..)
   , OpOp(..)
   , OpOpInv(..)
-  , EndoHask(..)
   
   -- *** Related to the product category
   , Proj1(..)
@@ -46,9 +45,6 @@
   
 ) where
   
-import Prelude hiding ((.), Functor)
-import qualified Prelude
-  
 import Data.Category
 import Data.Category.Product
 
@@ -87,14 +83,14 @@
 
 
 
-data Id ((~>) :: * -> * -> *) = Id
+data Id (k :: * -> * -> *) = Id
 
-type instance Dom (Id (~>)) = (~>)
-type instance Cod (Id (~>)) = (~>)
-type instance Id (~>) :% a = a
+type instance Dom (Id k) = k
+type instance Cod (Id k) = k
+type instance Id k :% a = a
 
--- | The identity functor on (~>)
-instance Category (~>) => Functor (Id (~>)) where 
+-- | The identity functor on k
+instance Category k => Functor (Id k) where 
   _ % f = f
 
 
@@ -134,43 +130,31 @@
 
 -- | The dual of a functor
 instance (Category (Dom f), Category (Cod f)) => Functor (Opposite f) where
-  Opposite f % Op a = Op $ f % a
+  Opposite f % Op a = Op (f % a)
 
 
-data OpOp ((~>) :: * -> * -> *) = OpOp
+data OpOp (k :: * -> * -> *) = OpOp
 
-type instance Dom (OpOp (~>)) = Op (Op (~>))
-type instance Cod (OpOp (~>)) = (~>)
-type instance OpOp (~>) :% a = a
+type instance Dom (OpOp k) = Op (Op k)
+type instance Cod (OpOp k) = k
+type instance OpOp k :% a = a
 
 -- | The @Op (Op x) = x@ functor.
-instance Category (~>) => Functor (OpOp (~>)) where
+instance Category k => Functor (OpOp k) where
   OpOp % Op (Op f) = f
 
 
-data OpOpInv ((~>) :: * -> * -> *) = OpOpInv
+data OpOpInv (k :: * -> * -> *) = OpOpInv
 
-type instance Dom (OpOpInv (~>)) = (~>)
-type instance Cod (OpOpInv (~>)) = Op (Op (~>))
-type instance OpOpInv (~>) :% a = a
+type instance Dom (OpOpInv k) = k
+type instance Cod (OpOpInv k) = Op (Op k)
+type instance OpOpInv k :% a = a
 
 -- | The @x = Op (Op x)@ functor.
-instance Category (~>) => Functor (OpOpInv (~>)) where
+instance Category k => Functor (OpOpInv k) where
   OpOpInv % f = Op (Op f)
 
 
-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
-
--- | 'EndoHask' is a wrapper to turn instances of the 'Functor' class into categorical functors.
-instance Functor (EndoHask f) where
-  EndoHask % f = fmap f
-
-
 data Proj1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Proj1
 
 type instance Dom (Proj1 c1 c2) = c1 :**: c2
@@ -204,14 +188,14 @@
   (g1 :***: g2) % (f1 :**: f2) = (g1 % f1) :**: (g2 % f2)
   
   
-data DiagProd ((~>) :: * -> * -> *) = DiagProd
+data DiagProd (k :: * -> * -> *) = DiagProd
 
-type instance Dom (DiagProd (~>)) = (~>)
-type instance Cod (DiagProd (~>)) = (~>) :**: (~>)
-type instance DiagProd (~>) :% a = (a, a)
+type instance Dom (DiagProd k) = k
+type instance Cod (DiagProd k) = k :**: k
+type instance DiagProd k :% a = (a, a)
 
 -- | 'DiagProd' is the diagonal functor for products.
-instance Category (~>) => Functor (DiagProd (~>)) where 
+instance Category k => Functor (DiagProd k) where 
   DiagProd % f = f :**: f
 
 
@@ -237,23 +221,23 @@
   Tuple2 a % f = f :**: a
 
 
-data Hom ((~>) :: * -> * -> *) = Hom  
+data Hom (k :: * -> * -> *) = Hom  
 
-type instance Dom (Hom (~>)) = Op (~>) :**: (~>)
-type instance Cod (Hom (~>)) = (->)
-type instance (Hom (~>)) :% (a1, a2) = a1 ~> a2
+type instance Dom (Hom k) = Op k :**: k
+type instance Cod (Hom k) = (->)
+type instance (Hom k) :% (a1, a2) = k a1 a2
 
 -- | The Hom functor, Hom(--,--), a bifunctor contravariant in its first argument and covariant in its second argument.
-instance Category (~>) => Functor (Hom (~>)) where 
+instance Category k => Functor (Hom k) where 
   Hom % (Op f1 :**: f2) = \g -> f2 . g . f1
 
 
-type x :*-: (~>) = Hom (~>) :.: Tuple1 (Op (~>)) (~>) x
+type x :*-: k = Hom k :.: Tuple1 (Op k) k x
 -- | The covariant functor Hom(X,--)
-homX_ :: Category (~>) => Obj (~>) x -> x :*-: (~>)
+homX_ :: Category k => Obj k x -> x :*-: k
 homX_ x = Hom :.: Tuple1 (Op x)
 
-type (~>) :-*: x = Hom (~>) :.: Tuple2 (Op (~>)) (~>) x
+type k :-*: x = Hom k :.: Tuple2 (Op k) k x
 -- | The contravariant functor Hom(--,X)
-hom_X :: Category (~>) => Obj (~>) x -> (~>) :-*: x
+hom_X :: Category k => Obj k x -> k :-*: 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, UndecidableInstances  #-}
+{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, FlexibleInstances, FlexibleContexts, RankNTypes, ScopedTypeVariables, UndecidableInstances, NoImplicitPrelude  #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Kleisli
@@ -13,8 +13,6 @@
 -----------------------------------------------------------------------------
 module Data.Category.Kleisli where
   
-import Prelude hiding ((.), id, Functor(..), Monad(..))
-
 import Data.Category
 import Data.Category.Functor
 import Data.Category.NaturalTransformation
@@ -23,10 +21,10 @@
 
 
 data Kleisli m a b where
-  Kleisli :: (Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Monad m -> Obj (~>) b -> a ~> (m :% b) -> Kleisli m a b
+  Kleisli :: (Functor m, Dom m ~ k, Cod m ~ k) => Monad m -> Obj k b -> k a (m :% b) -> Kleisli m a b
 
-kleisliId :: (Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Monad m -> Obj (~>) a -> Kleisli m a a
-kleisliId m a = Kleisli m a $ unit m ! a
+kleisliId :: (Functor m, Dom m ~ k, Cod m ~ k) => Monad m -> Obj k a -> Kleisli m a a
+kleisliId m a = Kleisli m a (unit m ! a)
 
 -- | The category of Kleisli arrows.
 instance Category (Kleisli m) where
@@ -34,7 +32,7 @@
   src (Kleisli m _ f) = kleisliId m (src f)
   tgt (Kleisli m b _) = kleisliId m b
   
-  (Kleisli m c f) . (Kleisli _ _ g) = Kleisli m c $ (multiply m ! c) . (monadFunctor m % f) . g
+  (Kleisli m c f) . (Kleisli _ _ g) = Kleisli m c ((multiply m ! c) . (monadFunctor m % f) . g)
 
 
 
@@ -42,18 +40,18 @@
 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
+instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (KleisliAdjF m) where
+  KleisliAdjF m % f = Kleisli m (tgt f) ((unit m ! tgt f) . f)
    
 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
+instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (KleisliAdjG m) where
   KleisliAdjG m % Kleisli _ b f = (multiply m ! b) . (monadFunctor m % f)
 
-kleisliAdj :: (Functor m, Dom m ~ (~>), Cod m ~ (~>)) 
-  => Monad m -> A.Adjunction (Kleisli m) (~>) (KleisliAdjF m) (KleisliAdjG m)
+kleisliAdj :: (Functor m, Dom m ~ k, Cod m ~ k) 
+  => Monad m -> A.Adjunction (Kleisli m) k (KleisliAdjF m) (KleisliAdjG m)
 kleisliAdj m = A.mkAdjunction (KleisliAdjF m) (KleisliAdjG m)
   (\x -> unit m ! x)
-  (\(Kleisli _ x _) -> Kleisli m x $ monadFunctor m % x)
+  (\(Kleisli _ x _) -> Kleisli m x (monadFunctor m % x))
diff --git a/Data/Category/Limit.hs b/Data/Category/Limit.hs
--- a/Data/Category/Limit.hs
+++ b/Data/Category/Limit.hs
@@ -8,7 +8,9 @@
   TypeOperators, 
   TypeFamilies,
   TypeSynonymInstances,
-  UndecidableInstances  #-}
+  UndecidableInstances, 
+  LambdaCase,
+  NoImplicitPrelude  #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Limit
@@ -67,9 +69,6 @@
   
 ) where
 
-import Prelude hiding ((.), Functor, product)
-import qualified Control.Arrow as A ((&&&), (***), (|||), (+++))
-
 import Data.Category
 import Data.Category.Functor
 import Data.Category.NaturalTransformation
@@ -77,7 +76,8 @@
 
 import Data.Category.Product
 import Data.Category.Coproduct
-import Data.Category.Discrete
+import Data.Category.Unit
+import Data.Category.Void
 
 infixl 3 ***
 infixl 3 &&&
@@ -86,15 +86,15 @@
 
 
 data Diag :: (* -> * -> *) -> (* -> * -> *) -> * where
-  Diag :: Diag j (~>)
+  Diag :: Diag j k
   
-type instance Dom (Diag j (~>)) = (~>)
-type instance Cod (Diag j (~>)) = Nat j (~>)
-type instance Diag j (~>) :% a = Const j (~>) a
+type instance Dom (Diag j k) = k
+type instance Cod (Diag j k) = Nat j k
+type instance Diag j k :% a = Const j k a
 
--- | The diagonal functor from (index-) category J to (~>).
-instance (Category j, Category (~>)) => Functor (Diag j (~>)) where 
-  Diag % f = Nat (Const $ src f) (Const $ tgt f) $ const f
+-- | The diagonal functor from (index-) category J to k.
+instance (Category j, Category k) => Functor (Diag j k) where 
+  Diag % f = Nat (Const (src f)) (Const (tgt f)) (\_ -> f)
 
 -- | The diagonal functor with the same domain and codomain as @f@.
 type DiagF f = Diag (Dom f) (Cod f)
@@ -118,77 +118,77 @@
 
 
 
--- | Limits in a category @(~>)@ by means of a diagram of type @j@, which is a functor from @j@ to @(~>)@.
-type family LimitFam j (~>) f :: *
+-- | Limits in a category @k@ by means of a diagram of type @j@, which is a functor from @j@ to @k@.
+type family LimitFam (j :: * -> * -> *) (k :: * -> * -> *) (f :: *) :: *
 
 type Limit f = LimitFam (Dom f) (Cod f) f
 
--- | An instance of @HasLimits j (~>)@ says that @(~>)@ has all limits of type @j@.
-class (Category j, Category (~>)) => HasLimits j (~>) where
+-- | An instance of @HasLimits j k@ says that @k@ has all limits of type @j@.
+class (Category j, Category k) => HasLimits j k where
   -- | 'limit' returns the limiting cone for a functor @f@.
-  limit           :: Obj (Nat j (~>)) f -> Cone f (Limit f)
+  limit           :: Obj (Nat j k) f -> Cone f (Limit f)
   -- | 'limitFactorizer' shows that the limiting cone is universal – i.e. any other cone of @f@ factors through it –
   --   by returning the morphism between the vertices of the cones.
-  limitFactorizer :: Obj (Nat j (~>)) f -> (forall n. Cone f n -> n ~> Limit f)
+  limitFactorizer :: Obj (Nat j k) f -> (forall n. Cone f n -> k n (Limit f))
 
-data LimitFunctor (j :: * -> * -> *) ((~>)  :: * -> * -> *) = LimitFunctor
-type instance Dom (LimitFunctor j (~>)) = Nat j (~>)
-type instance Cod (LimitFunctor j (~>)) = (~>)
-type instance LimitFunctor j (~>) :% f = LimitFam j (~>) f
--- | If every diagram of type @j@ has a limit in @(~>)@ there exists a limit functor.
+data LimitFunctor (j :: * -> * -> *) (k  :: * -> * -> *) = LimitFunctor
+type instance Dom (LimitFunctor j k) = Nat j k
+type instance Cod (LimitFunctor j k) = k
+type instance LimitFunctor j k :% f = LimitFam j k f
+-- | If every diagram of type @j@ has a limit in @k@ there exists a limit functor.
 --   It can be seen as a generalisation of @(***)@.
-instance HasLimits j (~>) => Functor (LimitFunctor j (~>)) where
+instance HasLimits j k => Functor (LimitFunctor j k) where
   LimitFunctor % n @ Nat{}  = limitFactorizer (tgt n) (n . limit (src n))
 
 -- | The limit functor is right adjoint to the diagonal functor.
-limitAdj :: HasLimits j (~>) => Adjunction (Nat j (~>)) (~>) (Diag j (~>)) (LimitFunctor j (~>))
+limitAdj :: forall j k. HasLimits j k => Adjunction (Nat j k) k (Diag j k) (LimitFunctor j k)
 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.
+  where diag = Diag :: Diag j k -- 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 :: *
+-- | Colimits in a category @k@ by means of a diagram of type @j@, which is a functor from @j@ to @k@.
+type family ColimitFam (j :: * -> * -> *) (k :: * -> * -> *) (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
+-- | An instance of @HasColimits j k@ says that @k@ has all colimits of type @j@.
+class (Category j, Category k) => HasColimits j k where
   -- | 'colimit' returns the limiting co-cone for a functor @f@.
-  colimit           :: Obj (Nat j (~>)) f -> Cocone f (Colimit f)
+  colimit           :: Obj (Nat j k) f -> Cocone f (Colimit f)
   -- | 'colimitFactorizer' shows that the limiting co-cone is universal – i.e. any other co-cone of @f@ factors through it –
   --   by returning the morphism between the vertices of the cones.
-  colimitFactorizer :: Obj (Nat j (~>)) f -> (forall n. Cocone f n -> Colimit f ~> n)
+  colimitFactorizer :: Obj (Nat j k) f -> (forall n. Cocone f n -> k (Colimit f) n)
 
-data ColimitFunctor (j :: * -> * -> *) ((~>)  :: * -> * -> *) = ColimitFunctor
-type instance Dom (ColimitFunctor j (~>)) = Nat j (~>)
-type instance Cod (ColimitFunctor j (~>)) = (~>)
-type instance ColimitFunctor j (~>) :% f = ColimitFam j (~>) f
--- | If every diagram of type @j@ has a colimit in @(~>)@ there exists a colimit functor.
+data ColimitFunctor (j :: * -> * -> *) (k  :: * -> * -> *) = ColimitFunctor
+type instance Dom (ColimitFunctor j k) = Nat j k
+type instance Cod (ColimitFunctor j k) = k
+type instance ColimitFunctor j k :% f = ColimitFam j k f
+-- | If every diagram of type @j@ has a colimit in @k@ there exists a colimit functor.
 --   It can be seen as a generalisation of @(+++)@.
-instance HasColimits j (~>) => Functor (ColimitFunctor j (~>)) where
+instance HasColimits j k => Functor (ColimitFunctor j k) 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 :: forall j k. HasColimits j k => Adjunction k (Nat j k) (ColimitFunctor j k) (Diag j k)
 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.
+  where diag = Diag :: Diag j k -- Forces the type of all Diags to be the same.
   
 
 
-class Category (~>) => HasTerminalObject (~>) where
+class Category k => HasTerminalObject k where
   
-  type TerminalObject (~>) :: *
+  type TerminalObject k :: *
   
-  terminalObject :: Obj (~>) (TerminalObject (~>))
+  terminalObject :: Obj k (TerminalObject k)
   
-  terminate :: Obj (~>) a -> a ~> TerminalObject (~>)
+  terminate :: Obj k a -> k a (TerminalObject k)
 
 
-type instance LimitFam Void (~>) f = TerminalObject (~>)
+type instance LimitFam Void k f = TerminalObject k
 
--- | A terminal object is the limit of the functor from /0/ to (~>).
-instance (HasTerminalObject (~>)) => HasLimits Void (~>) where
+-- | A terminal object is the limit of the functor from /0/ to k.
+instance (HasTerminalObject k) => HasLimits Void k where
   
   limit (Nat f _ _) = voidNat (Const terminalObject) f
   limitFactorizer Nat{} = terminate . coneVertex
@@ -199,7 +199,7 @@
   
   type TerminalObject (->) = ()
   
-  terminalObject = id
+  terminalObject = \x -> x
   
   terminate _ _ = ()
 
@@ -210,17 +210,26 @@
   
   terminalObject = CatA Id
   
-  terminate (CatA _) = CatA $ Const Z
+  terminate (CatA _) = CatA (Const Unit)
 
 -- | The constant functor to the terminal object is itself the terminal object in its functor category.
 instance (Category c, HasTerminalObject d) => HasTerminalObject (Nat c d) where
   
   type TerminalObject (Nat c d) = Const c d (TerminalObject d)
   
-  terminalObject = natId $ Const terminalObject
+  terminalObject = natId (Const terminalObject)
   
-  terminate (Nat f _ _) = Nat f (Const terminalObject) $ terminate . (f %)
+  terminate (Nat f _ _) = Nat f (Const terminalObject) (terminate . (f %))
 
+-- | The category of one object has that object as terminal object.
+instance HasTerminalObject Unit where
+  
+  type TerminalObject Unit = ()
+  
+  terminalObject = Unit
+  
+  terminate Unit = Unit
+  
 -- | The terminal object of the product of 2 categories is the product of their terminal objects.
 instance (HasTerminalObject c1, HasTerminalObject c2) => HasTerminalObject (c1 :**: c2) where
   
@@ -230,21 +239,31 @@
   
   terminate (a1 :**: a2) = terminate a1 :**: terminate a2
   
+-- | The terminal object of the direct coproduct of categories is the terminal object of the terminal category.
+instance (Category c1, HasTerminalObject c2) => HasTerminalObject (c1 :>>: c2) where
   
+  type TerminalObject (c1 :>>: c2) = I2 (TerminalObject c2)
+  
+  terminalObject = I2A terminalObject
+  
+  terminate (I1A a) = I12 a terminalObject
+  terminate (I2A a) = I2A (terminate a)
 
-class Category (~>) => HasInitialObject (~>) where
+
+
+class Category k => HasInitialObject k where
   
-  type InitialObject (~>) :: *
+  type InitialObject k :: *
   
-  initialObject :: Obj (~>) (InitialObject (~>))
+  initialObject :: Obj k (InitialObject k)
 
-  initialize :: Obj (~>) a -> InitialObject (~>) ~> a
+  initialize :: Obj k a -> k (InitialObject k) a
 
 
-type instance ColimitFam Void (~>) f = InitialObject (~>)
+type instance ColimitFam Void k f = InitialObject k
 
--- | An initial object is the colimit of the functor from /0/ to (~>).
-instance HasInitialObject (~>) => HasColimits Void (~>) where
+-- | An initial object is the colimit of the functor from /0/ to k.
+instance HasInitialObject k => HasColimits Void k where
   
   colimit (Nat f _ _) = voidNat f (Const initialObject)
   colimitFactorizer Nat{} = initialize . coconeVertex
@@ -257,10 +276,9 @@
   
   type InitialObject (->) = Zero
   
-  initialObject = id
+  initialObject = \x -> x
   
-  -- With thanks to Conor McBride
-  initialize _ x = x `seq` error "we never get this far"
+  initialize = initialize
 
 -- | The empty category is the initial object in @Cat@.
 instance HasInitialObject Cat where
@@ -269,16 +287,16 @@
   
   initialObject = CatA Id
   
-  initialize (CatA _) = CatA Nil
+  initialize (CatA _) = CatA Magic
 
 -- | The constant functor to the initial object is itself the initial object in its functor category.
 instance (Category c, HasInitialObject d) => HasInitialObject (Nat c d) where
   
   type InitialObject (Nat c d) = Const c d (InitialObject d)
   
-  initialObject = natId $ Const initialObject
+  initialObject = natId (Const initialObject)
   
-  initialize (Nat f _ _) = Nat (Const initialObject) f $ initialize . (f %)
+  initialize (Nat f _ _) = Nat (Const initialObject) f (initialize . (f %))
 
 -- | The initial object of the product of 2 categories is the product of their initial objects.
 instance (HasInitialObject c1, HasInitialObject c2) => HasInitialObject (c1 :**: c2) where
@@ -289,38 +307,63 @@
   
   initialize (a1 :**: a2) = initialize a1 :**: initialize a2
 
+-- | The category of one object has that object as initial object. 
+instance HasInitialObject Unit where
+  
+  type InitialObject Unit = ()
+  
+  initialObject = Unit
+  
+  initialize Unit = Unit
 
+-- | The initial object of the direct coproduct of categories is the initial object of the initial category.
+instance (HasInitialObject c1, Category c2) => HasInitialObject (c1 :>>: c2) where
+  
+  type InitialObject (c1 :>>: c2) = I1 (InitialObject c1)
+  
+  initialObject = I1A initialObject
+  
+  initialize (I1A a) = I1A (initialize a)
+  initialize (I2A a) = I12 initialObject a
 
-type family BinaryProduct ((~>) :: * -> * -> *) x y :: *
 
-class Category (~>) => HasBinaryProducts (~>) where
+type family BinaryProduct (k :: * -> * -> *) x y :: *
+
+class Category k => HasBinaryProducts k where
   
-  proj1 :: Obj (~>) x -> Obj (~>) y -> BinaryProduct (~>) x y ~> x
-  proj2 :: Obj (~>) x -> Obj (~>) y -> BinaryProduct (~>) x y ~> y
+  proj1 :: Obj k x -> Obj k y -> k (BinaryProduct k x y) x
+  proj2 :: Obj k x -> Obj k y -> k (BinaryProduct k x y) y
 
-  (&&&) :: (a ~> x) -> (a ~> y) -> (a ~> BinaryProduct (~>) x y)
+  (&&&) :: (k a x) -> (k a y) -> (k a (BinaryProduct k x y))
 
-  (***) :: (a1 ~> b1) -> (a2 ~> b2) -> (BinaryProduct (~>) a1 a2 ~> BinaryProduct (~>) b1 b2)
+  (***) :: (k a1 b1) -> (k a2 b2) -> (k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2))
   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) (~>) (f :.: Succ n))
 
--- | The product of @n@ objects is the limit of the functor from @Discrete n@ to @(~>)@.
-instance (HasLimits (Discrete n) (~>), HasBinaryProducts (~>)) => HasLimits (Discrete (S n)) (~>) where
+type instance LimitFam (i :++: j) k f = BinaryProduct k 
+  (LimitFam i k (f :.: Inj1 i j))
+  (LimitFam j k (f :.: Inj2 i j))
+
+-- | If `k` has binary products, we can take the limit of 2 joined diagrams.
+instance (HasLimits i k, HasLimits j k, HasBinaryProducts k) => HasLimits (i :++: j) k where
   
   limit = limit'
     where
-      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)
+      limit' :: forall f. Obj (Nat (i :++: j) k) f -> Cone f (Limit f)
+      limit' l@Nat{} = Nat (Const (x *** y)) (srcF l) (\z -> unCom (h z))
         where
-          x = l ! Z
-          y = coneVertex limNext
-          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
+          x = coneVertex lim1
+          y = coneVertex lim2
+          lim1 = limit (l `o` natId Inj1)
+          lim2 = limit (l `o` natId Inj2)
+          h :: Obj (i :++: j) z -> Com (ConstF f (LimitFam (i :++: j) k f)) f z
+          h (I1 n) = Com (lim1 ! n . proj1 x y)
+          h (I2 n) = Com (lim2 ! n . proj2 x y)
 
-  limitFactorizer l@Nat{} c = c ! Z &&& limitFactorizer (l `o` natId Succ) ((c `o` natId Succ) . constPostcompInv (srcF c) Succ)
+  limitFactorizer l@Nat{} c = 
+    limitFactorizer (l `o` natId Inj1) ((c `o` natId Inj1) . constPostcompInv (srcF c) Inj1)
+    &&& 
+    limitFactorizer (l `o` natId Inj2) ((c `o` natId Inj2) . constPostcompInv (srcF c) Inj2)
 
 
 type instance BinaryProduct (->) x y = (x, y)
@@ -328,15 +371,15 @@
 -- | The tuple is the binary product in @Hask@.
 instance HasBinaryProducts (->) where
   
-  proj1 _ _ = fst
-  proj2 _ _ = snd
+  proj1 _ _ = \(x, _) -> x
+  proj2 _ _ = \(_, y) -> y
   
-  (&&&) = (A.&&&)
-  (***) = (A.***)
+  f &&& g = \x -> (f x, g x)
+  f *** g = \(x, y) -> (f x, g y)
 
 type instance BinaryProduct Cat (CatW c1) (CatW c2) = CatW (c1 :**: c2)
 
--- | The product of categories '(:**:)' is the binary product in 'Cat'.
+-- | The product of categories ':**:' is the binary product in 'Cat'.
 instance HasBinaryProducts Cat where
   
   proj1 (CatA _) (CatA _) = CatA Proj1
@@ -345,6 +388,17 @@
   CatA f1 &&& CatA f2 = CatA ((f1 :***: f2) :.: DiagProd)
   CatA f1 *** CatA f2 = CatA (f1 :***: f2)
 
+type instance BinaryProduct Unit () () = ()
+
+-- | In the category of one object that object is its own product.
+instance HasBinaryProducts Unit where
+
+  proj1 Unit Unit = Unit
+  proj2 Unit Unit = Unit
+  
+  Unit &&& Unit = Unit
+  Unit *** Unit = Unit
+
 type instance BinaryProduct (c1 :**: c2) (x1, x2) (y1, y2) = (BinaryProduct c1 x1 y1, BinaryProduct c2 x2 y2)
 
 -- | The binary product of the product of 2 categories is the product of their binary products.
@@ -356,17 +410,39 @@
   (f1 :**: f2) &&& (g1 :**: g2) = (f1 &&& g1) :**: (f2 &&& g2)
   (f1 :**: f2) *** (g1 :**: g2) = (f1 *** g1) :**: (f2 *** g2)
 
+type instance BinaryProduct (c1 :>>: c2) (I1 a) (I1 b) = I1 (BinaryProduct c1 a b)
+type instance BinaryProduct (c1 :>>: c2) (I1 a) (I2 b) = I1 a
+type instance BinaryProduct (c1 :>>: c2) (I2 a) (I1 b) = I1 b
+type instance BinaryProduct (c1 :>>: c2) (I2 a) (I2 b) = I2 (BinaryProduct c2 a b)
 
-data ProductFunctor ((~>) :: * -> * -> *) = ProductFunctor
-type instance Dom (ProductFunctor (~>)) = (~>) :**: (~>)
-type instance Cod (ProductFunctor (~>)) = (~>)
-type instance ProductFunctor (~>) :% (a, b) = BinaryProduct (~>) a b
+instance (HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts (c1 :>>: c2) where
+
+  proj1 (I1A a) (I1A b) = I1A (proj1 a b)
+  proj1 (I1A a) (I2A _) = I1A a
+  proj1 (I2A a) (I1A b) = I12 b a
+  proj1 (I2A a) (I2A b) = I2A (proj1 a b)
+  
+  proj2 (I1A a) (I1A b) = I1A (proj2 a b)
+  proj2 (I1A a) (I2A b) = I12 a b
+  proj2 (I2A _) (I1A b) = I1A b
+  proj2 (I2A a) (I2A b) = I2A (proj2 a b)
+
+  I1A a &&& I1A b = I1A (a &&& b)
+  I1A a &&& I12 _ _ = I1A a
+  I12 _ _ &&& I1A b = I1A b
+  I2A a &&& I2A b = I2A (a &&& b)
+
+
+data ProductFunctor (k :: * -> * -> *) = ProductFunctor
+type instance Dom (ProductFunctor k) = k :**: k
+type instance Cod (ProductFunctor k) = k
+type instance ProductFunctor k :% (a, b) = BinaryProduct k a b
 -- | Binary product as a bifunctor.
-instance HasBinaryProducts (~>) => Functor (ProductFunctor (~>)) where
+instance HasBinaryProducts k => Functor (ProductFunctor k) where
   ProductFunctor % (a1 :**: a2) = a1 *** a2
 
 data p :*: q where 
-  (:*:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ (~>), Cod q ~ (~>), HasBinaryProducts (~>)) => p -> q -> p :*: q
+  (:*:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k, HasBinaryProducts k) => p -> q -> p :*: q
 type instance Dom (p :*: q) = Dom p
 type instance Cod (p :*: q) = Cod p
 type instance (p :*: q) :% a = BinaryProduct (Cod p) (p :% a) (q :% a)
@@ -376,64 +452,59 @@
 
 type instance BinaryProduct (Nat c d) x y = x :*: y
 
--- | The functor product '(:*:)' is the binary product in functor categories.
+-- | The functor product ':*:' is the binary product in functor categories.
 instance (Category c, HasBinaryProducts d) => HasBinaryProducts (Nat c d) where
   
-  proj1 (Nat f _ _) (Nat g _ _) = Nat (f :*: g) f $ \z -> proj1 (f % z) (g % z)
-  proj2 (Nat f _ _) (Nat g _ _) = Nat (f :*: g) g $ \z -> proj2 (f % z) (g % z)
+  proj1 (Nat f _ _) (Nat g _ _) = Nat (f :*: g) f (\z -> proj1 (f % z) (g % z))
+  proj2 (Nat f _ _) (Nat g _ _) = Nat (f :*: g) g (\z -> proj2 (f % z) (g % z))
   
-  Nat a f af &&& Nat _ g ag = Nat a (f :*: g) $ \z -> af z &&& ag z
-  Nat f1 f2 f *** Nat g1 g2 g = Nat (f1 :*: g1) (f2 :*: g2) $ \z -> f z *** g z
+  Nat a f af &&& Nat _ g ag = Nat a (f :*: g) (\z -> af z &&& ag z)
+  Nat f1 f2 f *** Nat g1 g2 g = Nat (f1 :*: g1) (f2 :*: g2) (\z -> f z *** g z)
   
   
 
-type family BinaryCoproduct ((~>) :: * -> * -> *) x y :: *
+type family BinaryCoproduct (k :: * -> * -> *) x y :: *
 
-class Category (~>) => HasBinaryCoproducts (~>) where
+class Category k => HasBinaryCoproducts k where
 
-  inj1 :: Obj (~>) x -> Obj (~>) y -> x ~> BinaryCoproduct (~>) x y
-  inj2 :: Obj (~>) x -> Obj (~>) y -> y ~> BinaryCoproduct (~>) x y
+  inj1 :: Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
+  inj2 :: Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
 
-  (|||) :: (x ~> a) -> (y ~> a) -> (BinaryCoproduct (~>) x y ~> a)
+  (|||) :: (k x a) -> (k y a) -> (k (BinaryCoproduct k x y) a)
     
-  (+++) :: (a1 ~> b1) -> (a2 ~> b2) -> (BinaryCoproduct (~>) a1 a2 ~> BinaryCoproduct (~>) b1 b2)
+  (+++) :: (k a1 b1) -> (k a2 b2) -> (k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2))
   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) (~>) (f :.: Succ n))
+type instance ColimitFam (i :++: j) k f = BinaryCoproduct k 
+  (ColimitFam i k (f :.: Inj1 i j))
+  (ColimitFam j k (f :.: Inj2 i j))
 
--- | The coproduct of @n@ objects is the colimit of the functor from @Discrete n@ to @(~>)@.
-instance (HasColimits (Discrete n) (~>), HasBinaryCoproducts (~>)) => HasColimits (Discrete (S n)) (~>) where
+-- | If `k` has binary coproducts, we can take the colimit of 2 joined diagrams.
+instance (HasColimits i k, HasColimits j k, HasBinaryCoproducts k) => HasColimits (i :++: j) k where
   
   colimit = colimit'
     where
-      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)
+      colimit' :: forall f. Obj (Nat (i :++: j) k) f -> Cocone f (Colimit f)
+      colimit' l@Nat{} = Nat (srcF l) (Const (x +++ y)) (\z -> unCom (h z))
         where
-          x = l ! Z
-          y = coconeVertex colNext
-          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
+          x = coconeVertex col1
+          y = coconeVertex col2
+          col1 = colimit (l `o` natId Inj1)
+          col2 = colimit (l `o` natId Inj2)
+          h :: Obj (i :++: j) z -> Com f (ConstF f (ColimitFam (i :++: j) k f)) z
+          h (I1 n) = Com (inj1 x y . col1 ! n)
+          h (I2 n) = Com (inj2 x y . col2 ! n)
   
-  colimitFactorizer l@Nat{} c = c ! Z ||| colimitFactorizer (l `o` natId Succ) (constPostcomp (tgtF c) Succ . (c `o` natId Succ))
+  colimitFactorizer l@Nat{} c = 
+    colimitFactorizer (l `o` natId Inj1) (constPostcomp (tgtF c) Inj1 . (c `o` natId Inj1))
+    ||| 
+    colimitFactorizer (l `o` natId Inj2) (constPostcomp (tgtF c) Inj2 . (c `o` natId Inj2))
 
 
-type instance BinaryCoproduct (->) x y = Either x y
-
--- | 'Either' is the coproduct in @Hask@.
-instance HasBinaryCoproducts (->) where
-  
-  inj1 _ _ = Left
-  inj2 _ _ = Right
-  
-  (|||) = (A.|||)
-  (+++) = (A.+++)
-
 type instance BinaryCoproduct Cat (CatW c1) (CatW c2) = CatW (c1 :++: c2)
 
--- | The coproduct of categories '(:++:)' is the binary coproduct in 'Cat'.
+-- | The coproduct of categories ':++:' is the binary coproduct in 'Cat'.
 instance HasBinaryCoproducts Cat where
   
   inj1 (CatA _) (CatA _) = CatA Inj1
@@ -442,6 +513,17 @@
   CatA f1 ||| CatA f2 = CatA (CodiagCoprod :.: (f1 :+++: f2))
   CatA f1 +++ CatA f2 = CatA (f1 :+++: f2)
 
+type instance BinaryCoproduct Unit () () = ()
+
+-- | In the category of one object that object is its own coproduct.
+instance HasBinaryCoproducts Unit where
+  
+  inj1 Unit Unit = Unit
+  inj2 Unit Unit = Unit
+  
+  Unit ||| Unit = Unit
+  Unit +++ Unit = Unit
+  
 type instance BinaryCoproduct (c1 :**: c2) (x1, x2) (y1, y2) = (BinaryCoproduct c1 x1 y1, BinaryCoproduct c2 x2 y2)
 
 -- | The binary coproduct of the product of 2 categories is the product of their binary coproducts.
@@ -453,17 +535,39 @@
   (f1 :**: f2) ||| (g1 :**: g2) = (f1 ||| g1) :**: (f2 ||| g2)
   (f1 :**: f2) +++ (g1 :**: g2) = (f1 +++ g1) :**: (f2 +++ g2)
 
+type instance BinaryCoproduct (c1 :>>: c2) (I1 a) (I1 b) = I1 (BinaryCoproduct c1 a b)
+type instance BinaryCoproduct (c1 :>>: c2) (I1 a) (I2 b) = I2 b
+type instance BinaryCoproduct (c1 :>>: c2) (I2 a) (I1 b) = I2 a
+type instance BinaryCoproduct (c1 :>>: c2) (I2 a) (I2 b) = I2 (BinaryCoproduct c2 a b)
 
-data CoproductFunctor ((~>) :: * -> * -> *) = CoproductFunctor
-type instance Dom (CoproductFunctor (~>)) = (~>) :**: (~>)
-type instance Cod (CoproductFunctor (~>)) = (~>)
-type instance CoproductFunctor (~>) :% (a, b) = BinaryCoproduct (~>) a b
+instance (HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts (c1 :>>: c2) where
+
+  inj1 (I1A a) (I1A b) = I1A (inj1 a b)
+  inj1 (I1A a) (I2A b) = I12 a b
+  inj1 (I2A a) (I1A _) = I2A a
+  inj1 (I2A a) (I2A b) = I2A (inj1 a b)
+
+  inj2 (I1A a) (I1A b) = I1A (inj2 a b)
+  inj2 (I1A _) (I2A b) = I2A b
+  inj2 (I2A a) (I1A b) = I12 b a
+  inj2 (I2A a) (I2A b) = I2A (inj2 a b)
+
+  I1A a ||| I1A b = I1A (a ||| b)
+  I2A a ||| I12 _ _ = I2A a
+  I12 _ _ ||| I2A b = I2A b
+  I2A a ||| I2A b = I2A (a ||| b)
+
+
+data CoproductFunctor (k :: * -> * -> *) = CoproductFunctor
+type instance Dom (CoproductFunctor k) = k :**: k
+type instance Cod (CoproductFunctor k) = k
+type instance CoproductFunctor k :% (a, b) = BinaryCoproduct k a b
 -- | Binary coproduct as a bifunctor.
-instance HasBinaryCoproducts (~>) => Functor (CoproductFunctor (~>)) where
+instance HasBinaryCoproducts k => Functor (CoproductFunctor k) where
   CoproductFunctor % (a1 :**: a2) = a1 +++ a2
 
 data p :+: q where 
-  (:+:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ (~>), Cod q ~ (~>), HasBinaryCoproducts (~>)) => p -> q -> p :+: q
+  (:+:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k, HasBinaryCoproducts k) => p -> q -> p :+: q
 type instance Dom (p :+: q) = Dom p
 type instance Cod (p :+: q) = Cod p
 type instance (p :+: q) :% a = BinaryCoproduct (Cod p) (p :% a) (q :% a)
@@ -473,31 +577,75 @@
 
 type instance BinaryCoproduct (Nat c d) x y = x :+: y
 
--- | The functor coproduct '(:+:)' is the binary coproduct in functor categories.
+-- | The functor coproduct ':+:' is the binary coproduct in functor categories.
 instance (Category c, HasBinaryCoproducts d) => HasBinaryCoproducts (Nat c d) where
   
-  inj1 (Nat f _ _) (Nat g _ _) = Nat f (f :+: g) $ \z -> inj1 (f % z) (g % z)
-  inj2 (Nat f _ _) (Nat g _ _) = Nat g (f :+: g) $ \z -> inj2 (f % z) (g % z)
+  inj1 (Nat f _ _) (Nat g _ _) = Nat f (f :+: g) (\z -> inj1 (f % z) (g % z))
+  inj2 (Nat f _ _) (Nat g _ _) = Nat g (f :+: g) (\z -> inj2 (f % z) (g % z))
   
-  Nat f a fa ||| Nat g _ ga = Nat (f :+: g) a $ \z -> fa z ||| ga z
-  Nat f1 f2 f +++ Nat g1 g2 g = Nat (f1 :+: g1) (f2 :+: g2) $ \z -> f z +++ g z
+  Nat f a fa ||| Nat g _ ga = Nat (f :+: g) a (\z -> fa z ||| ga z)
+  Nat f1 f2 f +++ Nat g1 g2 g = Nat (f1 :+: g1) (f2 :+: g2) (\z -> f z +++ g z)
 
+-- | Terminal objects are the dual of initial objects.
+instance HasInitialObject k => HasTerminalObject (Op k) where
+  type TerminalObject (Op k) = InitialObject k
+  terminalObject = Op initialObject
+  terminate (Op f) = Op (initialize f)
 
--- 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
+-- | Terminal objects are the dual of initial objects.
+instance HasTerminalObject k => HasInitialObject (Op k) where
+  type InitialObject (Op k) = TerminalObject k
+  initialObject = Op terminalObject
+  initialize (Op f) = Op (terminate f)
+
+type instance BinaryProduct (Op k) x y = BinaryCoproduct k x y
+-- | Binary products are the dual of binary coproducts.
+instance HasBinaryCoproducts k => HasBinaryProducts (Op k) where
+  proj1 (Op x) (Op y) = Op (inj1 x y)
+  proj2 (Op x) (Op y) = Op (inj2 x y)
+  Op f &&& Op g = Op (f ||| g)
+  Op f *** Op g = Op (f +++ g)
+
+type instance BinaryCoproduct (Op k) x y = BinaryProduct k x y
+-- | Binary products are the dual of binary coproducts.
+instance HasBinaryProducts k => HasBinaryCoproducts (Op k) where
+  inj1 (Op x) (Op y) = Op (proj1 x y)
+  inj2 (Op x) (Op y) = Op (proj2 x y)
+  Op f ||| Op g = Op (f &&& g)
+  Op f +++ Op g = Op (f *** g)
+
+
+
+
+type instance LimitFam Unit k f = f :% ()
+
+-- | The limit of a single object is that object.
+instance Category k => HasLimits Unit k where
+  
+  limit (Nat f _ _) = Nat (Const (f % Unit)) f (\Unit -> f % Unit)
+  limitFactorizer Nat{} n = n ! Unit
+
+type instance LimitFam (i :>>: j) k f = f :% InitialObject (i :>>: j)
+
+-- | The limit of any diagram with an initial object, has the limit at the initial object.
+instance (HasInitialObject (i :>>: j), Category k) => HasLimits (i :>>: j) k where
+  
+  limit (Nat f _ _) = Nat (Const (f % initialObject)) f (\z -> f % initialize z)
+  limitFactorizer Nat{} n = n ! initialObject
+
+
+type instance ColimitFam Unit k f = f :% ()
+
+-- | The colimit of a single object is that object.
+instance Category k => HasColimits Unit k where
+  
+  colimit (Nat f _ _) = Nat f (Const (f % Unit)) (\Unit -> f % Unit)
+  colimitFactorizer Nat{} n = n ! Unit
+  
+type instance ColimitFam (i :>>: j) k f = f :% TerminalObject (i :>>: j)
+
+-- | The colimit of any diagram with a terminal object, has the limit at the terminal object.
+instance (HasTerminalObject (i :>>: j), Category k) => HasColimits (i :>>: j) k where
+
+  colimit (Nat f _ _) = Nat f (Const (f % terminalObject)) (\z -> f % terminate z)
+  colimitFactorizer Nat{} n = n ! terminalObject
diff --git a/Data/Category/Monoid.hs b/Data/Category/Monoid.hs
deleted file mode 100644
--- a/Data/Category/Monoid.hs
+++ /dev/null
@@ -1,82 +0,0 @@
-{-# LANGUAGE TypeFamilies, GADTs, FlexibleInstances #-}
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Category.Monoid
--- License     :  BSD-style (see the file LICENSE)
---
--- Maintainer  :  sjoerd@w3future.com
--- Stability   :  experimental
--- Portability :  non-portable
---
--- A monoid as a category with one object.
------------------------------------------------------------------------------
-module Data.Category.Monoid where
-
-import Prelude hiding ((.), Functor)
-import Data.Monoid
-
-import Data.Category
-import Data.Category.Functor
-import Data.Category.NaturalTransformation
-import Data.Category.Adjunction
-import Data.Category.Monoidal as M
-
--- | The arrows are the values of the monoid.
-data MonoidA m a b where
-  MonoidA :: Monoid m => m -> MonoidA m m m
-
--- | A (prelude) monoid as a category with one object.
-instance Monoid m => Category (MonoidA m) where
-  
-  src (MonoidA _) = MonoidA mempty
-  tgt (MonoidA _) = MonoidA mempty
-  
-  MonoidA a . MonoidA b = MonoidA $ a `mappend` b
-
-
-data Mon :: * -> * -> * where
-  MonoidMorphism :: (Monoid m1, Monoid m2) => (m1 -> m2) -> Mon m1 m2
-
--- | The category of all monoids, with monoid morphisms as arrows.
-instance Category Mon where
-  
-  src (MonoidMorphism _) = MonoidMorphism id
-  tgt (MonoidMorphism _) = MonoidMorphism id
-  
-  MonoidMorphism f . MonoidMorphism g = MonoidMorphism $ f . g
-
-
-data ForgetMonoid = ForgetMonoid
-type instance Dom ForgetMonoid = Mon
-type instance Cod ForgetMonoid = (->)
-type instance ForgetMonoid :% a = a
--- | The 'ForgetMonoid' functor forgets the monoid structure.
-instance Functor ForgetMonoid where
-  ForgetMonoid % MonoidMorphism f = f
-  
-data FreeMonoid = FreeMonoid
-type instance Dom FreeMonoid = (->)
-type instance Cod FreeMonoid = Mon
-type instance FreeMonoid :% a = [a]
--- | The 'FreeMonoid' functor is the list functor.
-instance Functor FreeMonoid where
-  FreeMonoid % f = MonoidMorphism $ map f
-
--- | The free monoid functor is left adjoint to the forgetful functor.
-freeMonoidAdj :: Adjunction Mon (->) FreeMonoid ForgetMonoid
-freeMonoidAdj = mkAdjunction FreeMonoid ForgetMonoid (\_ -> (:[])) (\(MonoidMorphism _) -> MonoidMorphism mconcat)
-
-foldMap :: Monoid m => (a -> m) -> [a] -> m
-foldMap = (ForgetMonoid %) . rightAdjunct freeMonoidAdj (MonoidMorphism id)
-
-listMonadReturn :: a -> [a]
-listMonadReturn = M.unit (adjunctionMonad freeMonoidAdj) ! id
-
-listMonadJoin :: [[a]] -> [a]
-listMonadJoin = M.multiply (adjunctionMonad freeMonoidAdj) ! id
-
-listComonadExtract :: Monoid m => [m] -> m
-listComonadExtract = ForgetMonoid % (M.counit (adjunctionComonad freeMonoidAdj) ! MonoidMorphism id)
-
-listComonadDuplicate :: Monoid m => [m] -> [[m]]
-listComonadDuplicate = ForgetMonoid % (M.comultiply (adjunctionComonad freeMonoidAdj) ! MonoidMorphism id)
diff --git a/Data/Category/Monoidal.hs b/Data/Category/Monoidal.hs
--- a/Data/Category/Monoidal.hs
+++ b/Data/Category/Monoidal.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, Rank2Types, ViewPatterns #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, Rank2Types, ViewPatterns, NoImplicitPrelude #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Monoidal
@@ -10,10 +10,6 @@
 -----------------------------------------------------------------------------
 module Data.Category.Monoidal where
 
-import Prelude (($), uncurry)
-import qualified Control.Monad as M
-import qualified Data.Monoid as M
-
 import Data.Category
 import Data.Category.Functor
 import Data.Category.NaturalTransformation
@@ -24,25 +20,25 @@
 
 -- | A monoidal category is a category with some kind of tensor product.
 --   A tensor product is a bifunctor, with a unit object.
-class Functor f => TensorProduct f where
+class (Functor f, Dom f ~ (Cod f :**: Cod f)) => TensorProduct f where
   
   type Unit f :: *
   unitObject :: f -> Obj (Cod f) (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))
+  leftUnitor     :: Cod f ~ k => f -> Obj k a -> k (f :% (Unit f, a)) a
+  leftUnitorInv  :: Cod f ~ k => f -> Obj k a -> k a (f :% (Unit f, a))
+  rightUnitor    :: Cod f ~ k => f -> Obj k a -> k (f :% (a, Unit f)) a
+  rightUnitorInv :: Cod f ~ k => f -> Obj k a -> k a (f :% (a, Unit f))
   
-  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))
+  associator     :: Cod f ~ k => f -> Obj k a -> Obj k b -> Obj k c -> k (f :% (f :% (a, b), c)) (f :% (a, f :% (b, c)))
+  associatorInv  :: Cod f ~ k => f -> Obj k a -> Obj k b -> Obj k c -> k (f :% (a, f :% (b, c))) (f :% (f :% (a, b), c))
 
 
 -- | If a category has all products, then the product functor makes it a monoidal category,
 --   with the terminal object as unit.
-instance (HasTerminalObject (~>), HasBinaryProducts (~>)) => TensorProduct (ProductFunctor (~>)) where
+instance (HasTerminalObject k, HasBinaryProducts k) => TensorProduct (ProductFunctor k) where
   
-  type Unit (ProductFunctor (~>)) = TerminalObject (~>)
+  type Unit (ProductFunctor k) = TerminalObject k
   unitObject _ = terminalObject
 
   leftUnitor     _ a = proj2 terminalObject a
@@ -55,9 +51,9 @@
 
 -- | If a category has all coproducts, then the coproduct functor makes it a monoidal category,
 --   with the initial object as unit.
-instance (HasInitialObject (~>), HasBinaryCoproducts (~>)) => TensorProduct (CoproductFunctor (~>)) where
+instance (HasInitialObject k, HasBinaryCoproducts k) => TensorProduct (CoproductFunctor k) where
   
-  type Unit (CoproductFunctor (~>)) = InitialObject (~>)
+  type Unit (CoproductFunctor k) = InitialObject k
   unitObject _ = initialObject
 
   leftUnitor     _ a = initialize a ||| a
@@ -69,9 +65,9 @@
   associatorInv _ a b c = (inj1 (a +++ b) c . inj1 a b) ||| (inj2 a b +++ c)
   
 -- | Functor composition makes the category of endofunctors monoidal, with the identity functor as unit.
-instance Category (~>) => TensorProduct (FunctorCompose (~>)) where
+instance Category k => TensorProduct (FunctorCompose k) where
   
-  type Unit (FunctorCompose (~>)) = Id (~>)
+  type Unit (FunctorCompose k) = Id k
   unitObject _ = natId Id
   
   leftUnitor     _ (Nat g _ _) = idPostcomp g
@@ -85,50 +81,42 @@
 
 -- | @MonoidObject f a@ defines a monoid @a@ in a monoidal category with tensor product @f@.
 data MonoidObject f a = MonoidObject
-  { unit     :: (Cod f ~ (~>)) => Unit f        ~> a
-  , multiply :: (Cod f ~ (~>)) => (f :% (a, a)) ~> a
+  { unit     :: (Cod f ~ k) => k (Unit f)        a
+  , multiply :: (Cod f ~ k) => k ((f :% (a, a))) a
   }
   
 -- | @ComonoidObject f a@ defines a comonoid @a@ in a comonoidal category with tensor product @f@.
 data ComonoidObject f a = ComonoidObject
-  { counit     :: (Cod f ~ (~>)) => a ~> Unit f
-  , comultiply :: (Cod f ~ (~>)) => a ~> (f :% (a, a))
+  { counit     :: (Cod f ~ k) => k a (Unit f)
+  , comultiply :: (Cod f ~ k) => k a (f :% (a, a))
   }
 
--- | Monoids as defined in the prelude are monoids in @Hask@ with the product functor as tensor product.
-preludeMonoid :: M.Monoid m => MonoidObject (ProductFunctor (->)) m
-preludeMonoid = MonoidObject M.mempty (uncurry M.mappend)
-
-
 data MonoidAsCategory f m a b where
-  MonoidValue :: (TensorProduct f, Dom f ~ ((~>) :**: (~>)), Cod f ~ (~>))
-              => f -> MonoidObject f m -> Unit f ~> m -> MonoidAsCategory f m m m
+  MonoidValue :: (TensorProduct f, Dom f ~ (k :**: k), Cod f ~ k)
+              => f -> MonoidObject f m -> k (Unit f) m -> MonoidAsCategory f m m m
 
 -- | A monoid as a category with one object.
 instance Category (MonoidAsCategory f m) where
   
-  src (MonoidValue f m _) = MonoidValue f m $ unit m
-  tgt (MonoidValue f m _) = MonoidValue f m $ unit m
+  src (MonoidValue f m _) = MonoidValue f m (unit m)
+  tgt (MonoidValue f m _) = MonoidValue f m (unit m)
   
-  MonoidValue f m a . MonoidValue _ _ b = MonoidValue f m $ multiply m . f % (a :**: b) . leftUnitorInv f (unitObject f)
+  MonoidValue f m a . MonoidValue _ _ b = MonoidValue f m (multiply m . f % (a :**: b) . leftUnitorInv f (unitObject f))
 
 
 -- | A monad is a monoid in the category of endofunctors.
 type Monad f = MonoidObject (FunctorCompose (Dom f)) f
 
-mkMonad :: (Functor f, Dom f ~ (~>), Cod f ~ (~>), Category (~>)) 
+mkMonad :: (Functor f, Dom f ~ k, Cod f ~ k, Category k) 
   => f 
-  -> (forall a. Obj (~>) a -> Component (Id (~>)) f a) 
-  -> (forall a. Obj (~>) a -> Component (f :.: f) f a)
+  -> (forall a. Obj k a -> Component (Id k) f a) 
+  -> (forall a. Obj k a -> Component (f :.: f) f a)
   -> Monad f
 mkMonad f ret join = MonoidObject
   { unit     = Nat Id        f ret
   , multiply = Nat (f :.: f) f join
   }
 
-preludeMonad :: (M.Functor f, M.Monad f) => Monad (EndoHask f)
-preludeMonad = mkMonad EndoHask (\_ -> M.return) (\_ -> M.join)
-
 monadFunctor :: Monad f -> f
 monadFunctor (unit -> Nat _ f _) = f
 
@@ -136,10 +124,10 @@
 -- | A comonad is a comonoid in the category of endofunctors.
 type Comonad f = ComonoidObject (FunctorCompose (Dom f)) f
 
-mkComonad :: (Functor f, Dom f ~ (~>), Cod f ~ (~>), Category (~>)) 
+mkComonad :: (Functor f, Dom f ~ k, Cod f ~ k, Category k) 
   => f 
-  -> (forall a. Obj (~>) a -> Component f (Id (~>)) a) 
-  -> (forall a. Obj (~>) a -> Component f (f :.: f) a)
+  -> (forall a. Obj k a -> Component f (Id k) a) 
+  -> (forall a. Obj k a -> Component f (f :.: f) a)
   -> Comonad f
 mkComonad f extr dupl = ComonoidObject
   { counit     = Nat f Id        extr
diff --git a/Data/Category/NNO.hs b/Data/Category/NNO.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/NNO.hs
@@ -0,0 +1,62 @@
+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, UndecidableInstances, NoImplicitPrelude #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Category.Peano
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  sjoerd@w3future.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+-----------------------------------------------------------------------------
+module Data.Category.NNO where
+
+import Data.Category
+import Data.Category.Functor
+import Data.Category.Limit
+import Data.Category.Unit
+import Data.Category.Coproduct
+import Data.Category.Fix
+
+
+class HasTerminalObject k => HasNaturalNumberObject k where
+  
+  type NaturalNumberObject k :: *
+  
+  zero :: k (TerminalObject k) (NaturalNumberObject k)
+  succ :: k (NaturalNumberObject k) (NaturalNumberObject k)
+  
+  primRec :: k (TerminalObject k) a -> k a a -> k (NaturalNumberObject k) a
+  
+  
+data NatNum = Z | S NatNum
+
+instance HasNaturalNumberObject (->) where
+  
+  type NaturalNumberObject (->) = NatNum
+  
+  zero = \() -> Z
+  succ = S
+  
+  primRec z _  Z    = z ()
+  primRec z s (S n) = s (primRec z s n)
+
+
+type Nat = Fix ((:++:) Unit)
+
+instance HasNaturalNumberObject Cat where
+  
+  type NaturalNumberObject Cat = CatW Nat
+  
+  zero = CatA (Const (Fix (I1 Unit)))
+  succ = CatA (Wrap :.: Inj2)
+  
+  primRec (CatA z) (CatA s) = CatA (PrimRec z s)
+  
+data PrimRec z s = PrimRec z s
+type instance Dom (PrimRec z s) = Nat
+type instance Cod (PrimRec z s) = Cod z
+type instance PrimRec z s :% I1 () = z :% ()
+type instance PrimRec z s :% I2 n  = s :% PrimRec z s :% n
+instance (Functor z, Functor s, Dom z ~ Unit, Cod z ~ Dom s, Dom s ~ Cod s) => Functor (PrimRec z s) where
+  PrimRec z s % Fix (I1 Unit) = z % Unit
+  PrimRec z s % Fix (I2 n) = s % PrimRec z s % n
diff --git a/Data/Category/NaturalTransformation.hs b/Data/Category/NaturalTransformation.hs
--- a/Data/Category/NaturalTransformation.hs
+++ b/Data/Category/NaturalTransformation.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, GADTs #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, GADTs, NoImplicitPrelude #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.NaturalTransformation
@@ -44,8 +44,6 @@
   
 ) where
   
-import Prelude hiding ((.), Functor)
-
 import Data.Category
 import Data.Category.Functor
 import Data.Category.Product
@@ -77,12 +75,12 @@
 
 -- | Horizontal composition of natural transformations.
 o :: (Category c, Category d, Category e) => Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
-njk@(Nat j k _) `o` nfg@(Nat f g _) = Nat (j :.: f) (k :.: g) $ (njk !) . (nfg !)
--- Nat j k njk `o` Nat f g nfg = Nat (j :.: f) (k :.: g) $ \x -> njk (g % x) . j % nfg x -- or k % nfg x . njk (f % x)
+njk@(Nat j k _) `o` nfg@(Nat f g _) = Nat (j :.: f) (k :.: g) ((njk !) . (nfg !))
+-- Nat j k njk `o` Nat f g nfg = Nat (j :.: f) (k :.: g) (\x -> njk (g % x) . j % nfg x) -- or k % nfg x . njk (f % x)
 
 -- | The identity natural transformation of a functor.
 natId :: Functor f => f -> Nat (Dom f) (Cod f) f f
-natId f = Nat f f $ \i -> f % i
+natId f = Nat f f (\i -> f % i)
 
 srcF :: Nat c d f g -> f
 srcF (Nat f _ _) = f
@@ -98,16 +96,16 @@
   src (Nat f _ _)           = natId f
   tgt (Nat _ g _)           = natId g
   
-  Nat _ h ngh . Nat f _ nfg = Nat f h $ \i -> ngh i . nfg i
+  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
+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
+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 %)
@@ -123,31 +121,31 @@
 
 
 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
+constPrecomp (Const x) f = let fx = f % x in Nat (f :.: Const x) (Const fx) (\_ -> 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
+constPrecompInv (Const x) f = let fx = f % x in Nat (Const fx) (f :.: Const x) (\_ -> 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
+constPostcomp (Const x) f = Nat (Const x :.: f) (Const x) (\_ -> 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
+constPostcompInv (Const x) f = Nat (Const x) (Const x :.: f) (\_ -> x)
 
 
 
 -- | The category of endofunctors.
-type Endo (~>) = Nat (~>) (~>)
+type Endo k = Nat k k
 
 
-data FunctorCompose ((~>) :: * -> * -> *) = FunctorCompose
+data FunctorCompose (k :: * -> * -> *) = FunctorCompose
 
-type instance Dom (FunctorCompose (~>)) = Endo (~>) :**: Endo (~>)
-type instance Cod (FunctorCompose (~>)) = Endo (~>)
-type instance FunctorCompose (~>) :% (f, g) = f :.: g
+type instance Dom (FunctorCompose k) = Endo k :**: Endo k
+type instance Cod (FunctorCompose k) = Endo k
+type instance FunctorCompose k :% (f, g) = f :.: g
 
 -- | Composition of endofunctors is a functor.
-instance Category (~>) => Functor (FunctorCompose (~>)) where
+instance Category k => Functor (FunctorCompose k) where
   FunctorCompose % (n1 :**: n2) = n1 `o` n2
 
 
diff --git a/Data/Category/Omega.hs b/Data/Category/Omega.hs
deleted file mode 100644
--- a/Data/Category/Omega.hs
+++ /dev/null
@@ -1,119 +0,0 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleInstances #-}
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Category.Omega
--- License     :  BSD-style (see the file LICENSE)
---
--- Maintainer  :  sjoerd@w3future.com
--- Stability   :  experimental
--- Portability :  non-portable
---
--- Omega, the category 0 -> 1 -> 2 -> 3 -> ... 
--- The objects are the natural numbers, and there's an arrow from a to b iff a <= b.
------------------------------------------------------------------------------
-module Data.Category.Omega where
-
-import Prelude hiding ((.), id, Functor, product)
-
-import Data.Category
-import Data.Category.Limit
-import Data.Category.Monoidal
-
-
-data Z
-data S n
-
--- | The arrows of omega, there's an arrow from a to b iff a <= b.
-data Omega :: * -> * -> * where
-  Z   :: Omega Z Z
-  Z2S :: Omega Z n -> Omega Z (S n)
-  S   :: Omega a b -> Omega (S a) (S b)
-  
--- | The objects of omega are the natural numbers, and there's an arrow from a to b iff a <= b.
-instance Category Omega where
-  
-  src Z       = Z
-  src (Z2S _) = Z
-  src (S   a) = S (src a)
-  
-  tgt Z       = Z
-  tgt (Z2S a) = S (tgt a)
-  tgt (S   a) = S (tgt a)
-  
-  a     . Z       = a
-  (S a) . (Z2S n) = Z2S (a . n)
-  (S a) . (S   b) = S   (a . b)
-  _       . _     = error "Other combinations should not type check"
-
-
--- | 'Z' (zero) is the initial object of omega.
-instance HasInitialObject Omega where
-  
-  type InitialObject Omega = Z
-  
-  initialObject    = Z
-  
-  initialize Z     = Z
-  initialize (S n) = Z2S $ initialize n
-  initialize _     = error "Other combinations should not type check"
-
-
-
-type instance BinaryProduct Omega Z     n = Z
-type instance BinaryProduct Omega n     Z = Z
-type instance BinaryProduct Omega (S a) (S b) = S (BinaryProduct Omega a b)
-
--- | The product in omega is the minimum.
-instance HasBinaryProducts Omega where 
-
-  proj1 Z     Z     = Z
-  proj1 Z     (S _) = Z
-  proj1 (S n) Z     = Z2S $ proj1 n Z
-  proj1 (S a) (S b) = S $ proj1 a b
-  proj1 _     _     = error "Other combinations should not type check"
-
-  proj2 Z     Z     = Z
-  proj2 Z     (S n) = Z2S $ proj2 Z n
-  proj2 (S _) Z     = Z
-  proj2 (S a) (S b) = S $ proj2 a b
-  proj2 _     _     = error "Other combinations should not type check"
-  
-  Z     &&& _     = Z
-  _     &&& Z     = Z
-  Z2S a &&& Z2S b = Z2S (a &&& b)
-  S a   &&& S b   = S (a &&& b)
-  _     &&& _     = error "Other combinations should not type check"
-
-
-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 HasBinaryCoproducts Omega where 
-  
-  inj1 Z     Z     = Z
-  inj1 Z     (S n) = Z2S $ inj1 Z n
-  inj1 (S n) Z     = S $ inj1 n Z
-  inj1 (S a) (S b) = S $ inj1 a b
-  inj1 _     _     = error "Other combinations should not type check"
-  inj2 Z     Z     = Z
-  inj2 Z     (S n) = S $ inj2 Z n
-  inj2 (S n) Z     = Z2S $ inj2 n Z
-  inj2 (S a) (S b) = S $ inj2 a b
-  inj2 _     _     = error "Other combinations should not type check"
-  
-  Z     ||| Z     = Z
-  Z2S _ ||| a     = a
-  a     ||| Z2S _ = a
-  S a   ||| S b   = S (a ||| b)
-  _     ||| _     = error "Other combinations should not type check"
-
-
--- | Zero is a monoid object wrt the maximum.
-zeroMonoid :: MonoidObject (CoproductFunctor Omega) Z
-zeroMonoid = MonoidObject Z Z
-
--- | Zero is also a comonoid object wrt the maximum.
-zeroComonoid :: ComonoidObject (CoproductFunctor Omega) Z
-zeroComonoid = ComonoidObject Z Z
diff --git a/Data/Category/Peano.hs b/Data/Category/Peano.hs
deleted file mode 100644
--- a/Data/Category/Peano.hs
+++ /dev/null
@@ -1,57 +0,0 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleInstances, ViewPatterns #-}
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Category.Peano
--- 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 PeanoO (~>) a where
-  PeanoO :: (TerminalObject (~>) ~> x) -> (x ~> x) -> PeanoO (~>) x
-    
-data Peano :: (* -> * -> *) -> * -> * -> * where
-  PeanoA :: PeanoO (~>) a -> PeanoO (~>) b -> (a ~> b) -> Peano (~>) a b
-
-peanoId :: Category (~>) => PeanoO (~>) a -> Obj (Peano (~>)) a
-peanoId o@(PeanoO z _) = PeanoA o o $ tgt z
-
-peanoO :: Category (~>) => Obj (Peano (~>)) a -> PeanoO (~>) a
-peanoO (PeanoA o _ _) = o
-
--- | The 'Peano' category.
-instance HasTerminalObject (~>) => Category (Peano (~>)) where
-  
-  src (PeanoA s _ _) = peanoId s
-  tgt (PeanoA _ t _) = peanoId t
-  
-  (PeanoA _ t f) . (PeanoA s _ g) = PeanoA s t $ f . g
-  
-  
-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)
-  
--- | The natural numbers are the initial object for the 'Peano' category.
-instance HasInitialObject (Peano (->)) where
-  
-  type InitialObject (Peano (->)) = NatNum
-  
-  initialObject = peanoId $ PeanoO Z S
-  
-  initialize (peanoO -> o@(PeanoO z s)) = PeanoA (peanoO initialObject) o $ primRec z s
diff --git a/Data/Category/Presheaf.hs b/Data/Category/Presheaf.hs
--- a/Data/Category/Presheaf.hs
+++ b/Data/Category/Presheaf.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, TypeSynonymInstances, GADTs #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, TypeSynonymInstances, GADTs, FlexibleInstances, NoImplicitPrelude #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Presheaf
@@ -10,8 +10,6 @@
 -----------------------------------------------------------------------------
 module Data.Category.Presheaf where
 
-import Prelude (($))
-
 import Data.Category
 import Data.Category.Functor
 import Data.Category.NaturalTransformation
@@ -20,23 +18,23 @@
 import Data.Category.Yoneda
 
 
-type Presheaves (~>) = Nat (Op (~>)) (->)
+type Presheaves k = Nat (Op k) (->)
 
-type PShExponential (~>) y z = (Presheaves (~>) :-*: z) :.: Opposite 
-  (   ProductFunctor (Presheaves (~>))
-  :.: Tuple2 (Presheaves (~>)) (Presheaves (~>)) y
-  :.: YonedaEmbedding (~>)
+type PShExponential k y z = (Presheaves k :-*: z) :.: Opposite 
+  (   ProductFunctor (Presheaves k)
+  :.: Tuple2 (Presheaves k) (Presheaves k) y
+  :.: YonedaEmbedding k
   )
-pshExponential :: Category (~>) => Obj (Presheaves (~>)) y -> Obj (Presheaves (~>)) z -> PShExponential (~>) y z
+pshExponential :: Category k => Obj (Presheaves k) y -> Obj (Presheaves k) z -> PShExponential k y z
 pshExponential y z = hom_X z :.: Opposite (ProductFunctor :.: Tuple2 y :.: yonedaEmbedding)
 
-type instance Exponential (Presheaves (~>)) y z = PShExponential (~>) y z
+type instance Exponential (Presheaves k) y z = PShExponential k y z
 
 -- | The category of presheaves on a category @C@ is cartesian closed for any @C@.
-instance Category (~>) => CartesianClosed (Presheaves (~>)) where
+instance Category k => CartesianClosed (Presheaves k) where
   
-  apply yn@(Nat y _ _) zn@(Nat z _ _) = Nat (pshExponential yn zn :*: y) z $ \(Op i) (n, yi) -> (n ! Op i) (i, yi)
-  tuple yn zn@(Nat z _ _) = Nat z (pshExponential yn (zn *** yn)) $ \(Op i) zi -> (Nat (hom_X i) z $ \_ j2i -> (z % Op j2i) zi) *** yn
-  zn ^^^ yn = Nat (pshExponential (tgt yn) (src zn)) (pshExponential (src yn) (tgt zn)) $ \(Op i) n -> zn . n . (natId (hom_X i) *** yn)
+  apply yn@(Nat y _ _) zn@(Nat z _ _) = Nat (pshExponential yn zn :*: y) z (\(Op i) (n, yi) -> (n ! Op i) (i, yi))
+  tuple yn zn@(Nat z _ _) = Nat z (pshExponential yn (zn *** yn)) (\(Op i) zi -> (Nat (hom_X i) z (\_ j2i -> (z % Op j2i) zi) *** yn))
+  zn ^^^ yn = Nat (pshExponential (tgt yn) (src zn)) (pshExponential (src yn) (tgt zn)) (\(Op i) n -> zn . n . (natId (hom_X i) *** yn))
 
     
diff --git a/Data/Category/Product.hs b/Data/Category/Product.hs
--- a/Data/Category/Product.hs
+++ b/Data/Category/Product.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, FlexibleContexts #-}
+{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, FlexibleContexts, NoImplicitPrelude #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Product
@@ -9,8 +9,6 @@
 -- Portability :  non-portable
 -----------------------------------------------------------------------------
 module Data.Category.Product where
-
-import Prelude ()
 
 import Data.Category
 
diff --git a/Data/Category/RepresentableFunctor.hs b/Data/Category/RepresentableFunctor.hs
--- a/Data/Category/RepresentableFunctor.hs
+++ b/Data/Category/RepresentableFunctor.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, RankNTypes #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, RankNTypes, NoImplicitPrelude #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.RepresentableFunctor
@@ -10,8 +10,6 @@
 -----------------------------------------------------------------------------
 module Data.Category.RepresentableFunctor where
 
-import Prelude (($), id)
-
 import Data.Category
 import Data.Category.Functor
 
@@ -19,22 +17,22 @@
 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
+  , represent          :: (Dom f ~ k, Cod f ~ (->)) => Obj k z -> f :% z -> k repObj z
+  , universalElement   :: (Dom f ~ k, 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
+unrepresent :: (Functor f, Dom f ~ k, Cod f ~ (->)) => Representable f repObj -> k repObj z -> f :% z
+unrepresent rep h = (representedFunctor rep % h) (universalElement rep)
 
-covariantHomRepr :: Category (~>) => Obj (~>) x -> Representable (x :*-: (~>)) x
+covariantHomRepr :: Category k => Obj k x -> Representable (x :*-: k) x
 covariantHomRepr x = Representable
   { representedFunctor = homX_ x
   , representingObject = x
-  , represent          = \_ -> id
+  , represent          = \_ h -> h
   , universalElement   = x
   }
 
-contravariantHomRepr :: Category (~>) => Obj (~>) x -> Representable ((~>) :-*: x) x
+contravariantHomRepr :: Category k => Obj k x -> Representable (k :-*: x) x
 contravariantHomRepr x = Representable
   { representedFunctor = hom_X x
   , representingObject = Op x
diff --git a/Data/Category/Simplex.hs b/Data/Category/Simplex.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/Simplex.hs
@@ -0,0 +1,200 @@
+{-# LANGUAGE TypeFamilies, GADTs, RankNTypes, TypeOperators, UndecidableInstances, NoImplicitPrelude #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Category.Simplex
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  sjoerd@w3future.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- The (augmented) simplex category.
+-----------------------------------------------------------------------------
+module Data.Category.Simplex (
+  
+  -- * Simplex Category
+    Simplex(..)
+  , Z, S
+  , suc
+  
+  -- * Functor
+  , Forget(..)
+  , Fin(..)
+  , Add(..)
+  
+  -- * The universal monoid
+  , universalMonoid
+  , Replicate(..)
+        
+) where
+  
+import Data.Category
+import Data.Category.Product
+import Data.Category.Functor
+import Data.Category.Monoidal
+import Data.Category.Limit
+
+
+data Z
+data S n
+
+
+-- A Simplex x y structure plots a non-decreasing line, ending with Z
+--
+--   ^  +-----Z
+--   |  |   XXY
+--   y  |   Y |
+--      |XXXY |
+--      XY----+
+--         x ->
+
+data Simplex :: * -> * -> * where
+  Z ::                    Simplex    Z     Z
+  Y :: Simplex x    y  -> Simplex    x  (S y)
+  X :: Simplex x (S y) -> Simplex (S x) (S y)
+
+suc :: Obj Simplex n -> Obj Simplex (S n)
+suc = X . Y
+-- Note: Objects are represented by their identity arrows, 
+-- which are in the shape of the elements of `iterate suc Z`.
+
+-- | The (augmented) simplex category is the category of finite ordinals and order preserving maps.
+instance Category Simplex where
+  src Z = Z
+  src (Y f) = src f
+  src (X f) = suc (src f)
+  
+  tgt Z = Z
+  tgt (Y f) = suc (tgt f)
+  tgt (X f) = tgt f
+  
+  Z     .    f  = f
+  f     .    Z  = f
+  (Y f) .    g  = Y (f . g)
+  (X f) . (Y g) = f . g
+  (X f) . (X g) = X ((X f) . g)
+
+
+-- | The ordinal @0@ is the initial object of the simplex category.
+instance HasInitialObject Simplex where
+  type InitialObject Simplex = Z
+  
+  initialObject = Z
+  
+  initialize Z = Z
+  initialize (X (Y f)) = Y (initialize f)
+
+-- | The ordinal @1@ is the terminal object of the simplex category.
+instance HasTerminalObject Simplex where
+  type TerminalObject Simplex = S Z
+
+  terminalObject = suc Z
+
+  terminate Z = Y Z
+  terminate (X (Y f)) = X (terminate f)
+
+
+
+type Merge m n = BinaryCoproduct Simplex m n
+type instance BinaryCoproduct Simplex  Z       Z  = Z
+type instance BinaryCoproduct Simplex  Z    (S n) = S (Merge Z n)
+type instance BinaryCoproduct Simplex (S m)    Z  = S (Merge m Z)
+type instance BinaryCoproduct Simplex (S m) (S n) = S (S (Merge m n))
+
+mergeLS :: Obj Simplex m -> Obj Simplex n -> Simplex (Merge (S m) n) (S (Merge m n))
+mergeLS Z Z = X (Y Z)
+mergeLS Z (X (Y n)) = X (Y (X (Y (Z +++ n))))
+mergeLS (X (Y m)) Z = X (Y (X (Y (m +++ Z))))
+mergeLS (X (Y m)) (X (Y n)) = X (Y (X (Y (mergeLS m n))))
+
+mergeRS :: Obj Simplex m -> Obj Simplex n -> Simplex (Merge m (S n)) (S (Merge m n))
+mergeRS Z Z = X (Y Z)
+mergeRS Z (X (Y n)) = X (Y (X (Y (Z +++ n))))
+mergeRS (X (Y m)) Z = X (Y (X (Y (m +++ Z))))
+mergeRS (X (Y m)) (X (Y n)) = X (Y (X (Y (mergeRS m n))))
+
+-- | The coproduct in the simplex category is a merge operation.
+instance HasBinaryCoproducts Simplex where
+  inj1       Z         Z   = Z
+  inj1       Z   (X (Y n)) = Y (inj1 Z n)
+  inj1 (X (Y m))       Z   = X (Y (inj1 m Z))
+  inj1 (X (Y m)) (X (Y n)) = X (Y (Y (inj1 m n)))
+
+  inj2       Z         Z   = Z
+  inj2       Z   (X (Y n)) = X (Y (inj2 Z n))
+  inj2 (X (Y m))       Z   = Y (inj2 m Z)
+  inj2 (X (Y m)) (X (Y n)) = Y (X (Y (inj2 m n)))
+
+  Z   ||| Z   = Z
+  X f ||| X g = X (X (f ||| g))
+  X f ||| Y g = X (f ||| Y g) . mergeLS (src f) (src g)
+  Y f ||| X g = X (Y f ||| g) . mergeRS (src f) (src g)
+  Y f ||| Y g = Y (f ||| g)
+
+
+data Fin :: * -> * where
+  Fz ::          Fin (S n)
+  Fs :: Fin n -> Fin (S n)
+
+data Forget = Forget
+type instance Dom Forget = Simplex
+type instance Cod Forget = (->)
+type instance Forget :% n = Fin n
+-- | Turn @Simplex x y@ arrows into @Fin x -> Fin y@ functions.
+instance Functor Forget where 
+  Forget %  Z    = \x -> x
+  Forget % (Y f) = \x -> Fs ((Forget % f) x)
+  Forget % (X f) = \x -> case x of
+    Fz -> Fz
+    Fs n -> (Forget % f) n
+
+
+data Add = Add
+type instance Dom Add = Simplex :**: Simplex
+type instance Cod Add = Simplex
+type instance Add :% (Z  , n) = n
+type instance Add :% (S m, n) = S (Add :% (m, n))
+-- | Ordinal addition is a bifuntor, it concattenates the maps as it were.
+instance Functor Add where
+  Add % (Z   :**: g) = g
+  Add % (Y f :**: g) = Y (Add % (f :**: g))
+  Add % (X f :**: g) = X (Add % (f :**: g))
+
+-- | Ordinal addition makes the simplex category a monoidal category, with @0@ as unit.
+instance TensorProduct Add where
+  type Unit Add = Z
+  unitObject Add = Z
+  
+  leftUnitor     Add       a   = a
+  leftUnitorInv  Add       a   = a
+  rightUnitor    Add       Z   = Z
+  rightUnitor    Add (X (Y n)) = X (Y (rightUnitor Add n))
+  rightUnitorInv Add       Z   = Z
+  rightUnitorInv Add (X (Y n)) = X (Y (rightUnitorInv Add n))
+  associator     Add Z       Z   n = n
+  associator     Add Z (X (Y m)) n = X (Y (associator Add Z m n))
+  associator     Add (X (Y l)) m n = X (Y (associator Add l m n))
+  associatorInv  Add Z       Z   n = n
+  associatorInv  Add Z (X (Y m)) n = X (Y (associatorInv Add Z m n))
+  associatorInv  Add (X (Y l)) m n = X (Y (associatorInv Add l m n))
+
+
+-- | The maps @0 -> 1@ and @2 -> 1@ form a monoid, which is universal, c.f. `Replicate`.
+universalMonoid :: MonoidObject (CoproductFunctor Simplex) (S Z)
+universalMonoid = MonoidObject { unit = Y Z, multiply = X (X (Y Z)) }
+
+data Replicate f a = Replicate f (MonoidObject f a)
+type instance Dom (Replicate f a) = Simplex
+type instance Cod (Replicate f a) = Cod f
+type instance Replicate f a :% Z = Unit f
+type instance Replicate f a :% S n = f :% (a, Replicate f a :% n)
+-- | Replicate a monoid a number of times.
+instance TensorProduct f => Functor (Replicate f a) where
+  Replicate f _ % Z = unitObject f
+  Replicate f m % Y n = f % (unit m :**: tgt n') . leftUnitorInv f (tgt n') . n' where n' = Replicate f m % n
+  Replicate f m % X (Y n) = f % (tgt (unit m) :**: (Replicate f m % n))
+  Replicate f m % X (X n) = n' . (f % (multiply m :**: b)) . associatorInv f a a b 
+    where
+      n' = Replicate f m % X n
+      a = tgt (unit m)
+      b = src (Replicate f m % n)
diff --git a/Data/Category/Unit.hs b/Data/Category/Unit.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/Unit.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE GADTs, NoImplicitPrelude #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Category.Unit
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  sjoerd@w3future.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+-----------------------------------------------------------------------------
+module Data.Category.Unit where
+
+import Data.Category
+
+
+data Unit a b where
+  Unit :: Unit () ()
+
+-- | `Unit` is the category with one object.
+instance Category Unit where
+
+  src Unit = Unit
+  tgt Unit = Unit
+
+  Unit . Unit = Unit
diff --git a/Data/Category/Void.hs b/Data/Category/Void.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/Void.hs
@@ -0,0 +1,42 @@
+{-# LANGUAGE GADTs, TypeFamilies, NoImplicitPrelude #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Category.Void
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  sjoerd@w3future.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+-----------------------------------------------------------------------------
+module Data.Category.Void where
+
+import Data.Category
+import Data.Category.Functor
+import Data.Category.NaturalTransformation
+
+
+data Void a b
+
+magic :: Void a b -> x
+magic x = magic x
+
+-- | `Void` is the category with no objects.
+instance Category Void where
+
+  src = magic
+  tgt = magic
+
+  (.) = magic
+
+
+voidNat :: (Functor f, Functor g, Category d, Dom f ~ Void, Dom g ~ Void, Cod f ~ d, Cod g ~ d)
+  => f -> g -> Nat Void d f g
+voidNat f g = Nat f g magic
+
+
+data Magic (k :: * -> * -> *) = Magic
+type instance Dom (Magic k) = Void
+type instance Cod (Magic k) = k
+-- | Since there is nothing to map in `Void`, there's a functor from it to any other category.
+instance Category k => Functor (Magic k) where
+  Magic % f = magic f
diff --git a/Data/Category/Yoneda.hs b/Data/Category/Yoneda.hs
--- a/Data/Category/Yoneda.hs
+++ b/Data/Category/Yoneda.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators, TypeFamilies #-}
+{-# LANGUAGE TypeOperators, RankNTypes, TypeFamilies, NoImplicitPrelude #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Yoneda
@@ -10,32 +10,30 @@
 -----------------------------------------------------------------------------
 module Data.Category.Yoneda where
 
-import Prelude (($))
-
 import Data.Category
 import Data.Category.Functor
 import Data.Category.NaturalTransformation
 import Data.Category.CartesianClosed
 
-type YonedaEmbedding (~>) = Postcompose (Hom (~>)) (Op (~>)) :.: ToTuple2 (~>) (Op (~>)) 
+type YonedaEmbedding k = Postcompose (Hom k) (Op k) :.: ToTuple2 k (Op k) 
 
 -- | The Yoneda embedding functor, @C -> Set^(C^op)@.
-yonedaEmbedding :: Category (~>) => YonedaEmbedding (~>)
+yonedaEmbedding :: Category k => YonedaEmbedding k
 yonedaEmbedding = Postcompose Hom :.: ToTuple2
 
 
-data Yoneda ((~>) :: * -> * -> *) f = Yoneda
-type instance Dom (Yoneda (~>) f) = Op (~>)
-type instance Cod (Yoneda (~>) f) = (->)
-type instance Yoneda (~>) f :% a = Nat (Op (~>)) (->) ((~>) :-*: a) f
+data Yoneda (k :: * -> * -> *) f = Yoneda
+type instance Dom (Yoneda k f) = Op k
+type instance Cod (Yoneda k f) = (->)
+type instance Yoneda k f :% a = Nat (Op k) (->) (k :-*: a) f
 -- | 'Yoneda' converts a functor @f@ into a natural transformation from the hom functor to f.
-instance (Category (~>), Functor f, Dom f ~ Op (~>), Cod f ~ (->)) => Functor (Yoneda (~>) f) where
+instance (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => Functor (Yoneda k f) where
   Yoneda % Op ab = \n -> n . yonedaEmbedding % ab
       
   
 -- | 'fromYoneda' and 'toYoneda' are together the isomophism from the Yoneda lemma.
-fromYoneda :: (Category (~>), Functor f, Dom f ~ Op (~>), Cod f ~ (->)) => f -> Yoneda (~>) f :~> f
-fromYoneda f = Nat Yoneda f $ \(Op a) n -> (n ! Op a) a
+fromYoneda :: (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => f -> Yoneda k f :~> f
+fromYoneda f = Nat Yoneda f (\(Op a) n -> (n ! Op a) a)
 
-toYoneda   :: (Category (~>), Functor f, Dom f ~ Op (~>), Cod f ~ (->)) => f -> f :~> Yoneda (~>) f
-toYoneda   f = Nat f Yoneda $ \(Op a) fa -> Nat (hom_X a) f $ \_ h -> (f % Op h) fa
+toYoneda   :: (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => f -> f :~> Yoneda k f
+toYoneda   f = Nat f Yoneda (\(Op a) fa -> Nat (hom_X a) f (\_ h -> (f % Op h) fa))
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.4.1
+version:             0.5.0
 synopsis:            Category theory
 
 description:         Data-category is a collection of categories, and some categorical constructions on them.
@@ -31,25 +31,25 @@
     Data.Category,
     Data.Category.Functor,
     Data.Category.NaturalTransformation,
+    Data.Category.Unit,
+    Data.Category.Void,
+    Data.Category.Product,
+    Data.Category.Coproduct,
     Data.Category.RepresentableFunctor,
     Data.Category.Adjunction,
     Data.Category.Limit,
     Data.Category.Monoidal,
     Data.Category.CartesianClosed,
-    Data.Category.Product,
-    Data.Category.Coproduct,
-    Data.Category.Discrete,
     Data.Category.Yoneda,
     Data.Category.Presheaf,
-    Data.Category.Monoid,
     Data.Category.Boolean,
-    Data.Category.Omega,
+    Data.Category.Fix,
     Data.Category.Kleisli,
     Data.Category.Dialg,
-    Data.Category.Peano,
+    Data.Category.NNO,
+    Data.Category.Simplex,
     Data.Category.Comma
     
-  build-depends:       base >= 3 && < 5
   default-language:    Haskell2010
 
 source-repository head