diff --git a/Data/Category.hs b/Data/Category.hs
--- a/Data/Category.hs
+++ b/Data/Category.hs
@@ -43,7 +43,7 @@
   f . g = \x -> f (g x)
 
 
-data Op k a b = Op { unOp :: k b a }
+newtype Op k a b = Op { unOp :: k b a }
 
 -- | @Op k@ is opposite category of the category @k@.
 instance Category k => Category (Op k) where
diff --git a/Data/Category/CartesianClosed.hs b/Data/Category/CartesianClosed.hs
--- a/Data/Category/CartesianClosed.hs
+++ b/Data/Category/CartesianClosed.hs
@@ -27,6 +27,7 @@
 import Data.Category.Adjunction
 import Data.Category.Monoidal as M
 import Data.Category.Yoneda
+import qualified Data.Category.Unit as U
 
 
 -- | A category is cartesian closed if it has all products and exponentials for all objects.
@@ -48,6 +49,10 @@
   ExpFunctor % (Op y :**: z) = z ^^^ y
 
 
+flip :: CartesianClosed k => Obj k a -> Obj k b -> Obj k c -> k (Exponential k a (Exponential k b c)) (Exponential k b (Exponential k a c))
+flip a b c = flip a b c -- TODO
+
+
 -- | Exponentials in @Hask@ are functions.
 instance CartesianClosed (->) where
   type Exponential (->) y z = y -> z
@@ -56,6 +61,12 @@
   tuple _ _ z      = \y -> (z, y)
   f ^^^ h          = \g -> f . g . h
 
+
+instance CartesianClosed U.Unit where
+  type Exponential U.Unit () () = ()
+  apply U.Unit U.Unit = U.Unit
+  tuple U.Unit U.Unit = U.Unit
+  U.Unit ^^^ U.Unit = U.Unit
 
 
 -- | Exponentials in @Cat@ are the functor categories.
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, ScopedTypeVariables, NoImplicitPrelude #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, GADTs, FlexibleContexts, FlexibleInstances, ScopedTypeVariables, UndecidableInstances, NoImplicitPrelude #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Comma
@@ -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
 
 
@@ -53,7 +53,7 @@
                        . (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/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, NoImplicitPrelude #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving, TypeFamilies, TypeOperators, UndecidableInstances, GADTs, FlexibleContexts, NoImplicitPrelude #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Coproduct
@@ -96,27 +96,28 @@
   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
+data Cograph f :: * -> * -> * where
+  I1A :: Dom f ~ (Op c :**: d) => c a1 b1 -> Cograph f (I1 a1) (I1 b1)
+  I2A :: Dom f ~ (Op c :**: d) => d a2 b2 -> Cograph f (I2 a2) (I2 b2)
+  I12 :: Dom f ~ (Op c :**: d) => Obj c a -> Obj d b -> f -> f :% (a, b) -> Cograph f (I1 a) (I2 b)
+  
+-- | The cograph of the profunctor @f@.
+instance (Functor f, Dom f ~ (Op c :**: d), Cod f ~ (->), Category c, Category d) => Category (Cograph f) 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)
+  src (I1A a)       = I1A (src a)
+  src (I2A a)       = I2A (src a)
+  src (I12 a _ _ _) = I1A a
+  tgt (I1A a)       = I1A (tgt a)
+  tgt (I2A a)       = I2A (tgt a)
+  tgt (I12 _ b _ _) = I2A b
 
   (I1A a) . (I1A b) = I1A (a . b)
-  (I12 _ a) . (I1A b) = I12 (src b) a
-  (I2A a) . (I12 b _) = I12 b (tgt a)
+  (I12 _ b f ab) . (I1A a) = I12 (src a) b f ((f % (Op a :**: b)) ab)
+  (I2A b) . (I12 a _ f ab) = I12 a (tgt b) f ((f % (Op a :**: b)) ab)
   (I2A a) . (I2A b) = I2A (a . b)
 
-
+-- | The directed coproduct category of categories @c1@ and @c2@.
+newtype (c1 :>>: c2) a b = DC (Cograph (Const (Op c1 :**: c2) (->) ()) a b) deriving Category
 
 
 data NatAsFunctor f g = NatAsFunctor (Nat (Dom f) (Cod f) f g)
@@ -124,11 +125,11 @@
 -- | 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
   
-  type Dom (NatAsFunctor f g) = Dom f :**: (Unit :>>: Unit)
+  type Dom (NatAsFunctor f g) = Dom f :**: Cograph (Hom Unit)
   type Cod (NatAsFunctor f g) = Cod f
   type NatAsFunctor f g :% (a, I1 ()) = f :% a
   type NatAsFunctor f g :% (a, I2 ()) = g :% a
   
   NatAsFunctor (Nat f _ _) % (a :**: I1A Unit) = f % a
   NatAsFunctor (Nat _ g _) % (a :**: I2A Unit) = g % a
