diff --git a/Data/Category/Adjunction.hs b/Data/Category/Adjunction.hs
--- a/Data/Category/Adjunction.hs
+++ b/Data/Category/Adjunction.hs
@@ -14,6 +14,8 @@
     Adjunction(..)
   , mkAdjunction
   , mkAdjunctionUnits
+  , mkAdjunctionUnit
+  , mkAdjunctionCounit
 
   , leftAdjunct
   , rightAdjunct
@@ -67,6 +69,20 @@
   -> (forall a. Obj c a -> Component (f :.: g) (Id c) a)
   -> Adjunction c d f g
 mkAdjunctionUnits f g un coun = mkAdjunction f g (\a h -> (g % h) . un a) (\b h -> coun b . (f % h))
+
+mkAdjunctionUnit :: (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
+  => f -> g
+  -> (forall a. Obj d a -> Component (Id d) (g :.: f) a)
+  -> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b)
+  -> Adjunction c d f g
+mkAdjunctionUnit f g un adj = mkAdjunction f g (\a h -> (g % h) . un a) adj
+
+mkAdjunctionCounit :: (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
+  => f -> g
+  -> (forall a b. Obj d a -> c (f :% a) b -> d a (g :% b))
+  -> (forall a. Obj c a -> Component (f :.: g) (Id c) a)
+  -> Adjunction c d f g
+mkAdjunctionCounit f g adj coun = mkAdjunction f g adj (\b h -> coun b . (f % h))
 
 leftAdjunct :: Adjunction c d f g -> Obj d a -> c (f :% a) b -> d a (g :% b)
 leftAdjunct (Adjunction _ _ l _) a h = (l ! (Op a :**: tgt h)) h
diff --git a/Data/Category/Boolean.hs b/Data/Category/Boolean.hs
--- a/Data/Category/Boolean.hs
+++ b/Data/Category/Boolean.hs
@@ -175,10 +175,10 @@
 -- | The limit of a functor from the Boolean category is the source of the arrow it points to.
 instance Category k => HasLimits Boolean k where
   limit (Nat f _ _) = Nat (Const (f % Fls)) f (\case Fls -> f % Fls; Tru -> f % F2T)
-  limitFactorizer Nat{} = \n -> n ! Fls
+  limitFactorizer n = n ! Fls
 
 type instance ColimitFam Boolean k f = f :% Tru
 -- | The colimit of a functor from the Boolean category is the target of the arrow it points to.
 instance Category k => HasColimits Boolean k where
   colimit (Nat f _ _) = Nat f (Const (f % Tru)) (\case Fls -> f % F2T; Tru -> f % Tru)
-  colimitFactorizer Nat{} = \n -> n ! Tru
+  colimitFactorizer n = n ! Tru
diff --git a/Data/Category/Comma.hs b/Data/Category/Comma.hs
--- a/Data/Category/Comma.hs
+++ b/Data/Category/Comma.hs
@@ -21,12 +21,12 @@
 data CommaO :: * -> * -> * -> * where
   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 :: 
+
+data (:/\:) :: * -> * -> * -> * -> * where
+  CommaA ::
     CommaO t s (a, b) ->
-    Dom t a a' -> 
-    Dom s b b' -> 
+    Dom t a a' ->
+    Dom s b b' ->
     CommaO t s (a', b') ->
     (t :/\: s) (a, b) (a', b')
 
@@ -35,10 +35,10 @@
 
 -- | The comma category T \\downarrow S
 instance (Category (Dom t), Category (Dom s)) => Category (t :/\: s) where
-    
+
   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
 
 
@@ -48,12 +48,14 @@
 type (c `ObjectsUnder` a) = Id c `ObjectsFUnder` a
 type (c `ObjectsOver`  a) = Id c `ObjectsFOver`  a
 
+type Arrows c = Id c :/\: Id c
 
+
 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) _ _ _ -> 
+  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
diff --git a/Data/Category/Dialg.hs b/Data/Category/Dialg.hs
--- a/Data/Category/Dialg.hs
+++ b/Data/Category/Dialg.hs
@@ -39,10 +39,10 @@
 
 -- | The category of (F,G)-dialgebras.
 instance Category (Dialg f g) where
