diff --git a/Data/Category/Boolean.hs b/Data/Category/Boolean.hs
--- a/Data/Category/Boolean.hs
+++ b/Data/Category/Boolean.hs
@@ -8,8 +8,8 @@
 -- Stability   :  experimental
 -- Portability :  non-portable
 --
--- /2/, or the Boolean category.
--- It contains 2 objects, one for true and one for false.
+-- /2/ a.k.a. the Boolean category a.k.a. the walking arrow.
+-- It contains 2 objects, one for false and one for true.
 -- It contains 3 arrows, 2 identity arrows and one from false to true.
 -----------------------------------------------------------------------------
 module Data.Category.Boolean where
@@ -21,6 +21,7 @@
 
 import Data.Category.Functor
 import Data.Category.NaturalTransformation
+import Data.Category.Adjunction
 
 
 data Fls
@@ -171,14 +172,50 @@
   Arrow f % Tru = tgt f
 
 
-type instance LimitFam Boolean k f = f :% Fls
 -- | The limit of a functor from the Boolean category is the source of the arrow it points to.
 instance Category k => HasLimits Boolean k where
+  type LimitFam Boolean k f = f :% Fls
   limit (Nat f _ _) = Nat (Const (f % Fls)) f (\case Fls -> f % Fls; Tru -> f % F2T)
   limitFactorizer n = n ! Fls
 
-type instance ColimitFam Boolean k f = f :% Tru
+-- | The source functor sends arrows (as functors from the Boolean category) to their source.
+type SrcFunctor = LimitFunctor Boolean
+
 -- | The colimit of a functor from the Boolean category is the target of the arrow it points to.
 instance Category k => HasColimits Boolean k where
+  type ColimitFam Boolean k f = f :% Tru
   colimit (Nat f _ _) = Nat f (Const (f % Tru)) (\case Fls -> f % F2T; Tru -> f % Tru)
   colimitFactorizer n = n ! Tru
+
+-- | The target functor sends arrows (as functors from the Boolean category) to their target.
+type TgtFunctor = ColimitFunctor Boolean
+
+
+data Terminator (k :: * -> * -> *) = 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
+  type Cod (Terminator k) = Nat Boolean k
+  type Terminator k :% a = Arrow k a (TerminalObject k)
+  Terminator % f = Nat (Arrow (terminate (src f))) (Arrow (terminate (tgt f))) (\case Fls -> f; Tru -> terminalObject)
+
+-- | @Terminator@ is right adjoint to the source functor.
+terminatorLimitAdj :: HasTerminalObject k => Adjunction k (Nat Boolean k) (SrcFunctor k) (Terminator k)
+terminatorLimitAdj = mkAdjunctionInit LimitFunctor Terminator
+  (\(Nat b _ _) -> Nat b (Arrow (terminate (b % Fls))) (\case Fls -> b % Fls; Tru -> terminate (b % Tru)))
+  (\_ n -> n ! Fls)
+
+
+data Initializer (k :: * -> * -> *) = 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
+  type Cod (Initializer k) = Nat Boolean k
+  type Initializer k :% a = Arrow k (InitialObject k) a
+  Initializer % f = Nat (Arrow (initialize (src f))) (Arrow (initialize (tgt f))) (\case Fls -> initialObject; Tru -> f)
+
+-- | @Initializer@ is left adjoint to the target functor.
+initializerColimitAdj :: HasInitialObject k => Adjunction (Nat Boolean k) k (Initializer k) (TgtFunctor k)
+initializerColimitAdj = mkAdjunctionTerm Initializer ColimitFunctor
+  (\_ n -> n ! Tru)
+  (\(Nat b _ _) -> Nat (Arrow (initialize (b % Tru))) b (\case Fls -> initialize (b % Fls); Tru -> b % Tru))
diff --git a/Data/Category/Enriched.hs b/Data/Category/Enriched.hs
--- a/Data/Category/Enriched.hs
+++ b/Data/Category/Enriched.hs
@@ -23,7 +23,7 @@
 
 import Data.Category (Category(..), Obj, Op(..))
 import Data.Category.Product
-import Data.Category.Functor (Functor(..), Hom(..), (:*-:), pattern HomX_)
+import Data.Category.Functor (Functor(..), Hom(..))
 import Data.Category.Limit hiding (HasLimits)
 import Data.Category.CartesianClosed
 import Data.Category.Boolean
@@ -247,16 +247,16 @@
 
 type VProfunctor k l t = EFunctorOf (EOp k :<>: l) (Self (V k)) t
 
-type family End (v :: * -> * -> *) 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) }
-type instance End (->) t = HaskEnd t
 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)
diff --git a/Data/Category/KanExtension.hs b/Data/Category/KanExtension.hs
--- a/Data/Category/KanExtension.hs
+++ b/Data/Category/KanExtension.hs
@@ -26,18 +26,18 @@
 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