-  NatAsFunctor n           % (a :**: I12 Unit Unit) = n ! a
+  NatAsFunctor n           % (a :**: I12 Unit Unit Hom Unit) = n ! a
diff --git a/Data/Category/Enriched.hs b/Data/Category/Enriched.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/Enriched.hs
@@ -0,0 +1,404 @@
+{-# LANGUAGE
+    TypeOperators
+  , TypeFamilies
+  , GADTs
+  , RankNTypes
+  , FlexibleContexts
+  , NoImplicitPrelude
+  , UndecidableInstances
+  , ScopedTypeVariables
+  , ConstraintKinds
+  , AllowAmbiguousTypes
+  , TypeApplications
+  #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Category.Enriched
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  sjoerd@w3future.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+-----------------------------------------------------------------------------
+module Data.Category.Enriched where
+
+import Data.Category (Category(..), Obj, Op(..))
+import Data.Category.Product
+import Data.Category.Functor (Functor(..), Hom(..), (:*-:), homX_)
+import Data.Category.Limit hiding (HasLimits)
+import Data.Category.CartesianClosed
+import Data.Category.Boolean
+
+
+-- | An enriched category
+class CartesianClosed (V k) => ECategory (k :: * -> * -> *) where
+  -- | The tensor product of the category V which k is enriched in
+  type V k :: * -> * -> *
+
+  -- | The hom object in V from a to b
+  type k $ ab :: *
+  hom :: Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
+
+  id :: Obj k a -> Arr k a a
+  comp :: Obj k a -> Obj k b -> Obj k c -> V k (BinaryProduct (V k) (k $ (b, c)) (k $ (a, b))) (k $ (a, c))
+
+
+-- | The elements of @k@ as a functor from @V k@ to @(->)@ 
+type Elem k = TerminalObject (V k) :*-: (V k)
+elem :: CartesianClosed (V k) => Elem k
+elem = homX_ terminalObject
+
+-- | Arrows as elements of @k@
+type Arr k a b = Elem k :% (k $ (a, b))
+
+compArr :: ECategory k => Obj k a -> Obj k b -> Obj k c -> Arr k b c -> Arr k a b -> Arr k a c
+compArr a b c f g = comp a b c . (f &&& g)
+
+
+data Underlying k a b = Underlying (Obj k a) (Arr k a b) (Obj k b)
+-- | The underlying category of an enriched category
+instance ECategory k => Category (Underlying k) where
+  src (Underlying a _ _) = Underlying a (id a) a
+  tgt (Underlying _ _ b) = Underlying b (id b) b
+  Underlying b f c . Underlying a g _ = Underlying a (compArr a b c f g) c
+
+
+newtype EOp k a b = EOp (k b a)
+-- | The opposite of an enriched category
+instance ECategory k => ECategory (EOp k) where
+  type V (EOp k) = V k
+  type EOp k $ (a, b) = k $ (b, a)
+  hom (EOp a) (EOp b) = hom b a
+  id (EOp a) = id a
+  comp (EOp a) (EOp b) (EOp c) = comp c b a . (proj2 (hom c b) (hom b a) &&& proj1 (hom c b) (hom b a))
+
+
+data (:<>:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where
+  (:<>:) :: (V k1 ~ V k2) => Obj k1 a1 -> Obj k2 a2 -> (:<>:) k1 k2 (a1, a2) (a1, a2)
+  
+-- | The enriched product category of enriched categories @c1@ and @c2@.
+instance (ECategory k1, ECategory k2, V k1 ~ V k2) => ECategory (k1 :<>: k2) where
+  type V (k1 :<>: k2) = V k1
+  type (k1 :<>: k2) $ ((a1, a2), (b1, b2)) = BinaryProduct (V k1) (k1 $ (a1, b1)) (k2 $ (a2, b2))
+  hom (a1 :<>: a2) (b1 :<>: b2) = hom a1 b1 *** hom a2 b2
+  id (a1 :<>: a2) = id a1 &&& id a2
+  comp (a1 :<>: a2) (b1 :<>: b2) (c1 :<>: c2) = 
+    comp a1 b1 c1 . (proj1 bc1 bc2 . proj1 l r &&& proj1 ab1 ab2 . proj2 l r) &&& 
+    comp a2 b2 c2 . (proj2 bc1 bc2 . proj1 l r &&& proj2 ab1 ab2 . proj2 l r)
+    where 
+      ab1 = hom a1 b1
+      ab2 = hom a2 b2
+      bc1 = hom b1 c1
+      bc2 = hom b2 c2
+      l = bc1 *** bc2
+      r = ab1 *** ab2
+
+
+newtype Self v a b = Self { getSelf :: v a b }
+-- | Self enrichment
+instance CartesianClosed v => ECategory (Self v) where
+  type V (Self v) = v
+  type Self v $ (a, b) = Exponential v a b
+  hom (Self a) (Self b) = ExpFunctor % (Op a :**: b)
+  id (Self a) = toSelf a
+  comp (Self a) (Self b) (Self c) = curry (bc *** ab) a c (apply b c . (proj1 bc ab *** apply a b) . shuffle)
+    where
+      bc = c ^^^ b
+      ab = b ^^^ a
+      shuffle = proj1 (bc *** ab) a &&& (proj2 bc ab *** a)
+
+toSelf :: CartesianClosed v => v a b -> Arr (Self v) a b
+toSelf v = curry terminalObject (src v) (tgt v) (v . proj2 terminalObject (src v))
+
+fromSelf :: forall v a b. CartesianClosed v => Obj v a -> Obj v b -> Arr (Self v) a b -> v a b
+fromSelf a b arr = uncurry terminalObject a b arr . (terminate a &&& a)
+
+
+newtype InHask k a b = InHask (k a b)
+-- | Any regular category is enriched in (->), aka Hask
+instance Category k => ECategory (InHask k) where
+  type V (InHask k) = (->)
+  type InHask k $ (a, b) = k a b
+  hom (InHask a) (InHask b) = Hom % (Op a :**: b)
+  id (InHask f) () = f -- meh
+  comp _ _ _ (f, g) = f . g
+
+
+-- | Enriched functors.
+class (ECategory (EDom ftag), ECategory (ECod ftag), V (EDom ftag) ~ V (ECod ftag)) => EFunctor ftag where
+
+  -- | The domain, or source category, of the functor.
+  type EDom ftag :: * -> * -> *
+  -- | The codomain, or target category, of the functor.
+  type ECod ftag :: * -> * -> *
+
+  -- | @:%%@ maps objects at the type level
+  type ftag :%% a :: *
+
+  -- | @%%@ maps object at the value level
+  (%%) :: ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
+
+  -- | `map` maps arrows.
+  map :: (EDom ftag ~ k) => ftag -> Obj k a -> Obj k b -> V k (k $ (a, b)) (ECod ftag $ (ftag :%% a, ftag :%% b))
+
+type EFunctorOf a b t = (EFunctor t, EDom t ~ a, ECod t ~ b)
+
+
+data Id (k :: * -> * -> *) = Id
+-- | The identity functor on k
+instance ECategory k => EFunctor (Id k) where
+  type EDom (Id k) = k
+  type ECod (Id k) = k
+  type Id k :%% a = a
+  Id %% a = a
+  map Id = hom
+
+data (g :.: h) where
+  (:.:) :: (EFunctor g, EFunctor h, ECod h ~ EDom g) => g -> h -> g :.: h
+-- | The composition of two functors.
+instance (ECategory (ECod g), ECategory (EDom h), V (EDom h) ~ V (ECod g), ECod h ~ EDom g) => EFunctor (g :.: h) where
+  type EDom (g :.: h) = EDom h
+  type ECod (g :.: h) = ECod g
+  type (g :.: h) :%% a = g :%% (h :%% a)
+  (g :.: h) %% a = g %% (h %% a)
+  map (g :.: h) a b = map g (h %% a) (h %% b) . map h a b
+
+data Const (c1 :: * -> * -> *) (c2 :: * -> * -> *) x where
+  Const :: Obj c2 x -> Const c1 c2 x
+-- | The constant functor.
+instance (ECategory c1, ECategory c2, V c1 ~ V c2) => EFunctor (Const c1 c2 x) where
+  type EDom (Const c1 c2 x) = c1
+  type ECod (Const c1 c2 x) = c2
+  type Const c1 c2 x :%% a = x
+  Const x %% _ = x
+  map (Const x) a b = id x . terminate (hom a b)
+
+data Opposite f where
+  Opposite :: EFunctor f => f -> Opposite f
+-- | The dual of a functor
+instance (EFunctor f) => EFunctor (Opposite f) where
+  type EDom (Opposite f) = EOp (EDom f)
+  type ECod (Opposite f) = EOp (ECod f)
+  type Opposite f :%% a = f :%% a
+  Opposite f %% EOp a = EOp (f %% a)
+  map (Opposite f) (EOp a) (EOp b) = map f b a
+
+data f1 :<*>: f2 = f1 :<*>: f2
+-- | @f1 :<*>: f2@ is the product of the functors @f1@ and @f2@.
+instance (EFunctor f1, EFunctor f2, V (ECod f1) ~ V (ECod f2)) => EFunctor (f1 :<*>: f2) where
+  type EDom (f1 :<*>: f2) = EDom f1 :<>: EDom f2
+  type ECod (f1 :<*>: f2) = ECod f1 :<>: ECod f2
+  type (f1 :<*>: f2) :%% (a1, a2) = (f1 :%% a1, f2 :%% a2)
+  (f1 :<*>: f2) %% (a1 :<>: a2) = (f1 %% a1) :<>: (f2 %% a2)
+  map (f1 :<*>: f2) (a1 :<>: a2) (b1 :<>: b2) = map f1 a1 b1 *** map f2 a2 b2
+
+data DiagProd (k :: * -> * -> *) = DiagProd
+-- | 'DiagProd' is the diagonal functor for products.
+instance ECategory k => EFunctor (DiagProd k) where
+  type EDom (DiagProd k) = k
+  type ECod (DiagProd k) = k :<>: k
+  type DiagProd k :%% a = (a, a)
+  DiagProd %% a = a :<>: a
+  map DiagProd a b = hom a b &&& hom a b
+
+newtype UnderlyingF f = UnderlyingF f
+-- | The underlying functor of an enriched functor @f@
+instance EFunctor f => Functor (UnderlyingF f) where
+  type Dom (UnderlyingF f) = Underlying (EDom f)
+  type Cod (UnderlyingF f) = Underlying (ECod f)
+  type UnderlyingF f :% a = f :%% a
+  UnderlyingF f % Underlying a ab b = Underlying (f %% a) (map f a b . ab) (f %% b)
+  
+
+data EHom (k :: * -> * -> *) = EHom
+instance ECategory k => EFunctor (EHom k) where
+  type EDom (EHom k) = EOp k :<>: k
+  type ECod (EHom k) = Self (V k)
+  type EHom k :%% (a, b) = k $ (a, b)
+  EHom %% (EOp a :<>: b) = Self (hom a b)
+  map EHom (EOp a1 :<>: a2) (EOp b1 :<>: b2) = curry (ba *** ab) a b (comp b1 a1 b2 . (comp a1 a2 b2 . (proj2 ba ab *** a) &&& proj1 ba ab . proj1 (ba *** ab) a))
+    where
+      a = hom a1 a2
+      b = hom b1 b2
+      ba = hom b1 a1
+      ab = hom a2 b2
+
+
+-- | Enriched natural transformations.
+data ENat :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where
+  ENat :: (EFunctorOf c d f, EFunctorOf c d g)
+    => f -> g -> (forall z. Obj c z -> Arr d (f :%% z) (g :%% z)) -> ENat c d f g
+
+
+
+-- | The enriched functor @k(x, -)@
+data EHomX_ k x = EHomX_ (Obj k x)
+instance ECategory k => EFunctor (EHomX_ k x) where
+  type EDom (EHomX_ k x) = k
+  type ECod (EHomX_ k x) = Self (V k)
+  type EHomX_ k x :%% y = k $ (x, y)
+  EHomX_ x %% y = Self (hom x y)
+  map (EHomX_ x) a b = curry (hom a b) (hom x a) (hom x b) (comp x a b)
+
+-- | The enriched functor @k(-, x)@
+data EHom_X k x = EHom_X (Obj (EOp k) x)
+instance ECategory k => EFunctor (EHom_X k x) where
+  type EDom (EHom_X k x) = EOp k
+  type ECod (EHom_X k x) = Self (V k)
+  type EHom_X k x :%% y = k $ (y, x)
+  EHom_X x %% y = Self (hom x y)
+  map (EHom_X x) a b = curry (hom a b) (hom x a) (hom x b) (comp x a b)
+
+
+
+type VProfunctor k l t = EFunctorOf (EOp k :<>: l) (Self (V k)) t
+
+type family End (v :: * -> * -> *) t :: *
+class CartesianClosed v => HasEnds v where
+  end :: (VProfunctor k k t, V k ~ v) => t -> Obj v (End v t)
+  endCounit :: (VProfunctor k k t, V k ~ v) => t -> Obj k a -> v (End v t) (t :%% (a, a))
+  endFactorizer :: (VProfunctor k k t, V k ~ v) => t -> (forall a. Obj k a -> v x (t :%% (a, a))) -> v x (End v t)
+  
+
+newtype HaskEnd t = HaskEnd { getHaskEnd :: forall k a. VProfunctor k k t => t -> Obj k a -> t :%% (a, a) }
+type instance End (->) t = HaskEnd t
+instance HasEnds (->) where
+  end _ e = e
+  endCounit t a (HaskEnd e) = e t a
+  endFactorizer _ e x = HaskEnd (\_ a -> e a x)
+
+
+data FunCat a b t s where
+  FArr :: (EFunctorOf a b t, EFunctorOf a b s) => t -> s -> FunCat a b t s
+
+type t :->>: s = EHom (ECod t) :.: (Opposite t :<*>: s)
+(->>) :: (EFunctor t, EFunctor s, ECod t ~ ECod s, V (ECod t) ~ V (ECod s)) => t -> s -> t :->>: s
+t ->> s = EHom :.: (Opposite t :<*>: s)
+-- | The enriched functor category @[a, b]@
+instance (HasEnds (V a), V a ~ V b) => ECategory (FunCat a b) where
+  type V (FunCat a b) = V a
+  type FunCat a b $ (t, s) = End (V a) (t :->>: s)
+  hom (FArr t _) (FArr s _) = end (t ->> s)
+  id (FArr t _) = endFactorizer (t ->> t) (\a -> id (t %% a))
+  comp (FArr t _) (FArr s _) (FArr r _) = endFactorizer (t ->> r) 
+    (\a -> comp (t %% a) (s %% a) (r %% a) . (endCounit (s ->> r) a *** endCounit (t ->> s) a))
+
+
+data EndFunctor (k :: * -> * -> *) = EndFunctor
+instance (HasEnds (V k), ECategory k) => EFunctor (EndFunctor k) where
+  type EDom (EndFunctor k) = FunCat (EOp k :<>: k) (Self (V k))
+  type ECod (EndFunctor k) = Self (V k)
+  type EndFunctor k :%% t = End (V k) t
+  EndFunctor %% (FArr t _) = Self (end t)
+  map EndFunctor (FArr f _) (FArr g _) = curry (end (f ->> g)) (end f) (end g) (endFactorizer g (\a -> 
+    let aa = EOp a :<>: a in apply (getSelf (f %% aa)) (getSelf (g %% aa)) . (endCounit (f ->> g) aa *** endCounit f a)))
+    
+
+-- d :: j -> k, w :: j -> Self (V k)
+type family WeigtedLimit (k :: * -> * -> *) w d :: *
+type Lim w d = WeigtedLimit (ECod d) w d
+
+class HasEnds (V k) => HasLimits k where
+  limitObj :: (EFunctorOf j k d, EFunctorOf j (Self (V k)) w) => w -> d -> Obj k (Lim w d)
+  limit    :: (EFunctorOf j k d, EFunctorOf j (Self (V k)) w) => w -> d -> Obj k e -> V k (End (V k) (w :->>: (EHomX_ k e :.: d))) (k $ (e, Lim w d))
+  limitInv :: (EFunctorOf j k d, EFunctorOf j (Self (V k)) w) => w -> d -> Obj k e -> V k (k $ (e, Lim w d)) (End (V k) (w :->>: (EHomX_ k e :.: d)))
+
+-- d :: j -> k, w :: EOp j -> Self (V k)
+type family WeigtedColimit (k :: * -> * -> *) w d :: *
+type Colim w d = WeigtedColimit (ECod d) w d
+
+class HasEnds (V k) => HasColimits k where
+  colimitObj :: (EFunctorOf j k d, EFunctorOf (EOp j) (Self (V k)) w) => w -> d -> Obj k (Colim w d)
+  colimit    :: (EFunctorOf j k d, EFunctorOf (EOp j) (Self (V k)) w) => w -> d -> Obj k e -> V k (End (V k) (w :->>: (EHom_X k e :.: Opposite d))) (k $ (Colim w d, e))
+  colimitInv :: (EFunctorOf j k d, EFunctorOf (EOp j) (Self (V k)) w) => w -> d -> Obj k e -> V k (k $ (Colim w d, e)) (End (V k) (w :->>: (EHom_X k e :.: Opposite d)))
+  
+
+type instance WeigtedLimit (Self v) w d = End v (w :->>: d)
+instance HasEnds v => HasLimits (Self v) where
+  limitObj w d = Self (end (w ->> d))
+  limit w d (Self e) = let wed = w ->> (EHomX_ (Self e) :.: d) in curry (end wed) e (end (w ->> d)) 
+    (endFactorizer (w ->> d) (\a -> let { Self wa = w %% a; Self da = d %% a } in apply e (da ^^^ wa) . (flip wa e da . endCounit wed a *** e)))
+  limitInv w d (Self e) = let wed = w ->> (EHomX_ (Self e) :.: d) in endFactorizer wed 
+    (\a -> let { Self wa = w %% a; Self da = d %% a } in flip e wa da . (endCounit (w ->> d) a ^^^ e))
+
+
+
+yoneda    :: forall f k x. (HasEnds (V k), EFunctorOf k (Self (V k)) f) => f -> Obj k x -> V k (End (V k) (EHomX_ k x :->>: f)) (f :%% x)
+yoneda f x = apply (hom x x) (getSelf (f %% x)) . (endCounit (EHomX_ x ->> f) x &&& id x . terminate (end (EHomX_ x ->> f)))
+
+yonedaInv :: forall f k x. (HasEnds (V k), EFunctorOf k (Self (V k)) f) => f -> Obj k x -> V k (f :%% x) (End (V k) (EHomX_ k x :->>: f))
+yonedaInv f x = endFactorizer (EHomX_ x ->> f) h
+  where
+    h :: Obj k a -> V k (f :%% x) (Exponential (V k) (k $ (x, a)) (f :%% a))
+    h a = curry fx xa fa (apply fx fa . (map f x a . proj2 fx xa &&& proj1 fx xa))
+      where
+        xa = hom x a
+        Self fx = f %% x
+        Self fa = f %% a
+
+data Y (k :: * -> * -> *) = Y
+-- | Yoneda embedding
+instance (ECategory k, HasEnds (V k)) => EFunctor (Y k) where
+  type EDom (Y k) = EOp k
+  type ECod (Y k) = FunCat k (Self (V k))
+  type Y k :%% x = EHomX_ k x
+  Y %% EOp x = FArr (EHomX_ x) (EHomX_ x)
+  map Y (EOp a) (EOp b) = yonedaInv (EHomX_ b) a
+
+
+data One
+data Two
+data Three
+data PosetTest a b where
+  One :: PosetTest One One
+  Two :: PosetTest Two Two
+  Three :: PosetTest Three Three
+
+type family Poset3 a b where
+  Poset3 Two One = Fls
+  Poset3 Three One = Fls
+  Poset3 Three Two = Fls
+  Poset3 a b = Tru
+instance ECategory PosetTest where
+  type V PosetTest = Boolean
+  type PosetTest $ (a, b) = Poset3 a b
+  hom One One = Tru
+  hom One Two = Tru
+  hom One Three = Tru
+  hom Two One = Fls
+  hom Two Two = Tru
+  hom Two Three = Tru
+  hom Three One = Fls
+  hom Three Two = Fls
+  hom Three Three = Tru
+
+  id One = Tru
+  id Two = Tru
+  id Three = Tru
+  comp One One One = Tru
+  comp One One Two = Tru
+  comp One One Three = Tru
+  comp One Two One = F2T
+  comp One Two Two = Tru
+  comp One Two Three = Tru
+  comp One Three One = F2T
+  comp One Three Two = F2T
+  comp One Three Three = Tru
+  comp Two One One = Fls
+  comp Two One Two = F2T
+  comp Two One Three = F2T
+  comp Two Two One = Fls
+  comp Two Two Two = Tru
+  comp Two Two Three = Tru
+  comp Two Three One = Fls
+  comp Two Three Two = F2T
+  comp Two Three Three = Tru
+  comp Three One One = Fls
+  comp Three One Two = Fls
+  comp Three One Three = F2T
+  comp Three Two One = Fls
+  comp Three Two Two = Fls
+  comp Three Two Three = F2T
+  comp Three Three One = Fls
+  comp Three Three Two = Fls
+  comp Three Three Three = Tru
diff --git a/Data/Category/Fix.hs b/Data/Category/Fix.hs
--- a/Data/Category/Fix.hs
+++ b/Data/Category/Fix.hs
@@ -1,7 +1,7 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, UndecidableInstances, NoImplicitPrelude #-}
+{-# LANGUAGE FlexibleInstances, GeneralizedNewtypeDeriving, StandaloneDeriving, PatternSynonyms, TypeOperators, TypeFamilies, UndecidableInstances, NoImplicitPrelude #-}
 -----------------------------------------------------------------------------
 -- |
--- Module      :  Data.Category.AddObject
+-- Module      :  Data.Category.Fix
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  sjoerd@w3future.com
@@ -14,60 +14,70 @@
 import Data.Category.Functor
 import Data.Category.Limit
 import Data.Category.CartesianClosed
+import Data.Category.Monoidal
 
-import Data.Category.Unit
+import qualified Data.Category.Unit as U
 import Data.Category.Coproduct
 
 
-newtype Fix f a b = Fix (f (Fix f) a b)
+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)
+deriving instance Category (f (Fix f)) => Category (Fix f)
 
 -- | @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)
+deriving instance HasInitialObject (f (Fix f)) => HasInitialObject (Fix f)
 
 -- | @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)
