diff --git a/Data/Category.hs b/Data/Category.hs
--- a/Data/Category.hs
+++ b/Data/Category.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies, GADTs, RankNTypes, PolyKinds, NoImplicitPrelude #-}
+{-# LANGUAGE TypeFamilies, GADTs, RankNTypes, PolyKinds, LinearTypes, FlexibleInstances, NoImplicitPrelude #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category
@@ -18,10 +18,15 @@
   -- * Opposite category
   , Op(..)
 
+  -- * `(->)`/Hask
+  , obj
+
 ) where
 
-infixr 8 .
+import GHC.Exts
+import Data.Kind (Type)
 
+infixr 8 .
 
 -- | Whenever objects are required at value level, they are represented by their identity arrows.
 type Obj k a = k a a
@@ -35,12 +40,16 @@
   (.) :: k b c -> k a b -> k a c
 
 
--- | The category with Haskell types as objects and Haskell functions as arrows.
-instance Category (->) where
+obj :: Obj (FUN m) a
+obj x = x
 
-  src _ = \x -> x
-  tgt _ = \x -> x
+-- | For @m ~ Many@: The category with Haskell types as objects and Haskell functions as arrows, i.e. @(->)@.
+-- For @m ~ One@: The category with Haskell types as objects and Haskell linear functions as arrows, i.e. @(%1->)@.
+instance Category (FUN m) where
 
+  src _ = obj
+  tgt _ = obj
+
   f . g = \x -> f (g x)
 
 
@@ -56,5 +65,5 @@
 
 
 -- | @Kind k@ is the kind of the objects of the category @k@.
-type family Kind (k :: o -> o -> *) :: * where
-  Kind (k :: o -> o -> *) = o
+type family Kind (k :: o -> o -> Type) :: Type where
+  Kind (k :: o -> o -> Type) = o
diff --git a/Data/Category/Adjunction.hs b/Data/Category/Adjunction.hs
--- a/Data/Category/Adjunction.hs
+++ b/Data/Category/Adjunction.hs
@@ -104,8 +104,8 @@
 -- | The category with categories as objects and adjunctions as arrows.
 instance Category AdjArrow where
 
-  src (AdjArrow (Adjunction _ _ _ _)) = AdjArrow idAdj
-  tgt (AdjArrow (Adjunction _ _ _ _)) = AdjArrow idAdj
+  src (AdjArrow Adjunction{}) = AdjArrow idAdj
+  tgt (AdjArrow Adjunction{}) = AdjArrow idAdj
 
   AdjArrow x . AdjArrow y = AdjArrow (composeAdj x y)
 
@@ -127,7 +127,7 @@
 
 contAdj :: Adjunction (Op (->)) (->) (Opposite ((->) :-*: r) :.: OpOpInv (->)) ((->) :-*: r)
 contAdj = mkAdjunction
-  (Opposite (Hom_X (\x -> x)) :.: OpOpInv)
-  (Hom_X (\x -> x))
+  (Opposite (Hom_X obj) :.: OpOpInv)
+  (Hom_X obj)
   (\_ -> \(Op f) -> \b a -> f a b)
   (\_ -> \f -> Op (\b a -> f a b))
diff --git a/Data/Category/Boolean.hs b/Data/Category/Boolean.hs
--- a/Data/Category/Boolean.hs
+++ b/Data/Category/Boolean.hs
@@ -14,6 +14,8 @@
 -----------------------------------------------------------------------------
 module Data.Category.Boolean where
 
+import Data.Kind (Type)
+
 import Data.Category
 import Data.Category.Limit
 import Data.Category.Monoidal
@@ -160,7 +162,7 @@
 falseProductComonoid = ComonoidObject F2T Fls
 
 
-data Arrow k a b = Arrow (k a b)
+newtype Arrow k a b = Arrow (k a b)
 -- | Any functor from the Boolean category points to an arrow in its target category.
 instance Category k => Functor (Arrow k a b) where
   type Dom (Arrow k a b) = Boolean
@@ -191,7 +193,7 @@
 type TgtFunctor = ColimitFunctor Boolean
 
 
-data Terminator (k :: * -> * -> *) = Terminator
+data Terminator (k :: Type -> Type -> Type) = Terminator
 -- | @Terminator k@ is the functor that sends an object to its terminating arrow.
 instance HasTerminalObject k => Functor (Terminator k) where
   type Dom (Terminator k) = k
@@ -206,7 +208,7 @@
   (\_ n -> n ! Fls)
 
 
-data Initializer (k :: * -> * -> *) = Initializer
+data Initializer (k :: Type -> Type -> Type) = Initializer
 -- | @Initializer k@ is the functor that sends an object to its initializing arrow.
 instance HasInitialObject k => Functor (Initializer k) where
   type Dom (Initializer k) = k
diff --git a/Data/Category/CartesianClosed.hs b/Data/Category/CartesianClosed.hs
--- a/Data/Category/CartesianClosed.hs
+++ b/Data/Category/CartesianClosed.hs
@@ -10,6 +10,7 @@
   UndecidableInstances,
   TypeSynonymInstances,
   FlexibleInstances,
+  TupleSections,
   NoImplicitPrelude #-}
 -----------------------------------------------------------------------------
 -- |
@@ -22,6 +23,8 @@
 -----------------------------------------------------------------------------
 module Data.Category.CartesianClosed where
 
+import Data.Kind (Type)
+
 import Data.Category
 import Data.Category.Functor
 import Data.Category.NaturalTransformation
@@ -42,7 +45,7 @@
   (^^^) :: k z1 z2 -> k y2 y1 -> k (Exponential k y1 z1) (Exponential k y2 z2)
 
 
-data ExpFunctor (k :: * -> * -> *) = ExpFunctor
+data ExpFunctor (k :: Type -> Type -> Type) = ExpFunctor
 -- | The exponential as a bifunctor.
 instance CartesianClosed k => Functor (ExpFunctor k) where
   type Dom (ExpFunctor k) = Op k :**: k
@@ -61,7 +64,7 @@
   type Exponential (->) y z = y -> z
 
   apply _ _ (f, y) = f y
-  tuple _ _ z      = \y -> (z, y)
+  tuple _ _ z      = (z,)
   f ^^^ h          = \g -> f . g . h
 
 
@@ -94,7 +97,7 @@
   type Exponential (Presheaves k) y z = PShExponential k y z
 
   apply yn@(Nat y _ _) zn@(Nat z _ _) = Nat (PshExponential yn zn :*: y) z (\(Op i) (n, yi) -> (n ! Op i) (i, yi))
-  tuple yn zn@(Nat z _ _) = Nat z (PshExponential yn (zn *** yn)) (\(Op i) zi -> (Nat (Hom_X i) z (\_ j2i -> (z % Op j2i) zi) *** yn))
+  tuple yn zn@(Nat z _ _) = Nat z (PshExponential yn (zn *** yn)) (\(Op i) zi -> Nat (Hom_X i) z (\_ j2i -> (z % Op j2i) zi) *** yn)
   zn ^^^ yn = Nat (PshExponential (tgt yn) (src zn)) (PshExponential (src yn) (tgt zn)) (\(Op i) n -> zn . n . (natId (Hom_X i) *** yn))
 
 
@@ -109,26 +112,26 @@
 
 -- | From the adjunction between the product functor and the exponential functor we get the curry and uncurry functions,
 --   generalized to any cartesian closed category.
-curry :: (CartesianClosed k, Kind k ~ *) => Obj k x -> Obj k y -> Obj k z -> k (BinaryProduct k x y) z -> k x (Exponential k y z)
+curry :: (CartesianClosed k, Kind k ~ Type) => Obj k x -> Obj k y -> Obj k z -> k (BinaryProduct k x y) z -> k x (Exponential k y z)
 curry x y _ = leftAdjunct (curryAdj y) x
 
-uncurry :: (CartesianClosed k, Kind k ~ *) => Obj k x -> Obj k y -> Obj k z -> k x (Exponential k y z) -> k (BinaryProduct k x y) z
+uncurry :: (CartesianClosed k, Kind k ~ Type) => Obj k x -> Obj k y -> Obj k z -> k x (Exponential k y z) -> k (BinaryProduct k x y) z
 uncurry _ y z = rightAdjunct (curryAdj y) z
 
 -- | From every adjunction we get a monad, in this case the State monad.
 type State k s a = Exponential k s (BinaryProduct k a s)
 
-stateMonadReturn :: (CartesianClosed k, Kind k ~ *) => Obj k s -> Obj k a -> k a (State k s a)
+stateMonadReturn :: (CartesianClosed k, Kind k ~ Type) => Obj k s -> Obj k a -> k a (State k s a)
 stateMonadReturn s a = M.unit (adjunctionMonad (curryAdj s)) ! a
 
-stateMonadJoin :: (CartesianClosed k, Kind k ~ *) => Obj k s -> Obj k a -> k (State k s (State k s a)) (State k s a)
+stateMonadJoin :: (CartesianClosed k, Kind k ~ Type) => Obj k s -> Obj k a -> k (State k s (State k s a)) (State k s a)
 stateMonadJoin s a = M.multiply (adjunctionMonad (curryAdj s)) ! a
 
 -- ! From every adjunction we also get a comonad, the Context comonad in this case.
 type Context k s a = BinaryProduct k (Exponential k s a) s
 
-contextComonadExtract :: (CartesianClosed k, Kind k ~ *) => Obj k s -> Obj k a -> k (Context k s a) a
+contextComonadExtract :: (CartesianClosed k, Kind k ~ Type) => Obj k s -> Obj k a -> k (Context k s a) a
 contextComonadExtract s a = M.counit (adjunctionComonad (curryAdj s)) ! a
 
-contextComonadDuplicate :: (CartesianClosed k, Kind k ~ *) => Obj k s -> Obj k a -> k (Context k s a) (Context k s (Context k s a))
+contextComonadDuplicate :: (CartesianClosed k, Kind k ~ Type) => Obj k s -> Obj k a -> k (Context k s a) (Context k s (Context k s a))
 contextComonadDuplicate s a = M.comultiply (adjunctionComonad (curryAdj s)) ! a
diff --git a/Data/Category/Comma.hs b/Data/Category/Comma.hs
--- a/Data/Category/Comma.hs
+++ b/Data/Category/Comma.hs
@@ -12,17 +12,20 @@
 -----------------------------------------------------------------------------
 module Data.Category.Comma where
 
+import Data.Kind (Type)
+
 import Data.Category
+import Data.Category.Adjunction
 import Data.Category.Functor
 import Data.Category.Limit
 import Data.Category.RepresentableFunctor
 
 
-data CommaO :: * -> * -> * -> * where
+data CommaO :: Type -> Type -> Type -> Type 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
+data (:/\:) :: Type -> Type -> Type -> Type -> Type where
   CommaA ::
     CommaO t s (a, b) ->
     Dom t a a' ->
@@ -48,9 +51,7 @@
 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
@@ -59,7 +60,7 @@
     initialUniversal u a mor factorizer
       where
         factorizer :: forall y. Obj (Dom u) y -> Cod u x (u :% y) -> Dom u a y
-        factorizer y arr = case (init (commaId (CommaO y arr y))) of CommaA _ _ f _ -> f
+        factorizer y arr = case init (commaId (CommaO y arr y)) of CommaA _ _ f _ -> f
           where
             init :: Obj c (y, y) -> c (a_, a) (y, y)
             init = initialize
@@ -72,7 +73,43 @@
     terminalUniversal u a mor factorizer
       where
         factorizer :: forall y. Obj (Dom u) y -> Cod u (u :% y) x -> Dom u y a
-        factorizer y arr = case (term (commaId (CommaO y arr y))) of CommaA _ f _ _ -> f
+        factorizer y arr = case term (commaId (CommaO y arr y)) of CommaA _ f _ _ -> f
           where
             term :: Obj c (y, y) -> c (y, y) (a, a_)
             term = terminate