+  -- | The right Kan extension of a functor @p@ for functors @f@ with codomain @k@.
+  type RanFam p k (f :: *) :: *
   -- | '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)
 
+type Ran p f = RanFam p (Cod f) 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)
 
@@ -57,18 +57,17 @@
 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
+  -- | The left Kan extension of a functor @p@ for functors @f@ with codomain @k@.
+  type LanFam (p :: *) (k :: * -> * -> *) (f :: *) :: *
   -- | '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
 
+type Lan p f = LanFam p (Cod f) f
+
 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)
 
@@ -88,42 +87,42 @@
 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
+  type RanFam (Const j Unit ()) k f = Const Unit k (LimitFam j k f)
   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)
+  ranFactorizer n@(Nat (h :.: _) _ _) = 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
+  type LanFam (Const j Unit ()) k f = Const Unit k (ColimitFam j k f)
   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)
+  lanFactorizer n@(Nat _ (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
+  type RanFam (Id j) k f = f
   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
+  type LanFam (Id j) k f = f
   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
+  type RanFam (q :.: p) k f = RanFam q k (RanFam p k f)
   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
+  type LanFam (q :.: p) k f = LanFam q k (LanFam p k f)
   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))
@@ -137,10 +136,10 @@
   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
+  type RanFam (Any p) (->) f = RanHaskF p f
   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)))
+  ranFactorizer (Nat (h :.: _) _ n) = Nat h RanHaskF (\_ 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
@@ -151,7 +150,7 @@
   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
+  type LanFam (Any p) (->) f = LanHaskF p f
   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))
+  lanFactorizer (Nat _ (h :.: _) n) = Nat LanHaskF h (\_ (LanHask c pcz fc) -> (h % pcz) (n c fc))
diff --git a/Data/Category/Limit.hs b/Data/Category/Limit.hs
--- a/Data/Category/Limit.hs
+++ b/Data/Category/Limit.hs
@@ -36,9 +36,8 @@
   , coconeVertex
 
   -- * Limits
-  , LimitFam
-  , Limit
   , HasLimits(..)
+  , Limit
   , LimitFunctor(..)
   , limitAdj
   , adjLimit
@@ -47,9 +46,8 @@
   , rightAdjointPreservesLimitsInv
 
   -- * Colimits
-  , ColimitFam
-  , Colimit
   , HasColimits(..)
+  , Colimit
   , ColimitFunctor(..)
   , colimitAdj
   , adjColimit
@@ -122,20 +120,18 @@
 coconeVertex (Nat _ (Const x) _) = x
 
 
-
--- | Limits in a category @k@ by means of a diagram of type @j@, which is a functor from @j@ to @k@.
-type family LimitFam (j :: * -> * -> *) (k :: * -> * -> *) (f :: *) :: *
-
-type Limit f = LimitFam (Dom f) (Cod f) f
-
 -- | 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 :: *) :: *
   -- | '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
   --   by returning the morphism between the vertices of the cones.
   limitFactorizer :: Cone j k f n -> k n (LimitFam j k f)
 
+type Limit f = LimitFam (Dom f) (Cod f) f
+
 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 @(***)@.
@@ -182,19 +178,19 @@
   => Obj (Nat c d) g -> Obj (Nat j c) t -> d (g :% LimitFam j c t) (LimitFam j d (g :.: t))
 rightAdjointPreservesLimitsInv g t = limitFactorizer (constPrecompIn (g `o` limit t))
 
--- | Colimits in a category @k@ by means of a diagram of type @j@, which is a functor from @j@ to @k@.
-type family ColimitFam (j :: * -> * -> *) (k :: * -> * -> *) (f :: *) :: *
 
-type Colimit f = ColimitFam (Dom f) (Cod f) f
-
 -- | 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 :: *) :: *
   -- | '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
   --   by returning the morphism between the vertices of the cones.
   colimitFactorizer :: Cocone j k f n -> k (ColimitFam j k f) n
 
+type Colimit f = ColimitFam (Dom f) (Cod f) f
+
 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 @(+++)@.
@@ -241,11 +237,9 @@
   terminate :: Obj k a -> k a (TerminalObject k)
 
 
-type instance LimitFam Void k f = TerminalObject k
-
 -- | A terminal object is the limit of the functor from /0/ to k.
 instance (Category k, HasTerminalObject k) => HasLimits Void k where
-
+  type LimitFam Void k f = TerminalObject k
   limit (Nat f _ _) = voidNat (Const terminalObject) f
   limitFactorizer = terminate . coneVertex
 
@@ -309,11 +303,9 @@
   initialize :: Obj k a -> k (InitialObject k) a
 
 
-type instance ColimitFam Void k f = InitialObject k
-
 -- | An initial object is the colimit of the functor from /0/ to k.
 instance (Category k, HasInitialObject k) => HasColimits Void k where
-
+  type ColimitFam Void k f = InitialObject k
   colimit (Nat f _ _) = voidNat f (Const initialObject)
   colimitFactorizer = initialize . coconeVertex
 