+deriving instance HasTerminalObject (f (Fix f)) => HasTerminalObject (Fix f)
 
 -- | @Fix f@ inherits its (co)limits from @f (Fix f)@.
-instance HasBinaryProducts (f (Fix f)) => HasBinaryProducts (Fix f) where
-  type BinaryProduct (Fix f) a b = BinaryProduct (f (Fix f)) a b
-  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)
+deriving instance HasBinaryProducts (f (Fix f)) => HasBinaryProducts (Fix f)
   
 -- | @Fix f@ inherits its (co)limits from @f (Fix f)@.
-instance HasBinaryCoproducts (f (Fix f)) => HasBinaryCoproducts (Fix f) where
-  type BinaryCoproduct (Fix f) a b = BinaryCoproduct (f (Fix f)) a b
-  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)
+deriving instance HasBinaryCoproducts (f (Fix f)) => HasBinaryCoproducts (Fix f)
 
 -- | @Fix f@ inherits its exponentials from @f (Fix f)@.
-instance CartesianClosed (f (Fix f)) => CartesianClosed (Fix f) where
-  type Exponential (Fix f) a b = Exponential (f (Fix f)) a b
-  apply (Fix a) (Fix b) = Fix (apply a b)
-  tuple (Fix a) (Fix b) = Fix (tuple a b)
-  Fix a ^^^ Fix b = Fix (a ^^^ b)
+deriving instance CartesianClosed (f (Fix f)) => CartesianClosed (Fix f)
   
