diff --git a/Data/Category.hs b/Data/Category.hs
--- a/Data/Category.hs
+++ b/Data/Category.hs
@@ -54,5 +54,7 @@
 
   (Op a) . (Op b) = Op (b . a)
 
-type family Kind (cat :: k -> k -> *) :: * where
-  Kind (cat :: k -> k -> *) = k
+
+-- | @Kind k@ is the kind of the objects of the category @k@.
+type family Kind (k :: o -> o -> *) :: * where
+  Kind (k :: o -> o -> *) = o
diff --git a/Data/Category/Adjunction.hs b/Data/Category/Adjunction.hs
--- a/Data/Category/Adjunction.hs
+++ b/Data/Category/Adjunction.hs
@@ -14,8 +14,8 @@
     Adjunction(..)
   , mkAdjunction
   , mkAdjunctionUnits
-  , mkAdjunctionUnit
-  , mkAdjunctionCounit
+  , mkAdjunctionInit
+  , mkAdjunctionTerm
 
   , leftAdjunct
   , rightAdjunct
@@ -27,14 +27,6 @@
   , composeAdj
   , AdjArrow(..)
 
-  -- * Adjunctions from universal morphisms
-  , initialPropAdjunction
-  , terminalPropAdjunction
-
-  -- * Universal morphisms from adjunctions
-  , adjunctionInitialProp
-  , adjunctionTerminalProp
-
   -- * Examples
   , precomposeAdj
   , postcomposeAdj
@@ -46,7 +38,6 @@
 import Data.Category.Functor
 import Data.Category.Product
 import Data.Category.NaturalTransformation
-import Data.Category.RepresentableFunctor
 
 data Adjunction c d f g = (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
   => Adjunction
@@ -56,6 +47,7 @@
   , rightAdjunctN :: Profunctors c d (Star g) (Costar f)
   }
 