+
+
+type Arrows k = Id k :/\: Id k
+
+data IdArrow (k :: Type -> Type -> Type) = IdArrow
+instance Category k => Functor (IdArrow k) where
+  type Dom (IdArrow k) = k
+  type Cod (IdArrow k) = Arrows k
+  type IdArrow k :% a = (a, a)
+  IdArrow % f = CommaA
+    (CommaO (src f) (src f) (src f))
+    f
+    f
+    (CommaO (tgt f) (tgt f) (tgt f))
+
+data Src (k :: Type -> Type -> Type) = Src
+instance Category k => Functor (Src k) where
+  type Dom (Src k) = Arrows k
+  type Cod (Src k) = k
+  type Src k :% (a, b) = a
+  Src % (CommaA _ aa' _ _) = aa'
+
+data Tgt (k :: Type -> Type -> Type) = Tgt
+instance Category k => Functor (Tgt k) where
+  type Dom (Tgt k) = Arrows k
+  type Cod (Tgt k) = k
+  type Tgt k :% (a, b) = b
+  Tgt % (CommaA _ _ bb' _) = bb'
+
+-- | Taking the target of an arrow is left adjoint to taking the identity of an object
+tgtIdAdj :: Category k => Adjunction k (Arrows k) (Tgt k) (IdArrow k)
+tgtIdAdj = mkAdjunctionUnits Tgt IdArrow (\(CommaA o@(CommaO _ ab b) _ _ _) -> CommaA o ab b (CommaO b b b)) (\o -> o)
+
+-- | Taking the source of an arrow is right adjoint to taking the identity of an object
+idSrcAdj :: Category k => Adjunction (Arrows k) k (IdArrow k) (Src k)
+idSrcAdj = mkAdjunctionUnits IdArrow Src (\o -> o) (\(CommaA o@(CommaO a ab _) _ _ _) -> CommaA (CommaO a a a) a ab o)
diff --git a/Data/Category/Coproduct.hs b/Data/Category/Coproduct.hs
--- a/Data/Category/Coproduct.hs
+++ b/Data/Category/Coproduct.hs
@@ -10,6 +10,8 @@
 -----------------------------------------------------------------------------
 module Data.Category.Coproduct where
 
+import Data.Kind (Type)
+
 import Data.Category
 import Data.Category.Functor
 
@@ -21,13 +23,13 @@
 data I1 a
 data I2 a
 
-data (:++:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where
+data (:++:) :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type where
   I1 :: c1 a1 b1 -> (:++:) c1 c2 (I1 a1) (I1 b1)
   I2 :: c2 a2 b2 -> (:++:) c1 c2 (I2 a2) (I2 b2)
 
 -- | The coproduct category of categories @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)
@@ -36,10 +38,10 @@
   (I1 a) . (I1 b) = I1 (a . b)
   (I2 a) . (I2 b) = I2 (a . b)
 
-  
-  
-    
-data Inj1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Inj1
+
+
+
+data Inj1 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) = Inj1
 -- | 'Inj1' is a functor which injects into the left category.
 instance (Category c1, Category c2) => Functor (Inj1 c1 c2) where
   type Dom (Inj1 c1 c2) = c1
@@ -47,7 +49,7 @@
   type Inj1 c1 c2 :% a = I1 a
   Inj1 % f = I1 f
 
-data Inj2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Inj2
+data Inj2 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) = Inj2
 -- | 'Inj2' is a functor which injects into the right category.
 instance (Category c1, Category c2) => Functor (Inj2 c1 c2) where
   type Dom (Inj2 c1 c2) = c2
@@ -64,8 +66,8 @@
   type (f1 :+++: f2) :% (I2 a) = I2 (f2 :% a)
   (g :+++: _) % I1 f = I1 (g % f)
   (_ :+++: g) % I2 f = I2 (g % f)
-  
-data CodiagCoprod (k :: * -> * -> *) = CodiagCoprod
+
+data CodiagCoprod (k :: Type -> Type -> Type) = CodiagCoprod
 -- | 'CodiagCoprod' is the codiagonal functor for coproducts.
 instance Category k => Functor (CodiagCoprod k) where
   type Dom (CodiagCoprod k) = k :++: k
@@ -75,7 +77,7 @@
   CodiagCoprod % I1 f = f
   CodiagCoprod % I2 f = f
 
-data Cotuple1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Cotuple1 (Obj c1 a)
+newtype Cotuple1 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) a = Cotuple1 (Obj c1 a)
 -- | 'Cotuple1' projects out to the left category, replacing a value from the right category with a fixed object.
 instance (Category c1, Category c2) => Functor (Cotuple1 c1 c2 a1) where
   type Dom (Cotuple1 c1 c2 a1) = c1 :++: c2
@@ -85,7 +87,7 @@
   Cotuple1 _ % I1 f = f
   Cotuple1 a % I2 _ = a
 
-data Cotuple2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Cotuple2 (Obj c2 a)
+newtype Cotuple2 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) a = Cotuple2 (Obj c2 a)
 -- | 'Cotuple2' projects out to the right category, replacing a value from the left category with a fixed object.
 instance (Category c1, Category c2) => Functor (Cotuple2 c1 c2 a2) where
   type Dom (Cotuple2 c1 c2 a2) = c1 :++: c2
@@ -96,13 +98,13 @@
   Cotuple2 _ % I2 f = f
 
 
-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)
-  
+data Cograph c d f :: Type -> Type -> Type where
+  I1A :: c a1 b1 -> Cograph c d f (I1 a1) (I1 b1)
+  I2A :: d a2 b2 -> Cograph c d f (I2 a2) (I2 b2)
+  I12 :: Obj c a -> Obj d b -> f -> f :% (a, b) -> Cograph c d 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
+instance ProfunctorOf c d f => Category (Cograph c d f) where
 
   src (I1A a)       = I1A (src a)
   src (I2A a)       = I2A (src a)
@@ -117,19 +119,19 @@
   (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
+newtype (c1 :>>: c2) a b = DC (Cograph c1 c2 (Const (Op c1 :**: c2) (->) ()) a b) deriving Category
 
 
-data NatAsFunctor f g = NatAsFunctor (Nat (Dom f) (Cod f) f g)
+newtype NatAsFunctor f g = NatAsFunctor (Nat (Dom f) (Cod f) f g)
 
 -- | 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 :**: Cograph (Hom Unit)
+
+  type Dom (NatAsFunctor f g) = Dom f :**: Cograph Unit Unit (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 Hom Unit) = n ! a
diff --git a/Data/Category/Cube.hs b/Data/Category/Cube.hs
--- a/Data/Category/Cube.hs
+++ b/Data/Category/Cube.hs
@@ -12,6 +12,8 @@
 -----------------------------------------------------------------------------
 module Data.Category.Cube where
 
+import Data.Kind (Type)
+
 import Data.Category
 import Data.Category.Product
 import Data.Category.Functor
@@ -25,7 +27,7 @@
 
 data Sign = M | P
 
-data Cube :: * -> * -> * where
+data Cube :: Type -> Type -> Type where
   Z :: Cube Z Z
   S :: Cube x y -> Cube (S x) (S y)
   Y :: Sign -> Cube x y -> Cube x (S y) -- face maps
@@ -64,7 +66,7 @@
 
 data Sign0 = SM | S0 | SP
 
-data ACube :: * -> * where
+data ACube :: Type -> Type where
   Nil :: ACube Z
   Cons :: Sign0 -> ACube n -> ACube (S n)
 
diff --git a/Data/Category/Dialg.hs b/Data/Category/Dialg.hs
--- a/Data/Category/Dialg.hs
+++ b/Data/Category/Dialg.hs
@@ -79,13 +79,13 @@
 
   type InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) = NatNum
 
-  initialObject = dialgId (Dialgebra (\x -> x) (Z :**: S))
+  initialObject = dialgId (Dialgebra obj (Z :**: S))
 
   initialize (dialgebra -> d@(Dialgebra _ (z :**: s))) = DialgA (dialgebra initialObject) d (primRec z s)
 
 
 
-data FreeAlg m = FreeAlg (Monad m)
+newtype FreeAlg m = FreeAlg (Monad m)
 -- | @FreeAlg@ M takes @x@ to the free algebra @(M x, mu_x)@ of the monad @M@.
 instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (FreeAlg m) where
   type Dom (FreeAlg m) = Dom m
diff --git a/Data/Category/Enriched.hs b/Data/Category/Enriched.hs
--- a/Data/Category/Enriched.hs
+++ b/Data/Category/Enriched.hs
@@ -5,10 +5,12 @@
   , RankNTypes
   , PatternSynonyms
   , FlexibleContexts
+  , FlexibleInstances
   , NoImplicitPrelude
   , UndecidableInstances
   , ScopedTypeVariables
   , ConstraintKinds
+  , MultiParamTypeClasses
   #-}
 -----------------------------------------------------------------------------
 -- |
@@ -21,21 +23,21 @@
 -----------------------------------------------------------------------------
 module Data.Category.Enriched where
 
+import Data.Kind (Type)
+
 import Data.Category (Category(..), Obj, Op(..))
 import Data.Category.Product
 import Data.Category.Functor (Functor(..), Hom(..))
-import Data.Category.Limit hiding (HasLimits)
-import Data.Category.CartesianClosed
-import Data.Category.Boolean
-
+import Data.Category.Limit (HasBinaryProducts(..), HasTerminalObject(..))
+import Data.Category.CartesianClosed (CartesianClosed(..), ExpFunctor(..), curry, uncurry)
 
 -- | An enriched category
-class CartesianClosed (V k) => ECategory (k :: * -> * -> *) where
+class CartesianClosed (V k) => ECategory (k :: Type -> Type -> Type) where
   -- | The category V which k is enriched in
-  type V k :: * -> * -> *
+  type V k :: Type -> Type -> Type
 
   -- | The hom object in V from a to b
-  type k $ ab :: *
+  type k $ ab :: Type
   hom :: Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
 
   id :: Obj k a -> Arr k a a
@@ -67,7 +69,7 @@
   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
+data (:<>:) :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type 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@.
@@ -114,285 +116,5 @@
   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
+  id (InHask f) () = f
   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