-data Wrap (f :: (* -> * -> *) -> * -> * -> *) = Wrap
+data Wrap (f :: * -> * -> *) = Wrap
 -- | The `Wrap` functor wraps `Fix` around @f (Fix f)@.
-instance Category (f (Fix f)) => Functor (Wrap f) where
-  type Dom (Wrap f) = f (Fix f)
-  type Cod (Wrap f) = Fix f
-  type Wrap f :% a = a
+instance Category (f (Fix f)) => Functor (Wrap (Fix f)) where
+  type Dom (Wrap (Fix f)) = f (Fix f)
+  type Cod (Wrap (Fix f)) = Fix f
+  type Wrap (Fix f) :% a = a
   Wrap % f = Fix f
 
+data Unwrap (f :: * -> * -> *) = Unwrap
+-- | The `Unwrap` functor unwraps @Fix f@ to @f (Fix f)@.
+instance Category (f (Fix f)) => Functor (Unwrap (Fix f)) where
+  type Dom (Unwrap (Fix f)) = Fix f
+  type Cod (Unwrap (Fix f)) = f (Fix f)
+  type Unwrap (Fix f) :% a = a
+  Unwrap % Fix f = f
+
+type WrapTensor f t = Wrap f :.: t :.: (Unwrap f :***: Unwrap f)
+-- | @Fix f@ inherits tensor products from @f (Fix f)@.
+instance (TensorProduct t, Cod t ~ f (Fix f)) => TensorProduct (WrapTensor (Fix f) t) where
+  type Unit (WrapTensor (Fix f) t) = Unit t
+  unitObject (_ :.: t :.: _) = Fix (unitObject t)
+  
+  leftUnitor (_ :.: t :.: _) (Fix a) = Fix (leftUnitor t a)
+  leftUnitorInv (_ :.: t :.: _) (Fix a) = Fix (leftUnitorInv t a)
+  rightUnitor (_ :.: t :.: _) (Fix a) = Fix (rightUnitor t a)
+  rightUnitorInv (_ :.: t :.: _) (Fix a) = Fix (rightUnitorInv t a)
+  associator (_ :.: t :.: _) (Fix a) (Fix b) (Fix c) = Fix (associator t a b c)
+  associatorInv (_ :.: t :.: _) (Fix a) (Fix b) (Fix c) = Fix (associatorInv t a b c)
+
 -- | 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)