-  
+
   src (DialgA s _ _) = dialgId s
   tgt (DialgA _ t _) = dialgId t
-  
+
   DialgA _ t f . DialgA s _ g = DialgA s t (f . g)
 
 
@@ -76,11 +76,11 @@
 -- | The category for defining the natural numbers and primitive recursion can be described as
 -- @Dialg(F,G)@, with @F(A)=\<1,A>@ and @G(A)=\<A,A>@.
 instance HasInitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) where
-  
+
   type InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) = NatNum
-    
+
   initialObject = dialgId (Dialgebra (\x -> x) (Z :**: S))
-  
+
   initialize (dialgebra -> d@(Dialgebra _ (z :**: s))) = DialgA (dialgebra initialObject) d (primRec z s)
 
 
@@ -91,11 +91,11 @@
   type Dom (FreeAlg m) = Dom m
   type Cod (FreeAlg m) = Alg m
   type FreeAlg m :% a = m :% a
-  FreeAlg m % f = DialgA (alg (src f)) (alg (tgt f)) (monadFunctor m % f)
-    where
-      alg :: Obj k x -> Algebra m (m :% x)
-      alg x = Dialgebra (monadFunctor m % x) (multiply m ! x)
+  FreeAlg m % f = DialgA (freeAlg m (src f)) (freeAlg m (tgt f)) (monadFunctor m % f)
 
+freeAlg :: (Functor m, Dom m ~ k, Cod m ~ k) => Monad m -> Obj (Cod m) x -> Algebra m (m :% x)
+freeAlg m x = Dialgebra (monadFunctor m % x) (multiply m ! x)
+
 data ForgetAlg m = ForgetAlg
 -- | @ForgetAlg m@ is the forgetful functor for @Alg m@.
 instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (ForgetAlg m) where
@@ -107,5 +107,5 @@
 eilenbergMooreAdj :: (Functor m, Dom m ~ k, Cod m ~ k)
   => Monad m -> A.Adjunction (Alg m) k (FreeAlg m) (ForgetAlg m)
 eilenbergMooreAdj m = A.mkAdjunctionUnits (FreeAlg m) ForgetAlg
-  (\x -> unit m ! x)
-  (\(DialgA (Dialgebra _ h) _ _) -> DialgA (Dialgebra (src h) (monadFunctor m % h)) (Dialgebra (tgt h) h) h)
+  (unit m !)
+  (\(DialgA b@(Dialgebra _ h) _ _) -> DialgA (Dialgebra (src h) (monadFunctor m % h)) b h)
diff --git a/Data/Category/Kleisli.hs b/Data/Category/Kleisli.hs
--- a/Data/Category/Kleisli.hs
+++ b/Data/Category/Kleisli.hs
@@ -12,7 +12,7 @@
 -- of an adjunction for each monad.
 -----------------------------------------------------------------------------
 module Data.Category.Kleisli where
-  
+
 import Data.Category
 import Data.Category.Functor
 import Data.Category.NaturalTransformation
@@ -28,30 +28,28 @@
 
 -- | The category of Kleisli arrows.
 instance Category (Kleisli m) where
-  
+
   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)
 
 
 
-data KleisliAdjF m = KleisliAdjF (Monad m)
-instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (KleisliAdjF m) where
-  type Dom (KleisliAdjF m) = Dom m
-  type Cod (KleisliAdjF m) = Kleisli m
-  type KleisliAdjF m :% a = a
-  KleisliAdjF m % f = Kleisli m (tgt f) ((unit m ! tgt f) . f)
-   
-data KleisliAdjG m = KleisliAdjG (Monad m)
-instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (KleisliAdjG m) where
-  type Dom (KleisliAdjG m) = Kleisli m
-  type Cod (KleisliAdjG m) = Dom m
-  type KleisliAdjG m :% a = m :% a
-  KleisliAdjG m % Kleisli _ b f = (multiply m ! b) . (monadFunctor m % f)
+newtype KleisliFree m = KleisliFree (Monad m)
+instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (KleisliFree m) where
+  type Dom (KleisliFree m) = Dom m
+  type Cod (KleisliFree m) = Kleisli m
+  type KleisliFree m :% a = a
+  KleisliFree m % f = Kleisli m (tgt f) ((unit m ! tgt f) . f)
 
