diff --git a/Data/Category/Adjunction.hs b/Data/Category/Adjunction.hs
--- a/Data/Category/Adjunction.hs
+++ b/Data/Category/Adjunction.hs
@@ -117,19 +117,13 @@
 limitAdj :: forall j (~>). HasLimits j (~>) 
   => LimitFunctor j (~>) 
   -> Adjunction (Nat j (~>)) (~>) (Diag j (~>)) (LimitFunctor j (~>))
-limitAdj LimitFunctor = terminalPropAdjunction Diag LimitFunctor univ
-  where
-    univ :: Obj (Nat j (~>)) f -> TerminalUniversal f (Diag j (~>)) (LimitFam j (~>) f)
-    univ f@Nat{} = limitUniv f
+limitAdj LimitFunctor = terminalPropAdjunction Diag LimitFunctor (\f @ Nat{} -> limitUniv f)
 
 -- | The colimit functor is left adjoint to the diagonal functor.
 colimitAdj :: forall j (~>). HasColimits j (~>) 
   => ColimitFunctor j (~>) 
   -> Adjunction (~>) (Nat j (~>)) (ColimitFunctor j (~>)) (Diag j (~>))
-colimitAdj ColimitFunctor = initialPropAdjunction ColimitFunctor Diag univ
-  where
-    univ :: Obj (Nat j (~>)) f -> InitialUniversal f (Diag j (~>)) (ColimitFam j (~>) f)
-    univ f@Nat{} = colimitUniv f
+colimitAdj ColimitFunctor = initialPropAdjunction ColimitFunctor Diag (\f @ Nat{} -> colimitUniv f)
 
 
 adjunctionMonad :: Adjunction c d f g -> M.Monad (g :.: f)
diff --git a/Data/Category/Boolean.hs b/Data/Category/Boolean.hs
--- a/Data/Category/Boolean.hs
+++ b/Data/Category/Boolean.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies, GADTs, EmptyDataDecls, TypeOperators, ScopedTypeVariables, UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies, GADTs, TypeOperators, ScopedTypeVariables, UndecidableInstances #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Boolean
@@ -22,6 +22,8 @@
 import Data.Category.NaturalTransformation
 import Data.Category.Product
 import Data.Category.Limit
+import Data.Category.Monoidal
+import Data.Category.CartesianClosed
 
 
 data Fls
@@ -119,7 +121,55 @@
   _   ||| _   = error "Other combinations should not type check"
 
 
+type instance Exponential Boolean Fls Fls = Tru
+type instance Exponential Boolean Fls Tru = Tru
+type instance Exponential Boolean Tru Fls = Fls
+type instance Exponential Boolean Tru Tru = Tru
 
+instance CartesianClosed Boolean where
+  
+  apply Fls Fls = Fls
+  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
+  Fls ^^^ Tru = Fls
+  F2T ^^^ Fls = Tru
+  F2T ^^^ F2T = F2T
+  F2T ^^^ Tru = F2T
+  Tru ^^^ Fls = Tru
+  Tru ^^^ F2T = Tru
+  Tru ^^^ Tru = Tru
+
+
+trueProductMonoid :: MonoidObject (ProductFunctor Boolean) Tru
+trueProductMonoid = MonoidObject Tru Tru
+
+falseCoproductComonoid :: ComonoidObject (CoproductFunctor Boolean) Fls
+falseCoproductComonoid = ComonoidObject Fls Fls
+
+trueProductComonoid :: ComonoidObject (ProductFunctor Boolean) Tru
+trueProductComonoid = ComonoidObject Tru Tru
+
+falseCoproductMonoid :: MonoidObject (CoproductFunctor Boolean) Fls
+falseCoproductMonoid = MonoidObject Fls Fls
+
+trueCoproductMonoid :: MonoidObject (CoproductFunctor Boolean) Tru
+trueCoproductMonoid = MonoidObject F2T Tru
+
+falseProductComonoid :: ComonoidObject (ProductFunctor Boolean) Fls
+falseProductComonoid = ComonoidObject F2T Fls
+
+
 -- | A natural transformation @Nat c d@ is isomorphic to a functor from @c :**: 2@ to @d@.
 data NatAsFunctor f g = NatAsFunctor (Nat (Dom f) (Cod f) f g)
 type instance Dom (NatAsFunctor f g) = (Dom f) :**: Boolean