+type Omega = Fix ((:>>:) U.Unit)
+
+type Z = I1 ()
+type S n = I2 n
+pattern Z :: Obj Omega Z
+pattern Z = Fix (DC (I1A U.Unit))
+pattern S :: Omega a b -> Omega (S a) (S b)
+pattern S n = Fix (DC (I2A n))
+z2s :: Obj Omega n -> Omega Z (S n)
+z2s n = Fix (DC (I12 U.Unit n (Const (\() -> ())) ()))
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, NoImplicitPrelude #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, FlexibleContexts, FlexibleInstances, UndecidableInstances, GADTs, RankNTypes, ConstraintKinds, NoImplicitPrelude #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Functor
@@ -16,6 +16,7 @@
 
   -- * Functors
   , Functor(..)
+  , FunctorOf
 
   -- ** Functor instances
   , Id(..)
@@ -66,7 +67,7 @@
   -- | @%@ maps arrows.
   (%)  :: ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
 
-
+type FunctorOf a b t = (Functor t, Dom t ~ a, Cod t ~ b)
 
 
 -- | Functors are arrows in the category Cat.
diff --git a/Data/Category/Limit.hs b/Data/Category/Limit.hs
--- a/Data/Category/Limit.hs
+++ b/Data/Category/Limit.hs
@@ -128,7 +128,7 @@
   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 k) f -> (forall n. Cone f n -> k n (Limit f))