@@ -382,12 +374,11 @@
   l *** r = (l . proj1 (src l) (src r)) &&& (r . proj2 (src l) (src r))
 
 
-type instance LimitFam (i :++: j) k f = BinaryProduct k
-  (LimitFam i k (f :.: Inj1 i j))
-  (LimitFam j k (f :.: Inj2 i j))
-
 -- | If `k` has binary products, we can take the limit of 2 joined diagrams.
 instance (HasLimits i k, HasLimits j k, HasBinaryProducts k) => HasLimits (i :++: j) k where
+  type LimitFam (i :++: j) k f = BinaryProduct k
+    (LimitFam i k (f :.: Inj1 i j))
+    (LimitFam j k (f :.: Inj2 i j))
 
   limit = limit'
     where
@@ -518,12 +509,11 @@
   l +++ r = (inj1 (tgt l) (tgt r) . l) ||| (inj2 (tgt l) (tgt r) . r)
 
 
-type instance ColimitFam (i :++: j) k f = BinaryCoproduct k
-  (ColimitFam i k (f :.: Inj1 i j))
-  (ColimitFam j k (f :.: Inj2 i j))
-
 -- | If `k` has binary coproducts, we can take the colimit of 2 joined diagrams.
 instance (HasColimits i k, HasColimits j k, HasBinaryCoproducts k) => HasColimits (i :++: j) k where
+  type ColimitFam (i :++: j) k f = BinaryCoproduct k
+    (ColimitFam i k (f :.: Inj1 i j))
+    (ColimitFam j k (f :.: Inj2 i j))
 
   colimit = colimit'
     where
@@ -663,50 +653,42 @@
 
 
 
-type instance LimitFam Unit k f = f :% ()
-
 -- | The limit of a single object is that object.
 instance Category k => HasLimits Unit k where
-
+  type LimitFam Unit k f = f :% ()
   limit (Nat f _ _) = Nat (Const (f % Unit)) f (\Unit -> f % Unit)
   limitFactorizer n = n ! Unit
 
-type instance LimitFam (i :>>: j) k f = f :% InitialObject (i :>>: j)
-
 -- | The limit of any diagram with an initial object, has the limit at the initial object.
 instance (HasInitialObject (i :>>: j), Category i, Category j, Category k) => HasLimits (i :>>: j) k where
-
+  type LimitFam (i :>>: j) k f = f :% InitialObject (i :>>: j)
   limit (Nat f _ _) = Nat (Const (f % initialObject)) f (\z -> f % initialize z)
   limitFactorizer n = n ! initialObject
 
 
-type instance ColimitFam Unit k f = f :% ()
-
 -- | The colimit of a single object is that object.
 instance Category k => HasColimits Unit k where
-
+  type ColimitFam Unit k f = f :% ()
   colimit (Nat f _ _) = Nat f (Const (f % Unit)) (\Unit -> f % Unit)
   colimitFactorizer n = n ! Unit
 
-type instance ColimitFam (i :>>: j) k f = f :% TerminalObject (i :>>: j)
-
 -- | The colimit of any diagram with a terminal object, has the limit at the terminal object.
 instance (HasTerminalObject (i :>>: j), Category i, Category j, Category k) => HasColimits (i :>>: j) k where
-
+  type ColimitFam (i :>>: j) k f = f :% TerminalObject (i :>>: j)
   colimit (Nat f _ _) = Nat f (Const (f % terminalObject)) (\z -> f % terminate z)
   colimitFactorizer n = n ! terminalObject
 
 
 data ForAll f = ForAll (forall a. Obj (->) a -> f :% a)
-type instance LimitFam (->) (->) f = ForAll f
 
 instance HasLimits (->) (->) where
+  type LimitFam (->) (->) f = ForAll f
   limit (Nat f _ _) = Nat (Const (\x -> x)) f (\a (ForAll g) -> g a)
   limitFactorizer n = \z -> ForAll (\a -> (n ! a) z)
 
 data Exists f = forall a. Exists (Obj (->) a) (f :% a)
-type instance ColimitFam (->) (->) f = Exists f
 
 instance HasColimits (->) (->) where
+  type ColimitFam (->) (->) f = Exists f
   colimit (Nat f _ _) = Nat f (Const (\x -> x)) Exists
   colimitFactorizer n = \(Exists a fa) -> (n ! a) fa
diff --git a/Data/Category/Yoneda.hs b/Data/Category/Yoneda.hs
--- a/Data/Category/Yoneda.hs
+++ b/Data/Category/Yoneda.hs
@@ -53,4 +53,4 @@
 haskIsTotal :: Adjunction (->) (Nat (Op (->)) (->)) 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 ())
+  (\_ n 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.9
+version:             0.10
 synopsis:            Category theory
 
 description:         Data-category is a collection of categories, and some categorical constructions on them.