-
-class CartesianClosed v => HasEnds v where
-  type End (v :: * -> * -> *) t :: *
-  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) }
-instance HasEnds (->) where
-  type End (->) t = HaskEnd t
-  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/Enriched/Functor.hs b/Data/Category/Enriched/Functor.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/Enriched/Functor.hs
@@ -0,0 +1,187 @@
+{-# LANGUAGE
+    TypeOperators
+  , TypeFamilies
+  , GADTs
+  , RankNTypes
+  , PatternSynonyms
+  , FlexibleContexts
+  , FlexibleInstances
+  , NoImplicitPrelude
+  , UndecidableInstances
+  , ScopedTypeVariables
+  , ConstraintKinds
+  , MultiParamTypeClasses
+  #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Category.Enriched.Functor
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  sjoerd@w3future.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+-----------------------------------------------------------------------------
+module Data.Category.Enriched.Functor where
+
+import Data.Kind (Type)
+
+import Data.Category (Category(..), Obj)
+import Data.Category.Functor (Functor(..))
+import Data.Category.Limit (HasBinaryProducts(..), HasTerminalObject(..))
+import Data.Category.CartesianClosed
+import Data.Category.Enriched
+
+-- | 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 :: Type -> Type -> Type
+  -- | The codomain, or target category, of the functor.
+  type ECod ftag :: Type -> Type -> Type
+
+  -- | @:%%@ maps objects at the type level
+  type ftag :%% a :: Type
+
+  -- | @%%@ 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 :: Type -> Type -> Type) = 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 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) 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 :: Type -> Type -> Type) = 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)
+
+newtype InHaskF f = InHaskF f
+-- | A regular functor is a functor enriched in Hask.
+instance Functor f => EFunctor (InHaskF f) where
+  type EDom (InHaskF f) = InHask (Dom f)
+  type ECod (InHaskF f) = InHask (Cod f)
+  type InHaskF f :%% a = f :% a
+  InHaskF f %% InHask a = InHask (f % a)
+  map (InHaskF f) _ _ = \g -> f % g
+
+newtype InHaskToHask f = InHaskToHask f
+instance (Functor f, Cod f ~ (->)) => EFunctor (InHaskToHask f) where
+  type EDom (InHaskToHask f) = InHask (Dom f)
+  type ECod (InHaskToHask f) = Self (->)
+  type InHaskToHask f :%% a = f :% a
+  InHaskToHask f %% InHask a = Self (f % a)
+  map (InHaskToHask f) _ _ = \g -> f % g
+
+newtype UnderlyingHask (c :: Type -> Type -> Type) (d :: Type -> Type -> Type) f = UnderlyingHask f
+-- | The underlying functor of an enriched functor @f@ enriched in Hask.
+instance (EFunctor f, EDom f ~ InHask c, ECod f ~ InHask d, Category c, Category d) => Functor (UnderlyingHask c d f) where
+  type Dom (UnderlyingHask c d f) = c
+  type Cod (UnderlyingHask c d f) = d
+  type UnderlyingHask c d f :% a = f :%% a
+  UnderlyingHask f % g = map f (InHask (src g)) (InHask (tgt g)) g
+
+data EHom (k :: Type -> Type -> Type) = 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
+
+-- | 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)
+
+
+-- | A V-enrichment on a functor @F: V -> V@ is the same thing as tensorial strength @(a, f b) -> f (a, b)@.
+strength :: EFunctorOf (Self v) (Self v) f => f -> Obj v a -> Obj v b -> v (BinaryProduct v a (f :%% b)) (f :%% (BinaryProduct v a b))
+strength f a b = uncurry a fb fab (map f (Self b) (Self (a *** b)) . tuple b a)
+  where
+    Self fb = f %% Self b
+    Self fab = f %% Self (a *** b)
+
+
+-- | Enriched natural transformations.
+data ENat :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type 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
diff --git a/Data/Category/Enriched/Limit.hs b/Data/Category/Enriched/Limit.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/Enriched/Limit.hs
@@ -0,0 +1,111 @@
+{-# LANGUAGE
+    TypeOperators
+  , TypeFamilies
+  , GADTs
+  , RankNTypes
+  , PatternSynonyms
+  , FlexibleContexts
+  , FlexibleInstances
+  , NoImplicitPrelude
+  , UndecidableInstances
+  , ScopedTypeVariables
+  , ConstraintKinds
+  , MultiParamTypeClasses
+  #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Category.Enriched.Limit
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  sjoerd@w3future.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+-----------------------------------------------------------------------------
+module Data.Category.Enriched.Limit where
+
+import Data.Kind (Type)
+
+import Data.Category (Category(..), Obj)
+import Data.Category.Functor (Functor(..))
+import Data.Category.Limit (HasBinaryProducts(..))
+import Data.Category.CartesianClosed (CartesianClosed(..), curry, flip)
+import qualified Data.Category.WeightedLimit as Hask
+import Data.Category.Enriched
+import Data.Category.Enriched.Functor
+
+type VProfunctor k l t = EFunctorOf (EOp k :<>: l) (Self (V k)) t
+
+class CartesianClosed v => HasEnds v where
+  type End (v :: Type -> Type -> Type) t :: Type
+  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) }
+instance HasEnds (->) where
+  type End (->) t = HaskEnd t
+  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), CartesianClosed (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 :: Type -> Type -> Type) = 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 :: Type -> Type -> Type) w d :: Type
+type Lim w d = WeigtedLimit (ECod d) w d
+
+class (HasEnds (V k), EFunctor w, ECod w ~ Self (V k)) => HasLimits k w where
+  limitObj :: EFunctorOf (EDom w) k d => w -> d -> Obj k (Lim w d)
+  limit    :: EFunctorOf (EDom w) k d => w -> d -> Obj k e -> V k (k $ (e, Lim w d)) (End (V k) (w :->>: (EHomX_ k e :.: d)))
+  limitInv :: EFunctorOf (EDom w) k d => w -> d -> Obj k e -> V k (End (V k) (w :->>: (EHomX_ k e :.: d))) (k $ (e, Lim w d))
+
+-- d :: j -> k, w :: EOp j -> Self (V k)
+type family WeigtedColimit (k :: Type -> Type -> Type) w d :: Type
+type Colim w d = WeigtedColimit (ECod d) w d
+
+class (HasEnds (V k), EFunctor w, ECod w ~ Self (V k)) => HasColimits k w where
+  colimitObj :: (EFunctorOf j k d, EOp j ~ EDom w) => w -> d -> Obj k (Colim w d)
+  colimit    :: (EFunctorOf j k d, EOp j ~ EDom w) => w -> d -> Obj k e -> V k (k $ (Colim w d, e)) (End (V k) (w :->>: (EHom_X k e :.: Opposite d)))
+  colimitInv :: (EFunctorOf j k d, EOp j ~ EDom w) => w -> d -> Obj k e -> V k (End (V k) (w :->>: (EHom_X k e :.: Opposite d))) (k $ (Colim w d, e))
+
+
+type instance WeigtedLimit (Self v) w d = End v (w :->>: d)
+instance (HasEnds v, EFunctor w, ECod w ~ Self v) => HasLimits (Self v) w where
+  limitObj w d = Self (end (w ->> d))
+  limit    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))
+  limitInv 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)))
+
+type instance WeigtedLimit (InHask k) (InHaskToHask w) d = Hask.WeightedLimit k w (UnderlyingHask (Dom w) k d)
+instance Hask.HasWLimits k w => HasLimits (InHask k) (InHaskToHask w) where
+  limitObj (InHaskToHask w) d = InHask (Hask.limitObj w (UnderlyingHask d))
+  limit    (InHaskToHask w) d _ el = HaskEnd (\_ (InHask a) wa -> Hask.limit w (UnderlyingHask d) a wa . el)
+  limitInv (InHaskToHask w) d (InHask e) (HaskEnd n) =
+    Hask.limitFactorizer w (UnderlyingHask d) e (n (InHaskToHask w ->> (EHomX_ (InHask e) :.: d)) . InHask)
diff --git a/Data/Category/Enriched/Poset3.hs b/Data/Category/Enriched/Poset3.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/Enriched/Poset3.hs
@@ -0,0 +1,84 @@
+{-# LANGUAGE
+    TypeOperators
+  , TypeFamilies
+  , GADTs
+  , RankNTypes
+  , PatternSynonyms
+  , FlexibleContexts
+  , FlexibleInstances
+  , NoImplicitPrelude
+  , UndecidableInstances
+  , ScopedTypeVariables
+  , ConstraintKinds
+  , MultiParamTypeClasses
+  #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Category.Enriched.Poset3
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  sjoerd@w3future.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+-----------------------------------------------------------------------------
+module Data.Category.Enriched.Poset3 where
+
+import Data.Category.Boolean
+import Data.Category.Enriched
+
+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/Enriched/Yoneda.hs b/Data/Category/Enriched/Yoneda.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/Enriched/Yoneda.hs
@@ -0,0 +1,56 @@
+{-# LANGUAGE
+    TypeOperators
+  , TypeFamilies
+  , GADTs
+  , RankNTypes
+  , PatternSynonyms
+  , FlexibleContexts
+  , FlexibleInstances
+  , NoImplicitPrelude
+  , UndecidableInstances
+  , ScopedTypeVariables
+  , ConstraintKinds
+  , MultiParamTypeClasses
+  #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Category.Enriched.Yoneda
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  sjoerd@w3future.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+-----------------------------------------------------------------------------
+module Data.Category.Enriched.Yoneda where
+
+import Data.Kind (Type)
+
+import Data.Category (Category(..), Obj)
+import Data.Category.CartesianClosed (CartesianClosed(..), curry)
+import Data.Category.Limit (HasBinaryProducts(..), HasTerminalObject(..))
+import Data.Category.Enriched
+import Data.Category.Enriched.Functor
+import Data.Category.Enriched.Limit
+
+
+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), EFunctor f, EDom f ~ k, ECod f ~ Self (V k)) => 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 :: Type -> Type -> Type) = 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
diff --git a/Data/Category/Fin.hs b/Data/Category/Fin.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/Fin.hs
@@ -0,0 +1,139 @@
+{-# LANGUAGE TypeFamilies, GADTs, PolyKinds, DataKinds, FlexibleInstances, FlexibleContexts, UndecidableInstances, NoImplicitPrelude #-}
+{-# LANGUAGE EmptyCase, TypeApplications, ScopedTypeVariables, TypeOperators #-}
+module Data.Category.Fin where
+
+import Data.Category
+import Data.Category.Limit
+import Data.Category.CartesianClosed
+
+data Nat = Z | S Nat
+
+data Fin n where
+  FZ :: Fin ('S n)
+  FS :: Fin n -> Fin ('S n)
+
+data LTE (n :: Nat) (a :: Fin n) (b :: Fin n) where
+  ZEQ :: LTE ('S m) 'FZ 'FZ
+  ZLT :: LTE ('S m) 'FZ  b -> LTE ('S ('S m))  'FZ    ('FS b)
+  SLT :: LTE ('S m)  a   b -> LTE ('S ('S m)) ('FS a) ('FS b)
+
+instance Category (LTE n) where
+  src ZEQ = ZEQ
+  src (ZLT _) = ZEQ
+  src (SLT a) = SLT (src a)
+  tgt ZEQ = ZEQ
+  tgt (ZLT a) = SLT (tgt a)
+  tgt (SLT a) = SLT (tgt a)
+  ZEQ . a = a
+  a . ZEQ = a
+  SLT a . ZLT b = ZLT (a . b)
+  SLT a . SLT b = SLT (a . b)
+
+instance HasInitialObject (LTE ('S n)) where
+  type InitialObject (LTE ('S n)) = 'FZ
+  initialObject = ZEQ
+  initialize ZEQ = ZEQ
+  initialize (SLT a) = ZLT (initialize a)
+
+instance HasTerminalObject (LTE ('S 'Z)) where
+  type TerminalObject (LTE ('S 'Z)) = 'FZ
+  terminalObject = ZEQ
+  terminate ZEQ = ZEQ
+
+instance HasTerminalObject (LTE ('S n)) => HasTerminalObject (LTE ('S ('S n))) where
+  type TerminalObject (LTE ('S ('S n))) = 'FS (TerminalObject (LTE ('S n)))
+  terminalObject = SLT terminalObject
+  terminate ZEQ = ZLT (terminate ZEQ)
+  terminate (SLT a) = SLT (terminate a)
+
+instance HasBinaryCoproducts (LTE ('S 'Z)) where
+  type BinaryCoproduct (LTE ('S 'Z)) 'FZ 'FZ = 'FZ
+  inj1 ZEQ ZEQ = ZEQ
+  inj2 ZEQ ZEQ = ZEQ
+  ZEQ ||| ZEQ = ZEQ
+
+instance HasBinaryCoproducts (LTE ('S n)) => HasBinaryCoproducts (LTE ('S ('S n))) where
+  type BinaryCoproduct (LTE ('S ('S n))) 'FZ 'FZ = 'FZ
+  type BinaryCoproduct (LTE ('S ('S n))) 'FZ ('FS b) = 'FS (BinaryCoproduct (LTE ('S n)) 'FZ b)
+  type BinaryCoproduct (LTE ('S ('S n))) ('FS a) 'FZ = 'FS (BinaryCoproduct (LTE ('S n)) a 'FZ)
+  type BinaryCoproduct (LTE ('S ('S n))) ('FS a) ('FS b) = 'FS (BinaryCoproduct (LTE ('S n)) a b)
+  inj1 ZEQ ZEQ = ZEQ
+  inj1 ZEQ (SLT a) = ZLT (inj1 ZEQ a)
+  inj1 (SLT a) ZEQ = SLT (inj1 a ZEQ)
+  inj1 (SLT a) (SLT b) = SLT (inj1 a b)
+  inj2 ZEQ ZEQ = ZEQ
+  inj2 ZEQ (SLT a) = SLT (inj2 ZEQ a)
+  inj2 (SLT a) ZEQ = ZLT (inj2 a ZEQ)
+  inj2 (SLT a) (SLT b) = SLT (inj2 a b)
+  ZEQ ||| ZEQ = ZEQ
+  ZLT a ||| ZLT b = ZLT (case a ||| b of { ZEQ -> ZEQ; ZLT n -> ZLT n })
+  ZLT a ||| SLT b = SLT (a ||| b)
+  SLT a ||| ZLT b = SLT (a ||| b)
+  SLT a ||| SLT b = SLT (a ||| b)
+
+instance HasBinaryProducts (LTE ('S 'Z)) where
+  type BinaryProduct (LTE ('S 'Z)) 'FZ 'FZ = 'FZ
+  proj1 ZEQ ZEQ = ZEQ
+  proj2 ZEQ ZEQ = ZEQ
+  ZEQ &&& ZEQ = ZEQ
+
+instance HasBinaryProducts (LTE ('S n)) => HasBinaryProducts (LTE ('S ('S n))) where
+  type BinaryProduct (LTE ('S ('S n))) 'FZ 'FZ = 'FZ
+  type BinaryProduct (LTE ('S ('S n))) 'FZ ('FS b) = 'FZ
+  type BinaryProduct (LTE ('S ('S n))) ('FS a) 'FZ = 'FZ
+  type BinaryProduct (LTE ('S ('S n))) ('FS a) ('FS b) = 'FS (BinaryProduct (LTE ('S n)) a b)
+  proj1 ZEQ ZEQ = ZEQ
+  proj1 ZEQ (SLT _) = ZEQ
+  proj1 (SLT a) ZEQ = ZLT (case proj1 a ZEQ of { ZEQ -> ZEQ; ZLT n -> ZLT n })
+  proj1 (SLT a) (SLT b) = SLT (proj1 a b)
+  proj2 ZEQ ZEQ = ZEQ
+  proj2 ZEQ (SLT a) = ZLT (case proj2 ZEQ a of { ZEQ -> ZEQ; ZLT n -> ZLT n })
+  proj2 (SLT _) ZEQ = ZEQ
+  proj2 (SLT a) (SLT b) = SLT (proj2 a b)
+  ZEQ &&& ZEQ = ZEQ
+  ZEQ &&& ZLT _ = ZEQ
+  ZLT _ &&& ZEQ = ZEQ
+  ZLT a &&& ZLT b = ZLT (a &&& b)
+  SLT a &&& SLT b = SLT (a &&& b)
+
+data Proof a n where
+  Proof :: (BinaryProduct (LTE ('S n)) 'FZ a ~ 'FZ, BinaryProduct (LTE ('S n)) a 'FZ ~ 'FZ) => Proof a n
+proof :: Obj (LTE ('S n)) a -> Proof a n
+proof = proof -- trust me
+
+instance CartesianClosed (LTE ('S 'Z)) where
+  type Exponential (LTE ('S 'Z)) 'FZ 'FZ = 'FZ
+  apply ZEQ ZEQ = ZEQ
+  tuple ZEQ ZEQ = ZEQ
+  ZEQ ^^^ ZEQ = ZEQ
+
+-- b -> c = max(a: min(a, b) <= c)
+-- → 0 1 2 3
+--  +-------
+-- 0|3 3 3 3
+-- 1|0 3 3 3
+-- 2|0 1 3 3
+-- 3|0 1 2 3
+instance CartesianClosed (LTE ('S n)) => CartesianClosed (LTE ('S ('S n))) where
+  type Exponential (LTE ('S ('S n))) 'FZ 'FZ = 'FS (Exponential (LTE ('S n)) 'FZ 'FZ)
+  type Exponential (LTE ('S ('S n))) 'FZ ('FS b) = 'FS (Exponential (LTE ('S n)) 'FZ b)
+  type Exponential (LTE ('S ('S n))) ('FS a) 'FZ = 'FZ
+  type Exponential (LTE ('S ('S n))) ('FS a) ('FS b) = 'FS (Exponential (LTE ('S n)) a b)
+  apply ZEQ ZEQ = ZEQ
+  apply ZEQ (SLT a) = ZLT (case apply ZEQ a of { ZEQ -> ZEQ; ZLT n -> ZLT n })
+  apply (SLT _) ZEQ = ZEQ
+  apply (SLT a) (SLT b) = SLT (apply a b)
+  tuple ZEQ ZEQ = case proof (ZEQ @n) of Proof -> ZLT (tuple ZEQ ZEQ)
+  tuple ZEQ (SLT a) = case proof (src a) of Proof -> SLT (tuple ZEQ a)
+  tuple (SLT _) ZEQ = ZEQ
+  tuple (SLT a) (SLT b) = SLT (tuple a b)
+  ZEQ ^^^ ZEQ = SLT (ZEQ ^^^ ZEQ)
+  ZEQ ^^^ ZLT a = ZLT (initialize (tgt (ZEQ ^^^ a)))
+  ZEQ ^^^ SLT _ = ZEQ
+  ZLT a ^^^ ZEQ = SLT (a ^^^ ZEQ)
+  ZLT a ^^^ ZLT b = ZLT (initialize (tgt (a ^^^ b)))
+  ZLT a ^^^ SLT b = ZLT (initialize (tgt (a ^^^ b)))
+  SLT a ^^^ ZEQ = SLT (a ^^^ ZEQ)
+  SLT a ^^^ ZLT b = SLT (a ^^^ b)
+  SLT a ^^^ SLT b = SLT (a ^^^ b)
+
diff --git a/Data/Category/Fix.hs b/Data/Category/Fix.hs
--- a/Data/Category/Fix.hs
+++ b/Data/Category/Fix.hs
@@ -10,6 +10,8 @@
 -----------------------------------------------------------------------------
 module Data.Category.Fix where
 
