diff --git a/Data/Category/Adjunction.hs b/Data/Category/Adjunction.hs
--- a/Data/Category/Adjunction.hs
+++ b/Data/Category/Adjunction.hs
@@ -16,27 +16,27 @@
 
   , leftAdjunct
   , rightAdjunct
-  
+
   -- * Adjunctions as a category
   , idAdj
   , composeAdj
   , AdjArrow(..)
-  
+
   -- * Adjunctions from universal morphisms
   , initialPropAdjunction
   , terminalPropAdjunction
-  
+
   -- * Universal morphisms from adjunctions
   , adjunctionInitialProp
   , adjunctionTerminalProp
-  
+
   -- * Examples
   , precomposeAdj
   , postcomposeAdj
   , contAdj
-  
+
 ) where
-  
+
 import Data.Category
 import Data.Category.Functor
 import Data.Category.NaturalTransformation
@@ -50,9 +50,9 @@
   , counit       :: Nat c c (f :.: g) (Id c)
   }
 
-mkAdjunction :: (Functor f, Functor g, Category c, Category d, 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) 
+mkAdjunction :: (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 c a -> Component (f :.: g) (Id c) a)
   -> Adjunction c d f g
 mkAdjunction f g un coun = Adjunction f g (Nat Id (g :.: f) un) (Nat (f :.: g) Id coun)
@@ -74,24 +74,24 @@
 
 
 
