diff --git a/Data/Category/Adjunction.hs b/Data/Category/Adjunction.hs
--- a/Data/Category/Adjunction.hs
+++ b/Data/Category/Adjunction.hs
@@ -59,7 +59,7 @@
   -> (forall a b. Obj d a -> c (f :% a) b -> d a (g :% b))
   -> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b)
   -> 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))
+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))
 
 mkAdjunctionUnits :: (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
   => f -> g
@@ -124,21 +124,21 @@
 
 precomposeAdj :: Category e => Adjunction c d f g -> Adjunction (Nat c e) (Nat d e) (Precompose g e) (Precompose f e)
 precomposeAdj adj@(Adjunction f g _ _) = mkAdjunctionUnits
-  (precompose g)
-  (precompose f)
+  (Precompose g)
+  (Precompose f)
   (\nh@(Nat h _ _) -> compAssocInv h g f . (nh `o` adjunctionUnit adj) . idPrecompInv h)
   (\nh@(Nat h _ _) -> idPrecomp h . (nh `o` adjunctionCounit adj) . compAssoc h f g)
 
 postcomposeAdj :: Category e => Adjunction c d f g -> Adjunction (Nat e c) (Nat e d) (Postcompose f e) (Postcompose g e)
 postcomposeAdj adj@(Adjunction f g _ _) = mkAdjunctionUnits
-  (postcompose f)
-  (postcompose g)
+  (Postcompose f)
+  (Postcompose g)
   (\nh@(Nat h _ _) -> compAssoc g f h . (adjunctionUnit adj `o` nh) . idPostcompInv h)
   (\nh@(Nat h _ _) -> idPostcomp h . (adjunctionCounit adj `o` nh) . compAssocInv f g h)
 
 contAdj :: Adjunction (Op (->)) (->) (Opposite ((->) :-*: r) :.: OpOpInv (->)) ((->) :-*: r)
 contAdj = mkAdjunction
-  (Opposite (hom_X (\x -> x)) :.: OpOpInv)
-  (hom_X (\x -> x))
+  (Opposite (Hom_X (\x -> x)) :.: OpOpInv)
+  (Hom_X (\x -> x))
   (\_ -> \(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
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies, GADTs, TypeOperators, ScopedTypeVariables, UndecidableInstances, NoImplicitPrelude #-}
+{-# LANGUAGE TypeFamilies, GADTs, TypeOperators, LambdaCase, ScopedTypeVariables, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, NoImplicitPrelude #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Boolean
@@ -19,7 +19,10 @@
 import Data.Category.Monoidal
 import Data.Category.CartesianClosed
 
+import Data.Category.Functor
+import Data.Category.NaturalTransformation
 
+
 data Fls
 data Tru
 
@@ -154,3 +157,28 @@
 
 falseProductComonoid :: ComonoidObject (ProductFunctor Boolean) Fls
 falseProductComonoid = ComonoidObject F2T Fls
+
+
+data 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
+  type Cod (Arrow k a b) = k
+  type Arrow k a b :% Fls = a
+  type Arrow k a b :% Tru = b
+  Arrow f % Fls = src f
+  Arrow f % F2T = f
+  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
+  limit (Nat f _ _) = Nat (Const (f % Fls)) f (\case Fls -> f % Fls; Tru -> f % F2T)
+  limitFactorizer Nat{} = \n -> n ! Fls
+
+type instance ColimitFam Boolean k f = f :% Tru
+-- | The colimit of a functor from the Boolean category is the target of the arrow it points to.
+instance Category k => HasColimits Boolean k where
+  colimit (Nat f _ _) = Nat f (Const (f % Tru)) (\case Fls -> f % F2T; Tru -> f % Tru)
+  colimitFactorizer Nat{} = \n -> n ! Tru
diff --git a/Data/Category/CartesianClosed.hs b/Data/Category/CartesianClosed.hs
--- a/Data/Category/CartesianClosed.hs
+++ b/Data/Category/CartesianClosed.hs
@@ -3,6 +3,7 @@
   TypeFamilies,
   GADTs,
   Rank2Types,
+  PatternSynonyms,
   ScopedTypeVariables,
   UndecidableInstances,
   TypeSynonymInstances,
@@ -83,16 +84,16 @@
   :.: Tuple2 (Presheaves k) (Presheaves k) y
   :.: YonedaEmbedding k
   )
-pshExponential :: Category k => Obj (Presheaves k) y -> Obj (Presheaves k) z -> PShExponential k y z
-pshExponential y z = hom_X z :.: Opposite (ProductFunctor :.: tuple2 y :.: yonedaEmbedding)
+pattern PshExponential :: Category k => Obj (Presheaves k) y -> Obj (Presheaves k) z -> PShExponential k y z
+pattern PshExponential y z = Hom_X z :.: Opposite (ProductFunctor :.: Tuple2 y :.: YonedaEmbedding)
 
 -- | The category of presheaves on a category @C@ is cartesian closed for any @C@.
 instance Category k => CartesianClosed (Presheaves k) where
   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))
-  zn ^^^ yn = Nat (pshExponential (tgt yn) (src zn)) (pshExponential (src yn) (tgt zn)) (\(Op i) n -> zn . n . (natId (hom_X i) *** yn))
+  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))
+  zn ^^^ yn = Nat (PshExponential (tgt yn) (src zn)) (PshExponential (src yn) (tgt zn)) (\(Op i) n -> zn . n . (natId (Hom_X i) *** yn))
 
 
 