+  limitFactorizer :: Obj (Nat j k) f -> Cone f n -> k n (Limit f)
 
 data LimitFunctor (j :: * -> * -> *) (k  :: * -> * -> *) = LimitFunctor
 -- | If every diagram of type @j@ has a limit in @k@ there exists a limit functor.
@@ -181,7 +181,7 @@
   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 k) f -> (forall n. Cocone f n -> k (Colimit f) n)
+  colimitFactorizer :: Obj (Nat j k) f -> Cocone f n -> k (Colimit f) n
 
 data ColimitFunctor (j :: * -> * -> *) (k  :: * -> * -> *) = ColimitFunctor
 -- | If every diagram of type @j@ has a colimit in @k@ there exists a colimit functor.
@@ -277,10 +277,10 @@
 instance (Category c1, HasTerminalObject c2) => HasTerminalObject (c1 :>>: c2) where
   type TerminalObject (c1 :>>: c2) = I2 (TerminalObject c2)
 
-  terminalObject = I2A terminalObject
+  terminalObject = DC (I2A terminalObject)
 
-  terminate (I1A a) = I12 a terminalObject
-  terminate (I2A a) = I2A (terminate a)
+  terminate (DC (I1A a)) = DC (I12 a terminalObject (Const (\() -> ())) ())
+  terminate (DC (I2A a)) = DC (I2A (terminate a))
 
 
 