+import Data.Kind (Type)
+
 import Data.Category
 import Data.Category.Functor
 import Data.Category.Limit
@@ -58,7 +60,7 @@
   tuple (Fix a) (Fix b) = Fix (tuple a b)
   Fix a ^^^ Fix b = Fix (a ^^^ b)
 
-data Wrap (f :: * -> * -> *) = Wrap
+data Wrap (f :: Type -> Type -> Type) = Wrap
 -- | The `Wrap` functor wraps `Fix` around @f (Fix f)@.
 instance Category (f (Fix f)) => Functor (Wrap (Fix f)) where
   type Dom (Wrap (Fix f)) = f (Fix f)
@@ -66,7 +68,7 @@
   type Wrap (Fix f) :% a = a
   Wrap % f = Fix f
 
-data Unwrap (f :: * -> * -> *) = Unwrap
+data Unwrap (f :: Type -> Type -> Type) = 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
diff --git a/Data/Category/Functor.hs b/Data/Category/Functor.hs
--- a/Data/Category/Functor.hs
+++ b/Data/Category/Functor.hs
@@ -34,7 +34,6 @@
   , Id(..)
   , (:.:)(..)
   , Const(..), ConstF
-  , Opposite(..)
   , OpOp(..)
   , OpOpInv(..)
   , Any(..)
@@ -52,12 +51,14 @@
   , Hom(..)
   , (:*-:), pattern HomX_
   , (:-*:), pattern Hom_X
-  , HomF, pattern HomF
-  , Star, pattern Star
-  , Costar, pattern Costar
 
+  -- *** Profunctors
+  , ProfunctorOf
+
 ) where
 
+import Data.Kind (Type)
+
 import Data.Category
 import Data.Category.Product
 
@@ -70,12 +71,12 @@
 class (Category (Dom ftag), Category (Cod ftag)) => Functor ftag where
 
   -- | The domain, or source category, of the functor.
-  type Dom ftag :: * -> * -> *
+  type Dom ftag :: Type -> Type -> Type
   -- | The codomain, or target category, of the functor.
-  type Cod ftag :: * -> * -> *
+  type Cod ftag :: Type -> Type -> Type
 
   -- | @:%@ maps objects.
-  type ftag :% a :: *
+  type ftag :% a :: Type
 
   -- | @%@ maps arrows.
   (%)  :: ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
@@ -84,7 +85,7 @@
 
 
 -- | Functors are arrows in the category Cat.
-data Cat :: (* -> * -> *) -> (* -> * -> *) -> * where
+data Cat :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type where
   CatA :: (Functor ftag, Category (Dom ftag), Category (Cod ftag)) => ftag -> Cat (Dom ftag) (Cod ftag)
 
 
@@ -98,7 +99,7 @@
 
 
 
-data Id (k :: * -> * -> *) = Id
+data Id (k :: Type -> Type -> Type) = Id
 
 -- | The identity functor on k
 instance Category k => Functor (Id k) where
@@ -122,7 +123,7 @@
 
 
 
-data Const (c1 :: * -> * -> *) (c2 :: * -> * -> *) x where
+data Const (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) x where
   Const :: Obj c2 x -> Const c1 c2 x
 
 -- | The constant functor.
@@ -137,19 +138,8 @@
 type ConstF f = Const (Dom f) (Cod f)
 
 
-data Opposite f where
-  Opposite :: Functor f => f -> Opposite f
 
--- | The dual of a functor
-instance (Category (Dom f), Category (Cod f)) => Functor (Opposite f) where
-  type Dom (Opposite f) = Op (Dom f)
-  type Cod (Opposite f) = Op (Cod f)
-  type Opposite f :% a = f :% a
-
-  Opposite f % Op a = Op (f % a)
-
-
-data OpOp (k :: * -> * -> *) = OpOp
+data OpOp (k :: Type -> Type -> Type) = OpOp
 
 -- | The @Op (Op x) = x@ functor.
 instance Category k => Functor (OpOp k) where
@@ -160,7 +150,7 @@
   OpOp % Op (Op f) = f
 
 
-data OpOpInv (k :: * -> * -> *) = OpOpInv
+data OpOpInv (k :: Type -> Type -> Type) = OpOpInv
 
 -- | The @x = Op (Op x)@ functor.
 instance Category k => Functor (OpOpInv k) where
@@ -175,7 +165,7 @@
 newtype Any f = Any f deriving Functor
 
 
-data Proj1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Proj1
+data Proj1 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) = Proj1
 
 -- | 'Proj1' is a bifunctor that projects out the first component of a product.
 instance (Category c1, Category c2) => Functor (Proj1 c1 c2) where
@@ -186,7 +176,7 @@
   Proj1 % (f1 :**: _) = f1
 
 
-data Proj2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Proj2
+data Proj2 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) = Proj2
 
 -- | 'Proj2' is a bifunctor that projects out the second component of a product.
 instance (Category c1, Category c2) => Functor (Proj2 c1 c2) where
@@ -208,7 +198,7 @@
   (g1 :***: g2) % (f1 :**: f2) = (g1 % f1) :**: (g2 % f2)
 
 
-data DiagProd (k :: * -> * -> *) = DiagProd
+data DiagProd (k :: Type -> Type -> Type) = DiagProd
 
 -- | 'DiagProd' is the diagonal functor for products.
 instance Category k => Functor (DiagProd k) where
@@ -220,18 +210,11 @@
 
 
 type Tuple1 c1 c2 a = (Const c2 c1 a :***: Id c2) :.: DiagProd c2
-
 -- | 'Tuple1' tuples with a fixed object on the left.
 pattern Tuple1 :: (Category c1, Category c2) => Obj c1 a -> Tuple1 c1 c2 a
 pattern Tuple1 a = (Const a :***: Id) :.: DiagProd
 
--- type Tuple2 c1 c2 a = (Id c1 :***: Const c1 c2 a) :.: DiagProd c1
---
--- -- | 'Tuple2' tuples with a fixed object on the right.
--- tuple2 :: (Category c1, Category c2) => Obj c2 a -> Tuple2 c1 c2 a
--- tuple2 a = (Id :***: Const a) :.: DiagProd
-
-type Swap (c1 :: * -> * -> *) (c2 :: * -> * -> *) = (Proj2 c1 c2 :***: Proj1 c1 c2) :.: DiagProd (c1 :**: c2)
+type Swap (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) = (Proj2 c1 c2 :***: Proj1 c1 c2) :.: DiagProd (c1 :**: c2)
 -- | 'swap' swaps the 2 categories of the product of categories.
 pattern Swap :: (Category c1, Category c2) => Swap c1 c2
 pattern Swap = (Proj2 :***: Proj1) :.: DiagProd
@@ -243,7 +226,7 @@
 
 
 
-data Hom (k :: * -> * -> *) = Hom
+data Hom (k :: Type -> Type -> Type) = Hom
 
 -- | The Hom functor, Hom(--,--), a bifunctor contravariant in its first argument and covariant in its second argument.
 instance Category k => Functor (Hom k) where
@@ -265,14 +248,4 @@
 pattern Hom_X x = Hom :.: Tuple2 x
 
 
-type HomF f g = Hom (Cod f) :.: (Opposite f :***: g)
-pattern HomF :: (Functor f, Functor g, Cod f ~ Cod g) => f -> g -> HomF f g
-pattern HomF f g = Hom :.: (Opposite f :***: g)
-
-type Star f = HomF (Id (Cod f)) f
-pattern Star :: Functor f => f -> Star f
-pattern Star f = HomF Id f
-
-type Costar f = HomF f (Id (Cod f))
-pattern Costar :: Functor f => f -> Costar f
-pattern Costar f = HomF f Id
+type ProfunctorOf c d t = (FunctorOf (Op c :**: d) (->) t, Category c, Category d)
diff --git a/Data/Category/KanExtension.hs b/Data/Category/KanExtension.hs
--- a/Data/Category/KanExtension.hs
+++ b/Data/Category/KanExtension.hs
@@ -19,6 +19,8 @@
 -----------------------------------------------------------------------------
 module Data.Category.KanExtension where
 
+import Data.Kind (Type)
+
 import Data.Category
 import Data.Category.Functor
 import Data.Category.NaturalTransformation
@@ -30,7 +32,7 @@
 -- | An instance of @HasRightKan p k@ says there are right Kan extensions for all functors with codomain @k@.
 class (Functor p, Category k) => HasRightKan p k where
   -- | The right Kan extension of a functor @p@ for functors @f@ with codomain @k@.
