diff --git a/Data/Category.hs b/Data/Category.hs
--- a/Data/Category.hs
+++ b/Data/Category.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, ScopedTypeVariables #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category
@@ -15,6 +15,7 @@
     CategoryO(..)
   , CategoryA(..)
   , Apply(..)
+  , Obj, obj
   
   -- * Functors
   , F
@@ -30,6 +31,18 @@
   , (:*-:)(..)
   , (:-*:)(..)
   
+  -- * Natural transformations
+  , Nat
+  , (:~>)
+  , Component
+  
+  -- * Universal arrows
+  , InitialUniversal(..)
+  , TerminalUniversal(..)
+  
+  -- * Adjunctions
+  , Adjunction(..)
+  
   ) where
 
 import Prelude hiding ((.), id, ($))
@@ -37,7 +50,8 @@
 
 -- | An instance CategoryO (~>) a declares a as an object of the category (~>).
 class CategoryO (~>) a where
-  id :: a ~> a
+  id  :: a ~> a
+  (!) :: Nat (~>) d f g -> Obj a -> Component f g a
 
 -- | An instance CategoryA (~>) a b c defines composition of the arrows a ~> b and b ~> c.
 class (CategoryO (~>) a, CategoryO (~>) b, CategoryO (~>) c) => CategoryA (~>) a b c where
@@ -47,7 +61,18 @@
   -- Would have liked to use ($) here, but that causes GHC to crash.
   -- http://hackage.haskell.org/trac/ghc/ticket/3297
   ($$) :: a ~> b -> a -> b
-  
+
+-- | The type synonym @Obj a@, when used as the type of a function argument,
+-- is a promise that the value of the argument is not used, and only the type.
+-- This is used to pass objects (which are types) to functions.
+type Obj a = a
+-- | 'obj' is a synonym for 'undefined'. When you need to pass an object to
+-- a function, you can use @(obj :: type)@.
+obj :: Obj a
+obj = undefined
+
+
+
 -- | Functors are represented by a type tag. The type family 'F' turns the tag into the actual functor.
 type family F ftag a :: *
 -- | The domain, or source category, of the functor.
@@ -59,12 +84,12 @@
 -- To make this type check, we need to pass the type tag along.
 class (CategoryO (Dom ftag) a, CategoryO (Dom ftag) b) 
   => FunctorA ftag a b where
-  (%) :: ftag -> Dom ftag a b -> Cod ftag (F ftag a) (F ftag b)
+  (%) :: Obj ftag -> Dom ftag a b -> Cod ftag (F ftag a) (F ftag b)
 
 -- | The mapping of arrows by contravariant functors.
 class (CategoryO (Dom ftag) a, CategoryO (Dom ftag) b) 
   => ContraFunctorA ftag a b where
-  (-%) :: ftag -> Dom ftag a b -> Cod ftag (F ftag b) (F ftag a)
+  (-%) :: Obj ftag -> Dom ftag a b -> Cod ftag (F ftag b) (F ftag a)
 
 
 -- | The identity functor on (~>)
@@ -73,7 +98,7 @@
 type instance Dom (Id (~>)) = (~>)
 type instance Cod (Id (~>)) = (~>)
 instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Id (~>)) a b where
-  Id % f = f
+  _ % f = f
 
 -- | The composition of two functors.
 data (g :.: h) = g :.: h
@@ -81,7 +106,7 @@
 type instance Dom (g :.: h) = Dom h
 type instance Cod (g :.: h) = Cod g
 instance (FunctorA g (F h a) (F h b), FunctorA h a b, Cod h ~ Dom g) => FunctorA (g :.: h) a b where
-   (g :.: h) % f = g % (h % f)
+   _ % f = (obj :: g) % ((obj :: h) % f)
 
 -- | The constant functor.
 data Const (c1 :: * -> * -> *) (c2 :: * -> * -> *) x = Const
@@ -89,7 +114,7 @@
 type instance Dom (Const c1 c2 x) = c1
 type instance Cod (Const c1 c2 x) = c2
 instance (CategoryO c1 a, CategoryO c1 b, CategoryO c2 x) => FunctorA (Const c1 c2 x) a b where
-  Const % f = id
+  _ % _ = id
   
 -- | The covariant functor Hom(X,--)
 data (x :*-: ((~>) :: * -> * -> *)) = HomX_
@@ -97,7 +122,7 @@
 type instance Dom (x :*-: (~>)) = (~>)
 type instance Cod (x :*-: (~>)) = (->)
 instance (CategoryO (~>) a, CategoryO (~>) b, CategoryA (~>) x a b) => FunctorA (x :*-: (~>)) a b where
-  HomX_ % f = (f .)
+  _ % f = (f .)
 
 -- | The contravariant functor Hom(--,X)
 data (((~>) :: * -> * -> *) :-*: x) = Hom_X
@@ -105,4 +130,25 @@
 type instance Dom ((~>) :-*: x) = (~>)
 type instance Cod ((~>) :-*: x) = (->)
 instance (CategoryO (~>) a, CategoryO (~>) b, CategoryA (~>) a b x) => ContraFunctorA ((~>) :-*: x) a b where