+data KleisliForget m = KleisliForget
+instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (KleisliForget m) where
+  type Dom (KleisliForget m) = Kleisli m
+  type Cod (KleisliForget m) = Dom m
+  type KleisliForget m :% a = m :% a
+  KleisliForget % Kleisli m b f = (multiply m ! b) . (monadFunctor m % f)
+
 kleisliAdj :: (Functor m, Dom m ~ k, Cod m ~ k)
-  => Monad m -> A.Adjunction (Kleisli m) k (KleisliAdjF m) (KleisliAdjG m)
-kleisliAdj m = A.mkAdjunctionUnits (KleisliAdjF m) (KleisliAdjG m)
-  (\x -> unit m ! x)
-  (\(Kleisli _ x _) -> Kleisli m x (monadFunctor m % x))
+  => Monad m -> A.Adjunction (Kleisli m) k (KleisliFree m) (KleisliForget m)
+kleisliAdj m = A.mkAdjunctionUnit (KleisliFree m) KleisliForget (unit m !) (\(Kleisli _ x _) f -> Kleisli m x f)
diff --git a/Data/Category/Limit.hs b/Data/Category/Limit.hs
--- a/Data/Category/Limit.hs
+++ b/Data/Category/Limit.hs
@@ -41,6 +41,8 @@
   , HasLimits(..)
   , LimitFunctor(..)
   , limitAdj
+  , adjLimit
+  , adjLimitFactorizer
   , rightAdjointPreservesLimits
   , rightAdjointPreservesLimitsInv
 
@@ -50,6 +52,8 @@
   , HasColimits(..)
   , ColimitFunctor(..)
   , colimitAdj
+  , adjColimit
+  , adjColimitFactorizer
   , leftAdjointPreservesColimits
   , leftAdjointPreservesColimitsInv
 
@@ -103,18 +107,18 @@
 
 
 -- | A cone from N to F is a natural transformation from the constant functor to N to F.
-type Cone   f n = Nat (Dom f) (Cod f) (ConstF f n) f
+type Cone   j k f n = Nat j k (Const j k n) f
 
 -- | A co-cone from F to N is a natural transformation from F to the constant functor to N.
-type Cocone f n = Nat (Dom f) (Cod f) f (ConstF f n)
+type Cocone j k f n = Nat j k f (Const j k n)
 
 
 -- | The vertex (or apex) of a cone.
-coneVertex :: Cone f n -> Obj (Cod f) n
+coneVertex :: Cone j k f n -> Obj k n
 coneVertex (Nat (Const x) _ _) = x
 
 -- | The vertex (or apex) of a co-cone.
-coconeVertex :: Cocone f n -> Obj (Cod f) n
+coconeVertex :: Cocone j k f n -> Obj k n
 coconeVertex (Nat _ (Const x) _) = x
 
 
@@ -127,10 +131,10 @@
 -- | 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 k) f -> Cone f (Limit f)
+  limit           :: Obj (Nat j k) f -> Cone j k f (LimitFam j k 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 k) f -> Cone f n -> k n (Limit f)
+  limitFactorizer :: Cone j k f n -> k n (LimitFam j k f)
 
 data LimitFunctor (j :: * -> * -> *) (k  :: * -> * -> *) = LimitFunctor
 -- | If every diagram of type @j@ has a limit in @k@ there exists a limit functor.
@@ -140,13 +144,19 @@
   type Cod (LimitFunctor j k) = k
   type LimitFunctor j k :% f = LimitFam j k f
 
-  LimitFunctor % n @ Nat{}  = limitFactorizer (tgt n) (n . limit (src n))
+  LimitFunctor % n = limitFactorizer (n . limit (src n))
 
 -- | The limit functor is right adjoint to the diagonal functor.
 limitAdj :: forall j k. HasLimits j k => Adjunction (Nat j k) k (Diag j k) (LimitFunctor j k)