-  type RanFam p k (f :: *) :: *
+  type RanFam p k (f :: Type) :: Type
   -- | 'ran' gives the defining natural transformation of the right Kan extension of @f@ along @p@.
   ran           :: p -> Obj (Nat (Dom p) k) f -> Nat (Dom p) k (RanFam p k f :.: p) f
   -- | 'ranFactorizer' shows that this extension is universal.
@@ -44,7 +46,7 @@
 ranF' :: Nat (Dom p) k (RanFam p k f :.: p) f -> Obj (Nat (Cod p) k) (RanFam p k f)
 ranF' (Nat (r :.: _) _ _) = natId r
 
-data RanFunctor (p :: *) (k :: * -> * -> *) = RanFunctor p
+newtype RanFunctor (p :: Type) (k :: Type -> Type -> Type) = RanFunctor p
 instance HasRightKan p k => Functor (RanFunctor p k) where
   type Dom (RanFunctor p k) = Nat (Dom p) k
   type Cod (RanFunctor p k) = Nat (Cod p) k
@@ -60,7 +62,7 @@
 -- | An instance of @HasLeftKan p k@ says there are left Kan extensions for all functors with codomain @k@.
 class (Functor p, Category k) => HasLeftKan p k where
   -- | The left Kan extension of a functor @p@ for functors @f@ with codomain @k@.
-  type LanFam (p :: *) (k :: * -> * -> *) (f :: *) :: *
+  type LanFam (p :: Type) (k :: Type -> Type -> Type) (f :: Type) :: Type
   -- | 'lan' gives the defining natural transformation of the left Kan extension of @f@ along @p@.
   lan           :: p -> Obj (Nat (Dom p) k) f -> Nat (Dom p) k f (LanFam p k f :.: p)
   -- | 'lanFactorizer' shows that this extension is universal.
@@ -74,7 +76,7 @@
 lanF' :: Nat (Dom p) k f (LanFam p k f :.: p) -> Obj (Nat (Cod p) k) (LanFam p k f)
 lanF' (Nat _ (r :.: _) _) = natId r
 
-data LanFunctor (p :: *) (k :: * -> * -> *) = LanFunctor p
+newtype LanFunctor (p :: Type) (k :: Type -> Type -> Type) = LanFunctor p
 instance HasLeftKan p k => Functor (LanFunctor p k) where
   type Dom (LanFunctor p k) = Nat (Dom p) k
   type Cod (LanFunctor p k) = Nat (Cod p) k
diff --git a/Data/Category/Limit.hs b/Data/Category/Limit.hs
--- a/Data/Category/Limit.hs
+++ b/Data/Category/Limit.hs
@@ -4,6 +4,10 @@
   GADTs,
   PolyKinds,
   DataKinds,
+  LinearTypes,
+  LambdaCase,
+  EmptyCase,
+  BlockArguments,
   MultiParamTypeClasses,
   RankNTypes,
   ScopedTypeVariables,
@@ -65,13 +69,20 @@
   , ProductFunctor(..)
   , (:*:)(..)
   , prodAdj
+  , type (&)(..)
   , HasBinaryCoproducts(..)
   , CoproductFunctor(..)
   , (:+:)(..)
   , coprodAdj
+  , Either(..)
 
 ) where
 
+import Data.Kind (Type)
+import GHC.Exts (FUN)
+import GHC.Types (Multiplicity(One))
+import Prelude (Either(..))
+
 import Data.Category
 import Data.Category.Functor
 import Data.Category.NaturalTransformation
@@ -88,7 +99,7 @@
 infixl 2 |||
 
 
-data Diag :: (* -> * -> *) -> (* -> * -> *) -> * where
+data Diag :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type where
   Diag :: Diag j k
 
 -- | The diagonal functor from (index-) category J to k.
@@ -123,7 +134,7 @@
 -- | An instance of @HasLimits j k@ says that @k@ has all limits of type @j@.
 class (Category j, Category k) => HasLimits j k where
   -- | Limits in a category @k@ by means of a diagram of type @j@, which is a functor from @j@ to @k@.
-  type LimitFam (j :: * -> * -> *) (k :: * -> * -> *) (f :: *) :: *
+  type LimitFam (j :: Type -> Type -> Type) (k :: Type -> Type -> Type) (f :: Type) :: Type
   -- | 'limit' returns the limiting cone for a functor @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
@@ -132,7 +143,7 @@
 
 type Limit f = LimitFam (Dom f) (Cod f) f
 
-data LimitFunctor (j :: * -> * -> *) (k :: * -> * -> *) = LimitFunctor
+data LimitFunctor (j :: Type -> Type -> Type) (k :: Type -> Type -> Type) = LimitFunctor
 -- | If every diagram of type @j@ has a limit in @k@ there exists a limit functor.
 --   It can be seen as a generalisation of @(***)@.
 instance HasLimits j k => Functor (LimitFunctor j k) where
@@ -182,7 +193,7 @@
 -- | An instance of @HasColimits j k@ says that @k@ has all colimits of type @j@.
 class (Category j, Category k) => HasColimits j k where
   -- | Colimits in a category @k@ by means of a diagram of type @j@, which is a functor from @j@ to @k@.
-  type ColimitFam (j :: * -> * -> *) (k :: * -> * -> *) (f :: *) :: *
+  type ColimitFam (j :: Type -> Type -> Type) (k :: Type -> Type -> Type) (f :: Type) :: Type
   -- | 'colimit' returns the limiting co-cone for a functor @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
@@ -191,7 +202,7 @@
 
 type Colimit f = ColimitFam (Dom f) (Cod f) f
 
-data ColimitFunctor (j :: * -> * -> *) (k :: * -> * -> *) = ColimitFunctor
+data ColimitFunctor (j :: Type -> Type -> Type) (k :: Type -> Type -> Type) = ColimitFunctor
 -- | If every diagram of type @j@ has a colimit in @k@ there exists a colimit functor.
 --   It can be seen as a generalisation of @(+++)@.
 instance HasColimits j k => Functor (ColimitFunctor j k) where
@@ -248,10 +259,20 @@
 instance HasTerminalObject (->) where
   type TerminalObject (->) = ()
 
-  terminalObject = \x -> x
+  terminalObject = obj
 
   terminate _ _ = ()
 