-  Hom_X -% f = (. f)
+  _ -% f = (. f)
+  
+  
+data family Nat (c :: * -> * -> *) (d :: * -> * -> *) (f :: *) (g :: *) :: *
+
+-- | @f :~> g@ is a natural transformation from functor f to functor g.
+type f :~> g = (c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => Nat c d f g
+
+-- | Natural transformations are built up of components, 
+-- one for each object @z@ in the domain category of @f@ and @g@.
+-- This type synonym can be used when creating data instances of @Nat@.
+type Component f g z = Cod f (F f z) (F g z)
+  
+type InitMorF x u = (x :*-: Cod u) :.: u
+type TermMorF x u = (Cod u :-*: x) :.: u
+data InitialUniversal  x u a = InitialUniversal  (F (InitMorF x u) a) (InitMorF x u :~> (a :*-: Dom u))
+data TerminalUniversal x u a = TerminalUniversal (F (TermMorF x u) a) (TermMorF x u :~> (Dom u :-*: a))
+
+data Adjunction f g = Adjunction 
+  { unit :: Id (Dom f) :~> (g :.: f)
+  , counit :: (f :.: g) :~> Id (Dom g)
+  }
diff --git a/Data/Category/Alg.hs b/Data/Category/Alg.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/Alg.hs
@@ -0,0 +1,53 @@
+{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, RankNTypes #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Category.Alg
+-- Copyright   :  (c) Sjoerd Visscher 2010
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  sjoerd@w3future.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Alg(F), the category of F-algebras and F-homomorphisms.
+-----------------------------------------------------------------------------
+module Data.Category.Alg where
+
+import Prelude hiding ((.), id)
+
+import Data.Category
+import Data.Category.Void
+import Data.Category.Hask
+
+-- | Objects of Alg(F) are F-algebras.
+newtype Algebra f a = Algebra (Dom f (F f a) a)
+
+-- | Arrows of Alg(F) are F-homomorphisms.
+data family Alg f a b :: *
+data instance Alg f (Algebra f a) (Algebra f b) = AlgA (Dom f a b)
+
+newtype instance Nat (Alg f) d g h = 
+  AlgNat { unAlgNat :: forall a. Obj (Algebra f a) -> Component g h (Algebra f a) }
+
+instance (Dom f ~ (~>), Cod f ~ (~>), CategoryO (~>) a) => CategoryO (Alg f) (Algebra f a) where
+  id = AlgA id
+  (!) = unAlgNat
+instance (Dom f ~ (~>), Cod f ~ (~>), CategoryA (~>) a b c) => CategoryA (Alg f) (Algebra f a) (Algebra f b) (Algebra f c) where
+  AlgA f . AlgA g = AlgA (f . g)
+
+-- | The initial F-algebra is the initial object in the category of F-algebras.
+type InitialFAlgebra f = InitialObject (Alg f)
+
+-- | A catamorphism of an F-algebra is the arrow to it from the initial F-algebra.
+type Cata f a = Algebra f a -> Alg f (InitialFAlgebra f) (Algebra f a)
+
+-- | FixF provides the initial F-algebra for endofunctors in Hask.
+newtype FixF f = InF { outF :: f (FixF f) }
+
+-- | Catamorphisms for endofunctors in Hask.
+cataHask :: Functor f => Cata (EndoHask f) a
+cataHask (Algebra f) = AlgA $ cata f where cata f = f . fmap (cata f) . outF 
+
+instance Functor f => VoidColimit (Alg (EndoHask f)) where
+  type InitialObject (Alg (EndoHask f)) = Algebra (EndoHask f) (FixF f)
+  voidColimit = InitialUniversal VoidNat (AlgNat $ \f VoidNat -> cataHask f)
diff --git a/Data/Category/Boolean.hs b/Data/Category/Boolean.hs
--- a/Data/Category/Boolean.hs
+++ b/Data/Category/Boolean.hs
@@ -8,38 +8,39 @@
 -- Maintainer  :  sjoerd@w3future.com
 -- Stability   :  experimental
 -- Portability :  non-portable
+--
+-- /2/, or the Boolean category. 
+-- It contains 2 objects, one for true and one for false.
+-- It contains 3 arrows, 2 identity arrows and one from false to true.
 -----------------------------------------------------------------------------
 module Data.Category.Boolean where
 
 import Prelude hiding ((.), id)
 
 import Data.Category
-import Data.Category.Functor
 import Data.Category.Void
 import Data.Category.Pair
 
-
--- | /2/, or the Boolean category
-data family Boolean a b :: *
-
+-- | 'Fls', the object representing false.
 data Fls = Fls deriving Show
+-- | 'Tru', the object representing true.
 data Tru = Tru deriving Show
 
+-- | The arrows of the boolean category.
+data family Boolean a b :: *
 data instance Boolean Fls Fls = IdFls
 data instance Boolean Tru Tru = IdTru
 data instance Boolean Fls Tru = FlsTru
 
-instance Apply Boolean Fls Fls where
-  IdFls $$ Fls = Fls
-instance Apply Boolean Fls Tru where
-  FlsTru $$ Fls = Tru
-instance Apply Boolean Tru Tru where
-  IdTru $$ Tru = Tru
-  
+data instance Nat Boolean d f g = 
+  BooleanNat (Component f g Fls) (Component f g Tru)
+
 instance CategoryO Boolean Fls where
   id = IdFls
+  BooleanNat f _ ! Fls = f
 instance CategoryO Boolean Tru where
   id = IdTru
+  BooleanNat _ t ! Tru = t
 
 instance CategoryA Boolean Fls Fls Fls where
   IdFls . IdFls = IdFls
@@ -49,13 +50,15 @@
   IdTru . FlsTru = FlsTru  
 instance CategoryA Boolean Tru Tru Tru where
   IdTru . IdTru = IdTru
+    
+instance Apply Boolean Fls Fls where
+  IdFls $$ Fls = Fls
+instance Apply Boolean Fls Tru where
+  FlsTru $$ Fls = Tru
+instance Apply Boolean Tru Tru where
+  IdTru $$ Tru = Tru
   
 
-  
-data instance Funct Boolean d (FunctO Boolean d f) (FunctO Boolean d g) = 
-  BooleanNat { flsComp :: Component f g Fls, truComp :: Component f g Tru }
-instance (CategoryO (Cod f) (F f Fls), CategoryO (Cod f) (F f Tru)) => CategoryO (Funct Boolean d) (FunctO Boolean d f) where
-  id = BooleanNat id id
 
 instance VoidColimit Boolean where
   type InitialObject Boolean = Fls
@@ -66,26 +69,26 @@
 
 instance PairLimit Boolean Fls Fls where 
   type Product Fls Fls = Fls
-  pairLimit = TerminalUniversal (IdFls :***: IdFls) (BooleanNat fstComp sndComp)
+  pairLimit = TerminalUniversal (IdFls :***: IdFls) (BooleanNat (! Fst) (! Snd))
 instance PairLimit Boolean Fls Tru where 
   type Product Fls Tru = Fls
-  pairLimit = TerminalUniversal (IdFls :***: FlsTru) (BooleanNat fstComp fstComp)
+  pairLimit = TerminalUniversal (IdFls :***: FlsTru) (BooleanNat (! Fst) (! Fst))
 instance PairLimit Boolean Tru Fls where 
   type Product Tru Fls = Fls
-  pairLimit = TerminalUniversal (FlsTru :***: IdFls) (BooleanNat sndComp sndComp)
+  pairLimit = TerminalUniversal (FlsTru :***: IdFls) (BooleanNat (! Snd) (! Snd))
 instance PairLimit Boolean Tru Tru where 
   type Product Tru Tru = Tru
-  pairLimit = TerminalUniversal (IdTru :***: IdTru) (BooleanNat fstComp sndComp)
+  pairLimit = TerminalUniversal (IdTru :***: IdTru) (BooleanNat (! Fst) (! Snd))
 
 instance PairColimit Boolean Fls Fls where 
   type Coproduct Fls Fls = Fls
-  pairColimit = InitialUniversal (IdFls :***: IdFls) (BooleanNat fstComp sndComp)
+  pairColimit = InitialUniversal (IdFls :***: IdFls) (BooleanNat (! Fst) (! Snd))
 instance PairColimit Boolean Fls Tru where 
   type Coproduct Fls Tru = Tru
-  pairColimit = InitialUniversal (FlsTru :***: IdTru) (BooleanNat sndComp sndComp)
+  pairColimit = InitialUniversal (FlsTru :***: IdTru) (BooleanNat (! Snd) (! Snd))
 instance PairColimit Boolean Tru Fls where 
   type Coproduct Tru Fls = Tru
-  pairColimit = InitialUniversal (IdTru :***: FlsTru) (BooleanNat fstComp fstComp)
+  pairColimit = InitialUniversal (IdTru :***: FlsTru) (BooleanNat (! Fst) (! Fst))
 instance PairColimit Boolean Tru Tru where 
   type Coproduct Tru Tru = Tru
-  pairColimit = InitialUniversal (IdTru :***: IdTru) (BooleanNat fstComp sndComp)
+  pairColimit = InitialUniversal (IdTru :***: IdTru) (BooleanNat (! Fst) (! Snd))
diff --git a/Data/Category/Functor.hs b/Data/Category/Functor.hs
--- a/Data/Category/Functor.hs
+++ b/Data/Category/Functor.hs
@@ -11,50 +11,33 @@
 -----------------------------------------------------------------------------
 module Data.Category.Functor where
   
-import Prelude hiding ((.), id)
-
 import Data.Category
 
 
--- |Functor category Funct(C, D), or D^C.
+-- | Functor category Funct(C, D), or D^C.
+-- Objects of Funct(C, D) are functors from C to D.
 -- Arrows of Funct(C, D) are natural transformations.
 -- Each category C needs its own data instance.
-data family Funct (c :: * -> * -> *) (d :: * -> * -> *) (a :: *) (b :: *) :: *
 
--- |Objects of Funct(C, D) are functors from C to D.
-data FunctO (c :: * -> * -> *) (d :: * -> * -> *) (f :: *) = (Dom f ~ c, Cod f ~ d) => FunctO f
 
--- |Arrows of the category Funct(Funct(C, D), E)
+
+-- | Arrows of the category Funct(Funct(C, D), E)
 -- I.e. natural transformations between functors of type D^C -> E
-data instance Funct (Funct c d) e (FunctO (Funct c d) e f) (FunctO (Funct c d) e g) =
-  FunctNat (forall h. (Dom h ~ c, Cod h ~ d) => Component f g (FunctO c d h))
+data instance Nat (Nat c d) e f g = 
+  FunctNat { unFunctNat :: forall h. (Dom h ~ c, Cod h ~ d) => Obj h -> Component f g h }
 
 
-type Component f g z = Cod f (F f z) (F g z)
-type f :~> g = (c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => Funct c d (FunctO c d f) (FunctO c d g)
 
-
 -- | The diagonal functor from (index-) category J to (~>).
 data Diag (j :: * -> * -> *) ((~>) :: * -> * -> *) = Diag
 type instance Dom (Diag j (~>)) = (~>)
-type instance Cod (Diag j (~>)) = Funct j (~>)
-type instance F (Diag j (~>)) a = FunctO j (~>) (Const j (~>) a)
-
-
-type InitMorF x u = (x :*-: Cod u) :.: u
-type TermMorF x u = (Cod u :-*: x) :.: u
-data InitialUniversal  x u a = InitialUniversal  (F (InitMorF x u) a) (InitMorF x u :~> (a :*-: Dom u))
-data TerminalUniversal x u a = TerminalUniversal (F (TermMorF x u) a) (TermMorF x u :~> (Dom u :-*: a))
+type instance Cod (Diag j (~>)) = Nat j (~>)
+type instance F (Diag j (~>)) a = Const j (~>) a
 
--- |A cone from N to F is a natural transformation from the constant functor to N to F.
+-- | A cone from N to F is a natural transformation from the constant functor to N to F.
 type Cone   f n = Const (Dom f) (Cod f) n :~> f
--- |A co-cone from F to N is a natural transformation from F to the constant functor to N.
+-- | A co-cone from F to N is a natural transformation from F to the constant functor to N.
 type Cocone f n = f :~> Const (Dom f) (Cod f) n
 
-type Limit   f l = TerminalUniversal (FunctO (Dom f) (Cod f) f) (Diag (Dom f) (Cod f)) l
-type Colimit f l = InitialUniversal  (FunctO (Dom f) (Cod f) f) (Diag (Dom f) (Cod f)) l
-
-data Adjunction f g = Adjunction 
-  { unit :: Id (Dom f) :~> (g :.: f)
-  , counit :: (f :.: g) :~> Id (Dom g)
-  }
+type Limit   f l = TerminalUniversal f (Diag (Dom f) (Cod f)) l
+type Colimit f l = InitialUniversal  f (Diag (Dom f) (Cod f)) l
diff --git a/Data/Category/Hask.hs b/Data/Category/Hask.hs
--- a/Data/Category/Hask.hs
+++ b/Data/Category/Hask.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, GADTs, EmptyDataDecls #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, GADTs, EmptyDataDecls, ScopedTypeVariables #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Hask
@@ -14,13 +14,12 @@
 import Prelude hiding ((.), id)
 import qualified Prelude
 import Control.Arrow ((&&&), (***), (+++))
--- Getting desperate
-import Unsafe.Coerce
 
 import Data.Category
 import Data.Category.Functor
 import Data.Category.Void
 import Data.Category.Pair
+-- import Data.Category.Discrete
 
 type Hask = (->)
 
@@ -29,21 +28,24 @@
 
 instance CategoryO (->) a where
   id = Prelude.id
+  (!) = unHaskNat
   
 instance CategoryA (->) a b c where
   (.) = (Prelude..)
 
-
-
-newtype instance Funct (->) d (FunctO (->) d f) (FunctO (->) d g) = 
-  HaskNat (forall a. Component f g a)
-
--- | This isn't really working, and there really needs to be a solution for this.
-unHaskNat :: Funct (->) d (FunctO (->) d f) (FunctO (->) d g) -> Component f g a
-unHaskNat (HaskNat c) = unsafeCoerce c
+newtype instance Nat (->) d f g = 
+  HaskNat { unHaskNat :: forall a. Obj a -> Component f g a }
+  
+-- | 'EndoHask' is a wrapper to turn instances of the 'Functor' class into categorical functors.
+data EndoHask (f :: * -> *) = EndoHask
+type instance Dom (EndoHask f) = (->)
+type instance Cod (EndoHask f) = (->)
+type instance F (EndoHask f) r = f r
+instance Functor f => FunctorA (EndoHask f) a b where
+  _ % f = fmap f
 
 instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Diag (->) (~>)) a b where
-  Diag % f = HaskNat f
+  Diag % f = HaskNat $ const f
 
 -- | Any empty data type is an initial object in Hask.
 data Zero
@@ -53,45 +55,53 @@
 
 instance VoidColimit (->) where
   type InitialObject (->) = Zero
-  voidColimit = InitialUniversal VoidNat (HaskNat $ \VoidNat -> magic)
+  voidColimit = InitialUniversal VoidNat (HaskNat $ \_ VoidNat -> magic)
 instance VoidLimit (->) where
   type TerminalObject (->) = ()
-  voidLimit = TerminalUniversal VoidNat (HaskNat $ \VoidNat -> const ())
+  voidLimit = TerminalUniversal VoidNat (HaskNat $ \_ VoidNat -> const ())
 
 -- | An alternative way to define the initial object.
 initObjInHask :: Limit (Id (->)) Zero
-initObjInHask = TerminalUniversal (HaskNat $ magic) (HaskNat unHaskNat)
+initObjInHask = TerminalUniversal (HaskNat $ const magic) (HaskNat $ const (! (obj :: Zero)))
 -- | An alternative way to define the terminal object.
 termObjInHask :: Colimit (Id (->)) ()
-termObjInHask = InitialUniversal (HaskNat $ const ()) (HaskNat unHaskNat)
+termObjInHask = InitialUniversal (HaskNat $ \_ _ -> ()) (HaskNat $ const (! ()))
 
 instance PairColimit (->) x y where
   type Coproduct x y = Either x y
-  pairColimit = InitialUniversal (Left :***: Right) (HaskNat $ \(l :***: r) -> either l r)
+  pairColimit = InitialUniversal (Left :***: Right) (HaskNat $ \_ (l :***: r) -> either l r)
 instance PairLimit (->) x y where
   type Product x y = (x, y)
-  pairLimit = TerminalUniversal (fst :***: snd) (HaskNat $ \(f :***: s) -> f &&& s)
+  pairLimit = TerminalUniversal (fst :***: snd) (HaskNat $ \_ (f :***: s) -> f &&& s)
 
+-- type instance F (z, zs) Z = z
+-- type instance F (z, zs) (S a) = F zs a
+-- type instance ProductN (S n) f = (F f n, ProductN n f)
+-- type instance ProductN Z f = ()
+-- 
+-- instance DiscreteLimit (S n) (->) f where
+--   discreteLimit = TerminalUniversal (DiscreteNat fst (\_ _ c p -> snd c p in undefined)) undefined
+
 -- | The product functor, Hask^2 -> Hask
 data ProdInHask = ProdInHask
-type instance Dom ProdInHask = Funct Pair (->)
+type instance Dom ProdInHask = Nat Pair (->)
 type instance Cod ProdInHask = (->)
-type instance F ProdInHask (FunctO Pair (->) f) = (F f Fst, F f Snd)
-instance (Dom f ~ Pair, Cod f ~ (->), Dom g ~ Pair, Cod g ~ (->)) => FunctorA ProdInHask (FunctO Pair (->) f) (FunctO Pair (->) g) where
+type instance F ProdInHask f = (F f Fst, F f Snd)
+instance (Dom f ~ Pair, Cod f ~ (->), Dom g ~ Pair, Cod g ~ (->)) => FunctorA ProdInHask f g where
   ProdInHask % (f :***: g) = f *** g
 
 -- | The product functor is right adjoint to the diagonal functor.
 prodInHaskAdj :: Adjunction (Diag Pair (->)) ProdInHask
-prodInHaskAdj = Adjunction { unit = HaskNat $ id &&& id, counit = FunctNat $ fst :***: snd }
+prodInHaskAdj = Adjunction { unit = HaskNat $ const (id &&& id), counit = FunctNat $ const (fst :***: snd) }
 
 -- | The coproduct functor, Hask^2 -> Hask
 data CoprodInHask = CoprodInHask
-type instance Dom CoprodInHask = Funct Pair (->)
+type instance Dom CoprodInHask = Nat Pair (->)
 type instance Cod CoprodInHask = (->)
-type instance F CoprodInHask (FunctO Pair (->) f) = Either (F f Fst) (F f Snd)
-instance (Dom f ~ Pair, Cod f ~ (->), Dom g ~ Pair, Cod g ~ (->)) => FunctorA CoprodInHask (FunctO Pair (->) f) (FunctO Pair (->) g) where
+type instance F CoprodInHask f = Either (F f Fst) (F f Snd)
+instance (Dom f ~ Pair, Cod f ~ (->), Dom g ~ Pair, Cod g ~ (->)) => FunctorA CoprodInHask f g where
   CoprodInHask % (f :***: g) = f +++ g
 
 -- | The coproduct functor is left adjoint to the diagonal functor.
 coprodInHaskAdj :: Adjunction CoprodInHask (Diag Pair (->))
-coprodInHaskAdj = Adjunction { unit = FunctNat $ Left :***: Right, counit = HaskNat $ either id id }
+coprodInHaskAdj = Adjunction { unit = FunctNat $ const (Left :***: Right), counit = HaskNat $ const (either id id) }
diff --git a/Data/Category/Kleisli.hs b/Data/Category/Kleisli.hs
--- a/Data/Category/Kleisli.hs
+++ b/Data/Category/Kleisli.hs
@@ -11,16 +11,12 @@
 --
 -- This is an attempt at the Kleisli category, and the construction 
 -- of an adjunction for each monad.
--- But the typing issues with natural transformations in Hask make this problematic.
 -----------------------------------------------------------------------------
 module Data.Category.Kleisli where
   
 import Prelude hiding ((.), id, Monad(..))
--- Getting desperate
-import Unsafe.Coerce
 
 import Data.Category
-import Data.Category.Functor
 import Data.Category.Hask
 
 class Pointed m where
@@ -31,29 +27,35 @@
   
 data Kleisli ((~>) :: * -> * -> *) m a b = Kleisli (m -> a ~> F m b)
 
+newtype instance Nat (Kleisli (->) m) d f g = 
+  KleisliNat { unKleisliNat :: forall a. Obj a -> Component f g a }
+
 instance (Monad m, Dom m ~ (->), Cod m ~ (->)) => CategoryO (Kleisli (->) m) o where
-  id = Kleisli $ \m -> unHaskNat (point m)
+  id = Kleisli $ \m -> point m ! (obj :: o)
+  (!) = unKleisliNat
 instance (Monad m, Dom m ~ (->), Cod m ~ (->), FunctorA m b (F m c)) => CategoryA (Kleisli (->) m) a b c where
-  (Kleisli f) . (Kleisli g) = Kleisli $ \m -> unsafeCoerce (unHaskNat (join m)) . (m % f m) . g m
-newtype instance Funct (Kleisli (->) m) d (FunctO (Kleisli (->) m) d f) (FunctO (Kleisli (->) m) d g) = 
-  KleisliNat (forall a. CategoryO d (F f a) => Component f g a)
+  (Kleisli f) . (Kleisli g) = Kleisli $ \m -> join m ! (obj :: c) . (m % f m) . g m
 
+
+
 data KleisliAdjF ((~>) :: * -> * -> *) m = KleisliAdjF m
 type instance Dom (KleisliAdjF (~>) m) = (~>)
 type instance Cod (KleisliAdjF (~>) m) = Kleisli (~>) m
 type instance F (KleisliAdjF (~>) m) a = a
 instance (Monad m, Dom m ~ (->), Cod m ~ (->)) => FunctorA (KleisliAdjF (->) m) a b where
-  KleisliAdjF _ % f = Kleisli $ \m -> unHaskNat (point m) . f
+  KleisliAdjF _ % f = Kleisli $ \m -> point m ! (obj :: b) . f
   
 data KleisliAdjG ((~>) :: * -> * -> *) m = KleisliAdjG m
 type instance Dom (KleisliAdjG (~>) m) = Kleisli (~>) m
 type instance Cod (KleisliAdjG (~>) m) = (~>)
 type instance F (KleisliAdjG (~>) m) a = F m a
 instance (Monad m, Dom m ~ (->), Cod m ~ (->), FunctorA m a (F m b)) => FunctorA (KleisliAdjG (->) m) a b where
-  KleisliAdjG m % Kleisli f = unsafeCoerce (unHaskNat (join m)) . (m % f m)
+  KleisliAdjG m % Kleisli f = join m ! (obj :: b) . (m % f m)
 
 instance (Pointed m, Dom m ~ (->), Cod m ~ (->)) => Pointed (KleisliAdjG (->) m :.: KleisliAdjF (->) m) where
-  point (KleisliAdjG m :.: _) = HaskNat (unHaskNat (point m))
+  point (KleisliAdjG m :.: _) = HaskNat (point m !)
    
 kleisliAdj :: (Monad m, Dom m ~ (->), Cod m ~ (->)) => m -> Adjunction (KleisliAdjF (->) m) (KleisliAdjG (->) m)
-kleisliAdj m = Adjunction { unit = point (KleisliAdjG m :.: KleisliAdjF m), counit = KleisliNat (Kleisli $ \m -> undefined) }
+kleisliAdj m = Adjunction 
+  { unit = point (KleisliAdjG m :.: KleisliAdjF m)
+  , counit = KleisliNat (\obja -> Kleisli $ \_ -> undefined) }
diff --git a/Data/Category/Monoid.hs b/Data/Category/Monoid.hs
--- a/Data/Category/Monoid.hs
+++ b/Data/Category/Monoid.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Monoid
@@ -21,11 +21,13 @@
 -- | The arrows are the values of the monoid.
 newtype MonoidA m a b = MonoidA m
 
+newtype instance Nat (MonoidA m) d f g =
+  MonoidNat (Component f g m)
+
 instance Monoid m => CategoryO (MonoidA m) m where
   id = MonoidA mempty
-  
+  MonoidNat c ! _ = c  
 instance Monoid m => CategoryA (MonoidA m) m m m where
   MonoidA a . MonoidA b = MonoidA $ a `mappend` b
-  
 instance Monoid m => Apply (MonoidA m) m m where
   MonoidA a $$ b = a `mappend` b
diff --git a/Data/Category/Omega.hs b/Data/Category/Omega.hs
--- a/Data/Category/Omega.hs
+++ b/Data/Category/Omega.hs
@@ -25,18 +25,20 @@
 -- | The object Z represents zero.
 data Z = Z deriving Show
 -- | The object S n represents the successor of n.
-newtype S n = S { unS :: n } deriving Show
+newtype S n = S n deriving Show
 
 instance CategoryO Omega Z where
   id = IdZ
+  OmegaNat z _ ! Z = z  
 instance (CategoryO Omega n) => CategoryO Omega (S n) where
   id = StepS id
+  on@(OmegaNat _ s) ! (S n) = s n (on ! n)
 
 -- | The arrows of omega, there's an arrow from a to b iff a <= b.
-data family Omega a b :: * 
+data family Omega a b :: *
 data instance Omega Z Z = IdZ
-newtype instance Omega Z (S n) = GTZ { unGTZ :: Omega Z n }
-newtype instance Omega (S a) (S b) = StepS { unStepS :: Omega a b }
+newtype instance Omega Z (S n) = GTZ (Omega Z n)
+newtype instance Omega (S a) (S b) = StepS (Omega a b)
 
 instance (CategoryO Omega n) => CategoryA Omega Z Z n where
   a . IdZ = a
@@ -52,11 +54,9 @@
 instance Apply Omega a b => Apply Omega (S a) (S b) where
   StepS d $$ S a = S (d $$ a)
 
+data instance Nat Omega d f g = 
+  OmegaNat (Component f g Z) (forall n. Obj n -> Component f g n -> Component f g (S n))
 
-data instance Funct Omega d (FunctO Omega d f) (FunctO Omega d g) = 
-  OmegaNat (Component f g Z) (forall n. CategoryO d (F f (S n)) => Component f g n -> Component f g (S n))
-instance (Dom f ~ Omega, Cod f ~ d, CategoryO (Cod f) (F f Z)) => CategoryO (Funct Omega d) (FunctO Omega d f) where
-  id = OmegaNat id (const id)
 
 data OmegaF ((~>) :: * -> * -> *) z f = OmegaF
 type instance Dom (OmegaF (~>) z f) = Omega
@@ -76,19 +76,19 @@
 
 instance VoidColimit Omega where
   type InitialObject Omega = Z
-  voidColimit = InitialUniversal VoidNat (OmegaNat (\VoidNat -> IdZ) (\cpt VoidNat -> GTZ (cpt VoidNat)))
+  voidColimit = InitialUniversal VoidNat (OmegaNat (\VoidNat -> IdZ) (\_ cpt VoidNat -> GTZ (cpt VoidNat)))
 
 -- The product in omega is the minimum.
 instance PairLimit Omega Z Z where 
   type Product Z Z = Z
-  pairLimit = TerminalUniversal (IdZ :***: IdZ) (OmegaNat fstComp (\cpt -> sndComp))
+  pairLimit = TerminalUniversal (IdZ :***: IdZ) undefined
 instance (PairLimit Omega Z n, Product Z n ~ Z) => PairLimit Omega Z (S n) where 
   type Product Z (S n) = Z
-  pairLimit = TerminalUniversal (IdZ :***: GTZ p) (OmegaNat fstComp (\cpt -> fstComp)) where
+  pairLimit = TerminalUniversal (IdZ :***: GTZ p) undefined where
     TerminalUniversal (_ :***: p) _ = pairLimit :: Limit (PairF Omega Z n) (Product Z n)
 instance (PairLimit Omega n Z, Product n Z ~ Z) => PairLimit Omega (S n) Z where 
   type Product (S n) Z = Z
-  pairLimit = TerminalUniversal (GTZ p :***: IdZ) (OmegaNat sndComp (\cpt -> sndComp)) where
+  pairLimit = TerminalUniversal (GTZ p :***: IdZ) undefined where
     TerminalUniversal (p :***: _) _ = pairLimit :: Limit (PairF Omega n Z) (Product n Z)
 instance (PairLimit Omega a b) => PairLimit Omega (S a) (S b) where 
   type Product (S a) (S b) = S (Product a b)
@@ -98,14 +98,14 @@
 -- The coproduct in omega is the maximum.
 instance PairColimit Omega Z Z where 
   type Coproduct Z Z = Z
-  pairColimit = InitialUniversal (IdZ :***: IdZ) (OmegaNat fstComp (\cpt -> sndComp))
+  pairColimit = InitialUniversal (IdZ :***: IdZ) undefined
 instance (PairColimit Omega Z n, Coproduct Z n ~ n) => PairColimit Omega Z (S n) where 
   type Coproduct Z (S n) = S n
-  pairColimit = InitialUniversal (GTZ p1 :***: StepS p2) (OmegaNat sndComp (\cpt -> sndComp)) where
+  pairColimit = InitialUniversal (GTZ p1 :***: StepS p2) undefined where
     InitialUniversal (p1 :***: p2) _ = pairColimit :: Colimit (PairF Omega Z n) (Coproduct Z n)
 instance (PairColimit Omega n Z, Coproduct n Z ~ n) => PairColimit Omega (S n) Z where 
   type Coproduct (S n) Z = S n
-  pairColimit = InitialUniversal (StepS p1 :***: GTZ p2) (OmegaNat fstComp (\cpt -> fstComp)) where
+  pairColimit = InitialUniversal (StepS p1 :***: GTZ p2) undefined where
     InitialUniversal (p1 :***: p2) _ = pairColimit :: Colimit (PairF Omega n Z) (Coproduct n Z)
 instance (PairColimit Omega a b) => PairColimit Omega (S a) (S b) where 
   type Coproduct (S a) (S b) = S (Coproduct a b)
diff --git a/Data/Category/Pair.hs b/Data/Category/Pair.hs
--- a/Data/Category/Pair.hs
+++ b/Data/Category/Pair.hs
@@ -27,8 +27,10 @@
 
 instance CategoryO Pair Fst where
   id = IdFst
+  (f :***: _) ! Fst = f  
 instance CategoryO Pair Snd where
   id = IdSnd
+  (_ :***: s) ! Snd = s  
 
 -- | The arrows of Pair.
 data family Pair a b :: *
@@ -46,10 +48,10 @@
   IdSnd $$ Snd = Snd
 
   
-data instance Funct Pair d (FunctO Pair d f) (FunctO Pair d g) = 
-  (:***:) { fstComp :: Component f g Fst, sndComp :: Component f g Snd }
-instance (CategoryO (Cod f) (F f Fst), CategoryO (Cod f) (F f Snd)) => CategoryO (Funct Pair d) (FunctO Pair d f) where
+data instance Nat Pair d f g = Component f g Fst :***: Component f g Snd
+instance (Dom f ~ Pair, Cod f ~ (~>), CategoryO (~>) (F f Fst), CategoryO (~>) (F f Snd)) => CategoryO (Nat Pair (~>)) f where
   id = id :***: id
+  FunctNat n ! f = n f
 instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Diag Pair (~>)) a b where
   Diag % f = f :***: f
 
diff --git a/Data/Category/Unit.hs b/Data/Category/Unit.hs
--- a/Data/Category/Unit.hs
+++ b/Data/Category/Unit.hs
@@ -22,10 +22,13 @@
 data family Unit a b :: *
 data instance Unit UnitO UnitO = UnitId
 
-instance Apply Unit UnitO UnitO where
-  UnitId $$ UnitO = UnitO
+newtype instance Nat Unit d f g =
+  UnitNat (Component f g UnitO)
   
 instance CategoryO Unit UnitO where
   id = UnitId
+  UnitNat c ! UnitO = c
 instance CategoryA Unit UnitO UnitO UnitO where
   UnitId . UnitId = UnitId
+instance Apply Unit UnitO UnitO where
+  UnitId $$ UnitO = UnitO
diff --git a/Data/Category/Void.hs b/Data/Category/Void.hs
--- a/Data/Category/Void.hs
+++ b/Data/Category/Void.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies, FlexibleInstances, MultiParamTypeClasses, EmptyDataDecls #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, FlexibleInstances, FlexibleContexts, MultiParamTypeClasses, EmptyDataDecls, ScopedTypeVariables #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Void
@@ -21,12 +21,10 @@
 -- | The (empty) data type of the arrows in /0/. 
 data Void a b
 
-data instance Funct Void d (FunctO Void d f) (FunctO Void d g) = 
+data instance Nat Void d f g = 
   VoidNat
-instance CategoryO (Funct Void d) (FunctO Void d f) where
-  id = VoidNat
 instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Diag Void (~>)) a b where