@@ -102,7 +103,7 @@
          -> Adjunction k k
               (ProductFunctor k :.: Tuple2 k k y)
               (ExpFunctor k :.: Tuple1 (Op k) k y)
-curryAdj y = mkAdjunctionUnits (ProductFunctor :.: tuple2 y) (ExpFunctor :.: tuple1 (Op y)) (tuple y) (apply y)
+curryAdj y = mkAdjunctionUnits (ProductFunctor :.: Tuple2 y) (ExpFunctor :.: Tuple1 (Op y)) (tuple y) (apply y)
 
 -- | From the adjunction between the product functor and the exponential functor we get the curry and uncurry functions,
 --   generalized to any cartesian closed category.
diff --git a/Data/Category/Comma.hs b/Data/Category/Comma.hs
--- a/Data/Category/Comma.hs
+++ b/Data/Category/Comma.hs
@@ -21,12 +21,12 @@
 data CommaO :: * -> * -> * -> * where
   CommaO :: (Cod t ~ k, Cod s ~ k)
     => Obj (Dom t) a -> k (t :% a) (s :% b) -> Obj (Dom s) b -> CommaO t s (a, b)
-
-data (:/\:) :: * -> * -> * -> * -> * where
-  CommaA ::
+    
+data (:/\:) :: * -> * -> * -> * -> * where 
+  CommaA :: 
     CommaO t s (a, b) ->
-    Dom t a a' ->
-    Dom s b b' ->
+    Dom t a a' -> 
+    Dom s b b' -> 
     CommaO t s (a', b') ->
     (t :/\: s) (a, b) (a', b')
 
@@ -35,10 +35,10 @@
 
 -- | The comma category T \\downarrow S
 instance (Category (Dom t), Category (Dom s)) => Category (t :/\: s) where
-
+    
   src (CommaA so _ _ _) = commaId so
   tgt (CommaA _ _ _ to) = commaId to
-
+  
   (CommaA _ g h to) . (CommaA so g' h' _) = CommaA so (g . g') (h . h') to
 
 
@@ -53,7 +53,7 @@
                        . (Functor u, c ~ (u `ObjectsFUnder` x), HasInitialObject c, (a_, a) ~ InitialObject c)
                       => u -> InitialUniversal x u a
 initialUniversalComma u = case initialObject :: Obj c (a_, a) of
-  CommaA (CommaO _ mor a) _ _ _ ->
+  CommaA (CommaO _ mor a) _ _ _ -> 
     initialUniversal u a mor factorizer
       where
         factorizer :: forall y. Obj (Dom u) y -> Cod u x (u :% y) -> Dom u a y
diff --git a/Data/Category/Enriched.hs b/Data/Category/Enriched.hs
--- a/Data/Category/Enriched.hs
+++ b/Data/Category/Enriched.hs
@@ -3,6 +3,7 @@
   , TypeFamilies
   , GADTs
   , RankNTypes
+  , PatternSynonyms
   , FlexibleContexts
   , NoImplicitPrelude
   , UndecidableInstances
@@ -24,7 +25,7 @@
 
 import Data.Category (Category(..), Obj, Op(..))
 import Data.Category.Product