-limitAdj = mkAdjunctionUnits diag LimitFunctor (\a -> limitFactorizer (diag % a) (diag % a)) (\f @ Nat{} -> limit f)
-  where diag = Diag :: Diag j k -- Forces the type of all Diags to be the same.
+limitAdj = mkAdjunctionCounit Diag LimitFunctor (\_ -> limitFactorizer) limit
 
+adjLimit :: Category k => Adjunction (Nat j k) k (Diag j k) r -> Obj (Nat j k) f -> Cone j k f (r :% f)
+adjLimit adj f = adjunctionCounit adj ! f
+
+adjLimitFactorizer :: Category k => Adjunction (Nat j k) k (Diag j k) r -> Cone j k f n -> k n (r :% f)
+adjLimitFactorizer adj cone = leftAdjunct adj (coneVertex cone) cone
+
+
 -- Cone (g :.: t) (Limit (g :.: t))
 -- Obj j z -> d (Limit (g :.: t)) ((g :.: t) :% z)
 -- Obj j z -> d (f :% Limit (g :.: t)) (t :% z)
@@ -157,7 +167,7 @@
   :: (HasLimits j c, HasLimits j d)
   => Adjunction c d f g -> Obj (Nat j c) t -> d (Limit (g :.: t)) (g :% Limit t)
 rightAdjointPreservesLimits adj@(Adjunction f g _ _) (Nat t _ _) =
-  leftAdjunct adj x (limitFactorizer (natId t) cone)
+  leftAdjunct adj x (limitFactorizer cone)
     where
       l = limit (natId (g :.: t))
       x = coneVertex l
@@ -169,8 +179,8 @@
 -- d (g :% Limit t) (Limit (g :.: t))
 rightAdjointPreservesLimitsInv
   :: (HasLimits j c, HasLimits j d)
-  => Obj (Nat c d) g -> Obj (Nat j c) t -> d (g :% Limit t) (Limit (g :.: t))
-rightAdjointPreservesLimitsInv g@Nat{} t@Nat{} = limitFactorizer (g `o` t) (constPrecompIn (g `o` limit t))
+  => Obj (Nat c d) g -> Obj (Nat j c) t -> d (g :% LimitFam j c t) (LimitFam j d (g :.: t))
+rightAdjointPreservesLimitsInv g t = limitFactorizer (constPrecompIn (g `o` limit t))
 
 -- | 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 :: *) :: *
@@ -180,10 +190,10 @@
 -- | 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 k) f -> Cocone f (Colimit f)
+  colimit           :: Obj (Nat j k) f -> Cocone j k f (ColimitFam j k 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 k) f -> Cocone f n -> k (Colimit f) n
+  colimitFactorizer :: Cocone j k f n -> k (ColimitFam j k f) n
 
 data ColimitFunctor (j :: * -> * -> *) (k  :: * -> * -> *) = ColimitFunctor
 -- | If every diagram of type @j@ has a colimit in @k@ there exists a colimit functor.
@@ -193,19 +203,24 @@
   type Cod (ColimitFunctor j k) = k
   type ColimitFunctor j k :% f = ColimitFam j k f
 
-  ColimitFunctor % n @ Nat{}  = colimitFactorizer (src n) (colimit (tgt n) . n)
+  ColimitFunctor % n = colimitFactorizer (colimit (tgt n) . n)
 
 -- | The colimit functor is left adjoint to the diagonal functor.
 colimitAdj :: forall j k. HasColimits j k => Adjunction k (Nat j k) (ColimitFunctor j k) (Diag j k)
-colimitAdj = mkAdjunctionUnits ColimitFunctor diag (\f @ Nat{} -> colimit f) (\a -> colimitFactorizer (diag % a) (diag % a))
-  where diag = Diag :: Diag j k -- Forces the type of all Diags to be the same.
+colimitAdj = mkAdjunctionUnit ColimitFunctor Diag colimit (\_ -> colimitFactorizer)
 
+adjColimit :: Category k => Adjunction k (Nat j k) l (Diag j k) -> Obj (Nat j k) f -> Cocone j k f (l :% f)
+adjColimit adj f = adjunctionUnit adj ! f
 