-initialPropAdjunction :: forall f g c d. (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
+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 = mkAdjunction f g 
+initialPropAdjunction f g univ = mkAdjunction f g
   (universalElement . univ)
   (\a -> represent (univ (g % a)) a (g % a))
-   
-terminalPropAdjunction :: forall f g c d. (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
+
+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 = mkAdjunction f g 
+terminalPropAdjunction f g univ = mkAdjunction f g
   (\a -> unOp (represent (univ (f % a)) (Op a) (f % a)))
   (universalElement . univ)
-    
 
+
 idAdj :: Category k => Adjunction k k (Id k) (Id k)
 idAdj = mkAdjunction Id Id (\x -> x) (\x -> x)
 
 composeAdj :: Adjunction d e f g -> Adjunction c d f' g' -> Adjunction c e (f' :.: f) (g :.: g')
-composeAdj (Adjunction f g u c) (Adjunction f' g' u' c') = Adjunction (f' :.: f) (g :.: g') 
+composeAdj (Adjunction f g u c) (Adjunction f' g' u' c') = Adjunction (f' :.: f) (g :.: g')
   (compAssoc (g :.: g') f' f . precompose f % (compAssocInv g g' f' . postcompose g % u' . idPrecompInv g) . u)
   (c' . precompose g' % (idPrecomp f' . postcompose f' % c . compAssoc f' f g) . compAssocInv (f' :.: f) g g')
 
@@ -101,23 +101,23 @@
 
 -- | The category with categories as objects and adjunctions as arrows.
 instance Category AdjArrow where
-  
+
   src (AdjArrow (Adjunction _ _ _ _)) = AdjArrow idAdj
   tgt (AdjArrow (Adjunction _ _ _ _)) = AdjArrow idAdj
-  
+
   AdjArrow x . AdjArrow y = AdjArrow (composeAdj x y)
 
 
 
 precomposeAdj :: Category e => Adjunction c d f g -> Adjunction (Nat c e) (Nat d e) (Precompose g e) (Precompose f e)
-precomposeAdj (Adjunction f g un coun) = mkAdjunction 
+precomposeAdj (Adjunction f g un coun) = mkAdjunction
   (precompose g)
   (precompose f)
   (\nh@(Nat h _ _) -> compAssocInv h g f . (nh `o` un) . idPrecompInv h)
   (\nh@(Nat h _ _) -> idPrecomp h . (nh `o` coun) . 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 (Adjunction f g un coun) = mkAdjunction 
+postcomposeAdj (Adjunction f g un coun) = mkAdjunction
   (postcompose f)
   (postcompose g)
   (\nh@(Nat h _ _) -> compAssoc g f h . (un `o` nh) . idPostcompInv h)
diff --git a/Data/Category/Boolean.hs b/Data/Category/Boolean.hs
--- a/Data/Category/Boolean.hs
+++ b/Data/Category/Boolean.hs
@@ -15,9 +15,6 @@
 module Data.Category.Boolean where
 
 import Data.Category
-import Data.Category.Functor
-import Data.Category.NaturalTransformation
-import Data.Category.Product
 import Data.Category.Limit
 import Data.Category.Monoidal
 import Data.Category.CartesianClosed
@@ -25,7 +22,7 @@
 
 data Fls
 data Tru
-  
+
 data Boolean a b where
   Fls :: Boolean Fls Fls
   F2T :: Boolean Fls Tru
@@ -33,15 +30,15 @@
 
 -- | @Boolean@ is the category with true and false as objects, and an arrow from false to true.
 instance Category Boolean where
-  
+
   src Fls   = Fls
   src F2T   = Fls
   src Tru   = Tru
-  
+
   tgt Fls   = Fls
   tgt F2T   = Tru
   tgt Tru   = Tru
-  
+
   Fls . Fls = Fls
   F2T . Fls = F2T
   Tru . F2T = F2T
@@ -54,7 +51,7 @@
   initialObject = Fls
   initialize Fls = Fls
   initialize Tru = F2T
-  
+
 -- | True is the terminal object in the Boolean category.
 instance HasTerminalObject Boolean where
   type TerminalObject Boolean = Tru
@@ -65,12 +62,12 @@
 
 -- | Conjunction is the binary product in the Boolean category.
 instance HasBinaryProducts Boolean where
-  
+
   type BinaryProduct Boolean Fls Fls = Fls
   type BinaryProduct Boolean Fls Tru = Fls
   type BinaryProduct Boolean Tru Fls = Fls
   type BinaryProduct Boolean Tru Tru = Tru
-  
+
   proj1 Fls Fls = Fls
   proj1 Fls Tru = Fls
   proj1 Tru Fls = F2T
@@ -79,7 +76,7 @@
   proj2 Fls Tru = F2T
   proj2 Tru Fls = Fls
   proj2 Tru Tru = Tru
-    
+
   Fls &&& Fls = Fls
   Fls &&& F2T = Fls
   F2T &&& Fls = Fls
@@ -89,12 +86,12 @@
 
 -- | Disjunction is the binary coproduct in the Boolean category.
 instance HasBinaryCoproducts Boolean where
-  
+
   type BinaryCoproduct Boolean Fls Fls = Fls
   type BinaryCoproduct Boolean Fls Tru = Tru
   type BinaryCoproduct Boolean Tru Fls = Tru
   type BinaryCoproduct Boolean Tru Tru = Tru
-  
+
   inj1 Fls Fls = Fls
   inj1 Fls Tru = F2T
   inj1 Tru Fls = Tru
@@ -103,7 +100,7 @@
   inj2 Fls Tru = Tru
   inj2 Tru Fls = F2T
   inj2 Tru Tru = Tru
-    
+
   Fls ||| Fls = Fls
   F2T ||| F2T = F2T
   F2T ||| Tru = Tru
@@ -113,22 +110,22 @@
 
 -- | Implication makes the Boolean category cartesian closed.
 instance CartesianClosed Boolean where
-  
+
   type Exponential Boolean Fls Fls = Tru
   type Exponential Boolean Fls Tru = Tru
   type Exponential Boolean Tru Fls = Fls
   type Exponential Boolean Tru Tru = Tru
-  
+
   apply Fls Fls = Fls
   apply Fls Tru = F2T
   apply Tru Fls = Fls
   apply Tru Tru = Tru
-  
+
   tuple Fls Fls = F2T
   tuple Fls Tru = Tru
   tuple Tru Fls = Fls
   tuple Tru Tru = Tru
-  
+
   Fls ^^^ Fls = Tru
   Fls ^^^ F2T = F2T
   Fls ^^^ Tru = Fls
@@ -157,4 +154,3 @@
 
 falseProductComonoid :: ComonoidObject (ProductFunctor Boolean) Fls
 falseProductComonoid = ComonoidObject F2T Fls
-
diff --git a/Data/Category/CartesianClosed.hs b/Data/Category/CartesianClosed.hs
--- a/Data/Category/CartesianClosed.hs
+++ b/Data/Category/CartesianClosed.hs
@@ -1,4 +1,13 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, Rank2Types, ScopedTypeVariables, UndecidableInstances, TypeSynonymInstances, NoImplicitPrelude #-}
+{-# LANGUAGE
+  TypeOperators,
+  TypeFamilies,
+  GADTs,
+  Rank2Types,
+  ScopedTypeVariables,
+  UndecidableInstances,
+  TypeSynonymInstances,
+  FlexibleInstances,
+  NoImplicitPrelude #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.CartesianClosed
@@ -9,7 +18,7 @@
 -- Portability :  non-portable
 -----------------------------------------------------------------------------
 module Data.Category.CartesianClosed where
-  
+
 import Data.Category
 import Data.Category.Functor
 import Data.Category.NaturalTransformation
@@ -17,12 +26,13 @@
 import Data.Category.Limit
 import Data.Category.Adjunction
 import Data.Category.Monoidal as M
+import Data.Category.Yoneda
 
 
 -- | A category is cartesian closed if it has all products and exponentials for all objects.
 class (HasTerminalObject k, HasBinaryProducts k) => CartesianClosed k where
   type Exponential k y z :: *
-  
+
   apply :: Obj k y -> Obj k z -> k (BinaryProduct k (Exponential k y z) y) z
   tuple :: Obj k y -> Obj k z -> k z (Exponential k y (BinaryProduct k z y))
   (^^^) :: k z1 z2 -> k y2 y1 -> k (Exponential k y1 z1) (Exponential k y2 z2)
@@ -41,39 +51,40 @@
 -- | Exponentials in @Hask@ are functions.
 instance CartesianClosed (->) where
   type Exponential (->) y z = y -> z
-  
+
   apply _ _ (f, y) = f y
   tuple _ _ z      = \y -> (z, y)
   f ^^^ h          = \g -> f . g . h
 
 
 
-data Apply (c1 :: * -> * -> *) (c2 :: * -> * -> *) = 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
-  type Cod (Apply c1 c2) = c1
-  type Apply c1 c2 :% (f, a) = f :% a
-  Apply % (l :**: r) = l ! r
-
-data Tuple (c1 :: * -> * -> *) (c2 :: * -> * -> *) = 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)
-
-
 -- | Exponentials in @Cat@ are the functor categories.
 instance CartesianClosed Cat where
   type Exponential Cat (CatW c) (CatW d) = CatW (Nat c d)
-  
+
   apply CatA{} CatA{}   = CatA Apply
   tuple CatA{} CatA{}   = CatA Tuple
   (CatA f) ^^^ (CatA h) = CatA (Wrap f h)
 
 
+type PShExponential k y z = (Presheaves k :-*: z) :.: Opposite
+  (   ProductFunctor (Presheaves k)
+  :.: 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)
+
+-- | 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))
+
+
+
 -- | The product functor is left adjoint the the exponential functor.
 curryAdj :: CartesianClosed k
          => Obj k y
@@ -107,4 +118,3 @@
 
 contextComonadDuplicate :: CartesianClosed k => 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/Limit.hs b/Data/Category/Limit.hs
--- a/Data/Category/Limit.hs
+++ b/Data/Category/Limit.hs
@@ -22,36 +22,36 @@
 module Data.Category.Limit (
 
   -- * Preliminairies
-  
+
   -- ** Diagonal Functor
     Diag(..)
   , DiagF
-  
+
   -- ** Cones
   , Cone
   , Cocone
   , coneVertex
   , coconeVertex
-  
+
   -- * Limits
   , LimitFam
   , Limit
   , HasLimits(..)
   , LimitFunctor(..)
   , limitAdj
-  
+
   -- * Colimits
   , ColimitFam
   , Colimit
   , HasColimits(..)
   , ColimitFunctor(..)
   , colimitAdj
-  
+
   -- ** Limits of type Void
   , HasTerminalObject(..)
   , HasInitialObject(..)
   , Zero
-  
+
   -- ** Limits of type Pair
   , HasBinaryProducts(..)
   , ProductFunctor(..)
@@ -61,7 +61,7 @@
   , CoproductFunctor(..)
   , (:+:)(..)
   , coprodAdj
-  
+
 ) where
 
 import Data.Category
@@ -82,13 +82,13 @@
 
 data Diag :: (* -> * -> *) -> (* -> * -> *) -> * where
   Diag :: Diag j k
-  
+
 -- | The diagonal functor from (index-) category J to k.
 instance (Category j, Category k) => Functor (Diag j k) where
   type Dom (Diag j k) = k
   type Cod (Diag j k) = Nat j k
   type Diag j k :% a = Const j k a
-  
+
   Diag % f = Nat (Const (src f)) (Const (tgt f)) (\_ -> f)
 
 -- | The diagonal functor with the same domain and codomain as @f@.
@@ -170,15 +170,15 @@
 colimitAdj :: forall j k. HasColimits j k => Adjunction k (Nat j k) (ColimitFunctor j k) (Diag j k)
 colimitAdj = mkAdjunction ColimitFunctor diag (\f @ Nat{} -> colimit f) (\a -> colimitFactorizer (diag % a) (diag % a))
   where diag = Diag :: Diag j k -- Forces the type of all Diags to be the same.
-  
 
 
+
 class Category k => HasTerminalObject k where
-  
+
   type TerminalObject k :: *
-  
+
   terminalObject :: Obj k (TerminalObject k)
-  
+
   terminate :: Obj k a -> k a (TerminalObject k)
 
 
@@ -186,7 +186,7 @@
 
 -- | A terminal object is the limit of the functor from /0/ to k.
 instance (HasTerminalObject k) => HasLimits Void k where
-  
+
   limit (Nat f _ _) = voidNat (Const terminalObject) f
   limitFactorizer Nat{} = terminate . coneVertex
 
@@ -194,49 +194,49 @@
 -- | @()@ is the terminal object in @Hask@.
 instance HasTerminalObject (->) where
   type TerminalObject (->) = ()
-  
+
   terminalObject = \x -> x
-  
+
   terminate _ _ = ()
 
 -- | @Unit@ is the terminal category.
 instance HasTerminalObject Cat where
   type TerminalObject Cat = CatW Unit
-  
+
   terminalObject = CatA Id
-  
+
   terminate (CatA _) = CatA (Const Unit)
 
 -- | The constant functor to the terminal object is itself the terminal object in its functor category.
 instance (Category c, HasTerminalObject d) => HasTerminalObject (Nat c d) where
   type TerminalObject (Nat c d) = Const c d (TerminalObject d)
-  
+
   terminalObject = natId (Const terminalObject)
-  
+
   terminate (Nat f _ _) = Nat f (Const terminalObject) (terminate . (f %))
 
 -- | The category of one object has that object as terminal object.
 instance HasTerminalObject Unit where
   type TerminalObject Unit = ()
-  
+
   terminalObject = Unit
-  
+
   terminate Unit = Unit
-  
+
 -- | The terminal object of the product of 2 categories is the product of their terminal objects.
 instance (HasTerminalObject c1, HasTerminalObject c2) => HasTerminalObject (c1 :**: c2) where
   type TerminalObject (c1 :**: c2) = (TerminalObject c1, TerminalObject c2)
-  
+
   terminalObject = terminalObject :**: terminalObject
-  
+
   terminate (a1 :**: a2) = terminate a1 :**: terminate a2
-  
+
 -- | The terminal object of the direct coproduct of categories is the terminal object of the terminal category.
 instance (Category c1, HasTerminalObject c2) => HasTerminalObject (c1 :>>: c2) where
   type TerminalObject (c1 :>>: c2) = I2 (TerminalObject c2)
-  
+
   terminalObject = I2A terminalObject
-  
+
   terminate (I1A a) = I12 a terminalObject
   terminate (I2A a) = I2A (terminate a)
 
@@ -244,7 +244,7 @@
 
 class Category k => HasInitialObject k where
   type InitialObject k :: *
-  
+
   initialObject :: Obj k (InitialObject k)
 
   initialize :: Obj k a -> k (InitialObject k) a
@@ -254,7 +254,7 @@
 
 -- | An initial object is the colimit of the functor from /0/ to k.
 instance HasInitialObject k => HasColimits Void k where
-  
+
   colimit (Nat f _ _) = voidNat f (Const initialObject)
   colimitFactorizer Nat{} = initialize . coconeVertex
 
@@ -264,56 +264,56 @@
 -- | Any empty data type is an initial object in @Hask@.
 instance HasInitialObject (->) where
   type InitialObject (->) = Zero
-  
+
   initialObject = \x -> x
-  
+
   initialize = initialize
 
 -- | The empty category is the initial object in @Cat@.
 instance HasInitialObject Cat where
   type InitialObject Cat = CatW Void
-  
+
   initialObject = CatA Id
-  
+
   initialize (CatA _) = CatA Magic
 
 -- | The constant functor to the initial object is itself the initial object in its functor category.
 instance (Category c, HasInitialObject d) => HasInitialObject (Nat c d) where
   type InitialObject (Nat c d) = Const c d (InitialObject d)
-  
+
   initialObject = natId (Const initialObject)
-  
+
   initialize (Nat f _ _) = Nat (Const initialObject) f (initialize . (f %))
 
 -- | The initial object of the product of 2 categories is the product of their initial objects.
 instance (HasInitialObject c1, HasInitialObject c2) => HasInitialObject (c1 :**: c2) where
   type InitialObject (c1 :**: c2) = (InitialObject c1, InitialObject c2)
-  
+
   initialObject = initialObject :**: initialObject
-  
+
   initialize (a1 :**: a2) = initialize a1 :**: initialize a2
 
 -- | The category of one object has that object as initial object.
 instance HasInitialObject Unit where
   type InitialObject Unit = ()
-  
+
   initialObject = Unit
-  
+
   initialize Unit = Unit
 
 -- | The initial object of the direct coproduct of categories is the initial object of the initial category.
 instance (HasInitialObject c1, Category c2) => HasInitialObject (c1 :>>: c2) where
   type InitialObject (c1 :>>: c2) = I1 (InitialObject c1)
-  
+
   initialObject = I1A initialObject
-  
+
   initialize (I1A a) = I1A (initialize a)
   initialize (I2A a) = I12 initialObject a
 
 
 class Category k => HasBinaryProducts k where
   type BinaryProduct (k :: * -> * -> *) x y :: *
-  
+
   proj1 :: Obj k x -> Obj k y -> k (BinaryProduct k x y) x
   proj2 :: Obj k x -> Obj k y -> k (BinaryProduct k x y) y
 
@@ -329,7 +329,7 @@
 
 -- | 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
-  
+
   limit = limit'
     where
       limit' :: forall f. Obj (Nat (i :++: j) k) f -> Cone f (Limit f)
@@ -352,20 +352,20 @@
 -- | The tuple is the binary product in @Hask@.
 instance HasBinaryProducts (->) where
   type BinaryProduct (->) x y = (x, y)
-  
+
   proj1 _ _ = \(x, _) -> x
   proj2 _ _ = \(_, y) -> y
-  
+
   f &&& g = \x -> (f x, g x)
   f *** g = \(x, y) -> (f x, g y)
 
 -- | The product of categories ':**:' is the binary product in 'Cat'.
 instance HasBinaryProducts Cat where
   type BinaryProduct Cat (CatW c1) (CatW c2) = CatW (c1 :**: c2)
-  
+
   proj1 (CatA _) (CatA _) = CatA Proj1
   proj2 (CatA _) (CatA _) = CatA Proj2
-  
+
   CatA f1 &&& CatA f2 = CatA ((f1 :***: f2) :.: DiagProd)
   CatA f1 *** CatA f2 = CatA (f1 :***: f2)
 
@@ -375,17 +375,17 @@
 
   proj1 Unit Unit = Unit
   proj2 Unit Unit = Unit
-  
+
   Unit &&& Unit = Unit
   Unit *** Unit = Unit
 
 -- | The binary product of the product of 2 categories is the product of their binary products.
 instance (HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts (c1 :**: c2) where
   type BinaryProduct (c1 :**: c2) (x1, x2) (y1, y2) = (BinaryProduct c1 x1 y1, BinaryProduct c2 x2 y2)
-  
+
   proj1 (x1 :**: x2) (y1 :**: y2) = proj1 x1 y1 :**: proj1 x2 y2
   proj2 (x1 :**: x2) (y1 :**: y2) = proj2 x1 y1 :**: proj2 x2 y2
-  
+
   (f1 :**: f2) &&& (g1 :**: g2) = (f1 &&& g1) :**: (f2 &&& g2)
   (f1 :**: f2) *** (g1 :**: g2) = (f1 *** g1) :**: (f2 *** g2)
 
@@ -394,12 +394,12 @@
   type BinaryProduct (c1 :>>: c2) (I1 a) (I2 b) = I1 a
   type BinaryProduct (c1 :>>: c2) (I2 a) (I1 b) = I1 b
   type BinaryProduct (c1 :>>: c2) (I2 a) (I2 b) = I2 (BinaryProduct c2 a b)
-  
+
   proj1 (I1A a) (I1A b) = I1A (proj1 a b)
   proj1 (I1A a) (I2A _) = I1A a
   proj1 (I2A a) (I1A b) = I12 b a
   proj1 (I2A a) (I2A b) = I2A (proj1 a b)
-  
+
   proj2 (I1A a) (I1A b) = I1A (proj2 a b)
   proj2 (I1A a) (I2A b) = I12 a b
   proj2 (I2A _) (I1A b) = I1A b
@@ -409,6 +409,7 @@
   I1A a &&& I12 _ _ = I1A a
   I12 _ _ &&& I1A b = I1A b
   I2A a &&& I2A b = I2A (a &&& b)
+  I12 a b1 &&& I12 _ b2 = I12 a (b1 *** b2)
 
 
 data ProductFunctor (k :: * -> * -> *) = ProductFunctor
@@ -437,15 +438,15 @@
 -- | The functor product ':*:' is the binary product in functor categories.
 instance (Category c, HasBinaryProducts d) => HasBinaryProducts (Nat c d) where
   type BinaryProduct (Nat c d) x y = x :*: y
-    
+
   proj1 (Nat f _ _) (Nat g _ _) = Nat (f :*: g) f (\z -> proj1 (f % z) (g % z))
   proj2 (Nat f _ _) (Nat g _ _) = Nat (f :*: g) g (\z -> proj2 (f % z) (g % z))
-  
+
   Nat a f af &&& Nat _ g ag = Nat a (f :*: g) (\z -> af z &&& ag z)
   Nat f1 f2 f *** Nat g1 g2 g = Nat (f1 :*: g1) (f2 :*: g2) (\z -> f z *** g z)
-  
 
 
+
 class Category k => HasBinaryCoproducts k where
   type BinaryCoproduct (k :: * -> * -> *) x y :: *
 
@@ -453,18 +454,18 @@
   inj2 :: Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
 
   (|||) :: (k x a) -> (k y a) -> (k (BinaryCoproduct k x y) a)
-    
+
   (+++) :: (k a1 b1) -> (k a2 b2) -> (k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2))
   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
-  
+
   colimit = colimit'
     where
       colimit' :: forall f. Obj (Nat (i :++: j) k) f -> Cocone f (Colimit f)
@@ -477,7 +478,7 @@
           h :: Obj (i :++: j) z -> Com f (ConstF f (ColimitFam (i :++: j) k f)) z
           h (I1 n) = Com (inj1 x y . col1 ! n)
           h (I2 n) = Com (inj2 x y . col2 ! n)
-  
+
   colimitFactorizer l@Nat{} c =
     colimitFactorizer (l `o` natId Inj1) (constPostcomp (tgtF c) Inj1 . (c `o` natId Inj1))
     |||
@@ -487,30 +488,30 @@
 -- | The coproduct of categories ':++:' is the binary coproduct in 'Cat'.
 instance HasBinaryCoproducts Cat where
   type BinaryCoproduct Cat (CatW c1) (CatW c2) = CatW (c1 :++: c2)
-    
+
   inj1 (CatA _) (CatA _) = CatA Inj1
   inj2 (CatA _) (CatA _) = CatA Inj2
-  
+
   CatA f1 ||| CatA f2 = CatA (CodiagCoprod :.: (f1 :+++: f2))
   CatA f1 +++ CatA f2 = CatA (f1 :+++: f2)
 
 -- | In the category of one object that object is its own coproduct.
 instance HasBinaryCoproducts Unit where
   type BinaryCoproduct Unit () () = ()
-  
+
   inj1 Unit Unit = Unit
   inj2 Unit Unit = Unit
-  
+
   Unit ||| Unit = Unit
   Unit +++ Unit = Unit
-  
+
 -- | The binary coproduct of the product of 2 categories is the product of their binary coproducts.
 instance (HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts (c1 :**: c2) where
   type BinaryCoproduct (c1 :**: c2) (x1, x2) (y1, y2) = (BinaryCoproduct c1 x1 y1, BinaryCoproduct c2 x2 y2)
-  
+
   inj1 (x1 :**: x2) (y1 :**: y2) = inj1 x1 y1 :**: inj1 x2 y2
   inj2 (x1 :**: x2) (y1 :**: y2) = inj2 x1 y1 :**: inj2 x2 y2
-  
+
   (f1 :**: f2) ||| (g1 :**: g2) = (f1 ||| g1) :**: (f2 ||| g2)
   (f1 :**: f2) +++ (g1 :**: g2) = (f1 +++ g1) :**: (f2 +++ g2)
 
@@ -534,6 +535,7 @@
   I2A a ||| I12 _ _ = I2A a
   I12 _ _ ||| I2A b = I2A b
   I2A a ||| I2A b = I2A (a ||| b)
+  I12 a1 b ||| I12 a2 _ = I12 (a1 +++ a2) b
 
 
 data CoproductFunctor (k :: * -> * -> *) = CoproductFunctor
@@ -562,10 +564,10 @@
 -- | The functor coproduct ':+:' is the binary coproduct in functor categories.
 instance (Category c, HasBinaryCoproducts d) => HasBinaryCoproducts (Nat c d) where
   type BinaryCoproduct (Nat c d) x y = x :+: y
-  
+
   inj1 (Nat f _ _) (Nat g _ _) = Nat f (f :+: g) (\z -> inj1 (f % z) (g % z))
   inj2 (Nat f _ _) (Nat g _ _) = Nat g (f :+: g) (\z -> inj2 (f % z) (g % z))
-  
+
   Nat f a fa ||| Nat g _ ga = Nat (f :+: g) a (\z -> fa z ||| ga z)
   Nat f1 f2 f +++ Nat g1 g2 g = Nat (f1 :+: g1) (f2 :+: g2) (\z -> f z +++ g z)
 
@@ -606,7 +608,7 @@
 
 -- | The limit of a single object is that object.
 instance Category k => HasLimits Unit k where
-  
+
   limit (Nat f _ _) = Nat (Const (f % Unit)) f (\Unit -> f % Unit)
   limitFactorizer Nat{} n = n ! Unit
 
@@ -614,7 +616,7 @@
 
 -- | The limit of any diagram with an initial object, has the limit at the initial object.
 instance (HasInitialObject (i :>>: j), Category k) => HasLimits (i :>>: j) k where
-  
+
   limit (Nat f _ _) = Nat (Const (f % initialObject)) f (\z -> f % initialize z)
   limitFactorizer Nat{} n = n ! initialObject
 
@@ -623,10 +625,10 @@
 
 -- | The colimit of a single object is that object.
 instance Category k => HasColimits Unit k where
-  
+
   colimit (Nat f _ _) = Nat f (Const (f % Unit)) (\Unit -> f % Unit)
   colimitFactorizer Nat{} 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.
diff --git a/Data/Category/Monoidal.hs b/Data/Category/Monoidal.hs
--- a/Data/Category/Monoidal.hs
+++ b/Data/Category/Monoidal.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE 
+{-# LANGUAGE
     TypeOperators
   , TypeFamilies
   , GADTs
@@ -6,7 +6,7 @@
   , ViewPatterns
   , TypeSynonymInstances
   , FlexibleInstances
-  , NoImplicitPrelude 
+  , NoImplicitPrelude
   #-}
 -----------------------------------------------------------------------------
 -- |
@@ -30,7 +30,7 @@
 -- | 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 :: *
   unitObject :: f -> Obj (Cod f) (Unit f)
 
@@ -38,7 +38,7 @@
   leftUnitorInv  :: Cod f ~ k => f -> Obj k a -> k a (f :% (Unit f, a))
   rightUnitor    :: Cod f ~ k => f -> Obj k a -> k (f :% (a, Unit f)) a
   rightUnitorInv :: Cod f ~ k => f -> Obj k a -> k a (f :% (a, Unit f))
-  
+
   associator     :: Cod f ~ k => f -> Obj k a -> Obj k b -> Obj k c -> k (f :% (f :% (a, b), c)) (f :% (a, f :% (b, c)))
   associatorInv  :: Cod f ~ k => f -> Obj k a -> Obj k b -> Obj k c -> k (f :% (a, f :% (b, c))) (f :% (f :% (a, b), c))
 
@@ -46,7 +46,7 @@
 -- | If a category has all products, then the product functor makes it a monoidal category,
 --   with the terminal object as unit.
 instance (HasTerminalObject k, HasBinaryProducts k) => TensorProduct (ProductFunctor k) where
-  
+
   type Unit (ProductFunctor k) = TerminalObject k
   unitObject _ = terminalObject
 
@@ -61,7 +61,7 @@
 -- | If a category has all coproducts, then the coproduct functor makes it a monoidal category,
 --   with the initial object as unit.
 instance (HasInitialObject k, HasBinaryCoproducts k) => TensorProduct (CoproductFunctor k) where
-  
+
   type Unit (CoproductFunctor k) = InitialObject k
   unitObject _ = initialObject
 
@@ -69,16 +69,16 @@
   leftUnitorInv  _ a = inj2 initialObject a
   rightUnitor    _ a = a ||| initialize a
   rightUnitorInv _ a = inj1 a initialObject
-  
+
   associator    _ a b c = (a +++ inj1 b c) ||| (inj2 a (b +++ c) . inj2 b c)
   associatorInv _ a b c = (inj1 (a +++ b) c . inj1 a b) ||| (inj2 a b +++ c)
-  
+
 -- | Functor composition makes the category of endofunctors monoidal, with the identity functor as unit.
 instance Category k => TensorProduct (EndoFunctorCompose k) where
-  
+
   type Unit (EndoFunctorCompose k) = Id k
   unitObject _ = natId Id
-  
+
   leftUnitor     _ (Nat g _ _) = idPostcomp g
   leftUnitorInv  _ (Nat g _ _) = idPostcompInv g
   rightUnitor    _ (Nat g _ _) = idPrecomp g
@@ -90,10 +90,10 @@
 
 -- | @MonoidObject f a@ defines a monoid @a@ in a monoidal category with tensor product @f@.
 data MonoidObject f a = MonoidObject
-  { unit     :: (Cod f ~ k) => k (Unit f)        a
-  , multiply :: (Cod f ~ k) => k ((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)
 trivialMonoid f = MonoidObject (unitObject f) (leftUnitor f (unitObject f))
 
@@ -103,13 +103,13 @@
 
 -- | @ComonoidObject f a@ defines a comonoid @a@ in a comonoidal category with tensor product @f@.
 data ComonoidObject f a = ComonoidObject
-  { counit     :: (Cod f ~ k) => k a (Unit f)
-  , comultiply :: (Cod f ~ k) => k a (f :% (a, a))
+  { counit     :: Cod f a (Unit f)
+  , comultiply :: Cod f a (f :% (a, a))
   }
 
 trivialComonoid :: TensorProduct f => f -> ComonoidObject f (Unit f)
 trivialComonoid f = ComonoidObject (unitObject f) (leftUnitorInv f (unitObject f))
-  
+
 productComonoid :: (HasTerminalObject k, HasBinaryProducts k) => Obj k a -> ComonoidObject (ProductFunctor k) a
 productComonoid a = ComonoidObject (terminate a) (a &&& a)
 
@@ -120,19 +120,19 @@
 
 -- | A monoid as a category with one object.
 instance Category (MonoidAsCategory f m) where
-  
+
   src (MonoidValue f m _) = MonoidValue f m (unit m)
   tgt (MonoidValue f m _) = MonoidValue f m (unit m)
-  
+
   MonoidValue f m a . MonoidValue _ _ b = MonoidValue f m (multiply m . f % (a :**: b) . leftUnitorInv f (unitObject f))
 
 
 -- | A monad is a monoid in the category of endofunctors.
 type Monad f = MonoidObject (EndoFunctorCompose (Dom f)) f
 
-mkMonad :: (Functor f, Dom f ~ k, Cod f ~ k, Category k) 
-  => f 
-  -> (forall a. Obj k a -> Component (Id k) f a) 
+mkMonad :: (Functor f, Dom f ~ k, Cod f ~ k)
+  => f
+  -> (forall a. Obj k a -> Component (Id k) f a)
   -> (forall a. Obj k a -> Component (f :.: f) f a)
   -> Monad f
 mkMonad f ret join = MonoidObject
@@ -147,9 +147,9 @@
 -- | A comonad is a comonoid in the category of endofunctors.
 type Comonad f = ComonoidObject (EndoFunctorCompose (Dom f)) f
 
-mkComonad :: (Functor f, Dom f ~ k, Cod f ~ k, Category k) 
-  => f 
-  -> (forall a. Obj k a -> Component f (Id k) a) 
+mkComonad :: (Functor f, Dom f ~ k, Cod f ~ k)
+  => f
+  -> (forall a. Obj k a -> Component f (Id k) a)
   -> (forall a. Obj k a -> Component f (f :.: f) a)
   -> Comonad f
 mkComonad f extr dupl = ComonoidObject
diff --git a/Data/Category/NaturalTransformation.hs b/Data/Category/NaturalTransformation.hs
--- a/Data/Category/NaturalTransformation.hs
+++ b/Data/Category/NaturalTransformation.hs
@@ -23,7 +23,8 @@
   -- * Functor category
   , Nat(..)
   , Endo
-  
+  , Presheaves
+
   -- * Functor isomorphisms
   , compAssoc
   , compAssocInv
@@ -35,7 +36,7 @@
   , constPrecompInv
   , constPostcomp
   , constPostcompInv
-    
+
   -- * Related functors
   , FunctorCompose(..)
   , EndoFunctorCompose
@@ -44,9 +45,11 @@
   , Postcompose
   , postcompose
   , Wrap(..)
-  
+  , Apply(..)
+  , Tuple(..)
+
 ) where
-  
+
 import Data.Category
 import Data.Category.Functor
 import Data.Category.Product
@@ -54,7 +57,7 @@
 infixl 9 !
 
 -- | @f :~> g@ is a natural transformation from functor f to functor g.
-type f :~> g = (c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => Nat c d f g
+type f :~> g = forall c d. (c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => Nat c d f g
 
 -- | Natural transformations are built up of components,
 -- one for each object @z@ in the domain category of @f@ and @g@.
@@ -94,11 +97,11 @@
 -- | Functor category D^C.
 -- Objects of D^C are functors from C to D.
 -- Arrows of D^C are natural transformations.
-instance (Category c, Category d) => Category (Nat c d) where
-  
+instance Category d => Category (Nat c d) where
+
   src (Nat f _ _)           = natId f
   tgt (Nat _ g _)           = natId g
-  
+
   Nat _ h ngh . Nat f _ nfg = Nat f h (\i -> ngh i . nfg i)
 
 
@@ -123,19 +126,19 @@
 idPostcompInv f = Nat f (Id :.: f) (f %)
 
 
-constPrecomp :: (Category c1, Functor f) 
+constPrecomp :: (Category c1, Functor f)
              => Const c1 (Dom f) x -> f -> Nat c1 (Cod f) (f :.: Const c1 (Dom f) x) (Const c1 (Cod f) (f :% x))
 constPrecomp (Const x) f = let fx = f % x in Nat (f :.: Const x) (Const fx) (\_ -> fx)
 
-constPrecompInv :: (Category c1, Functor f) 
+constPrecompInv :: (Category c1, Functor f)
                 => Const c1 (Dom f) x -> f -> Nat c1 (Cod f) (Const c1 (Cod f) (f :% x)) (f :.: Const c1 (Dom f) x)
 constPrecompInv (Const x) f = let fx = f % x in Nat (Const fx) (f :.: Const x) (\_ -> fx)
 
-constPostcomp :: (Category c2, Functor f) 
+constPostcomp :: (Category c2, Functor f)
               => Const (Cod f) c2 x -> f -> Nat (Dom f) c2 (Const (Cod f) c2 x :.: f) (Const (Dom f) c2 x)
 constPostcomp (Const x) f = Nat (Const x :.: f) (Const x) (\_ -> x)
 
-constPostcompInv :: (Category c2, Functor f) 
+constPostcompInv :: (Category c2, Functor f)
                  => Const (Cod f) c2 x -> f -> Nat (Dom f) c2 (Const (Dom f) c2 x) (Const (Cod f) c2 x :.: f)
 constPostcompInv (Const x) f = Nat (Const x) (Const x :.: f) (\_ -> x)
 
@@ -147,7 +150,7 @@
   type Dom (FunctorCompose c d e) = Nat d e :**: Nat c d
   type Cod (FunctorCompose c d e) = Nat c e
   type FunctorCompose c d e :% (f, g) = f :.: g
-  
+
   FunctorCompose % (n1 :**: n2) = n1 `o` n2
 
 
@@ -156,6 +159,8 @@
 -- | Composition of endofunctors is a functor.
 type EndoFunctorCompose k = FunctorCompose k k k
 
+type Presheaves k = Nat (Op k) (->)
+
 -- | @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
@@ -177,5 +182,22 @@
   type Dom (Wrap f h) = Nat (Cod h) (Dom f)
   type Cod (Wrap f h) = Nat (Dom h) (Cod f)
   type Wrap f h :% g = f :.: g :.: h
-  
+
   Wrap f h % n = natId f `o` n `o` natId h
+
+
+data Apply (c1 :: * -> * -> *) (c2 :: * -> * -> *) = 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
+  type Cod (Apply c1 c2) = c1
+  type Apply c1 c2 :% (f, a) = f :% a
+  Apply % (l :**: r) = l ! r
+
+data Tuple (c1 :: * -> * -> *) (c2 :: * -> * -> *) = 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)
diff --git a/Data/Category/Presheaf.hs b/Data/Category/Presheaf.hs
deleted file mode 100644
--- a/Data/Category/Presheaf.hs
+++ /dev/null
@@ -1,39 +0,0 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, TypeSynonymInstances, GADTs, FlexibleInstances, UndecidableInstances, NoImplicitPrelude #-}
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Category.Presheaf
--- License     :  BSD-style (see the file LICENSE)
---
--- Maintainer  :  sjoerd@w3future.com
--- Stability   :  experimental
--- Portability :  non-portable
------------------------------------------------------------------------------
-module Data.Category.Presheaf where
-
-import Data.Category
-import Data.Category.Functor
-import Data.Category.NaturalTransformation
-import Data.Category.Limit
-import Data.Category.CartesianClosed
-import Data.Category.Yoneda
-
-
-type Presheaves k = Nat (Op k) (->)
-
-type PShExponential k y z = (Presheaves k :-*: z) :.: Opposite
-  (   ProductFunctor (Presheaves k)
-  :.: 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)
-
--- | 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))
-
-    
diff --git a/Data/Category/RepresentableFunctor.hs b/Data/Category/RepresentableFunctor.hs
--- a/Data/Category/RepresentableFunctor.hs
+++ b/Data/Category/RepresentableFunctor.hs
@@ -17,8 +17,8 @@
 data Representable f repObj = Representable
   { representedFunctor :: f
   , representingObject :: Obj (Dom f) repObj
-  , represent          :: (Dom f ~ k, Cod f ~ (->)) => Obj k z -> f :% z -> k repObj z
-  , universalElement   :: (Dom f ~ k, Cod f ~ (->)) => f :% repObj
+  , represent          :: forall k z. (Dom f ~ k, Cod f ~ (->)) => Obj k z -> f :% z -> k repObj z
+  , universalElement   :: forall k. (Dom f ~ k, Cod f ~ (->)) => f :% repObj
   }
 
 unrepresent :: (Functor f, Dom f ~ k, Cod f ~ (->)) => Representable f repObj -> k repObj z -> f :% z
@@ -43,10 +43,10 @@
 type InitialUniversal x u a = Representable ((x :*-: Cod u) :.: u) a
 -- | An initial universal property, a universal morphism from x to u.
 initialUniversal :: Functor u
-                 => u 
-                 -> Obj (Dom u) a 
-                 -> Cod u x (u :% a) 
-                 -> (forall y. Obj (Dom u) y -> Cod u x (u :% y) -> Dom u a y) 
+                 => u
+                 -> Obj (Dom u) a
+                 -> 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
@@ -54,14 +54,14 @@
   , represent          = factorizer
   , universalElement   = mor
   }
-  
+
 type TerminalUniversal x u a = Representable ((Cod u :-*: x) :.: Opposite u) a
 -- | A terminal universal property, a universal morphism from u to x.
 terminalUniversal :: Functor u
-                  => u 
+                  => u
                   -> Obj (Dom u) a
                   -> Cod u (u :% a) x
-                  -> (forall y. Obj (Dom u) y -> Cod u (u :% y) x -> Dom u y a) 
+                  -> (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
diff --git a/Data/Category/Void.hs b/Data/Category/Void.hs
--- a/Data/Category/Void.hs
+++ b/Data/Category/Void.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE GADTs, TypeFamilies, NoImplicitPrelude #-}
+{-# LANGUAGE EmptyCase, LambdaCase, TypeOperators, GADTs, TypeFamilies, NoImplicitPrelude #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Void
@@ -18,7 +18,7 @@
 data Void a b
 
 magic :: Void a b -> x
-magic x = magic x
+magic = \case { }
 
 -- | `Void` is the category with no objects.
 instance Category Void where
@@ -29,7 +29,7 @@
   (.) = magic
 
 
-voidNat :: (Functor f, Functor g, Category d, Dom f ~ Void, Dom g ~ Void, Cod f ~ d, Cod g ~ d)
+voidNat :: (Functor f, Functor g, Dom f ~ Void, Dom g ~ Void, Cod f ~ d, Cod g ~ d)
   => f -> g -> Nat Void d f g
 voidNat f g = Nat f g magic
 
diff --git a/Data/Category/Yoneda.hs b/Data/Category/Yoneda.hs
--- a/Data/Category/Yoneda.hs
+++ b/Data/Category/Yoneda.hs
@@ -13,10 +13,9 @@
 import Data.Category
 import Data.Category.Functor
 import Data.Category.NaturalTransformation
-import Data.Category.CartesianClosed
 
-type YonedaEmbedding k = 
-  Postcompose (Hom k) (Op k) :.: 
+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)@.
@@ -31,11 +30,11 @@
   type Cod (Yoneda k f) = (->)
   type Yoneda k f :% a = Nat (Op k) (->) (k :-*: a) f
   Yoneda % Op ab = \n -> n . yonedaEmbedding % ab
-      
-  
+
+
 -- | 'fromYoneda' and 'toYoneda' are together the isomophism from the Yoneda lemma.
-fromYoneda :: (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => f -> Yoneda k f :~> f
+fromYoneda :: (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => f -> Nat (Op k) (->) (Yoneda k f) f
 fromYoneda f = Nat Yoneda f (\(Op a) n -> (n ! Op a) a)
 
-toYoneda   :: (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => f -> f :~> Yoneda k f
+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))
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.6.1
+version:             0.6.2
 synopsis:            Category theory
 
 description:         Data-category is a collection of categories, and some categorical constructions on them.
@@ -41,7 +41,6 @@
     Data.Category.Monoidal,
     Data.Category.CartesianClosed,
     Data.Category.Yoneda,
-    Data.Category.Presheaf,
     Data.Category.Boolean,
     Data.Category.Fix,
     Data.Category.Kleisli,