-import Data.Category.Functor (Functor(..), Hom(..), (:*-:), homX_)
+import Data.Category.Functor (Functor(..), Hom(..), (:*-:), pattern HomX_)
 import Data.Category.Limit hiding (HasLimits)
 import Data.Category.CartesianClosed
 import Data.Category.Boolean
@@ -46,7 +47,7 @@
 -- | 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
+elem = HomX_ terminalObject
 
 -- | Arrows as elements of @k@
 type Arr k a b = Elem k :% (k $ (a, b))
diff --git a/Data/Category/Functor.hs b/Data/Category/Functor.hs
--- a/Data/Category/Functor.hs
+++ b/Data/Category/Functor.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, FlexibleContexts, FlexibleInstances, UndecidableInstances, GADTs, RankNTypes, ConstraintKinds, NoImplicitPrelude #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, PatternSynonyms, FlexibleContexts, FlexibleInstances, UndecidableInstances, GADTs, RankNTypes, ConstraintKinds, NoImplicitPrelude #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Functor
@@ -31,17 +31,17 @@
   , Proj2(..)
   , (:***:)(..)
   , DiagProd(..)
-  , Tuple1, tuple1
-  , Tuple2, tuple2
-  , Swap, swap
+  , Tuple1, pattern Tuple1
+  , Tuple2, pattern Tuple2
+  , Swap, pattern Swap
 
   -- *** Hom functors
   , Hom(..)
-  , (:*-:), homX_
-  , (:-*:), hom_X
-  , HomF, homF
-  , Star, star
-  , Costar, costar
+  , (:*-:), pattern HomX_
+  , (:-*:), pattern Hom_X
+  , HomF, pattern HomF
+  , Star, pattern Star
+  , Costar, pattern Costar
 
 ) where
 
@@ -138,7 +138,7 @@
 
   Opposite f % Op a = Op (f % a)
 
-
+  
 data OpOp (k :: * -> * -> *) = OpOp
 
 -- | The @Op (Op x) = x@ functor.
@@ -183,7 +183,7 @@
   Proj2 % (_ :**: f2) = f2
 
 
-data f1 :***: f2 = f1 :***: f2
+data f1 :***: f2 where (:***:) :: (Functor f1, Functor f2) => f1 -> f2 -> f1 :***: f2
 
 -- | @f1 :***: f2@ is the product of the functors @f1@ and @f2@.
 instance (Functor f1, Functor f2) => Functor (f1 :***: f2) where
@@ -208,8 +208,8 @@
 type Tuple1 c1 c2 a = (Const c2 c1 a :***: Id c2) :.: DiagProd c2
 
 -- | 'Tuple1' tuples with a fixed object on the left.
-tuple1 :: (Category c1, Category c2) => Obj c1 a -> Tuple1 c1 c2 a
-tuple1 a = (Const a :***: Id) :.: DiagProd
+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
 --
@@ -219,13 +219,13 @@
 
 type Swap (c1 :: * -> * -> *) (c2 :: * -> * -> *) = (Proj2 c1 c2 :***: Proj1 c1 c2) :.: DiagProd (c1 :**: c2)
 -- | 'swap' swaps the 2 categories of the product of categories.
-swap :: (Category c1, Category c2) => Swap c1 c2
-swap = (Proj2 :***: Proj1) :.: DiagProd
+pattern Swap :: (Category c1, Category c2) => Swap c1 c2
+pattern Swap = (Proj2 :***: Proj1) :.: DiagProd
 
 type Tuple2 c1 c2 a = Swap c2 c1 :.: Tuple1 c2 c1 a
 -- | 'Tuple2' tuples with a fixed object on the right.
-tuple2 :: (Category c1, Category c2) => Obj c2 a -> Tuple2 c1 c2 a
-tuple2 a = swap :.: tuple1 a
+pattern Tuple2 :: (Category c1, Category c2) => Obj c2 a -> Tuple2 c1 c2 a
+pattern Tuple2 a = Swap :.: Tuple1 a
 
 
 
@@ -242,23 +242,23 @@
 
 type x :*-: k = Hom k :.: Tuple1 (Op k) k x
 -- | The covariant functor Hom(X,--)
-homX_ :: Category k => Obj k x -> x :*-: k
-homX_ x = Hom :.: tuple1 (Op x)
+pattern HomX_ :: Category k => Obj k x -> x :*-: k
+pattern HomX_ x = Hom :.: Tuple1 (Op x)
 
 type k :-*: x = Hom k :.: Tuple2 (Op k) k x
 -- | The contravariant functor Hom(--,X)