+data Top where
+  Top :: a %1 -> Top
+-- | The terminal object in the category of linear types is `Top`.
+instance HasTerminalObject (FUN 'One) where
+  type TerminalObject (FUN 'One) = Top
+
+  terminalObject = obj
+
+  terminate _ = Top
+
 -- | @Unit@ is the terminal category.
 instance HasTerminalObject Cat where
   type TerminalObject Cat = Unit
@@ -311,14 +332,16 @@
 
 
 data Zero
+absurd :: FUN m Zero a
+absurd = \case
 
 -- | Any empty data type is an initial object in @Hask@.
-instance HasInitialObject (->) where
-  type InitialObject (->) = Zero
+instance HasInitialObject (FUN m) where
+  type InitialObject (FUN m) = Zero
 
-  initialObject = \x -> x
+  initialObject = obj
 
-  initialize = initialize
+  initialize _ = absurd
 
 -- | The empty category is the initial object in @Cat@.
 instance HasInitialObject Cat where
@@ -409,6 +432,25 @@
   f &&& g = \x -> (f x, g x)
   f *** g = \(x, y) -> (f x, g y)
 
+
+newtype x & y = AddConj (forall r. Either (x %1-> r) (y %1-> r) %1-> r)
+
+-- | The product in the category of linear types is a & b, where you have access to a and b, but not both at the same time.
+instance HasBinaryProducts (FUN 'One) where
+  type BinaryProduct (FUN 'One) x y = x & y
+
+  proj1 _ _ = \(AddConj f) -> f (Left obj)
+  proj2 _ _ = \(AddConj f) -> f (Right obj)
+
+  f &&& g = \x -> AddConj \case
+    Left h -> h (f x)
+    Right h -> h (g x)
+  f *** g = \(AddConj h) -> AddConj \case
+    Left l -> h (Left (\x -> l (f x)))
+    Right r -> h (Right (\x -> r (g x)))
+
+
+
 -- | The product of categories ':**:' is the binary product in 'Cat'.
 instance HasBinaryProducts Cat where
   type BinaryProduct Cat c1 c2 = c1 :**: c2
@@ -456,13 +498,13 @@
   proj2 (DC (I2A a)) (DC (I2A b)) = DC (I2A (proj2 a b))
 
   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 (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
+data ProductFunctor (k :: Type -> Type -> Type) = ProductFunctor
 -- | Binary product as a bifunctor.
 instance HasBinaryProducts k => Functor (ProductFunctor k) where
   type Dom (ProductFunctor k) = k :**: k
@@ -534,6 +576,19 @@
     colimitFactorizer (constPostcompOut (c `o` natId Inj2))
 
 
+instance HasBinaryCoproducts (FUN m) where
+  type BinaryCoproduct (FUN m) a b = Either a b
+
+  inj1 _ _ = Left
+  inj2 _ _ = Right
+
+  f ||| g = \case
+    Left a -> f a
+    Right b -> g b
+  f +++ g = \case
+    Left a -> Left (f a)
+    Right b -> Right (g b)
+
 -- | The coproduct of categories ':++:' is the binary coproduct in 'Cat'.
 instance HasBinaryCoproducts Cat where
   type BinaryCoproduct Cat c1 c2 = c1 :++: c2
@@ -581,13 +636,13 @@
   inj2 (DC (I2A a)) (DC (I2A b)) = DC (I2A (inj2 a 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 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
+data CoproductFunctor (k :: Type -> Type -> Type) = CoproductFunctor
 -- | Binary coproduct as a bifunctor.
 instance HasBinaryCoproducts k => Functor (CoproductFunctor k) where
   type Dom (CoproductFunctor k) = k :**: k
@@ -679,16 +734,16 @@
   colimitFactorizer n = n ! terminalObject
 
 
-data ForAll f = ForAll (forall a. Obj (->) a -> f :% a)
+newtype ForAll f = ForAll (forall a. Obj (->) a -> f :% a)
 
 instance HasLimits (->) (->) where
   type LimitFam (->) (->) f = ForAll f
-  limit (Nat f _ _) = Nat (Const (\x -> x)) f (\a (ForAll g) -> g a)
+  limit (Nat f _ _) = Nat (Const obj) f (\a (ForAll g) -> g a)
   limitFactorizer n = \z -> ForAll (\a -> (n ! a) z)
 
 data Exists f = forall a. Exists (Obj (->) a) (f :% a)
 
 instance HasColimits (->) (->) where
   type ColimitFam (->) (->) f = Exists f
-  colimit (Nat f _ _) = Nat f (Const (\x -> x)) Exists
+  colimit (Nat f _ _) = Nat f (Const obj) Exists
   colimitFactorizer n = \(Exists a fa) -> (n ! a) fa
diff --git a/Data/Category/Monoidal.hs b/Data/Category/Monoidal.hs
--- a/Data/Category/Monoidal.hs
+++ b/Data/Category/Monoidal.hs
@@ -2,9 +2,12 @@
     TypeOperators
   , TypeFamilies
   , GADTs
+  , PolyKinds
+  , DataKinds
   , Rank2Types
   , ViewPatterns
   , TypeSynonymInstances
+  , FlexibleContexts
   , FlexibleInstances
   , UndecidableInstances
   , NoImplicitPrelude
@@ -26,13 +29,17 @@
 import Data.Category.Adjunction
 import Data.Category.Limit
 import Data.Category.Product
+import Data.Category.KanExtension
 
+import GHC.Exts (FUN)
+import GHC.Types (Multiplicity(One))
 
+
 -- | A monoidal category is a category with some kind of tensor product.
 --   A tensor product is a bifunctor, with a unit object.
 class (Functor f, Dom f ~ (Cod f :**: Cod f)) => TensorProduct f where
 
-  type Unit f :: *
+  type Unit f :: Kind (Cod f)
   unitObject :: f -> Obj (Cod f) (Unit f)
 
   leftUnitor     :: Cod f ~ k => f -> Obj k a -> k (f :% (Unit f, a)) a
@@ -96,11 +103,63 @@
   associator    _ (Nat f _ _) (Nat g _ _) (Nat h _ _) = compAssoc f g h
   associatorInv _ (Nat f _ _) (Nat g _ _) (Nat h _ _) = compAssocInv f g h
 
+data LinearTensor = LinearTensor
+instance Functor LinearTensor where
+  type Dom LinearTensor = FUN 'One :**: FUN 'One
+  type Cod LinearTensor = FUN 'One
+  type LinearTensor :% (a, b) = (a, b)
 
+  LinearTensor % (f :**: g) = \(a, b) -> (f a, g b)
+
+instance TensorProduct LinearTensor where
+  type Unit LinearTensor = ()
+  unitObject _ = obj
+
+  leftUnitor     _ _ = \((), a) -> a
+  leftUnitorInv  _ _ = \a -> ((), a)
+  rightUnitor    _ _ = \(a, ()) -> a
+  rightUnitorInv _ _ = \a -> (a, ())
+  associator    _ _ _ _ = \((a, b), c) -> (a, (b, c))
+  associatorInv _ _ _ _ = \(a, (b, c)) -> ((a, b), c)
+
+instance SymmetricTensorProduct LinearTensor where
+  swap _ _ _ = \(a, b) -> (b, a)
+
+
+-- | Day convolution
+data Day t = Day t
+instance TensorProduct t => Functor (Day t) where
+  type Dom (Day t) = Nat (Cod t) (->) :**: Nat (Cod t) (->)
+  type Cod (Day t) = Nat (Cod t) (->)
+  type Day t :% (f, g) = LanHaskF t (ProductFunctor (->) :.: (f :***: g))
+  Day _ % (nf :**: ng) =
+    Nat LanHaskF LanHaskF (\_ (LanHask x@(x1 :**: x2) tx fgx) -> LanHask x tx ((nf ! x1 *** ng ! x2) fgx))
+
+instance TensorProduct t => TensorProduct (Day t) where
+  type Unit (Day t) = Curry1 (Op (Cod t)) (Cod t) (Hom (Cod t)) :% Unit t
+  unitObject (Day t) = Curry1 Hom % Op (unitObject t)
+  leftUnitor (Day t) (NatId a) =
+    Nat LanHaskF a (\_ (LanHask (_ :**: c2) tcz (uc1, ac2)) -> (a % (tcz . t % (uc1 :**: c2) . leftUnitorInv t c2)) ac2)
+  leftUnitorInv (Day t) (NatId a) =
+    Nat a LanHaskF (\z az -> LanHask (unitObject t :**: z) (leftUnitor t z) (unitObject t, az))
+  rightUnitor (Day t) (NatId a) =
+    Nat LanHaskF a (\_ (LanHask (c1 :**: _) tcz (ac1, uc2)) -> (a % (tcz . t % (c1 :**: uc2) . rightUnitorInv t c1)) ac1)
+  rightUnitorInv (Day t) (NatId a) =
+    Nat a LanHaskF (\z az -> LanHask (z :**: unitObject t) (rightUnitor t z) (az, unitObject t))
+  associator (Day t) _ _ _ =
+    Nat LanHaskF LanHaskF (\_ (LanHask (_e :**: d) eda (LanHask (b :**: c) bce (fb, gc), hd)) ->
+      let cd = c :**: d; tcd = t % cd
+      in LanHask (b :**: tcd) (eda . t % (bce :**: d) . associatorInv t b c d) (fb, LanHask cd tcd (gc, hd)))
+  associatorInv (Day t) _ _ _ =
+    Nat LanHaskF LanHaskF (\_ (LanHask (b :**: _c) bca (fb, LanHask (d :**: e) dec (gd, he))) ->
+      let bd = b :**: d; tbd = t % bd
+      in LanHask (tbd :**: e) (bca . t % (b :**: dec) . associator t b d e) (LanHask bd tbd (fb, gd), he))
+
+
 -- | @MonoidObject f a@ defines a monoid @a@ in a monoidal category with tensor product @f@.
 data MonoidObject f a = MonoidObject
-  { unit     :: Cod f (Unit f)        a
-  , multiply :: Cod f ((f :% (a, a))) a
+  { unit     :: Cod f (Unit f)      a
+  , multiply :: Cod f (f :% (a, a)) a
   }
 
 trivialMonoid :: TensorProduct f => f -> MonoidObject f (Unit f)
diff --git a/Data/Category/NNO.hs b/Data/Category/NNO.hs
--- a/Data/Category/NNO.hs
+++ b/Data/Category/NNO.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, UndecidableInstances, NoImplicitPrelude #-}
+{-# LANGUAGE TypeFamilies, GADTs, UndecidableInstances, NoImplicitPrelude #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Peano
@@ -10,6 +10,8 @@
 -----------------------------------------------------------------------------
 module Data.Category.NNO where
 
+import Data.Kind (Type)
+
 import Data.Category.Functor
 import Data.Category.Limit
 import Data.Category.Unit
@@ -18,24 +20,24 @@
 
 
 class HasTerminalObject k => HasNaturalNumberObject k where
-  
-  type NaturalNumberObject k :: *
-  
+
+  type NaturalNumberObject k :: Type
+
   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 +45,14 @@
 -- type Nat = Fix ((:++:) Unit)
 
 -- instance HasNaturalNumberObject Cat where
-  
+
 --   type NaturalNumberObject Cat = CatW Nat
-  
+
 --   zero = CatA (Const (Fix (I1 Unit)))
 --   succ = CatA (Wrap :.: Inj2)
-  
+
 --   primRec (CatA z) (CatA s) = CatA (PrimRec z s)
-  
+
 -- data PrimRec z s = PrimRec z s
 -- 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/NaturalTransformation.hs b/Data/Category/NaturalTransformation.hs
--- a/Data/Category/NaturalTransformation.hs
+++ b/Data/Category/NaturalTransformation.hs
@@ -16,6 +16,7 @@
   , (!)
   , o
   , natId
+  , pattern NatId
   , srcF
   , tgtF
 
@@ -42,12 +43,22 @@
   , EndoFunctorCompose
   , Precompose, pattern Precompose
   , Postcompose, pattern Postcompose
+  , Curry1, pattern Curry1
+  , Curry2, pattern Curry2
   , Wrap(..)
   , Apply(..)
   , Tuple(..)
+  , Opp(..), Opposite, pattern Opposite
+  , HomF, pattern HomF
+  , Star, pattern Star
+  , Costar, pattern Costar
+  , (:*%:), pattern HomXF
+  , (:%*:), pattern HomFX
 
 ) where
 
+import Data.Kind (Type)
+
 import Data.Category
 import Data.Category.Functor
 import Data.Category.Product
@@ -59,7 +70,7 @@
 
 -- | Natural transformations are built up of components,
 -- one for each object @z@ in the domain category of @f@ and @g@.
-data Nat :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where
+data Nat :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type where
   Nat :: (Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g)
     => f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
 
@@ -80,11 +91,12 @@
 
 -- | The identity natural transformation of a functor.
 natId :: Functor f => f -> Nat (Dom f) (Cod f) f f
-natId f = Nat f f (\i -> f % i)
+natId f = Nat f f (f %)
 
-pattern NatId :: Functor f => f -> Nat (Dom f) (Cod f) f f
-pattern NatId f <- Nat f _ _ where 
-  NatId f = Nat f f (\i -> f % i)
+pattern NatId :: () => (Functor f, c ~ Dom f, d ~ Cod f) => f -> Nat c d f f
+pattern NatId f <- Nat f _ _ where
+  NatId f = Nat f f (f %)
+{-# COMPLETE NatId #-}
 
 srcF :: Nat c d f g -> f
 srcF (Nat f _ _) = f
@@ -137,7 +149,7 @@
 constPostcompOut (Nat f (Const x :.: _) n) = Nat f (Const x) n
 
 
-data FunctorCompose (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) = FunctorCompose
+data FunctorCompose (c :: Type -> Type -> Type) (d :: Type -> Type -> Type) (e :: Type -> Type -> Type) = FunctorCompose
 
 -- | Composition of functors is a functor.
 instance (Category c, Category d, Category e) => Functor (FunctorCompose c d e) where
@@ -157,6 +169,7 @@
 
 type Profunctors c d = Nat (Op d :**: c) (->)
 
+
 -- | @Precompose f e@ is the functor such that @Precompose f e :% g = g :.: f@,
 --   for functors @g@ that compose with @f@ and with codomain @e@.
 type Precompose f e = FunctorCompose (Dom f) (Cod f) e :.: Tuple2 (Nat (Cod f) e) (Nat (Dom f) (Cod f)) f
@@ -166,10 +179,21 @@
 -- | @Postcompose f c@ is the functor such that @Postcompose f c :% g = f :.: g@,
 --   for functors @g@ that compose with @f@ and with domain @c@.
 type Postcompose f c = FunctorCompose c (Dom f) (Cod f) :.: Tuple1 (Nat (Dom f) (Cod f)) (Nat c (Dom f)) f
-pattern Postcompose :: (Category e, Functor f) => f -> Postcompose f e
+pattern Postcompose :: (Category c, Functor f) => f -> Postcompose f c
 pattern Postcompose f = FunctorCompose :.: Tuple1 (NatId f)
 
 
+type Curry1 c1 c2 f = Postcompose f c2 :.: Tuple c1 c2
+-- | Curry on the first "argument" of a functor from a product category.
+pattern Curry1 :: (Functor f, Dom f ~ c1 :**: c2, Category c1, Category c2) => f -> Curry1 c1 c2 f
+pattern Curry1 f = Postcompose f :.: Tuple
+
+type Curry2 c1 c2 f = Postcompose f c1 :.: Curry1 c2 c1 (Swap c2 c1)
+-- | Curry on the second "argument" of a functor from a product category.
+pattern Curry2 :: (Functor f, Dom f ~ c1 :**: c2, Category c1, Category c2) => f -> Curry2 c1 c2 f
+pattern Curry2 f = Postcompose f :.: Curry1 Swap
+
+
 data Wrap f h = Wrap f h
 
 -- | @Wrap f h@ is the functor such that @Wrap f h :% g = f :.: g :.: h@,
@@ -182,7 +206,7 @@
   Wrap f h % n = natId f `o` n `o` natId h
 
 
-data Apply (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Apply
+data Apply (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) = Apply
 -- | 'Apply' is a bifunctor, @Apply :% (f, a)@ applies @f@ to @a@, i.e. @f :% a@.
 instance (Category c1, Category c2) => Functor (Apply c1 c2) where
   type Dom (Apply c1 c2) = Nat c2 c1 :**: c2
@@ -190,10 +214,53 @@
   type Apply c1 c2 :% (f, a) = f :% a
   Apply % (l :**: r) = l ! r
 
-data Tuple (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Tuple
+data Tuple (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) = Tuple
 -- | 'Tuple' converts an object @a@ to the functor 'Tuple1' @a@.
 instance (Category c1, Category c2) => Functor (Tuple c1 c2) where
   type Dom (Tuple c1 c2) = c1
   type Cod (Tuple c1 c2) = Nat c2 (c1 :**: c2)
   type Tuple c1 c2 :% a = Tuple1 c1 c2 a
-  Tuple % f = Nat (Tuple1 (src f)) (Tuple1 (tgt f)) (\z -> f :**: z)
+  Tuple % f = Nat (Tuple1 (src f)) (Tuple1 (tgt f)) (f :**:)
+
+
+data Opp (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) = Opp
+-- | Turning a functor into its dual is contravariantly functorial.
+instance (Category c1, Category c2) => Functor (Opp c1 c2) where
+  type Dom (Opp c1 c2) = Op (Nat c1 c2) :**: Op c1
+  type Cod (Opp c1 c2) = Op c2
+  type Opp c1 c2 :% (f, a) = f :% a
+  Opp % (Op n :**: Op f) = Op (n ! f)
+
+type Opposite f = Opp (Dom f) (Cod f) :.: Tuple1 (Op (Nat (Dom f) (Cod f))) (Op (Dom f)) f
+-- | The dual of a functor
+pattern Opposite :: Functor f => f -> Opposite f
+pattern Opposite f = Opp :.: Tuple1 (Op (NatId f))
+{-# COMPLETE Opposite #-}
+
+
+type HomF f g = Hom (Cod f) :.: (Opposite f :***: g)
+pattern HomF :: (Functor f, Functor g, Cod f ~ Cod g) => f -> g -> HomF f g
+pattern HomF f g = Hom :.: (Opposite f :***: g)
+{-# COMPLETE HomF #-}
+
+type Star f = HomF (Id (Cod f)) f
+pattern Star :: Functor f => f -> Star f
+pattern Star f = HomF Id f
+{-# COMPLETE Star #-}
+
+type Costar f = HomF f (Id (Cod f))
+pattern Costar :: Functor f => f -> Costar f
+pattern Costar f = HomF f Id
+{-# COMPLETE Costar #-}
+
+type x :*%: f = (x :*-: Cod f) :.: f
+-- | The covariant functor Hom(X,F-)
+pattern HomXF :: Functor f => Obj (Cod f) x -> f -> x :*%: f
+pattern HomXF x f = HomX_ x :.: f
+{-# COMPLETE HomXF #-}
+
+type f :%*: x = (Cod f :-*: x) :.: Opposite f
+-- | The contravariant functor Hom(F-,X)
+pattern HomFX :: Functor f => f -> Obj (Cod f) x -> f :%*: x
+pattern HomFX f x = Hom_X x :.: Opposite f
+{-# COMPLETE HomFX #-}
diff --git a/Data/Category/Preorder.hs b/Data/Category/Preorder.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/Preorder.hs
@@ -0,0 +1,106 @@
+{-# LANGUAGE GADTs, TypeFamilies, PatternSynonyms, ScopedTypeVariables, RankNTypes, TypeOperators #-}
+module Data.Category.Preorder where
+
+import Prelude hiding ((.), id, Functor)
+
+import Data.Category
+import Data.Category.Limit
+import Data.Category.CartesianClosed
+import Data.Category.Functor
+import Data.Category.Adjunction
+import Data.Category.Enriched
+import Data.Category.Enriched.Functor
+import Data.Category.Enriched.Limit hiding (HasEnds(..))
+
+data Preorder a x y where
+  (:<=:) :: a -> a -> Preorder a x y
+
+pattern Obj :: a -> Preorder a x y
+pattern Obj a <- a :<=: _ where
+  Obj a = a :<=: a
+{-# COMPLETE Obj #-} -- Note: only complete for identity arrows `Obj Preorder a`
+
+unObj :: Obj (Preorder a) x -> a
+unObj (Obj a) = a
+
+instance Eq a => Category (Preorder a) where
+  src (s :<=: _) = Obj s
+  tgt (_ :<=: t) = Obj t
+  (b :<=: c) . (a :<=: b') = if b == b' then a :<=: c else error "Invalid composition"
+
+instance (Eq a, Bounded a) => HasInitialObject (Preorder a) where
+  type InitialObject (Preorder a) = ()
+  initialObject = Obj minBound
+  initialize (Obj a) = minBound :<=: a
+
+instance (Eq a, Bounded a) => HasTerminalObject (Preorder a) where
+  type TerminalObject (Preorder a) = ()
+  terminalObject = Obj maxBound
+  terminate (Obj a) = a :<=: maxBound
+
+instance Ord a => HasBinaryProducts (Preorder a) where
+  type BinaryProduct (Preorder a) x y = ()
+  proj1 (Obj a) (Obj b) = min a b :<=: a
+  proj2 (Obj a) (Obj b) = min a b :<=: b
+  (a :<=: x) &&& (_a :<=: y) = a :<=: min x y
+
+instance Ord a => HasBinaryCoproducts (Preorder a) where
+  type BinaryCoproduct (Preorder a) x y = ()
+  inj1 (Obj a) (Obj b) = a :<=: max a b
+  inj2 (Obj a) (Obj b) = b :<=: max a b
+  (x :<=: a) ||| (y :<=: _a) = max x y :<=: a
+
+-- | `ordExp a b` is the largest x such that min x a <= b
+ordExp :: (Ord a, Bounded a) => a -> a -> a
+ordExp a b = if a <= b then maxBound else b
+
+instance (Ord a, Bounded a) => CartesianClosed (Preorder a) where
+  type Exponential (Preorder a) x y = ()
+  apply (Obj a) (Obj b) = min (ordExp a b) a :<=: b
+  tuple (Obj a) (Obj b) = b :<=: ordExp a (min a b)
+  (z1 :<=: z2) ^^^ (y2 :<=: y1) = ordExp y1 z1 :<=: ordExp y2 z2
+
+
+class Category k => EnumObjs k where
+  enumObjs :: (forall a. Obj k a -> r) -> [r]
+
+glb :: (Ord a, Bounded a) => [a] -> a
+glb [] = maxBound
+glb xs = minimum xs
+
+
+type End' t = ()
+end
+  :: (VProfunctor k k t, V k ~ Preorder a, EnumObjs k, Ord a, Bounded a)
+  => t -> Obj (Preorder a) (End' t)
+end t = Obj $ glb (enumObjs (\a -> unObj (getSelf (t %% (EOp a :<>: a)))))
+
+endCounit
+  :: (VProfunctor k k t, V k ~ Preorder a, EnumObjs k, Ord a, Bounded a)
+  => t -> Obj k b -> Preorder a (End' t) (t :%% (b, b))
+endCounit t a = unObj (end t) :<=: unObj (getSelf (t %% (EOp a :<>: a)))
+
+endFactorizer
+  :: (VProfunctor k k t, V k ~ Preorder a, EnumObjs k, Ord a, Bounded a)
+  => t -> Obj (Preorder a) x -> (forall b. Obj k b -> Preorder a x (t :%% (b, b))) -> Preorder a x (End' t)
+endFactorizer _ (Obj x) f = x :<=: glb (enumObjs (\b -> case f b of _ :<=: tbb -> tbb))
+
+
+data Floor = Floor
+instance Functor Floor where
+  type Dom Floor = Preorder Double
+  type Cod Floor = Preorder Integer
+  type Floor :% a = ()
+  Floor % (a :<=: b) = floor a :<=: floor b
+
+data FromInteger = FromInteger
+instance Functor FromInteger where
+  type Dom FromInteger = Preorder Integer
+  type Cod FromInteger = Preorder Double
+  type FromInteger :% a = ()
+  FromInteger % (a :<=: b) = fromInteger a :<=: fromInteger b
+
+floorGaloisConnection :: Adjunction (Preorder Double) (Preorder Integer) FromInteger Floor
+floorGaloisConnection = mkAdjunction FromInteger Floor
+  (\(Obj a) (_fromIntegerA :<=: b) -> a :<=: floor b)
+  (\(Obj b) (a :<=: _floorB) -> fromInteger a :<=: b)
diff --git a/Data/Category/Product.hs b/Data/Category/Product.hs
--- a/Data/Category/Product.hs
+++ b/Data/Category/Product.hs
@@ -10,16 +10,18 @@
 -----------------------------------------------------------------------------
 module Data.Category.Product where
 
+import Data.Kind (Type)
+
 import Data.Category
 
 
-data (:**:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where
+data (:**:) :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type where
   (:**:) :: c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
 
 -- | The product category of categories @c1@ and @c2@.
 instance (Category c1, Category c2) => Category (c1 :**: c2) where
-  
+
   src (a1 :**: a2)            = src a1 :**: src a2
   tgt (a1 :**: a2)            = tgt a1 :**: tgt a2
-  
+
   (a1 :**: a2) . (b1 :**: b2) = (a1 . b1) :**: (a2 . b2)
diff --git a/Data/Category/RepresentableFunctor.hs b/Data/Category/RepresentableFunctor.hs
--- a/Data/Category/RepresentableFunctor.hs
+++ b/Data/Category/RepresentableFunctor.hs
@@ -42,7 +42,7 @@
   , universalElement   = x
   }
 
-type InitialUniversal x u a = Representable ((x :*-: Cod u) :.: u) a
+type InitialUniversal x u a = Representable (x :*%: u) a
 -- | An initial universal property, a universal morphism from x to u.
 initialUniversal :: Functor u
                  => u
@@ -50,14 +50,14 @@
                  -> Cod u x (u :% a)
                  -> (forall y. Obj (Dom u) y -> Cod u x (u :% y) -> Dom u a y)
                  -> InitialUniversal x u a
-initialUniversal u obj mor factorizer = Representable
-  { representedFunctor = HomX_ (src mor) :.: u
-  , representingObject = obj
+initialUniversal u ob mor factorizer = Representable
+  { representedFunctor = HomXF (src mor) u
+  , representingObject = ob
   , represent          = factorizer
   , universalElement   = mor
   }
 
-type TerminalUniversal x u a = Representable ((Cod u :-*: x) :.: Opposite u) a
+type TerminalUniversal x u a = Representable (u :%*: x) a
 -- | A terminal universal property, a universal morphism from u to x.
 terminalUniversal :: Functor u
                   => u
@@ -65,9 +65,9 @@
                   -> Cod u (u :% a) x
                   -> (forall y. Obj (Dom u) y -> Cod u (u :% y) x -> Dom u y a)
                   -> TerminalUniversal x u a
-terminalUniversal u obj mor factorizer = Representable
-  { representedFunctor = Hom_X (tgt mor) :.: Opposite u
-  , representingObject = Op obj
+terminalUniversal u ob mor factorizer = Representable
+  { representedFunctor = HomFX u (tgt mor)
+  , representingObject = Op ob
   , represent          = \(Op y) f -> Op (factorizer y f)
   , universalElement   = mor
   }
diff --git a/Data/Category/Simplex.hs b/Data/Category/Simplex.hs
--- a/Data/Category/Simplex.hs
+++ b/Data/Category/Simplex.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies, GADTs, RankNTypes, TypeOperators, UndecidableInstances, NoImplicitPrelude #-}
+{-# LANGUAGE TypeFamilies, GADTs, RankNTypes, TypeOperators, UndecidableInstances, LambdaCase, FlexibleContexts, NoImplicitPrelude #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Simplex
@@ -11,26 +11,29 @@
 -- The (augmented) simplex category.
 -----------------------------------------------------------------------------
 module Data.Category.Simplex (
-  
+
   -- * Simplex Category
     Simplex(..)
   , Z, S
   , suc
-  
+
   -- * Functor
   , Forget(..)
   , Fin(..)
   , Add(..)
-  
+
   -- * The universal monoid
   , universalMonoid
   , Replicate(..)
-        
+
 ) where
-  
+
+import Data.Kind (Type)
+
 import Data.Category
 import Data.Category.Product
 import Data.Category.Functor
+import Data.Category.NaturalTransformation
 import Data.Category.Monoidal
 import Data.Category.Limit
 
@@ -48,7 +51,7 @@
 --      XY----+
 --         x ->
 
-data Simplex :: * -> * -> * where
+data Simplex :: Type -> Type -> Type where
   Z ::                    Simplex    Z     Z
   Y :: Simplex x    y  -> Simplex    x  (S y)
   X :: Simplex x (S y) -> Simplex (S x) (S y)
@@ -63,11 +66,11 @@
   src Z = Z
   src (Y f) = src f
   src (X f) = suc (src f)
-  
+
   tgt Z = Z
   tgt (Y f) = suc (tgt f)
   tgt (X f) = tgt f
-  
+
   Z   .   f = f
   f   .   Z = f
   Y f .   g = Y (f . g)
@@ -78,9 +81,9 @@
 -- | The ordinal @0@ is the initial object of the simplex category.
 instance HasInitialObject Simplex where
   type InitialObject Simplex = Z
-  
+
   initialObject = Z
-  
+
   initialize Z = Z
   initialize (X (Y f)) = Y (initialize f)
 
@@ -94,7 +97,7 @@
   terminate (X (Y f)) = X (terminate f)
 
 
-data Fin :: * -> * where
+data Fin :: Type -> Type where
   Fz ::          Fin (S n)
   Fs :: Fin n -> Fin (S n)
 
@@ -104,9 +107,9 @@
   type Dom Forget = Simplex
   type Cod Forget = (->)
   type Forget :% n = Fin n
-  Forget % Z   = \x -> x
-  Forget % Y f = \x -> Fs ((Forget % f) x)
-  Forget % X f = \x -> case x of
+  Forget % Z   = obj
+  Forget % Y f = Fs . (Forget % f)
+  Forget % X f = \case
     Fz -> Fz
     Fs n -> (Forget % f) n
 
@@ -126,7 +129,7 @@
 instance TensorProduct Add where
   type Unit Add = Z
   unitObject Add = Z
-  
+
   leftUnitor     Add       a   = a
   leftUnitorInv  Add       a   = a
   rightUnitor    Add       Z   = Z
@@ -160,3 +163,11 @@
       n' = Replicate f m % X n
       a = tgt (unit m)
       b = src (Replicate f m % n)
+
+data Cobar f d = Cobar (Monad f) (Obj (Dom f) d)
+-- | The cobar construction
+instance Category (Dom f) => Functor (Cobar f d) where
+  type Dom (Cobar f d) = Simplex
+  type Cod (Cobar f d) = Dom f
+  type Cobar f d :% s = (Replicate (EndoFunctorCompose (Dom f)) f :% s) :% d
+  Cobar f d % s = (Replicate FunctorCompose f % s) ! d
diff --git a/Data/Category/Void.hs b/Data/Category/Void.hs
--- a/Data/Category/Void.hs
+++ b/Data/Category/Void.hs
@@ -10,6 +10,8 @@
 -----------------------------------------------------------------------------
 module Data.Category.Void where
 
+import Data.Kind (Type)
+
 import Data.Category
 import Data.Category.Functor
 import Data.Category.NaturalTransformation
@@ -34,7 +36,7 @@
 voidNat f g = Nat f g magic
 
 
-data Magic (k :: * -> * -> *) = Magic
+data Magic (k :: Type -> Type -> Type) = Magic
 -- | Since there is nothing to map in `Void`, there's a functor from it to any other category.
 instance Category k => Functor (Magic k) where
   type Dom (Magic k) = Void
diff --git a/Data/Category/WeightedLimit.hs b/Data/Category/WeightedLimit.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/WeightedLimit.hs
@@ -0,0 +1,142 @@
+{-# LANGUAGE TypeOperators, RankNTypes, GADTs, TypeFamilies, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, NoImplicitPrelude, FlexibleContexts #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Category.WeightedLimit
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  sjoerd@w3future.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+-----------------------------------------------------------------------------
+module Data.Category.WeightedLimit where
+
+import Data.Kind (Type)
+
+import Data.Category
+import Data.Category.Functor
+import Data.Category.Product
+import Data.Category.NaturalTransformation
+import qualified Data.Category.Limit as L
+
+
+type WeightedCone w d e = forall a. Obj (Dom w) a -> w :% a -> Cod d e (d :% a)
+
+-- | @w@-weighted limits in the category @k@.
+class (Functor w, Cod w ~ (->), Category k) => HasWLimits k w where
+  type WeightedLimit k w d :: Type
+  limitObj :: FunctorOf (Dom w) k d => w -> d -> Obj k (WLimit w d)
+  limit :: FunctorOf (Dom w) k d => w -> d -> WeightedCone w d (WLimit w d)
+  limitFactorizer :: FunctorOf (Dom w) k d => w -> d -> Obj k e -> WeightedCone w d e -> k e (WLimit w d)
+
+type WLimit w d = WeightedLimit (Cod d) w d
+
+data LimitFunctor (k :: Type -> Type -> Type) w = LimitFunctor w
+instance HasWLimits k w => Functor (LimitFunctor k w) where
+  type Dom (LimitFunctor k w) = Nat (Dom w) k
+  type Cod (LimitFunctor k w) = k
+  type LimitFunctor k w :% d = WeightedLimit k w d
+
+  LimitFunctor w % Nat d d' n = limitFactorizer w d' (limitObj w d) (\a wa -> n a . limit w d a wa)
+
+
+-- | Regular limits as weigthed limits, weighted by the constant functor to '()'.
+instance L.HasLimits j k => HasWLimits k (Const j (->) ()) where
+  type WeightedLimit k (Const j (->) ()) d = L.Limit d
+  limitObj Const{} d = L.coneVertex (L.limit (natId d))
+  limit Const{} d a () = L.limit (natId d) ! a
+  limitFactorizer Const{} d e f = L.limitFactorizer (Nat (Const e) d (`f` ()))
+
+
+class Category v => HasEnds v where
+  type End (v :: Type -> Type -> Type) t :: Type
+  end :: FunctorOf (Op k :**: k) v t => t -> Obj v (End v t)
+  endCounit :: FunctorOf (Op k :**: k) v t => t -> Obj k a -> v (End v t) (t :% (a, a))
+  endFactorizer :: FunctorOf (Op k :**: k) v t => t -> (forall a. Obj k a -> v x (t :% (a, a))) -> v x (End v t)
+
+-- | Ends as Hom-weighted limits
+instance HasEnds k => HasWLimits k (Hom k) where
+  type WeightedLimit k (Hom k) d = End k d
+  limitObj Hom d = end d
+  limit Hom d (Op a :**: _) ab = d % (Op a :**: ab) . endCounit d a
+  limitFactorizer Hom d _ f = endFactorizer d (\a -> f (Op a :**: a) a)
+
+data EndFunctor (k :: Type -> Type -> Type) (v :: Type -> Type -> Type) = EndFunctor
+instance (HasEnds v, Category k) => Functor (EndFunctor k v) where
+  type Dom (EndFunctor k v) = Nat (Op k :**: k) v
+  type Cod (EndFunctor k v) = v
+  type EndFunctor k v :% t = End v t
+
+  EndFunctor % Nat f g n = endFactorizer g (\a -> n (Op a :**: a) . endCounit f a)
+
+newtype HaskEnd t = HaskEnd { getHaskEnd :: forall k a. FunctorOf (Op k :**: k) (->) t => t -> Obj k a -> t :% (a, a) }
+instance HasEnds (->) where
+  type End (->) t = HaskEnd t
+  end _ e = e
+  endCounit t a (HaskEnd f) = f t a
+  endFactorizer _ e x = HaskEnd (\_ a -> e a x)
+
+
+type WeightedCocone w d e = forall a. Obj (Dom w) a -> w :% a -> Cod d (d :% a) e
+
+-- | @w@-weighted colimits in the category @k@.
+class (Functor w, Cod w ~ (->), Category k) => HasWColimits k w where
+  type WeightedColimit k w d :: Type
+  colimitObj :: (FunctorOf j k d, Op j ~ Dom w) => w -> d -> Obj k (WColimit w d)
+  colimit :: (FunctorOf j k d, Op j ~ Dom w) => w -> d -> WeightedCocone w d (WColimit w d)
+  colimitFactorizer :: (FunctorOf j k d, Op j ~ Dom w) => w -> d -> Obj k e -> WeightedCocone w d e -> k (WColimit w d) e
+
+type WColimit w d = WeightedColimit (Cod d) w d
+
+data ColimitFunctor (k :: Type -> Type -> Type) w = ColimitFunctor w
+instance (Functor w, Category k, HasWColimits k (w :.: OpOp (Dom w))) => Functor (ColimitFunctor k w) where
+  type Dom (ColimitFunctor k w) = Nat (Op (Dom w)) k
+  type Cod (ColimitFunctor k w) = k
+  type ColimitFunctor k w :% d = WeightedColimit k (w :.: OpOp (Dom w)) d
+
+  ColimitFunctor w % Nat d d' n = colimitFactorizer (w :.: OpOp) d (colimitObj (w :.: OpOp) d') (\(Op a) wa -> colimit (w :.: OpOp) d' (Op a) wa . n a)
+
+
+-- | Regular colimits as weigthed colimits, weighted by the constant functor to '()'.
+instance L.HasColimits j k => HasWColimits k (Const (Op j) (->) ()) where
+  type WeightedColimit k (Const (Op j) (->) ()) d = L.Colimit d
+  colimitObj (Const _) d = L.coconeVertex (L.colimit (natId d))
+  colimit (Const _) d (Op a) () = L.colimit (natId d) ! a
+  colimitFactorizer (Const _) d e f = L.colimitFactorizer (Nat d (Const e) (\z -> f (Op z) ()))
+
+
+class Category v => HasCoends v where
+  type Coend (v :: Type -> Type -> Type) t :: Type
+  coend :: FunctorOf (Op k :**: k) v t => t -> Obj v (Coend v t)
+  coendCounit :: FunctorOf (Op k :**: k) v t => t -> Obj k a -> v (t :% (a, a)) (Coend v t)
+  coendFactorizer :: FunctorOf (Op k :**: k) v t => t -> (forall a. Obj k a -> v (t :% (a, a)) x) -> v (Coend v t) x
+
+data OpHom (k :: Type -> Type -> Type) = OpHom
+-- | The Hom-functor but with opposite domain.
+instance Category k => Functor (OpHom k) where
+  type Dom (OpHom k) = Op (Op k :**: k)
+  type Cod (OpHom k) = (->)
+  type OpHom k :% (a1, a2) = k a2 a1
+  OpHom % Op (Op f1 :**: f2) = \g -> f1 . g . f2
+
+-- | Coends as OpHom-weighted colimits
+instance HasCoends k => HasWColimits k (OpHom k) where
+  type WeightedColimit k (OpHom k) d = Coend k d
+  colimitObj OpHom d = coend d
+  colimit OpHom d (Op (Op a :**: _)) ab = coendCounit d a . d % (Op a :**: ab)
+  colimitFactorizer OpHom d _ f = coendFactorizer d (\a -> f (Op (Op a :**: a)) a)
+
+data CoendFunctor (k :: Type -> Type -> Type) (v :: Type -> Type -> Type) = CoendFunctor
+instance (HasCoends v, Category k) => Functor (CoendFunctor k v) where
+  type Dom (CoendFunctor k v) = Nat (Op k :**: k) v
+  type Cod (CoendFunctor k v) = v
+  type CoendFunctor k v :% t = Coend v t
+
+  CoendFunctor % Nat f g n = coendFactorizer f (\a -> coendCounit g a . n (Op a :**: a))
+
+data HaskCoend t where
+  HaskCoend :: FunctorOf (Op k :**: k) (->) t => t -> Obj k a -> t :% (a, a) -> HaskCoend t
+instance HasCoends (->) where
+  type Coend (->) t = HaskCoend t
+  coend _ e = e
+  coendCounit t a taa = HaskCoend t a taa
+  coendFactorizer _ f (HaskCoend _ a taa) = f a taa
diff --git a/Data/Category/Yoneda.hs b/Data/Category/Yoneda.hs
--- a/Data/Category/Yoneda.hs
+++ b/Data/Category/Yoneda.hs
@@ -10,21 +10,20 @@
 -----------------------------------------------------------------------------
 module Data.Category.Yoneda where
 
+import Data.Kind (Type)
+
 import Data.Category
 import Data.Category.Functor
 import Data.Category.NaturalTransformation
 import Data.Category.Adjunction
 
-type YonedaEmbedding k =
-  Postcompose (Hom k) (Op k) :.:
-  (Postcompose (Swap k (Op k)) (Op k) :.: Tuple k (Op k))
-
+type YonedaEmbedding k = Curry2 (Op k) k (Hom k)
 -- | The Yoneda embedding functor, @C -> Set^(C^op)@.
 pattern YonedaEmbedding :: Category k => YonedaEmbedding k
-pattern YonedaEmbedding = Postcompose Hom :.: (Postcompose Swap :.: Tuple)
+pattern YonedaEmbedding = Curry2 Hom
 
 
-data Yoneda (k :: * -> * -> *) f = Yoneda
+data Yoneda (k :: Type -> Type -> Type) f = Yoneda
 -- | 'Yoneda' converts a functor @f@ into a natural transformation from the hom functor to f.
 instance (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => Functor (Yoneda k f) where
   type Dom (Yoneda k f) = Op k
@@ -40,8 +39,9 @@
 toYoneda   :: (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => f -> Nat (Op k) (->) f (Yoneda k f)
 toYoneda   f = Nat f Yoneda (\(Op a) fa -> Nat (Hom_X a) f (\_ h -> (f % Op h) fa))
 
+
 haskUnit :: Obj (->) ()
-haskUnit () = ()
+haskUnit = obj
 
 data M1 = M1
 instance Functor M1 where
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.10
+version:             0.11
 synopsis:            Category theory
 
 description:         Data-category is a collection of categories, and some categorical constructions on them.
@@ -38,19 +38,29 @@
     Data.Category.RepresentableFunctor,
     Data.Category.Adjunction,
     Data.Category.Limit,
+    Data.Category.WeightedLimit,
     Data.Category.KanExtension,
     Data.Category.Monoidal,
     Data.Category.CartesianClosed,
-    Data.Category.Enriched,
     Data.Category.Yoneda,
     Data.Category.Boolean,
+    Data.Category.Fin,
     Data.Category.Fix,
     Data.Category.Kleisli,
     Data.Category.Dialg,
     Data.Category.NNO,
     Data.Category.Simplex,
     Data.Category.Cube,
-    Data.Category.Comma
+    Data.Category.Comma,
+    Data.Category.Preorder,
+    Data.Category.Enriched,
+    Data.Category.Enriched.Functor,
+    Data.Category.Enriched.Limit,
+    Data.Category.Enriched.Yoneda,
+    Data.Category.Enriched.Poset3
+  build-depends:
+    base >=4.15 && <5,
+    ghc-prim
 
   default-language:    Haskell2010