diff --git a/Data/Category/Adjunction.hs b/Data/Category/Adjunction.hs
--- a/Data/Category/Adjunction.hs
+++ b/Data/Category/Adjunction.hs
@@ -81,18 +81,22 @@
 
 
 
-initialPropAdjunction :: (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, Category c, Category d, 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 un coun
   where
+    coun :: forall a. Obj c a -> c (f :% (g :% a)) a
     coun a = initialFactorizer (univ (g % a)) a (g % a)
+    un   :: forall a. Obj d a -> d a (g :% (f :% a))
     un   a = initialMorphism (univ a)
-    
-terminalPropAdjunction :: (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, Category c, Category d, 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 un coun
   where
+    un   :: forall a. Obj d a -> d a (g :% (f :% a))
     un   a = terminalFactorizer (univ (f % a)) a (f % a)
+    coun :: forall a. Obj c a -> c (f :% (g :% a)) a
     coun a = terminalMorphism (univ a)
     
 
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,4 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, Rank2Types, ScopedTypeVariables, UndecidableInstances #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, Rank2Types, ScopedTypeVariables, UndecidableInstances, TypeSynonymInstances #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.CartesianClosed
@@ -42,7 +42,7 @@
 
 type instance Exponential (->) y z = y -> z
 
-instance (CartesianClosed (->)) where
+instance CartesianClosed (->) where
   
   apply _ _ (f, y) = f y
   tuple _ _ z      = \y -> (z, y)
@@ -70,18 +70,36 @@
 
 type instance Exponential Cat (CatW c) (CatW d) = CatW (Nat c d)
 
-instance (CartesianClosed Cat) where
+instance CartesianClosed Cat where
   
   apply CatA{} CatA{}   = CatA CatApply
   tuple CatA{} CatA{}   = CatA CatTuple
   (CatA f) ^^^ (CatA h) = CatA (Wrap f h)
 
 
+data PShExponential ((~>) :: * -> * -> *) p q = PShExponential
+type instance Dom (PShExponential (~>) p q) = Op (~>)
+type instance Cod (PShExponential (~>) p q) = (->)
+type instance PShExponential (~>) p q :% a = Presheaves (~>) ((YonedaEmbedding (~>) :% a) :*: p) q
+instance (Category (~>), Dom p ~ Op (~>), Dom q ~ Op (~>), Cod p ~ (->), Cod q ~ (->), Functor p, Functor q)
+  => Functor (PShExponential (~>) p q) where
+  PShExponential % Op f = h f where
+    h :: a ~> b -> PShExponential (~>) p q :% b -> PShExponential (~>) p q :% a
+    h g (Nat (_ :*: p) q n) = Nat (Hom_X (src g) :*: p) q $ \i (i2a, pi) -> n i (g . i2a, pi)
 
+type instance Exponential (Presheaves (~>)) y z = PShExponential (~>) y z
+
+instance Category (~>) => CartesianClosed (Presheaves (~>)) where
+  
+  apply (Nat y _ _) (Nat z _ _) = Nat (PShExponential :*: y) z $ \(Op i) (n, yi) -> (n ! Op i) (i, yi)
+  tuple (Nat y _ _) (Nat z _ _) = Nat z PShExponential $ \(Op i) zi -> (Nat (Hom_X i) z $ \_ j2i -> (z % Op j2i) zi) *** natId y
+  zn@Nat{} ^^^ yn@Nat{} = Nat PShExponential PShExponential $ \(Op i) n -> zn . n . (natId (Hom_X i) *** yn)
+
+    
 data ProductWith (~>) y = ProductWith (Obj (~>) y)
 type instance Dom (ProductWith (~>) y) = (~>)
 type instance Cod (ProductWith (~>) y) = (~>)
-type instance ProductWith (~>) y :% z = ProductFunctor (~>) :% (z, y)
+type instance ProductWith (~>) y :% z = BinaryProduct (~>) z y
 instance HasBinaryProducts (~>) => Functor (ProductWith (~>) y) where
   ProductWith y % f = f *** y
   
@@ -117,3 +135,4 @@
 
 contextComonadDuplicate :: CartesianClosed (~>) => Obj (~>) s -> Obj (~>) a -> Context (~>) s a ~> Context (~>) s (Context (~>) 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,7 +22,7 @@
 -----------------------------------------------------------------------------
 module Data.Category.Limit (
 
-  -- * Prelimiairies
+  -- * Preliminairies
   
   -- ** Diagonal Functor
     Diag(..)
@@ -67,11 +67,11 @@
   , BinaryProduct
   , HasBinaryProducts(..)
   , ProductFunctor(..)
-  , (:*:)
+  , (:*:)(..)
   , BinaryCoproduct
   , HasBinaryCoproducts(..)
   , CoproductFunctor(..)
-  , (:+:)
+  , (:+:)(..)
   
   -- ** Limits of type Hask
   , ForAll(..)
@@ -267,7 +267,16 @@
   
   terminate (CatA _) = CatA $ Const Z
 
+-- | 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 %)
 
+
 -- | An initial object is the colimit of the functor from /0/ to (~>).
 class Category (~>) => HasInitialObject (~>) where
   
@@ -287,9 +296,9 @@
     (initialize . coconeVertex)
 
 
--- | Any empty data type is an initial object in Hask.
 data Zero
 
+-- | Any empty data type is an initial object in @Hask@.
 instance HasInitialObject (->) where
   
   type InitialObject (->) = Zero
@@ -299,6 +308,7 @@
   -- With thanks to Conor McBride
   initialize _ x = x `seq` error "we never get this far"
 
+-- | The empty category is the initial object in @Cat@.
 instance HasInitialObject Cat where
   
   type InitialObject Cat = CatW Void
@@ -306,6 +316,15 @@
   initialObject = CatA Id
   
   initialize (CatA _) = CatA Nil
+
+-- | 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 %)
 
 
 
diff --git a/Data/Category/NaturalTransformation.hs b/Data/Category/NaturalTransformation.hs
--- a/Data/Category/NaturalTransformation.hs
+++ b/Data/Category/NaturalTransformation.hs
@@ -29,6 +29,10 @@
   , Postcompose(..)
   , Wrap(..)
   
+  -- ** Presheaves
+  , Presheaves
+  , Representable(..)
+  
   -- ** Yoneda
   , YonedaEmbedding(..)
   , Yoneda(..)
@@ -114,7 +118,7 @@
 type instance Precompose f d :% g = g :.: f
 
 instance (Functor f, Category d) => Functor (Precompose f d) where
-  Precompose f % (Nat g h n) = Nat (g :.: f) (h :.: f) $ n . (f %)
+  Precompose f % n = n `o` natId f
 
 
 -- | @Postcompose f c@ is the functor such that @Postcompose f c :% g = f :.: g@, 
@@ -127,7 +131,7 @@
 type instance Postcompose f c :% g = f :.: g
 
 instance (Functor f, Category c) => Functor (Postcompose f c) where
-  Postcompose f % (Nat g h n) = Nat (f :.: g) (f :.: h) $ (f %) . n
+  Postcompose f % n = natId f `o` n
 
 
 -- | @Wrap f h@ is the functor such that @Wrap f h :% g = f :.: g :.: h@, 
@@ -139,9 +143,11 @@
 type instance Wrap f h :% g = f :.: g :.: h
 
 instance (Functor f, Functor h) => Functor (Wrap f h) where
-  Wrap f h % (Nat g1 g2 n) = Nat (f :.: g1 :.: h) (f :.: g2 :.: h) $ (f %) . n . (h %)
+  Wrap f h % n = natId f `o` n `o` natId h
 
 
+type Presheaves (~>) = Nat (Op (~>)) (->)
+
 -- | A functor F: Op(C) -> Set is representable if it is naturally isomorphic to the contravariant hom-functor.
 class Functor f => Representable f where
   type RepresentingObject f :: *
@@ -158,12 +164,12 @@
 data YonedaEmbedding :: (* -> * -> *) -> * where
   YonedaEmbedding :: Category (~>) => YonedaEmbedding (~>)
   
-type instance Dom (YonedaEmbedding (~>)) = Op (~>)
-type instance Cod (YonedaEmbedding (~>)) = Nat (~>) (->)
-type instance YonedaEmbedding (~>) :% a = a :*-: (~>)
+type instance Dom (YonedaEmbedding (~>)) = (~>)
+type instance Cod (YonedaEmbedding (~>)) = Nat (Op (~>)) (->)
+type instance YonedaEmbedding (~>) :% a = (~>) :-*: a
 
 instance Category (~>) => Functor (YonedaEmbedding (~>)) where
-  YonedaEmbedding % (Op f) = Nat (HomX_ $ tgt f) (HomX_ $ src f) $ \_ -> (. f)
+  YonedaEmbedding % f = Nat (Hom_X $ src f) (Hom_X $ tgt f) $ \_ -> (f .)
 
 
 data Yoneda f = Yoneda
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.3.0.1
+version:             0.3.0.2
 synopsis:            Restricted categories
 
 description:         Data-category is a collection of categories, and some categorical constructions on them.