@@ -127,9 +177,6 @@
 type instance NatAsFunctor f g :% (a, Fls) = f :% a
 type instance NatAsFunctor f g :% (a, Tru) = g :% a
 instance (Functor f, Functor g, Category c, Category d, Dom f ~ c, Cod f ~ d, Dom g ~ c, Cod g ~ d) => Functor (NatAsFunctor f g) where
-  NatAsFunctor n % (a :**: b) = natAsFunctor n a b
-    where
-      natAsFunctor :: Nat c d f g -> c a1 a2 -> Boolean b1 b2 -> d (NatAsFunctor f g :% (a1, b1)) (NatAsFunctor f g :% (a2, b2))
-      natAsFunctor (Nat f _ _) a Fls = f % a
-      natAsFunctor (Nat _ g _) a Tru = g % a
-      natAsFunctor n           a F2T = n ! a
+  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
@@ -55,10 +55,7 @@
 type instance Cod (CatApply y z) = z
 type instance CatApply y z :% (f, a) = f :% a
 instance (Category y, Category z) => Functor (CatApply y z) where
-  CatApply % (l :**: r) = catApply l r
-    where
-      catApply :: Nat y z f g -> y a b -> z (f :% a) (g :% b)
-      catApply n@Nat{} h = n ! h
+  CatApply % (l :**: r) = l ! r
 
 data CatTuple (y :: * -> * -> *) (z :: * -> * -> *) = CatTuple
 type instance Dom (CatTuple y z) = z
@@ -83,9 +80,7 @@
 type instance PShExponential (~>) p q :% a = Presheaves (~>) ((YonedaEmbedding (~>) :% a) :*: p) q
 instance (Category (~>), Dom p ~ Op (~>), Dom q ~ Op (~>), Cod p ~ (->), Cod q ~ (->), Functor p, Functor q)
   => Functor (PShExponential (~>) p q) where
-  PShExponential % Op f = h f where
-    h :: a ~> b -> PShExponential (~>) p q :% b -> PShExponential (~>) p q :% a
-    h g (Nat (_ :*: p) q n) = Nat (Hom_X (src g) :*: p) q $ \i (i2a, pi) -> n i (g . i2a, pi)
+  PShExponential % Op f = \(Nat (_ :*: p) q n) -> Nat (Hom_X (src f) :*: p) q $ \i (i2a, pi) -> n i (f . i2a, pi)
 
 type instance Exponential (Presheaves (~>)) y z = PShExponential (~>) y z
 