-hom_X :: Category k => Obj k x -> k :-*: x
-hom_X x = Hom :.: tuple2 x
+pattern Hom_X :: Category k => Obj k x -> k :-*: x
+pattern Hom_X x = Hom :.: Tuple2 x
 
 
 type HomF f g = Hom (Cod f) :.: (Opposite f :***: g)
-homF :: (Functor f, Functor g, Cod f ~ Cod g) => f -> g -> HomF f g
-homF f g = Hom :.: (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
-star :: Functor f => f -> Star f
-star f = homF Id f
+pattern Star :: Functor f => f -> Star f
+pattern Star f = HomF Id f
 
 type Costar f = HomF f (Id (Cod f))
-costar :: Functor f => f -> Costar f
-costar f = homF f Id
+pattern Costar :: Functor f => f -> Costar f
+pattern Costar f = HomF f Id
diff --git a/Data/Category/NNO.hs b/Data/Category/NNO.hs
--- a/Data/Category/NNO.hs
+++ b/Data/Category/NNO.hs
@@ -18,44 +18,44 @@
 
 
 class HasTerminalObject k => HasNaturalNumberObject k where
-
+  
   type NaturalNumberObject k :: *
-
+  
   zero :: k (TerminalObject k) (NaturalNumberObject k)
   succ :: k (NaturalNumberObject k) (NaturalNumberObject k)
-
+  
   primRec :: k (TerminalObject k) a -> k a a -> k (NaturalNumberObject k) a
-
-
+  
+  
 data NatNum = Z | S NatNum
 
 instance HasNaturalNumberObject (->) where
-
+  
   type NaturalNumberObject (->) = NatNum
-
+  
   zero = \() -> Z
   succ = S
-
+  
   primRec z _  Z    = z ()
   primRec z s (S n) = s (primRec z s n)
 
 
-type Nat = Fix ((:++:) Unit)
+-- 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
-  type Cod (PrimRec z s) = Cod z
-  type PrimRec z s :% I1 () = z :% ()
-  type PrimRec z s :% I2 n  = s :% PrimRec z s :% n
-  PrimRec z _ % Fix (I1 Unit) = z % Unit
-  PrimRec z s % Fix (I2 n) = s % PrimRec z s % n
+  
+-- 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
+--   type Cod (PrimRec z s) = Cod z
+--   type PrimRec z s :% I1 () = z :% ()
+--   type PrimRec z s :% I2 n  = s :% PrimRec z s :% n
+--   PrimRec z _ % Fix (I1 Unit) = z % Unit
+--   PrimRec z s % Fix (I2 n) = s % PrimRec z s % n
diff --git a/Data/Category/NaturalTransformation.hs b/Data/Category/NaturalTransformation.hs
--- a/Data/Category/NaturalTransformation.hs
+++ b/Data/Category/NaturalTransformation.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, GADTs, LiberalTypeSynonyms, NoImplicitPrelude #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, PatternSynonyms, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, GADTs, LiberalTypeSynonyms, NoImplicitPrelude #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.NaturalTransformation
@@ -40,10 +40,8 @@
   -- * Related functors
   , FunctorCompose(..)
   , EndoFunctorCompose
-  , Precompose
-  , precompose
-  , Postcompose
-  , postcompose
+  , Precompose, pattern Precompose
+  , Postcompose, pattern Postcompose
   , Wrap(..)
   , Apply(..)
   , Tuple(..)
@@ -84,6 +82,10 @@
 natId :: Functor f => f -> Nat (Dom f) (Cod f) f f
 natId f = Nat f f (\i -> f % i)
 
+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)
+
 srcF :: Nat c d f g -> f
 srcF (Nat f _ _) = f
 
@@ -158,14 +160,14 @@
 -- | @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
-precompose :: (Category e, Functor f) => f -> Precompose f e
-precompose f = FunctorCompose :.: tuple2 (natId f)
+pattern Precompose :: (Category e, Functor f) => f -> Precompose f e
+pattern Precompose f = FunctorCompose :.: Tuple2 (NatId f)
 
 -- | @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