@@ -347,10 +347,10 @@
 instance (HasInitialObject c1, Category c2) => HasInitialObject (c1 :>>: c2) where
   type InitialObject (c1 :>>: c2) = I1 (InitialObject c1)
 
-  initialObject = I1A initialObject
+  initialObject = DC (I1A initialObject)
 
-  initialize (I1A a) = I1A (initialize a)
-  initialize (I2A a) = I12 initialObject a
+  initialize (DC (I1A a)) = DC (I1A (initialize a))
+  initialize (DC (I2A a)) = DC (I12 initialObject a (Const (\() -> ())) ())
 
 
 class Category k => HasBinaryProducts k where
@@ -437,21 +437,21 @@
   type BinaryProduct (c1 :>>: c2) (I2 a) (I1 b) = I1 b
   type BinaryProduct (c1 :>>: c2) (I2 a) (I2 b) = I2 (BinaryProduct c2 a b)
 
-  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)
+  proj1 (DC (I1A a)) (DC (I1A b)) = DC (I1A (proj1 a b))
+  proj1 (DC (I1A a)) (DC (I2A _)) = DC (I1A a)
+  proj1 (DC (I2A a)) (DC (I1A b)) = DC (I12 b a (Const (\() -> ())) ())
+  proj1 (DC (I2A a)) (DC (I2A b)) = DC (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)
+  proj2 (DC (I1A a)) (DC (I1A b)) = DC (I1A (proj2 a b))
+  proj2 (DC (I1A a)) (DC (I2A b)) = DC (I12 a b (Const (\() -> ())) ())
+  proj2 (DC (I2A _)) (DC (I1A b)) = DC (I1A b)
+  proj2 (DC (I2A a)) (DC (I2A b)) = DC (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)
-  I12 a b1 &&& I12 _ b2 = I12 a (b1 *** b2)
+  DC (I1A a) &&& DC (I1A b) = DC (I1A (a &&& b))
+  DC (I1A a) &&& DC (I12 _ _ _ _) = DC (I1A a)
+  DC (I12 _ _ _ _) &&& DC (I1A b) = DC (I1A b)
+  DC (I2A a) &&& DC (I2A b) = DC (I2A (a &&& b))
+  DC (I12 a b1 _ _) &&& DC (I12 _ b2 _ _) = DC (I12 a (b1 *** b2) (Const (\() -> ())) ())
 
 
 data ProductFunctor (k :: * -> * -> *) = ProductFunctor