+-- | Make an adjunction from the hom-set isomorphism.
 mkAdjunction :: (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
   => f -> g
   -> (forall a b. Obj d a -> c (f :% a) b -> d a (g :% b))
@@ -63,6 +55,7 @@
   -> Adjunction c d f g
 mkAdjunction f g l r = Adjunction f g (Nat (Costar f) (Star g) (\(Op a :**: _) -> l a)) (Nat (Star g) (Costar f) (\(_ :**: b) -> r b))
 
+-- | Make an adjunction from the unit and counit.
 mkAdjunctionUnits :: (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
   => f -> g
   -> (forall a. Obj d a -> Component (Id d) (g :.: f) a)
@@ -70,19 +63,21 @@
   -> Adjunction c d f g
 mkAdjunctionUnits f g un coun = mkAdjunction f g (\a h -> (g % h) . un a) (\b h -> coun b . (f % h))
 
-mkAdjunctionUnit :: (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
+-- | Make an adjunction from an initial universal property.
+mkAdjunctionInit :: (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
   => f -> g
-  -> (forall a. Obj d a -> Component (Id d) (g :.: f) a)
+  -> (forall a. Obj d a -> d a (g :% (f :% a)))
   -> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b)
   -> Adjunction c d f g
-mkAdjunctionUnit f g un adj = mkAdjunction f g (\a h -> (g % h) . un a) adj
+mkAdjunctionInit f g un adj = mkAdjunction f g (\a h -> (g % h) . un a) adj
 
-mkAdjunctionCounit :: (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
+-- | Make an adjunction from a terminal universal property.
+mkAdjunctionTerm :: (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
   => f -> g
   -> (forall a b. Obj d a -> c (f :% a) b -> d a (g :% b))
-  -> (forall a. Obj c a -> Component (f :.: g) (Id c) a)
+  -> (forall b. Obj c b -> c (f :% (g :% b)) b)
   -> Adjunction c d f g
-mkAdjunctionCounit f g adj coun = mkAdjunction f g adj (\b h -> coun b . (f % h))
+mkAdjunctionTerm f g adj coun = mkAdjunction f g adj (\b h -> coun b . (f % h))
 
 leftAdjunct :: Adjunction c d f g -> Obj d a -> c (f :% a) b -> d a (g :% b)
 leftAdjunct (Adjunction _ _ l _) a h = (l ! (Op a :**: tgt h)) h
@@ -93,28 +88,6 @@
 adjunctionUnit adj@(Adjunction f g _ _) = Nat Id (g :.: f) (\a -> leftAdjunct adj a (f % a))
 adjunctionCounit :: Adjunction c d f g -> Nat c c (f :.: g) (Id c)
 adjunctionCounit adj@(Adjunction f g _ _) = Nat (f :.: g) Id (\b -> rightAdjunct adj b (g % b))
-
--- Each pair (FY, unit_Y) is an initial morphism from Y to G.
-adjunctionInitialProp :: Adjunction c d f g -> Obj d y -> InitialUniversal y g (f :% y)
-adjunctionInitialProp adj@(Adjunction f g _ _) y = initialUniversal g (f % y) (adjunctionUnit adj ! y) (rightAdjunct adj)
-
--- Each pair (GX, counit_X) is a terminal morphism from F to X.
-adjunctionTerminalProp :: Adjunction c d f g -> Obj c x -> TerminalUniversal x f (g :% x)
-adjunctionTerminalProp adj@(Adjunction f g _ _) x = terminalUniversal f (g % x) (adjunctionCounit adj ! x) (leftAdjunct adj)
-
-
-
-initialPropAdjunction :: forall f g c d. (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
-  => f -> g -> (forall y. Obj d y -> InitialUniversal y g (f :% y)) -> Adjunction c d f g
-initialPropAdjunction f g univ = mkAdjunctionUnits f g
-  (universalElement . univ)
-  (\a -> represent (univ (g % a)) a (g % a))
-
-terminalPropAdjunction :: forall f g c d. (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
-  => f -> g -> (forall x. Obj c x -> TerminalUniversal x f (g :% x)) -> Adjunction c d f g
-terminalPropAdjunction f g univ = mkAdjunctionUnits f g
-  (\a -> unOp (represent (univ (f % a)) (Op a) (f % a)))
-  (universalElement . univ)
 
 
 idAdj :: Category k => Adjunction k k (Id k) (Id k)
diff --git a/Data/Category/Enriched.hs b/Data/Category/Enriched.hs
--- a/Data/Category/Enriched.hs
+++ b/Data/Category/Enriched.hs
@@ -9,8 +9,6 @@
   , UndecidableInstances
   , ScopedTypeVariables
   , ConstraintKinds
-  , AllowAmbiguousTypes
-  , TypeApplications
   #-}
 -----------------------------------------------------------------------------
 -- |
@@ -33,7 +31,7 @@
 
 -- | An enriched category
 class CartesianClosed (V k) => ECategory (k :: * -> * -> *) where
-  -- | The tensor product of the category V which k is enriched in
+  -- | The category V which k is enriched in
   type V k :: * -> * -> *
 
   -- | The hom object in V from a to b
@@ -44,13 +42,8 @@
   comp :: Obj k a -> Obj k b -> Obj k c -> V k (BinaryProduct (V k) (k $ (b, c)) (k $ (a, b))) (k $ (a, c))
 
 
--- | The elements of @k@ as a functor from @V k@ to @(->)@ 
-type Elem k = TerminalObject (V k) :*-: (V k)
-elem :: CartesianClosed (V k) => Elem k
-elem = HomX_ terminalObject
-
 -- | Arrows as elements of @k@
-type Arr k a b = Elem k :% (k $ (a, b))
+type Arr k a b = V k (TerminalObject (V k)) (k $ (a, b))
 
 compArr :: ECategory k => Obj k a -> Obj k b -> Obj k c -> Arr k b c -> Arr k a b -> Arr k a c
 compArr a b c f g = comp a b c . (f &&& g)
@@ -76,17 +69,17 @@
 
 data (:<>:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where
   (:<>:) :: (V k1 ~ V k2) => Obj k1 a1 -> Obj k2 a2 -> (:<>:) k1 k2 (a1, a2) (a1, a2)
-  
+
 -- | The enriched product category of enriched categories @c1@ and @c2@.
 instance (ECategory k1, ECategory k2, V k1 ~ V k2) => ECategory (k1 :<>: k2) where
   type V (k1 :<>: k2) = V k1
   type (k1 :<>: k2) $ ((a1, a2), (b1, b2)) = BinaryProduct (V k1) (k1 $ (a1, b1)) (k2 $ (a2, b2))
   hom (a1 :<>: a2) (b1 :<>: b2) = hom a1 b1 *** hom a2 b2
   id (a1 :<>: a2) = id a1 &&& id a2
-  comp (a1 :<>: a2) (b1 :<>: b2) (c1 :<>: c2) = 
-    comp a1 b1 c1 . (proj1 bc1 bc2 . proj1 l r &&& proj1 ab1 ab2 . proj2 l r) &&& 
+  comp (a1 :<>: a2) (b1 :<>: b2) (c1 :<>: c2) =
+    comp a1 b1 c1 . (proj1 bc1 bc2 . proj1 l r &&& proj1 ab1 ab2 . proj2 l r) &&&
     comp a2 b2 c2 . (proj2 bc1 bc2 . proj1 l r &&& proj2 ab1 ab2 . proj2 l r)
-    where 
+    where
       ab1 = hom a1 b1
       ab2 = hom a2 b2
       bc1 = hom b1 c1
@@ -209,8 +202,8 @@
   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
@@ -259,8 +252,8 @@
   end :: (VProfunctor k k t, V k ~ v) => t -> Obj v (End v t)
   endCounit :: (VProfunctor k k t, V k ~ v) => t -> Obj k a -> v (End v t) (t :%% (a, a))
   endFactorizer :: (VProfunctor k k t, V k ~ v) => t -> (forall a. Obj k a -> v x (t :%% (a, a))) -> v x (End v t)
-  
 
+
 newtype HaskEnd t = HaskEnd { getHaskEnd :: forall k a. VProfunctor k k t => t -> Obj k a -> t :%% (a, a) }
 type instance End (->) t = HaskEnd t
 instance HasEnds (->) where
@@ -281,7 +274,7 @@
   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) 
+  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))
 
 
@@ -291,10 +284,10 @@
   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 -> 
+  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
@@ -312,14 +305,14 @@
   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)) 
+  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 
+  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))
 
 
diff --git a/Data/Category/Functor.hs b/Data/Category/Functor.hs
--- a/Data/Category/Functor.hs
+++ b/Data/Category/Functor.hs
@@ -1,4 +1,17 @@
-{-# LANGUAGE PolyKinds, TypeOperators, TypeFamilies, PatternSynonyms, FlexibleContexts, FlexibleInstances, UndecidableInstances, GADTs, RankNTypes, ConstraintKinds, NoImplicitPrelude #-}
+{-# LANGUAGE
+    GADTs
+  , PolyKinds
+  , RankNTypes
+  , ConstraintKinds
+  , NoImplicitPrelude
+  , TypeOperators
+  , TypeFamilies
+  , PatternSynonyms
+  , FlexibleContexts
+  , FlexibleInstances
+  , UndecidableInstances
+  , GeneralizedNewtypeDeriving
+  #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Functor
@@ -24,6 +37,7 @@
   , Opposite(..)
   , OpOp(..)
   , OpOpInv(..)
+  , Any(..)
 
   -- *** Related to the product category
   , Proj1(..)
@@ -155,6 +169,10 @@
   type OpOpInv k :% a = a
 
   OpOpInv % f = Op (Op f)
+
+
+-- | A functor wrapper in case of conflicting family instance declarations
+newtype Any f = Any f deriving Functor
 
 
 data Proj1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Proj1
diff --git a/Data/Category/KanExtension.hs b/Data/Category/KanExtension.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/KanExtension.hs
@@ -0,0 +1,157 @@
+{-# LANGUAGE
+    FlexibleInstances
+  , GADTs
+  , MultiParamTypeClasses
+  , RankNTypes
+  , TypeOperators
+  , TypeFamilies
+  , UndecidableInstances
+  , NoImplicitPrelude
+  #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Category.KanExtension
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  sjoerd@w3future.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+-----------------------------------------------------------------------------
+module Data.Category.KanExtension where
+
+import Data.Category
+import Data.Category.Functor
+import Data.Category.NaturalTransformation
+import Data.Category.Adjunction
+import Data.Category.Limit
+import Data.Category.Unit
+
+-- | The right Kan extension of a functor @p@ for functors @f@ with codomain @k@.
+type family RanFam (p :: *) (k :: * -> * -> *) (f :: *) :: *
+
+type Ran p f = RanFam p (Cod f) f
+
+-- | 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
+  -- | '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.
+  ranFactorizer :: Nat (Dom p) k (h :.: p) f -> Nat (Cod p) k h (RanFam p k f)
+
+ranF :: HasRightKan p k => p -> Obj (Nat (Dom p) k) f -> Obj (Nat (Cod p) k) (RanFam p k f)
+ranF p f = ranF' (ran p f)
+
+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
+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
+  type RanFunctor p k :% f = RanFam p k f
+
+  RanFunctor p % n = ranFactorizer (n . ran p (src n))
+
+-- | The right Kan extension along @p@ is right adjoint to precomposition with @p@.
+ranAdj :: forall p k. HasRightKan p k => p -> Adjunction (Nat (Dom p) k) (Nat (Cod p) k) (Precompose p k) (RanFunctor p k)
+ranAdj p = mkAdjunctionTerm (Precompose p) (RanFunctor p) (\_ -> ranFactorizer) (ran p)
+
+
+-- | The left Kan extension of a functor @p@ for functors @f@ with codomain @k@.
+type family LanFam (p :: *) (k :: * -> * -> *) (f :: *) :: *
+
+type Lan p f = LanFam p (Cod f) f
+
+-- | 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
+  -- | '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.
+  lanFactorizer :: Nat (Dom p) k f (h :.: p) -> Nat (Cod p) k (LanFam p k f) h
+
+lanF :: HasLeftKan p k => p -> Obj (Nat (Dom p) k) f -> Obj (Nat (Cod p) k) (LanFam p k f)
+lanF p f = lanF' (lan p f)
+
+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
+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
+  type LanFunctor p k :% f = LanFam p k f
+
+  LanFunctor p % n = lanFactorizer (lan p (tgt n) . n)
+
+-- | The left Kan extension along @p@ is left adjoint to precomposition with @p@.
+lanAdj :: forall p k. HasLeftKan p k => p -> Adjunction (Nat (Cod p) k) (Nat (Dom p) k) (LanFunctor p k) (Precompose p k)
+lanAdj p = mkAdjunctionInit (LanFunctor p) (Precompose p) (lan p) (\_ -> lanFactorizer)
+
+
+type instance RanFam (Const j Unit ()) k f = Const Unit k (LimitFam j k f)
+-- | The right Kan extension of @f@ along a functor to the unit category is the limit of @f@.
+instance HasLimits j k => HasRightKan (Const j Unit ()) k where
+  ran p f@Nat{} = let cone = limit f in Nat (Const (coneVertex cone) :.: p) (srcF f) (cone !)
+  ranFactorizer n@(Nat (h :.: _) f _) = let fact = limitFactorizer (constPrecompIn n) in Nat h (Const (tgt fact)) (\Unit -> fact)
+
+type instance LanFam (Const j Unit ()) k f = Const Unit k (ColimitFam j k f)
+-- | The left Kan extension of @f@ along a functor to the unit category is the colimit of @f@.
+instance HasColimits j k => HasLeftKan (Const j Unit ()) k where
+  lan p f@Nat{} = let cocone = colimit f in Nat (srcF f) (Const (coconeVertex cocone) :.: p) (cocone !)
+  lanFactorizer n@(Nat f (h :.: _) _) = let fact = colimitFactorizer (constPrecompOut n) in Nat (Const (src fact)) h (\Unit -> fact)
+
+
+type instance RanFam (Id j) k f = f
+-- | Ran id = id
+instance (Category j, Category k) => HasRightKan (Id j) k where
+  ran Id (Nat f _ _) = idPrecomp f
+  ranFactorizer n@(Nat (h :.: Id) _ _) = n . idPrecompInv h
+
+type instance LanFam (Id j) k f = f
+-- | Lan id = id
+instance (Category j, Category k) => HasLeftKan (Id j) k where
+  lan Id (Nat f _ _) = idPrecompInv f
+  lanFactorizer n@(Nat _ (h :.: Id) _) = idPrecomp h . n
+
+
+type instance RanFam (q :.: p) k f = RanFam q k (RanFam p k f)
+-- | Ran (q . p) = Ran q . Ran p
+instance (HasRightKan q k, HasRightKan p k) => HasRightKan (q :.: p) k where
+  ran (q :.: p) f = let ranp = ran p f in case ran q (ranF' ranp) of
+      ranq@(Nat (r :.: _) _ _) -> ranp . (ranq `o` natId p) . compAssocInv r q p
+  ranFactorizer n@(Nat (h :.: (q :.: p)) _ _) = ranFactorizer (ranFactorizer (n . compAssoc h q p))
+
+type instance LanFam (q :.: p) k f = LanFam q k (LanFam p k f)
+-- | Lan (q . p) = Lan q . Lan p
+instance (HasLeftKan q k, HasLeftKan p k) => HasLeftKan (q :.: p) k where
+  lan (q :.: p) f = let lanp = lan p f in case lan q (lanF' lanp) of
+      lanq@(Nat _ (l :.: _) _) -> compAssoc l q p . (lanq `o` natId p) . lanp
+  lanFactorizer n@(Nat _ (h :.: (q :.: p)) _) = lanFactorizer (lanFactorizer (compAssocInv h q p . n))
+
+
+newtype RanHask p f a = RanHask (forall c. Obj (Dom p) c -> Cod p a (p :% c) -> f :% c)
+data RanHaskF p f = RanHaskF
+instance Functor p => Functor (RanHaskF p f) where
+  type Dom (RanHaskF p f) = Cod p
+  type Cod (RanHaskF p f) = (->)
+  type RanHaskF p f :% a = RanHask p f a
+  RanHaskF % ab = \(RanHask r) -> RanHask (\c bpc -> r c (bpc . ab))
+
+type instance RanFam (Any p) (->) f = RanHaskF p f
+instance Functor p => HasRightKan (Any p) (->) where
+  ran (Any p) (Nat f _ _) = Nat (RanHaskF :.: Any p) f (\z (RanHask r) -> r z (p % z))
+  ranFactorizer (Nat (h :.: Any p) f n) = Nat h RanHaskF (\z hz -> RanHask (\c zpc -> n c ((h % zpc) hz)))
+
+data LanHask p f a where
+  LanHask :: Obj (Dom p) c -> Cod p (p :% c) a -> f :% c -> LanHask p f a
+data LanHaskF p f = LanHaskF
+instance Functor p => Functor (LanHaskF p f) where
+  type Dom (LanHaskF p f) = Cod p
+  type Cod (LanHaskF p f) = (->)
+  type LanHaskF p f :% a = LanHask p f a
+  LanHaskF % ab = \(LanHask c pca fc) -> LanHask c (ab . pca) fc
+
+type instance LanFam (Any p) (->) f = LanHaskF p f
+instance Functor p => HasLeftKan (Any p) (->) where
+  lan (Any p) (Nat f _ _) = Nat f (LanHaskF :.: Any p) (\z fz -> LanHask z (p % z) fz)
+  lanFactorizer (Nat f (h :.: Any p) n) = Nat LanHaskF h (\z (LanHask c pcz fc) -> (h % pcz) (n c fc))
diff --git a/Data/Category/Kleisli.hs b/Data/Category/Kleisli.hs
--- a/Data/Category/Kleisli.hs
+++ b/Data/Category/Kleisli.hs
@@ -52,4 +52,4 @@
 
 kleisliAdj :: (Functor m, Dom m ~ k, Cod m ~ k)
   => Monad m -> A.Adjunction (Kleisli m) k (KleisliFree m) (KleisliForget m)
-kleisliAdj m = A.mkAdjunctionUnit (KleisliFree m) KleisliForget (unit m !) (\(Kleisli _ x _) f -> Kleisli m x f)
+kleisliAdj m = A.mkAdjunctionInit (KleisliFree m) KleisliForget (unit m !) (\(Kleisli _ x _) f -> Kleisli m x f)
diff --git a/Data/Category/Limit.hs b/Data/Category/Limit.hs
--- a/Data/Category/Limit.hs
+++ b/Data/Category/Limit.hs
@@ -136,7 +136,7 @@
   --   by returning the morphism between the vertices of the cones.
   limitFactorizer :: Cone j k f n -> k n (LimitFam j k f)
 
-data LimitFunctor (j :: * -> * -> *) (k  :: * -> * -> *) = LimitFunctor
+data LimitFunctor (j :: * -> * -> *) (k :: * -> * -> *) = 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
@@ -148,7 +148,7 @@
 
 -- | The limit functor is right adjoint to the diagonal functor.
 limitAdj :: forall j k. HasLimits j k => Adjunction (Nat j k) k (Diag j k) (LimitFunctor j k)
-limitAdj = mkAdjunctionCounit Diag LimitFunctor (\_ -> limitFactorizer) limit
+limitAdj = mkAdjunctionTerm Diag LimitFunctor (\_ -> limitFactorizer) limit
 
 adjLimit :: Category k => Adjunction (Nat j k) k (Diag j k) r -> Obj (Nat j k) f -> Cone j k f (r :% f)
 adjLimit adj f = adjunctionCounit adj ! f
@@ -195,7 +195,7 @@
   --   by returning the morphism between the vertices of the cones.
   colimitFactorizer :: Cocone j k f n -> k (ColimitFam j k f) n
 
-data ColimitFunctor (j :: * -> * -> *) (k  :: * -> * -> *) = ColimitFunctor
+data ColimitFunctor (j :: * -> * -> *) (k :: * -> * -> *) = 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
@@ -207,7 +207,7 @@
 
 -- | The colimit functor is left adjoint to the diagonal functor.
 colimitAdj :: forall j k. HasColimits j k => Adjunction k (Nat j k) (ColimitFunctor j k) (Diag j k)
-colimitAdj = mkAdjunctionUnit ColimitFunctor Diag colimit (\_ -> colimitFactorizer)
+colimitAdj = mkAdjunctionInit ColimitFunctor Diag colimit (\_ -> colimitFactorizer)
 
 adjColimit :: Category k => Adjunction k (Nat j k) l (Diag j k) -> Obj (Nat j k) f -> Cocone j k f (l :% f)
 adjColimit adj f = adjunctionUnit adj ! f
@@ -482,7 +482,7 @@
 
 -- | A specialisation of the limit adjunction to products.
 prodAdj :: HasBinaryProducts k => Adjunction (k :**: k) k (DiagProd k) (ProductFunctor k)
-prodAdj = mkAdjunctionUnits DiagProd ProductFunctor (\x -> x &&& x) (\(l :**: r) -> proj1 l r :**: proj2 l r)
+prodAdj = mkAdjunctionTerm DiagProd ProductFunctor (\_ (l :**: r) -> l &&& r) (\(l :**: r) -> proj1 l r :**: proj2 l r)
 
 data p :*: q where
   (:*:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k, HasBinaryProducts k) => p -> q -> p :*: q
@@ -608,7 +608,7 @@
 
 -- | A specialisation of the colimit adjunction to coproducts.
 coprodAdj :: HasBinaryCoproducts k => Adjunction k (k :**: k) (CoproductFunctor k) (DiagProd k)
-coprodAdj = mkAdjunctionUnits CoproductFunctor DiagProd (\(l :**: r) -> inj1 l r :**: inj2 l r) (\x -> x ||| x)
+coprodAdj = mkAdjunctionInit CoproductFunctor DiagProd (\(l :**: r) -> inj1 l r :**: inj2 l r) (\_ (l :**: r) -> l ||| r)
 
 data p :+: q where
   (:+:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k, HasBinaryCoproducts k) => p -> q -> p :+: q
diff --git a/Data/Category/RepresentableFunctor.hs b/Data/Category/RepresentableFunctor.hs
--- a/Data/Category/RepresentableFunctor.hs
+++ b/Data/Category/RepresentableFunctor.hs
@@ -12,6 +12,8 @@
 
 import Data.Category
 import Data.Category.Functor
+import Data.Category.NaturalTransformation
+import Data.Category.Adjunction
 
 
 data Representable f repObj = Representable
@@ -69,3 +71,21 @@
   , represent          = \(Op y) f -> Op (factorizer y f)
   , universalElement   = mor
   }
+
+
+-- | For an adjunction F -| G, each pair (FY, unit_Y) is an initial morphism from Y to G.
+adjunctionInitialProp :: Adjunction c d f g -> Obj d y -> InitialUniversal y g (f :% y)
+adjunctionInitialProp adj@(Adjunction f g _ _) y = initialUniversal g (f % y) (adjunctionUnit adj ! y) (rightAdjunct adj)
+
+-- | For an adjunction F -| G, each pair (GX, counit_X) is a terminal morphism from F to X.
+adjunctionTerminalProp :: Adjunction c d f g -> Obj c x -> TerminalUniversal x f (g :% x)
+adjunctionTerminalProp adj@(Adjunction f g _ _) x = terminalUniversal f (g % x) (adjunctionCounit adj ! x) (leftAdjunct adj)
+
+
+initialPropAdjunction :: forall f g c d. (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
+  => f -> g -> (forall y. InitialUniversal y g (f :% y)) -> Adjunction c d f g
+initialPropAdjunction f g univ = mkAdjunctionInit f g (\_ -> universalElement univ) (represent univ)
+
+terminalPropAdjunction :: forall f g c d. (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
+  => f -> g -> (forall x. TerminalUniversal x f (g :% x)) -> Adjunction c d f g
+terminalPropAdjunction f g univ = mkAdjunctionTerm f g ((unOp .) . represent univ . Op) (\_ -> universalElement univ)
diff --git a/Data/Category/Yoneda.hs b/Data/Category/Yoneda.hs
--- a/Data/Category/Yoneda.hs
+++ b/Data/Category/Yoneda.hs
@@ -51,6 +51,6 @@
   M1 % n = n ! Op haskUnit
 
 haskIsTotal :: Adjunction (->) (Nat (Op (->)) (->)) M1 (YonedaEmbedding (->))
-haskIsTotal = mkAdjunctionUnit M1 YonedaEmbedding
+haskIsTotal = mkAdjunctionInit M1 YonedaEmbedding
   (\(Nat f _ _) -> Nat f (Hom_X (f % Op haskUnit)) (\_ fz z -> (f % Op (\() -> z)) fz))
   (\_ n@(Nat f _ _) fu -> (n ! Op haskUnit) fu ())
diff --git a/data-category.cabal b/data-category.cabal
--- a/data-category.cabal
+++ b/data-category.cabal
@@ -1,5 +1,5 @@
 name:                data-category
-version:             0.8.2
+version:             0.9
 synopsis:            Category theory
 
 description:         Data-category is a collection of categories, and some categorical constructions on them.
@@ -38,6 +38,7 @@
     Data.Category.RepresentableFunctor,
     Data.Category.Adjunction,
     Data.Category.Limit,
+    Data.Category.KanExtension,
     Data.Category.Monoidal,
     Data.Category.CartesianClosed,
     Data.Category.Enriched,