-  Diag % f = VoidNat
+  Diag % _ = VoidNat
 
 -- | The functor from /0/ to (~>), the empty diagram in (~>).
 data VoidF ((~>) :: * -> * -> *) = VoidF
@@ -37,7 +35,14 @@
 class VoidColimit (~>) where
   type InitialObject (~>) :: *
   voidColimit :: Colimit (VoidF (~>)) (InitialObject (~>))
+  initialize :: CategoryO (~>) a => InitialObject (~>) ~> a
+  initialize = (n ! (obj :: a)) VoidNat where 
+    InitialUniversal VoidNat n = voidColimit
+  
 -- | A terminal object is the limit of the functor from /0/ to (~>).
 class VoidLimit (~>) where
   type TerminalObject (~>) :: *
   voidLimit :: Limit (VoidF (~>)) (TerminalObject (~>))
+  terminate :: CategoryO (~>) a => a ~> TerminalObject (~>)
+  terminate = (n ! (obj :: a)) VoidNat where
+    TerminalUniversal VoidNat n = voidLimit
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.0.3.1
+version:             0.1.0
 synopsis:            Restricted categories
 description:         
   Data-category is a collection of categories, and some categorical constructions on them.
@@ -24,6 +24,7 @@
     Data.Category.Boolean,
     Data.Category.Omega,
     Data.Category.Hask,
-    Data.Category.Kleisli
+    Data.Category.Kleisli,
+    Data.Category.Alg
     
   build-depends:       base >= 3 && < 5