@@ -563,21 +563,21 @@
   type BinaryCoproduct (c1 :>>: c2) (I2 a) (I1 b) = I2 a
   type BinaryCoproduct (c1 :>>: c2) (I2 a) (I2 b) = I2 (BinaryCoproduct c2 a b)
 
-  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)
+  inj1 (DC (I1A a)) (DC (I1A b)) = DC (I1A (inj1 a b))
+  inj1 (DC (I1A a)) (DC (I2A b)) = DC (I12 a b (Const (\() -> ())) ())
+  inj1 (DC (I2A a)) (DC (I1A _)) = DC (I2A a)
+  inj1 (DC (I2A a)) (DC (I2A b)) = DC (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)
+  inj2 (DC (I1A a)) (DC (I1A b)) = DC (I1A (inj2 a b))
+  inj2 (DC (I1A _)) (DC (I2A b)) = DC (I2A b)
+  inj2 (DC (I2A a)) (DC (I1A b)) = DC (I12 b a (Const (\() -> ())) ())
+  inj2 (DC (I2A a)) (DC (I2A b)) = DC (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)
-  I12 a1 b ||| I12 a2 _ = I12 (a1 +++ a2) b
+  DC (I1A a) ||| DC (I1A b) = DC (I1A (a ||| b))
+  DC (I2A a) ||| DC (I12 _ _ _ _) = DC (I2A a)
+  DC (I12 _ _ _ _) ||| DC (I2A b) = DC (I2A b)
+  DC (I2A a) ||| DC (I2A b) = DC (I2A (a ||| b))
+  DC (I12 a1 b _ _) ||| DC (I12 a2 _ _ _) = DC (I12 (a1 +++ a2) b (Const (\() -> ())) ())
 
 
 data CoproductFunctor (k :: * -> * -> *) = CoproductFunctor
diff --git a/Data/Category/Monoidal.hs b/Data/Category/Monoidal.hs
--- a/Data/Category/Monoidal.hs
+++ b/Data/Category/Monoidal.hs
@@ -42,6 +42,8 @@
   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))
 
+class TensorProduct f => SymmetricTensorProduct f where
+  swap :: Cod f ~ k => f -> Obj k a -> Obj k b -> k (f :% (a, b)) (f :% (b, a))
 
 -- | If a category has all products, then the product functor makes it a monoidal category,
 --   with the terminal object as unit.
@@ -58,6 +60,9 @@
   associator    _ a b c = (proj1 a b . proj1 (a *** b) c) &&& (proj2 a b *** c)
   associatorInv _ a b c = (a *** proj1 b c) &&& (proj2 b c . proj2 a (b *** c))
 
+instance (HasTerminalObject k, HasBinaryProducts k) => SymmetricTensorProduct (ProductFunctor k) where
+  swap _ a b = proj2 a b &&& proj1 a b
+
 -- | If a category has all coproducts, then the coproduct functor makes it a monoidal category,
 --   with the initial object as unit.
 instance (HasInitialObject k, HasBinaryCoproducts k) => TensorProduct (CoproductFunctor k) where
@@ -72,6 +77,9 @@
 
   associator    _ a b c = (a +++ inj1 b c) ||| (inj2 a (b +++ c) . inj2 b c)
   associatorInv _ a b c = (inj1 (a +++ b) c . inj1 a b) ||| (inj2 a b +++ c)
+
+instance (HasInitialObject k, HasBinaryCoproducts k) => SymmetricTensorProduct (CoproductFunctor k) where
+  swap _ a b = inj2 b a ||| inj1 b a
 
 -- | Functor composition makes the category of endofunctors monoidal, with the identity functor as unit.
 instance Category k => TensorProduct (EndoFunctorCompose k) where
diff --git a/Data/Category/NNO.hs b/Data/Category/NNO.hs
--- a/Data/Category/NNO.hs
+++ b/Data/Category/NNO.hs
@@ -14,43 +14,43 @@
 import Data.Category.Limit
 import Data.Category.Unit
 import Data.Category.Coproduct
-import Data.Category.Fix
+import Data.Category.Fix (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)
-  
+-- 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
 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/Product.hs b/Data/Category/Product.hs
--- a/Data/Category/Product.hs
+++ b/Data/Category/Product.hs
@@ -16,7 +16,7 @@
 data (:**:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where
   (:**:) :: c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
 
--- | The product category of category @c1@ and @c2@.
+-- | The product category of categories @c1@ and @c2@.
 instance (Category c1, Category c2) => Category (c1 :**: c2) where
   
   src (a1 :**: a2)            = src a1 :**: src a2
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.7
+version:             0.7.1
 synopsis:            Category theory
 
 description:         Data-category is a collection of categories, and some categorical constructions on them.
@@ -40,6 +40,7 @@
     Data.Category.Limit,
     Data.Category.Monoidal,
     Data.Category.CartesianClosed,
+    Data.Category.Enriched,
     Data.Category.Yoneda,
     Data.Category.Boolean,
     Data.Category.Fix,