-postcompose :: (Category e, Functor f) => f -> Postcompose f e
-postcompose f = FunctorCompose :.: tuple1 (natId f)
+pattern Postcompose :: (Category e, Functor f) => f -> Postcompose f e
+pattern Postcompose f = FunctorCompose :.: Tuple1 (NatId f)
 
 
 data Wrap f h = Wrap f h
@@ -194,4 +196,4 @@
   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)) (\z -> f :**: z)
diff --git a/Data/Category/RepresentableFunctor.hs b/Data/Category/RepresentableFunctor.hs
--- a/Data/Category/RepresentableFunctor.hs
+++ b/Data/Category/RepresentableFunctor.hs
@@ -26,7 +26,7 @@
 
 covariantHomRepr :: Category k => Obj k x -> Representable (x :*-: k) x
 covariantHomRepr x = Representable
-  { representedFunctor = homX_ x
+  { representedFunctor = HomX_ x
   , representingObject = x
   , represent          = \_ h -> h
   , universalElement   = x
@@ -34,7 +34,7 @@
 
 contravariantHomRepr :: Category k => Obj k x -> Representable (k :-*: x) x
 contravariantHomRepr x = Representable
-  { representedFunctor = hom_X x
+  { representedFunctor = Hom_X x
   , representingObject = Op x
   , represent          = \_ h -> Op h
   , universalElement   = x
@@ -49,7 +49,7 @@
                  -> (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
+  { representedFunctor = HomX_ (src mor) :.: u
   , representingObject = obj
   , represent          = factorizer
   , universalElement   = mor
@@ -64,7 +64,7 @@
                   -> (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
+  { representedFunctor = Hom_X (tgt mor) :.: Opposite u
   , representingObject = Op obj
   , represent          = \(Op y) f -> Op (factorizer y f)
   , universalElement   = mor
diff --git a/Data/Category/Yoneda.hs b/Data/Category/Yoneda.hs
--- a/Data/Category/Yoneda.hs
+++ b/Data/Category/Yoneda.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators, RankNTypes, TypeFamilies, NoImplicitPrelude #-}
+{-# LANGUAGE TypeOperators, RankNTypes, TypeFamilies, PatternSynonyms, UndecidableInstances, NoImplicitPrelude #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Yoneda
@@ -13,14 +13,15 @@
 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))
 
 -- | The Yoneda embedding functor, @C -> Set^(C^op)@.
-yonedaEmbedding :: Category k => YonedaEmbedding k
-yonedaEmbedding = postcompose Hom :.: (postcompose swap :.: Tuple)
+pattern YonedaEmbedding :: Category k => YonedaEmbedding k
+pattern YonedaEmbedding = Postcompose Hom :.: (Postcompose Swap :.: Tuple)
 
 
 data Yoneda (k :: * -> * -> *) f = Yoneda
@@ -29,7 +30,7 @@
   type Dom (Yoneda k f) = Op k
   type Cod (Yoneda k f) = (->)
   type Yoneda k f :% a = Nat (Op k) (->) (k :-*: a) f
-  Yoneda % Op ab = \n -> n . yonedaEmbedding % ab
+  Yoneda % Op ab = \n -> n . YonedaEmbedding % ab
 
 
 -- | 'fromYoneda' and 'toYoneda' are together the isomophism from the Yoneda lemma.
@@ -37,4 +38,19 @@
 fromYoneda f = Nat Yoneda f (\(Op a) n -> (n ! Op a) a)
 
 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))
+toYoneda   f = Nat f Yoneda (\(Op a) fa -> Nat (Hom_X a) f (\_ h -> (f % Op h) fa))
+
+haskUnit :: Obj (->) ()
+haskUnit () = ()
+
+data M1 = M1
+instance Functor M1 where
+  type Dom M1 = Nat (Op (->)) (->)
+  type Cod M1 = (->)
+  type M1 :% f = f :% ()
+  M1 % n = n ! Op haskUnit
+
+haskIsTotal :: Adjunction (->) (Nat (Op (->)) (->)) M1 (YonedaEmbedding (->))
+haskIsTotal = mkAdjunction M1 YonedaEmbedding
+  (\(Nat f _ _) fu2b -> Nat f (Hom :.: (Swap :.: Tuple1 (\x -> x))) (\_ fz z -> fu2b ((f % Op (\() -> z)) fz)))
+  (\_ 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.7.1
+version:             0.7.2
 synopsis:            Category theory
 
 description:         Data-category is a collection of categories, and some categorical constructions on them.