+adjColimitFactorizer :: Category k => Adjunction k (Nat j k) l (Diag j k) -> Cocone j k f n -> k (l :% f) n
+adjColimitFactorizer adj cocone = rightAdjunct adj (coconeVertex cocone) cocone
+
+
 leftAdjointPreservesColimits
   :: (HasColimits j c, HasColimits j d)
   => Adjunction c d f g -> Obj (Nat j d) t -> c (f :% Colimit t) (Colimit (f :.: t))
 leftAdjointPreservesColimits adj@(Adjunction f g _ _) (Nat t _ _) =
-  rightAdjunct adj x (colimitFactorizer (natId t) cocone)
+  rightAdjunct adj x (colimitFactorizer cocone)
     where
       l = colimit (natId (f :.: t))
       x = coconeVertex l
@@ -213,8 +228,8 @@
 
 leftAdjointPreservesColimitsInv
   :: (HasColimits j c, HasColimits j d)
-  => Obj (Nat d c) f -> Obj (Nat j d) t -> c (Colimit (f :.: t)) (f :% Colimit t)
-leftAdjointPreservesColimitsInv f@Nat{} t@Nat{} = colimitFactorizer (f `o` t) (constPrecompOut (f `o` colimit t))
+  => Obj (Nat d c) f -> Obj (Nat j d) t -> c (ColimitFam j c (f :.: t)) (f :% ColimitFam j d t)
+leftAdjointPreservesColimitsInv f t = colimitFactorizer (constPrecompOut (f `o` colimit t))
 
 
 class Category k => HasTerminalObject k where
@@ -232,7 +247,7 @@
 instance (Category k, HasTerminalObject k) => HasLimits Void k where
 
   limit (Nat f _ _) = voidNat (Const terminalObject) f
-  limitFactorizer Nat{} = terminate . coneVertex
+  limitFactorizer = terminate . coneVertex
 
 
 -- | @()@ is the terminal object in @Hask@.
@@ -300,7 +315,7 @@
 instance (Category k, HasInitialObject k) => HasColimits Void k where
 
   colimit (Nat f _ _) = voidNat f (Const initialObject)
-  colimitFactorizer Nat{} = initialize . coconeVertex
+  colimitFactorizer = initialize . coconeVertex
 
 
 data Zero
@@ -376,7 +391,7 @@
 
   limit = limit'
     where
-      limit' :: forall f. Obj (Nat (i :++: j) k) f -> Cone f (Limit f)
+      limit' :: forall f. Obj (Nat (i :++: j) k) f -> Cone (i :++: j) k f (LimitFam (i :++: j) k f)
       limit' l@Nat{} = Nat (Const (x *** y)) (srcF l) h
         where
           x = coneVertex lim1
@@ -387,10 +402,10 @@
           h (I1 n) = lim1 ! n . proj1 x y
           h (I2 n) = lim2 ! n . proj2 x y
 
-  limitFactorizer l@Nat{} c =
-    limitFactorizer (l `o` natId Inj1) (constPostcompIn (c `o` natId Inj1))
+  limitFactorizer c =
+    limitFactorizer (constPostcompIn (c `o` natId Inj1))
     &&&
-    limitFactorizer (l `o` natId Inj2) (constPostcompIn (c `o` natId Inj2))
+    limitFactorizer (constPostcompIn (c `o` natId Inj2))
 
 
 -- | The tuple is the binary product in @Hask@.
@@ -512,7 +527,7 @@
 
   colimit = colimit'
     where
-      colimit' :: forall f. Obj (Nat (i :++: j) k) f -> Cocone f (Colimit f)
+      colimit' :: forall f. Obj (Nat (i :++: j) k) f -> Cocone (i :++: j) k f (ColimitFam (i :++: j) k f)
       colimit' l@Nat{} = Nat (srcF l) (Const (x +++ y)) h
         where
           x = coconeVertex col1
@@ -523,10 +538,10 @@
           h (I1 n) = inj1 x y . col1 ! n
           h (I2 n) = inj2 x y . col2 ! n
 
-  colimitFactorizer l@Nat{} c =
-    colimitFactorizer (l `o` natId Inj1) (constPostcompOut (c `o` natId Inj1))
+  colimitFactorizer c =
+    colimitFactorizer (constPostcompOut (c `o` natId Inj1))
     |||