diff --git a/Data/Category/Coproduct.hs b/Data/Category/Coproduct.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/Coproduct.hs
@@ -0,0 +1,91 @@
+{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, FlexibleContexts #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Category.Product
+-- Copyright   :  (c) Sjoerd Visscher 2010
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  sjoerd@w3future.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+-----------------------------------------------------------------------------
+module Data.Category.Coproduct where
+
+import Prelude (error)
+
+import Data.Category
+import Data.Category.Functor
+
+
+data I1 a
+data I2 a
+
+data (:++:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where
+  I1 :: c1 a1 b1 -> (:++:) c1 c2 (I1 a1) (I1 b1)
+  I2 :: c2 a2 b2 -> (:++:) c1 c2 (I2 a2) (I2 b2)
+
+-- | The product category of category @c1@ and @c2@.
+instance (Category c1, Category c2) => Category (c1 :++: c2) where
+  
+  src (I1 a)      = I1 (src a)
+  src (I2 a)      = I2 (src a)
+  tgt (I1 a)      = I1 (tgt a)
+  tgt (I2 a)      = I2 (tgt a)
+
+  (I1 a) . (I1 b) = I1 (a . b)
+  (I2 a) . (I2 b) = I2 (a . b)
+  _      . _      = error "Other combinations should not type check"
+
+  
+  
+    
+data Inj1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Inj1
+type instance Dom (Inj1 c1 c2) = c1
+type instance Cod (Inj1 c1 c2) = c1 :++: c2
+type instance Inj1 c1 c2 :% a = I1 a
+instance (Category c1, Category c2) => Functor (Inj1 c1 c2) where 
+  Inj1 % f = I1 f
+
+data Inj2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Inj2
+type instance Dom (Inj2 c1 c2) = c2
+type instance Cod (Inj2 c1 c2) = c1 :++: c2
+type instance Inj2 c1 c2 :% a = I2 a
+instance (Category c1, Category c2) => Functor (Inj2 c1 c2) where 
+  Inj2 % f = I2 f
+
+data f1 :+++: f2 = f1 :+++: f2
+type instance Dom (f1 :+++: f2) = Dom f1 :++: Dom f2
+type instance Cod (f1 :+++: f2) = Cod f1 :++: Cod f2
+type instance (f1 :+++: f2) :% (I1 a) = I1 (f1 :% a)
+type instance (f1 :+++: f2) :% (I2 a) = I2 (f2 :% a)
+instance (Functor f1, Functor f2) => Functor (f1 :+++: f2) where 
+  (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
+instance Category (~>) => Functor (CodiagCoprod (~>)) where 
+  CodiagCoprod % I1 f = f
+  CodiagCoprod % I2 f = f
+
+data Cotuple1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Cotuple1 (Obj c1 a)
+type instance Dom (Cotuple1 c1 c2 a1) = c1 :++: c2
+type instance Cod (Cotuple1 c1 c2 a1) = c1
+type instance Cotuple1 c1 c2 _1 :% I1 a1 = a1
+type instance Cotuple1 c1 c2 a1 :% I2 a2 = a1
+instance (Category c1, Category c2) => Functor (Cotuple1 c1 c2 a1) where
+  Cotuple1 _ % I1 f = f
+  Cotuple1 a % I2 _ = a
+
+data Cotuple2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Cotuple2 (Obj c2 a)
+type instance Dom (Cotuple2 c1 c2 a2) = c1 :++: c2
+type instance Cod (Cotuple2 c1 c2 a2) = c2
+type instance Cotuple2 c1 c2 a2 :% I1 a1 = a2
+type instance Cotuple2 c1 c2 _2 :% I2 a2 = a2
+instance (Category c1, Category c2) => Functor (Cotuple2 c1 c2 a2) where
+  Cotuple2 a % I1 _ = a
+  Cotuple2 _ % I2 f = f
+
diff --git a/Data/Category/Dialg.hs b/Data/Category/Dialg.hs
--- a/Data/Category/Dialg.hs
+++ b/Data/Category/Dialg.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleInstances, FlexibleContexts #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleInstances, FlexibleContexts, ViewPatterns #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Dialg
@@ -116,7 +116,5 @@
     
   initialObject = dialgId $ Dialgebra id (Z :**: S)
   
-  initialize a = DialgA (dialgebra initialObject) (dialgebra a) $ f undefined where
-    f :: ((->) :**: (->)) ((), t) (t, t) -> NatNum -> t
-    f (z :**: s) = primRec z s
+  initialize (dialgebra -> d@(Dialgebra _ (z :**: s))) = DialgA (dialgebra initialObject) d $ primRec z s
     
diff --git a/Data/Category/Discrete.hs b/Data/Category/Discrete.hs
--- a/Data/Category/Discrete.hs
+++ b/Data/Category/Discrete.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, RankNTypes, EmptyDataDecls, ScopedTypeVariables, FlexibleContexts, FlexibleInstances, UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, RankNTypes, ScopedTypeVariables, FlexibleContexts, FlexibleInstances, UndecidableInstances #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Discrete
@@ -20,16 +20,12 @@
   , Unit
   , Pair
   
-  -- * Diagrams
+  -- * Functors
+  , Next(..)
   , DiscreteDiagram(..)
-  , PairDiagram
-  , arrowPair
     
   -- * Natural Transformations
-  , discreteNat
-  , ComList(..)
   , voidNat
-  , pairNat
     
 ) where
 
@@ -121,41 +117,6 @@
   (_ ::: xs) % S n = xs % n
 
 
-infixr 7 ::::
-
-data ComList f g n z where
-  ComNil :: ComList f g Z z
-  (::::) :: Com f g z -> ComList f g n (S z) -> ComList f g (S n) z
-
-class DiscreteNat n where
-  discreteNat :: (Functor f, Functor g, Category d, Dom f ~ Discrete n, Dom g ~ Discrete n, Cod f ~ d, Cod g ~ d)
-    => f -> g -> ComList f g n Z -> Nat (Discrete n) d f g
-  shiftComList :: ComList f g n (S z) -> ComList (Next f) (Next g) n z
-  
-instance DiscreteNat Z where
-  discreteNat f g ComNil = Nat f g magicZ
-  shiftComList ComNil = ComNil
-
-instance (Category (Discrete n), DiscreteNat n) => DiscreteNat (S n) where
-  discreteNat f g comlist = Nat f g (\x -> unCom $ h f g comlist x) where
-    h :: (Functor f, Functor g, Category d, Dom f ~ Discrete (S n), Dom g ~ Discrete (S n), Cod f ~ d, Cod g ~ d)
-      => f -> g -> ComList f g (S n) Z -> Obj (Discrete (S n)) a -> Com f g a
-    h _  _  (c :::: _ ) Z     = c
-    h f' g' (_ :::: cs) (S n) = Com $ (discreteNat (Next f') (Next g') (shiftComList cs)) ! n
-  shiftComList (Com c :::: cs) = Com c :::: shiftComList cs
-
 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       = discreteNat f g ComNil
-
-pairNat :: (Functor f, Functor g, Category d, Dom f ~ Pair, Cod f ~ d, Dom g ~ Pair, Cod g ~ d) 
-  => f -> g -> Com f g Z -> Com f g (S Z) -> Nat Pair d f g
-pairNat f g c1 c2 = discreteNat f g (c1 :::: c2 :::: ComNil)
-
-
--- | The functor from @Pair@ to @(~>)@, a diagram of 2 objects in @(~>)@. 
-type PairDiagram (~>) x y = DiscreteDiagram (~>) (S (S Z)) (x, (y, ()))
-
-arrowPair :: Category (~>) => (x1 ~> x2) -> (y1 ~> y2) -> Nat Pair (~>) (PairDiagram (~>) x1 y1) (PairDiagram (~>) x2 y2)
-arrowPair l r = pairNat (src l ::: src r ::: Nil) (tgt l ::: tgt r ::: Nil) (Com l) (Com r)
-
+voidNat f g = Nat f g magicZ
diff --git a/Data/Category/Functor.hs b/Data/Category/Functor.hs
--- a/Data/Category/Functor.hs
+++ b/Data/Category/Functor.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, EmptyDataDecls, FlexibleContexts, UndecidableInstances, GADTs, RankNTypes #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, FlexibleContexts, UndecidableInstances, GADTs, RankNTypes #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Functor
diff --git a/Data/Category/Limit.hs b/Data/Category/Limit.hs
--- a/Data/Category/Limit.hs
+++ b/Data/Category/Limit.hs
@@ -1,5 +1,4 @@
 {-# LANGUAGE 
-  EmptyDataDecls, 
   FlexibleContexts, 
   FlexibleInstances, 
   GADTs, 
@@ -89,6 +88,7 @@
 import Data.Category.Functor
 import Data.Category.NaturalTransformation
 import Data.Category.Product
+import Data.Category.Coproduct
 import Data.Category.Discrete
 
 infixl 3 ***
@@ -276,6 +276,16 @@
   
   terminate (Nat f _ _) = Nat f (Const terminalObject) $ terminate . (f %)
 
+-- | 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
+  
+  type TerminalObject (c1 :**: c2) = (TerminalObject c1, TerminalObject c2)
+  
+  terminalObject = terminalObject :**: terminalObject
+  
+  terminate (a1 :**: a2) = terminate a1 :**: terminate a2
+  
+  
 
 -- | An initial object is the colimit of the functor from /0/ to (~>).
 class Category (~>) => HasInitialObject (~>) where
@@ -326,8 +336,17 @@
   
   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
+  
+  type InitialObject (c1 :**: c2) = (InitialObject c1, InitialObject c2)
+  
+  initialObject = initialObject :**: initialObject
+  
+  initialize (a1 :**: a2) = initialize a1 :**: initialize a2
 
 
+
 type family BinaryProduct ((~>) :: * -> * -> *) x y :: *
 
 -- | The product of 2 objects is the limit of the functor from Pair to (~>).
@@ -342,16 +361,25 @@
   l *** r = (l . proj1 (src l) (src r)) &&& (r . proj2 (src l) (src r)) where
 
 
-type instance LimitFam Pair (~>) f = BinaryProduct (~>) (f :% Z) (f :% S Z)
-
-instance HasBinaryProducts (~>) => HasLimits Pair (~>) where
+type instance LimitFam (Discrete (S n)) (~>) f = BinaryProduct (~>) (f :% Z) (LimitFam (Discrete n) (~>) (Next f))
 
-  limitUniv (Nat f _ _) = limitUniversal
-    (pairNat (Const $ x *** y) f (Com $ proj1 x y) (Com $ proj2 x y))
-    (\c -> c ! Z &&& c ! S Z)
+instance (HasLimits (Discrete n) (~>), HasBinaryProducts (~>)) => HasLimits (Discrete (S n)) (~>) where
+  
+  limitUniv (Nat l _ _) = limitUniv' l
     where
-      x = f % Z
-      y = f % S Z
+      limitUniv' :: forall f. (Functor f, Dom f ~ Discrete (S n), Cod f ~ (~>), HasLimits (Discrete n) (~>), HasBinaryProducts (~>)) 
+                 => f -> LimitUniversal f
+      limitUniv' f = limitUniversal
+        (Nat (Const $ x *** y) f (\z -> unCom $ h z))
+        (\c -> c ! Z &&& limitFactorizer luNext (Nat (Const $ coneVertex c) (Next f) $ \n -> c ! S n))
+        where
+          x = f % Z
+          y = coneVertex limNext
+          limNext = limit luNext
+          luNext = limitUniv (natId (Next f))
+          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
 
 
 type instance BinaryProduct (->) x y = (x, y)
@@ -374,7 +402,6 @@
   CatA f1 &&& CatA f2 = CatA ((f1 :***: f2) :.: DiagProd)
   CatA f1 *** CatA f2 = CatA (f1 :***: f2)
 
-
 type instance BinaryProduct (c1 :**: c2) (x1, x2) (y1, y2) = (BinaryProduct c1 x1 y1, BinaryProduct c2 x2 y2)
 
 instance (HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts (c1 :**: c2) where
@@ -429,16 +456,25 @@
   l +++ r = (inj1 (tgt l) (tgt r) . l) ||| (inj2 (tgt l) (tgt r) . r) where
     
 
-type instance ColimitFam Pair (~>) f = BinaryCoproduct (~>) (f :% Z) (f :% S Z)
+type instance ColimitFam (Discrete (S n)) (~>) f = BinaryCoproduct (~>) (f :% Z) (ColimitFam (Discrete n) (~>) (Next f))
 
-instance HasBinaryCoproducts (~>) => HasColimits Pair (~>) where
+instance (HasColimits (Discrete n) (~>), HasBinaryCoproducts (~>)) => HasColimits (Discrete (S n)) (~>) where
   
-  colimitUniv (Nat f _ _) = colimitUniversal
-    (pairNat f (Const $ x +++ y) (Com $ inj1 x y) (Com $ inj2 x y))
-    (\c -> c ! Z ||| c ! S Z)
+  colimitUniv (Nat l _ _) = colimitUniv' l
     where
-      x = f % Z
-      y = f % S Z
+      colimitUniv' :: forall f. (Functor f, Dom f ~ Discrete (S n), Cod f ~ (~>), HasColimits (Discrete n) (~>), HasBinaryCoproducts (~>)) 
+                   => f -> ColimitUniversal f
+      colimitUniv' f = colimitUniversal
+        (Nat f (Const $ x +++ y) (\z -> unCom $ h z))
+        (\c -> c ! Z ||| colimitFactorizer cluNext (Nat (Next f) (Const $ coconeVertex c) $ \n -> c ! S n))
+        where
+          x = f % Z
+          y = coconeVertex colNext
+          colNext = colimit cluNext
+          cluNext = colimitUniv (natId (Next f))
+          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
 
 
 type instance BinaryCoproduct (->) x y = Either x y
@@ -450,8 +486,17 @@
   
   (|||) = (A.|||)
   (+++) = (A.+++)
+
+type instance BinaryCoproduct Cat (CatW c1) (CatW c2) = CatW (c1 :++: c2)
+
+instance HasBinaryCoproducts Cat where
   
+  inj1 (CatA _) (CatA _) = CatA Inj1
+  inj2 (CatA _) (CatA _) = CatA Inj2
   
+  CatA f1 ||| CatA f2 = CatA (CodiagCoprod :.: (f1 :+++: f2))
+  CatA f1 +++ CatA f2 = CatA (f1 :+++: f2)
+
 type instance BinaryCoproduct (c1 :**: c2) (x1, x2) (y1, y2) = (BinaryCoproduct c1 x1 y1, BinaryCoproduct c2 x2 y2)
 
 instance (HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts (c1 :**: c2) where
@@ -489,7 +534,6 @@
   
   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
-
 
 
 newtype ForAll f = ForAll { unForAll :: forall a. f a }
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, ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, Rank2Types, ViewPatterns #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Monoidal
@@ -11,35 +11,37 @@
 -----------------------------------------------------------------------------
 module Data.Category.Monoidal where
 
-import Prelude (($))
+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
+import Data.Category.Product
 import Data.Category.Limit
 
 
 class Functor f => HasUnit f where
   
   type Unit f :: *
-  unitObject :: Obj (Cod f) (Unit f)
+  unitObject :: f -> Obj (Cod f) (Unit f)
 
 
 instance (HasTerminalObject (~>), HasBinaryProducts (~>)) => HasUnit (ProductFunctor (~>)) where
   
   type Unit (ProductFunctor (~>)) = TerminalObject (~>)
-  unitObject = terminalObject
+  unitObject _ = terminalObject
 
 instance (HasInitialObject (~>), HasBinaryCoproducts (~>)) => HasUnit (CoproductFunctor (~>)) where
   
   type Unit (CoproductFunctor (~>)) = InitialObject (~>)
-  unitObject = initialObject
+  unitObject _ = initialObject
 
 instance Category (~>) => HasUnit (FunctorCompose (~>)) where
   
   type Unit (FunctorCompose (~>)) = Id (~>)
-  unitObject = natId Id
+  unitObject _ = natId Id
   
 
 
@@ -97,6 +99,23 @@
   }
 
 
+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
+
+instance Category (MonoidAsCategory f m) where
+  
+  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)
+
+
+
 type Monad f = MonoidObject (FunctorCompose (Dom f)) f
 
 mkMonad :: (Functor f, Dom f ~ (~>), Cod f ~ (~>), Category (~>)) 
@@ -113,10 +132,7 @@
 preludeMonad = mkMonad EndoHask (\_ -> M.return) (\_ -> M.join)
 
 monadFunctor :: forall f. Monad f -> f
-monadFunctor m = f
-  where
-    u :: Nat (Dom f) (Dom f) (Id (Dom f)) f
-    u@(Nat _ f _) = unit m
+monadFunctor (unit -> Nat _ f _) = f
 
 
 type Comonad f = ComonoidObject (FunctorCompose (Dom f)) f
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, MultiParamTypeClasses, ScopedTypeVariables, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, GADTs #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, GADTs #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.NaturalTransformation
@@ -177,10 +177,7 @@
 type instance Cod (Yoneda f) = (->)
 type instance Yoneda f :% a = Nat (Dom f) (->) (a :*-: Dom f) f
 instance Functor f => Functor (Yoneda f) where
-  Yoneda % g = h g
-    where
-      h :: Dom f a b -> Yoneda f :% a -> Yoneda f :% b
-      h ab (Nat _ f n) = Nat (HomX_ $ tgt ab) f $ \z bz -> n z (bz . ab)
+  Yoneda % ab = \(Nat _ f n) -> Nat (HomX_ $ tgt ab) f $ \z bz -> n z (bz . ab)
       
   
 fromYoneda :: (Functor f, Cod f ~ (->)) => f -> Nat (Dom f) (->) (Yoneda f) f
diff --git a/Data/Category/Omega.hs b/Data/Category/Omega.hs
--- a/Data/Category/Omega.hs
+++ b/Data/Category/Omega.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, EmptyDataDecls, FlexibleInstances #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleInstances #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Omega
@@ -18,6 +18,7 @@
 
 import Data.Category
 import Data.Category.Limit
+import Data.Category.Monoidal
 
 
 data Z
@@ -76,18 +77,18 @@
   proj2 (S a) (S b) = S $ proj2 a b
   proj2 _     _     = error "Other combinations should not type check"
   
-  Z   &&& _     = Z
-  _     &&& Z   = Z
+  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"
+  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.
+-- The coproduct in omega is the maximum.
 instance HasBinaryCoproducts Omega where 
   
   inj1 Z     Z     = Z
@@ -101,8 +102,17 @@
   inj2 (S a) (S b) = S $ inj2 a b
   inj2 _     _     = error "Other combinations should not type check"
   
-  Z   ||| Z   = Z
+  Z     ||| Z     = Z
   Z2S _ ||| a     = a
   a     ||| Z2S _ = a
-  S a ||| S b = S (a ||| b)
-  _     ||| _      = error "Other combinations should not type check"
+  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
--- a/Data/Category/Peano.hs
+++ b/Data/Category/Peano.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleInstances #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleInstances, ViewPatterns #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Peano
@@ -54,6 +54,4 @@
   
   initialObject = peanoId $ PeanoO Z S
   
-  initialize a = PeanoA (peanoO initialObject) o $ primRec z s
-    where
-      o@(PeanoO z s) = peanoO a
+  initialize (peanoO -> o@(PeanoO z s)) = PeanoA (peanoO initialObject) o $ primRec z s
diff --git a/data-category.cabal b/data-category.cabal
--- a/data-category.cabal
+++ b/data-category.cabal
@@ -1,5 +1,5 @@
 name:                data-category
-version:             0.3.0.2
+version:             0.3.1
 synopsis:            Restricted categories
 
 description:         Data-category is a collection of categories, and some categorical constructions on them.
@@ -30,12 +30,13 @@
   exposed-modules:     
     Data.Category,
     Data.Category.Functor,
-    Data.Category.Product,
     Data.Category.NaturalTransformation,
-    Data.Category.Limit,
     Data.Category.Adjunction,
+    Data.Category.Limit,
     Data.Category.Monoidal,
     Data.Category.CartesianClosed,
+    Data.Category.Product,
+    Data.Category.Coproduct,
     Data.Category.Discrete,
     Data.Category.Monoid,
     Data.Category.Boolean,