-    colimitFactorizer (l `o` natId Inj2) (constPostcompOut (c `o` natId Inj2))
+    colimitFactorizer (constPostcompOut (c `o` natId Inj2))
 
 
 -- | The coproduct of categories ':++:' is the binary coproduct in 'Cat'.
@@ -654,7 +669,7 @@
 instance Category k => HasLimits Unit k where
 
   limit (Nat f _ _) = Nat (Const (f % Unit)) f (\Unit -> f % Unit)
-  limitFactorizer Nat{} n = n ! Unit
+  limitFactorizer n = n ! Unit
 
 type instance LimitFam (i :>>: j) k f = f :% InitialObject (i :>>: j)
 
@@ -662,7 +677,7 @@
 instance (HasInitialObject (i :>>: j), Category i, Category 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
+  limitFactorizer n = n ! initialObject
 
 
 type instance ColimitFam Unit k f = f :% ()
@@ -671,7 +686,7 @@
 instance Category k => HasColimits Unit k where
 
   colimit (Nat f _ _) = Nat f (Const (f % Unit)) (\Unit -> f % Unit)
-  colimitFactorizer Nat{} n = n ! Unit
+  colimitFactorizer n = n ! Unit
 
 type instance ColimitFam (i :>>: j) k f = f :% TerminalObject (i :>>: j)
 
@@ -679,7 +694,7 @@
 instance (HasTerminalObject (i :>>: j), Category i, Category 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
+  colimitFactorizer n = n ! terminalObject
 
 
 data ForAll f = ForAll (forall a. Obj (->) a -> f :% a)
@@ -687,11 +702,11 @@
 
 instance HasLimits (->) (->) where
   limit (Nat f _ _) = Nat (Const (\x -> x)) f (\a (ForAll g) -> g a)
-  limitFactorizer Nat{} n = \z -> ForAll (\a -> (n ! a) z)
+  limitFactorizer n = \z -> ForAll (\a -> (n ! a) z)
 
 data Exists f = forall a. Exists (Obj (->) a) (f :% a)
 type instance ColimitFam (->) (->) f = Exists f
 
 instance HasColimits (->) (->) where
   colimit (Nat f _ _) = Nat f (Const (\x -> x)) Exists
-  colimitFactorizer Nat{} n = \(Exists a fa) -> (n ! a) fa
+  colimitFactorizer n = \(Exists a fa) -> (n ! a) fa
diff --git a/Data/Category/NNO.hs b/Data/Category/NNO.hs
--- a/Data/Category/NNO.hs
+++ b/Data/Category/NNO.hs
@@ -18,24 +18,24 @@
 
 
 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)
 
@@ -43,14 +43,14 @@
 -- type Nat = Fix ((:++:) Unit)
 
 -- instance HasNaturalNumberObject Cat where
-
---   type NaturalNumberObject Cat = Nat
-
+  
+--   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
 -- instance (Functor z, Functor s, Dom z ~ Unit, Cod z ~ Dom s, Dom s ~ Cod s) => Functor (PrimRec z s) where
 --   type Dom (PrimRec z s) = Nat
diff --git a/Data/Category/Yoneda.hs b/Data/Category/Yoneda.hs
--- a/Data/Category/Yoneda.hs
+++ b/Data/Category/Yoneda.hs
@@ -51,6 +51,6 @@
   M1 % n = n ! Op haskUnit
 
 haskIsTotal :: Adjunction (->) (Nat (Op (->)) (->)) M1 (YonedaEmbedding (->))
-haskIsTotal = mkAdjunction M1 YonedaEmbedding
-  (\(Nat f _ _) fu2b -> Nat f (Hom :.: (Swap :.: Tuple1 (\x -> x))) (\_ fz z -> fu2b ((f % Op (\() -> z)) fz)))
+haskIsTotal = mkAdjunctionUnit M1 YonedaEmbedding
+  (\(Nat f _ _) -> Nat f (Hom_X (f % Op haskUnit)) (\_ fz z -> (f % Op (\() -> z)) fz))
   (\_ n@(Nat f _ _) fu -> (n ! Op haskUnit) fu ())
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.8
+version:             0.8.1
 synopsis:            Category theory
 
 description:         Data-category is a collection of categories, and some categorical constructions on them.