diff --git a/Data/Category/Adjunction.hs b/Data/Category/Adjunction.hs
--- a/Data/Category/Adjunction.hs
+++ b/Data/Category/Adjunction.hs
@@ -13,9 +13,12 @@
   -- * Adjunctions
     Adjunction(..)
   , mkAdjunction
+  , mkAdjunctionUnits
 
   , leftAdjunct
   , rightAdjunct
+  , adjunctionUnit
+  , adjunctionCounit
 
   -- * Adjunctions as a category
   , idAdj
@@ -39,6 +42,7 @@
 
 import Data.Category
 import Data.Category.Functor
+import Data.Category.Product
 import Data.Category.NaturalTransformation
 import Data.Category.RepresentableFunctor
 
@@ -46,54 +50,63 @@
   => Adjunction
   { leftAdjoint  :: f
   , rightAdjoint :: g
-  , unit         :: Nat d d (Id d) (g :.: f)
-  , counit       :: Nat c c (f :.: g) (Id c)
+  , leftAdjunctN  :: Profunctors c d (Costar f) (Star g)
+  , rightAdjunctN :: Profunctors c d (Star g) (Costar f)
   }
 
 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))
+  -> (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))
+
+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)
   -> (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)
+mkAdjunctionUnits f g un coun = mkAdjunction f g (\a h -> (g % h) . un a) (\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 _ g un _) i h = (g % h) . (un ! i)
+leftAdjunct (Adjunction _ _ l _) a h = (l ! (Op a :**: tgt h)) h
 rightAdjunct :: Adjunction c d f g -> Obj c b -> d a (g :% b) -> c (f :% a) b
-rightAdjunct (Adjunction f _ _ coun) i h = (coun ! i) . (f % h)
-
+rightAdjunct (Adjunction _ _ _ r) b h = (r ! (Op (src h) :**: b)) h
 
+adjunctionUnit :: Adjunction c d f g -> Nat d d (Id d) (g :.: f)
+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 un _) y = initialUniversal g (f % y) (un ! y) (rightAdjunct adj)
+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 _ coun) x = terminalUniversal f (g % x) (coun ! x) (leftAdjunct adj)
+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 = mkAdjunction 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 = mkAdjunction 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)
-idAdj = mkAdjunction Id Id (\x -> x) (\x -> x)
+idAdj = mkAdjunction Id Id (\_ f -> f) (\_ f -> f)
 
 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')
-  (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')
+composeAdj l@(Adjunction f g _ _) r@(Adjunction f' g' _ _) = mkAdjunction (f' :.: f) (g :.: g')
+  (\a -> leftAdjunct l a . leftAdjunct r (f % a)) (\b -> rightAdjunct r b . rightAdjunct l (g' % b))
 
 
 data AdjArrow c d where
@@ -110,22 +123,22 @@
 
 
 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 adj@(Adjunction f g _ _) = mkAdjunctionUnits
   (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)
+  (\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 (Adjunction f g un coun) = mkAdjunction
+postcomposeAdj adj@(Adjunction f g _ _) = mkAdjunctionUnits
   (postcompose f)
   (postcompose g)
-  (\nh@(Nat h _ _) -> compAssoc g f h . (un `o` nh) . idPostcompInv h)
-  (\nh@(Nat h _ _) -> idPostcomp h . (coun `o` nh) . compAssocInv f g h)
+  (\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))
-  (\_ x f -> f x)
-  (\_ -> Op (\x f -> f x))
+  (\_ -> \(Op f) -> \b a -> f a b)
+  (\_ -> \f -> Op (\b a -> f a b))
diff --git a/Data/Category/CartesianClosed.hs b/Data/Category/CartesianClosed.hs
--- a/Data/Category/CartesianClosed.hs
+++ b/Data/Category/CartesianClosed.hs
@@ -91,7 +91,7 @@
          -> Adjunction k k
               (ProductFunctor k :.: Tuple2 k k y)
               (ExpFunctor k :.: Tuple1 (Op k) k y)
-curryAdj y = mkAdjunction (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/Dialg.hs b/Data/Category/Dialg.hs
--- a/Data/Category/Dialg.hs
+++ b/Data/Category/Dialg.hs
@@ -106,6 +106,6 @@
 
 eilenbergMooreAdj :: (Functor m, Dom m ~ k, Cod m ~ k)
   => Monad m -> A.Adjunction (Alg m) k (FreeAlg m) (ForgetAlg m)
-eilenbergMooreAdj m = A.mkAdjunction (FreeAlg m) ForgetAlg
+eilenbergMooreAdj m = A.mkAdjunctionUnits (FreeAlg m) ForgetAlg
   (\x -> unit m ! x)
   (\(DialgA (Dialgebra _ h) _ _) -> DialgA (Dialgebra (src h) (monadFunctor m % h)) (Dialgebra (tgt h) h) h)
diff --git a/Data/Category/Functor.hs b/Data/Category/Functor.hs
--- a/Data/Category/Functor.hs
+++ b/Data/Category/Functor.hs
@@ -30,19 +30,20 @@
   , Proj2(..)
   , (:***:)(..)
   , DiagProd(..)
-  , Tuple1(..)
-  , Swap, swap
+  , Tuple1, tuple1
   , Tuple2, tuple2
+  , Swap, swap
 
   -- *** Hom functors
   , Hom(..)
-  , (:*-:)
-  , homX_
-  , (:-*:)
-  , hom_X
+  , (:*-:), homX_
+  , (:-*:), hom_X
+  , HomF, homF
+  , Star, star
+  , Costar, costar
 
 ) where
-  
+
 import Data.Category
 import Data.Category.Product
 
@@ -53,7 +54,7 @@
 
 -- | Functors map objects and arrows.
 class (Category (Dom ftag), Category (Cod ftag)) => Functor ftag where
-  
+
   -- | The domain, or source category, of the functor.
   type Dom ftag :: * -> * -> *
   -- | The codomain, or target category, of the functor.
@@ -61,7 +62,7 @@
 
   -- | @:%@ maps objects.
   type ftag :% a :: *
-  
+
   -- | @%@ maps arrows.
   (%)  :: ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
 
@@ -78,10 +79,10 @@
 
 -- | @Cat@ is the category with categories as objects and funtors as arrows.
 instance Category Cat where
-  
+
   src (CatA _)      = CatA Id
   tgt (CatA _)      = CatA Id
-  
+
   CatA f1 . CatA f2 = CatA (f1 :.: f2)
 
 
@@ -107,9 +108,9 @@
   type (g :.: h) :% a = g :% (h :% a)
 
   (g :.: h) % f = g % (h % f)
-  
 
 
+
 data Const (c1 :: * -> * -> *) (c2 :: * -> * -> *) x where
   Const :: Obj c2 x -> Const c1 c2 x
 
@@ -118,7 +119,7 @@
   type Dom (Const c1 c2 x) = c1
   type Cod (Const c1 c2 x) = c2
   type Const c1 c2 x :% a = x
-  
+
   Const x % _ = x
 
 -- | The constant functor with the same domain and codomain as f.
@@ -133,7 +134,7 @@
   type Dom (Opposite f) = Op (Dom f)
   type Cod (Opposite f) = Op (Cod f)
   type Opposite f :% a = f :% a
-  
+
   Opposite f % Op a = Op (f % a)
 
 
@@ -144,7 +145,7 @@
   type Dom (OpOp k) = Op (Op k)
   type Cod (OpOp k) = k
   type OpOp k :% a = a
-  
+
   OpOp % Op (Op f) = f
 
 
@@ -155,7 +156,7 @@
   type Dom (OpOpInv k) = k
   type Cod (OpOpInv k) = Op (Op k)
   type OpOpInv k :% a = a
-  
+
   OpOpInv % f = Op (Op f)
 
 
@@ -166,7 +167,7 @@
   type Dom (Proj1 c1 c2) = c1 :**: c2
   type Cod (Proj1 c1 c2) = c1
   type Proj1 c1 c2 :% (a1, a2) = a1
-  
+
   Proj1 % (f1 :**: _) = f1
 
 
@@ -177,7 +178,7 @@
   type Dom (Proj2 c1 c2) = c1 :**: c2
   type Cod (Proj2 c1 c2) = c2
   type Proj2 c1 c2 :% (a1, a2) = a2
-  
+
   Proj2 % (_ :**: f2) = f2
 
 
@@ -188,7 +189,7 @@
   type Dom (f1 :***: f2) = Dom f1 :**: Dom f2
   type Cod (f1 :***: f2) = Cod f1 :**: Cod f2
   type (f1 :***: f2) :% (a1, a2) = (f1 :% a1, f2 :% a2)
-  
+
   (g1 :***: g2) % (f1 :**: f2) = (g1 % f1) :**: (g2 % f2)
 
 
@@ -199,20 +200,22 @@
   type Dom (DiagProd k) = k
   type Cod (DiagProd k) = k :**: k
   type DiagProd k :% a = (a, a)
-  
+
   DiagProd % f = f :**: f
 
 
-data Tuple1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Tuple1 (Obj c1 a)
+type Tuple1 c1 c2 a = (Const c2 c1 a :***: Id c2) :.: DiagProd c2
 
 -- | 'Tuple1' tuples with a fixed object on the left.
-instance (Category c1, Category c2) => Functor (Tuple1 c1 c2 a1) where
-  type Dom (Tuple1 c1 c2 a1) = c2
-  type Cod (Tuple1 c1 c2 a1) = c1 :**: c2
-  type Tuple1 c1 c2 a1 :% a2 = (a1, a2)
-  
-  Tuple1 a % f = a :**: f
+tuple1 :: (Category c1, Category c2) => Obj c1 a -> Tuple1 c1 c2 a
+tuple1 a = (Const a :***: Id) :.: DiagProd
 
+-- type Tuple2 c1 c2 a = (Id c1 :***: Const c1 c2 a) :.: DiagProd c1
+--
+-- -- | 'Tuple2' tuples with a fixed object on the right.
+-- tuple2 :: (Category c1, Category c2) => Obj c2 a -> Tuple2 c1 c2 a
+-- tuple2 a = (Id :***: Const a) :.: DiagProd
+
 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
@@ -221,7 +224,7 @@
 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
+tuple2 a = swap :.: tuple1 a
 
 
 
@@ -232,16 +235,29 @@
   type Dom (Hom k) = Op k :**: k
   type Cod (Hom k) = (->)
   type (Hom k) :% (a1, a2) = k a1 a2
-  
+
   Hom % (Op f1 :**: f2) = \g -> f2 . g . f1
 
 
 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)
+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
+
+
+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)
+
+type Star f = HomF (Id (Cod f)) f
+star :: Functor f => f -> Star f
+star f = homF Id f
+
+type Costar f = HomF f (Id (Cod f))
+costar :: Functor f => f -> Costar f
+costar f = homF f Id
diff --git a/Data/Category/Kleisli.hs b/Data/Category/Kleisli.hs
--- a/Data/Category/Kleisli.hs
+++ b/Data/Category/Kleisli.hs
@@ -52,6 +52,6 @@
 
 kleisliAdj :: (Functor m, Dom m ~ k, Cod m ~ k)
   => Monad m -> A.Adjunction (Kleisli m) k (KleisliAdjF m) (KleisliAdjG m)
-kleisliAdj m = A.mkAdjunction (KleisliAdjF m) (KleisliAdjG m)
+kleisliAdj m = A.mkAdjunctionUnits (KleisliAdjF m) (KleisliAdjG m)
   (\x -> unit m ! x)
   (\(Kleisli _ x _) -> Kleisli m x (monadFunctor m % x))
diff --git a/Data/Category/Limit.hs b/Data/Category/Limit.hs
--- a/Data/Category/Limit.hs
+++ b/Data/Category/Limit.hs
@@ -39,6 +39,8 @@
   , HasLimits(..)
   , LimitFunctor(..)
   , limitAdj
+  , rightAdjointPreservesLimits
+  , rightAdjointPreservesLimitsInv
 
   -- * Colimits
   , ColimitFam
@@ -46,6 +48,8 @@
   , HasColimits(..)
   , ColimitFunctor(..)
   , colimitAdj
+  , leftAdjointPreservesColimits
+  , leftAdjointPreservesColimitsInv
 
   -- ** Limits of type Void
   , HasTerminalObject(..)
@@ -138,10 +142,33 @@
 
 -- | 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 = mkAdjunction diag LimitFunctor (\a -> limitFactorizer (diag % a) (diag % a)) (\f @ Nat{} -> limit f)
+limitAdj = mkAdjunctionUnits diag LimitFunctor (\a -> limitFactorizer (diag % a) (diag % a)) (\f @ Nat{} -> limit f)
   where diag = Diag :: Diag j k -- Forces the type of all Diags to be the same.
 
-
+-- Cone (g :.: t) (Limit (g :.: t))
+-- Obj j z -> d (Limit (g :.: t)) ((g :.: t) :% z)
+-- Obj j z -> d (f :% Limit (g :.: t)) (t :% z)
+-- Cone t (f :% Limit (g :.: t))
+-- d (f :% Limit (g :.: t)) (Limit t)
+-- d (Limit (g :.: t)) (g :% Limit t)
+rightAdjointPreservesLimits
+  :: (HasLimits j c, HasLimits j d) 
+  => Adjunction c d f g -> Obj (Nat j c) t -> d (Limit (g :.: t)) (g :% Limit t)
+rightAdjointPreservesLimits adj@(Adjunction f g _ _) (Nat t _ _) = 
+  leftAdjunct adj x (limitFactorizer (natId t) cone)
+    where
+      l = limit (natId (g :.: t))
+      x = coneVertex l
+      -- cone :: Cone t (f :% Limit (g :.: t))
+      cone = Nat (Const (f % x)) t (\z -> rightAdjunct adj (t % z) (l ! z))
+      
+-- Cone t (Limit t)
+-- Cone (g :.: t) (g :% Limit t)
+-- d (g :% Limit t) (Limit (g :.: t))
+rightAdjointPreservesLimitsInv
+  :: (HasLimits j c, HasLimits j d)
+  => Obj (Nat c d) g -> Obj (Nat j c) t -> d (g :% Limit t) (Limit (g :.: t))
+rightAdjointPreservesLimitsInv g@Nat{} t@Nat{} = limitFactorizer (g `o` t) (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 :: *) :: *
@@ -168,11 +195,26 @@
 
 -- | 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 = mkAdjunction ColimitFunctor diag (\f @ Nat{} -> colimit f) (\a -> colimitFactorizer (diag % a) (diag % a))
+colimitAdj = mkAdjunctionUnits 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.
 
 
+leftAdjointPreservesColimits
+  :: (HasColimits j c, HasColimits j d) 
+  => Adjunction c d f g -> Obj (Nat j d) t -> c (f :% Colimit t) (Colimit (f :.: t))
+leftAdjointPreservesColimits adj@(Adjunction f g _ _) (Nat t _ _) = 
+  rightAdjunct adj x (colimitFactorizer (natId t) cocone)
+    where
+      l = colimit (natId (f :.: t))
+      x = coconeVertex l
+      cocone = Nat t (Const (g % x)) (\z -> leftAdjunct adj (t % z) (l ! z))
 
+leftAdjointPreservesColimitsInv
+  :: (HasColimits j c, HasColimits j d) 
+  => Obj (Nat d c) f -> Obj (Nat j d) t -> c (Colimit (f :.: t)) (f :% Colimit t)
+leftAdjointPreservesColimitsInv f@Nat{} t@Nat{} = colimitFactorizer (f `o` t) (constPrecompOut (f `o` colimit t))
+
+
 class Category k => HasTerminalObject k where
 
   type TerminalObject k :: *
@@ -317,9 +359,9 @@
   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
 
-  (&&&) :: (k a x) -> (k a y) -> (k a (BinaryProduct k x y))
+  (&&&) :: k a x -> k a y -> k a (BinaryProduct k x y)
 
-  (***) :: (k a1 b1) -> (k a2 b2) -> (k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2))
+  (***) :: k a1 b1 -> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
   l *** r = (l . proj1 (src l) (src r)) &&& (r . proj2 (src l) (src r))
 
 
@@ -333,20 +375,20 @@
   limit = limit'
     where
       limit' :: forall f. Obj (Nat (i :++: j) k) f -> Cone f (Limit f)
-      limit' l@Nat{} = Nat (Const (x *** y)) (srcF l) (\z -> unCom (h z))
+      limit' l@Nat{} = Nat (Const (x *** y)) (srcF l) h
         where
           x = coneVertex lim1
           y = coneVertex lim2
           lim1 = limit (l `o` natId Inj1)
           lim2 = limit (l `o` natId Inj2)
-          h :: Obj (i :++: j) z -> Com (ConstF f (LimitFam (i :++: j) k f)) f z
-          h (I1 n) = Com (lim1 ! n . proj1 x y)
-          h (I2 n) = Com (lim2 ! n . proj2 x y)
+          h :: Obj (i :++: j) z -> Component (ConstF f (LimitFam (i :++: j) k f)) f z
+          h (I1 n) = lim1 ! n . proj1 x y
+          h (I2 n) = lim2 ! n . proj2 x y
 
   limitFactorizer l@Nat{} c =
-    limitFactorizer (l `o` natId Inj1) ((c `o` natId Inj1) . constPostcompInv (srcF c) Inj1)
+    limitFactorizer (l `o` natId Inj1) (constPostcompIn (c `o` natId Inj1))
     &&&
-    limitFactorizer (l `o` natId Inj2) ((c `o` natId Inj2) . constPostcompInv (srcF c) Inj2)
+    limitFactorizer (l `o` natId Inj2) (constPostcompIn (c `o` natId Inj2))
 
 
 -- | The tuple is the binary product in @Hask@.
@@ -423,7 +465,7 @@
 
 -- | A specialisation of the limit adjunction to products.
 prodAdj :: HasBinaryProducts k => Adjunction (k :**: k) k (DiagProd k) (ProductFunctor k)
-prodAdj = mkAdjunction DiagProd ProductFunctor (\x -> x &&& x) (\(l :**: r) -> proj1 l r :**: proj2 l r)
+prodAdj = mkAdjunctionUnits DiagProd ProductFunctor (\x -> x &&& x) (\(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
@@ -453,9 +495,9 @@
   inj1 :: Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
   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 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))
+  (+++) :: 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)
 
 
@@ -469,20 +511,20 @@
   colimit = colimit'
     where
       colimit' :: forall f. Obj (Nat (i :++: j) k) f -> Cocone f (Colimit f)
-      colimit' l@Nat{} = Nat (srcF l) (Const (x +++ y)) (\z -> unCom (h z))
+      colimit' l@Nat{} = Nat (srcF l) (Const (x +++ y)) h
         where
           x = coconeVertex col1
           y = coconeVertex col2
           col1 = colimit (l `o` natId Inj1)
           col2 = colimit (l `o` natId Inj2)
-          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)
+          h :: Obj (i :++: j) z -> Component f (ConstF f (ColimitFam (i :++: j) k f)) z
+          h (I1 n) = inj1 x y . col1 ! n
+          h (I2 n) = inj2 x y . col2 ! n
 
   colimitFactorizer l@Nat{} c =
-    colimitFactorizer (l `o` natId Inj1) (constPostcomp (tgtF c) Inj1 . (c `o` natId Inj1))
+    colimitFactorizer (l `o` natId Inj1) (constPostcompOut (c `o` natId Inj1))
     |||
-    colimitFactorizer (l `o` natId Inj2) (constPostcomp (tgtF c) Inj2 . (c `o` natId Inj2))
+    colimitFactorizer (l `o` natId Inj2) (constPostcompOut (c `o` natId Inj2))
 
 
 -- | The coproduct of categories ':++:' is the binary coproduct in 'Cat'.
@@ -549,7 +591,7 @@
 
 -- | A specialisation of the colimit adjunction to coproducts.
 coprodAdj :: HasBinaryCoproducts k => Adjunction k (k :**: k) (CoproductFunctor k) (DiagProd k)
-coprodAdj = mkAdjunction CoproductFunctor DiagProd (\(l :**: r) -> inj1 l r :**: inj2 l r) (\x -> x ||| x)
+coprodAdj = mkAdjunctionUnits CoproductFunctor DiagProd (\(l :**: r) -> inj1 l r :**: inj2 l r) (\x -> x ||| x)
 
 data p :+: q where
   (:+:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k, HasBinaryCoproducts k) => p -> q -> p :+: q
@@ -636,3 +678,18 @@
 
   colimit (Nat f _ _) = Nat f (Const (f % terminalObject)) (\z -> f % terminate z)
   colimitFactorizer Nat{} n = n ! terminalObject
+
+
+data ForAll f = ForAll (forall a. Obj (->) a -> f :% a)
+type instance LimitFam (->) (->) f = ForAll f
+
+instance HasLimits (->) (->) where
+  limit (Nat f _ _) = Nat (Const (\x -> x)) f (\a (ForAll g) -> g a)
+  limitFactorizer Nat{} 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
+  colimit (Nat f _ _) = Nat f (Const (\x -> x)) Exists
+  colimitFactorizer Nat{} n = \(Exists a fa) -> (n ! a) fa
diff --git a/Data/Category/Monoidal.hs b/Data/Category/Monoidal.hs
--- a/Data/Category/Monoidal.hs
+++ b/Data/Category/Monoidal.hs
@@ -22,7 +22,7 @@
 import Data.Category
 import Data.Category.Functor
 import Data.Category.NaturalTransformation
-import Data.Category.Adjunction (Adjunction(Adjunction))
+import Data.Category.Adjunction
 import Data.Category.Limit
 import Data.Category.Product
 
@@ -143,7 +143,10 @@
 monadFunctor :: Monad f -> f
 monadFunctor (unit -> Nat _ f _) = f
 
+idMonad :: Category k => Monad (Id k)
+idMonad = MonoidObject (natId Id) (idPrecomp Id)
 
+
 -- | A comonad is a comonoid in the category of endofunctors.
 type Comonad f = ComonoidObject (EndoFunctorCompose (Dom f)) f
 
@@ -157,11 +160,30 @@
   , comultiply = Nat f (f :.: f) dupl
   }
 
+idComonad :: Category k => Comonad (Id k)
+idComonad = ComonoidObject (natId Id) (idPrecompInv Id)
 
+
 -- | Every adjunction gives rise to an associated monad.
 adjunctionMonad :: Adjunction c d f g -> Monad (g :.: f)
-adjunctionMonad (Adjunction f g un coun) = mkMonad (g :.: f) (un !) ((Wrap g f % coun) !)
+adjunctionMonad adj@(Adjunction f g _ _) = 
+  let MonoidObject ret mult = adjunctionMonadT adj idMonad 
+  in mkMonad (g :.: f) (ret !) (mult !)
 
+-- | Every adjunction gives rise to an associated monad transformer.
+adjunctionMonadT :: (Dom m ~ c) => Adjunction c d f g -> Monad m -> Monad (g :.: m :.: f)
+adjunctionMonadT adj@(Adjunction f g _ _) (MonoidObject ret@(Nat _ m _) mult) = mkMonad (g :.: m :.: f) 
+  ((Wrap g f % ret . idPrecompInv g `o` natId f . adjunctionUnit adj) !) 
+  ((Wrap g f % (mult . idPrecomp m `o` natId m . Wrap m m % adjunctionCounit adj)) !)
+
 -- | Every adjunction gives rise to an associated comonad.
 adjunctionComonad :: Adjunction c d f g -> Comonad (f :.: g)
-adjunctionComonad (Adjunction f g un coun) = mkComonad (f :.: g) (coun !) ((Wrap f g % un) !)
+adjunctionComonad adj@(Adjunction f g _ _) = 
+  let ComonoidObject extr dupl = adjunctionComonadT adj idComonad
+  in mkComonad (f :.: g) (extr !) (dupl !)
+
+-- | Every adjunction gives rise to an associated comonad transformer.
+adjunctionComonadT :: (Dom w ~ d) => Adjunction c d f g -> Comonad w -> Comonad (f :.: w :.: g)
+adjunctionComonadT adj@(Adjunction f g _ _) (ComonoidObject extr@(Nat w _ _) dupl) = mkComonad (f :.: w :.: g) 
+  ((adjunctionCounit adj . idPrecomp f `o` natId g . Wrap f g % extr) !)
+  ((Wrap f g % (Wrap w w % adjunctionUnit adj . idPrecompInv w `o` natId w . dupl)) !)
diff --git a/Data/Category/NNO.hs b/Data/Category/NNO.hs
--- a/Data/Category/NNO.hs
+++ b/Data/Category/NNO.hs
@@ -10,7 +10,6 @@
 -----------------------------------------------------------------------------
 module Data.Category.NNO where
 
-import Data.Category
 import Data.Category.Functor
 import Data.Category.Limit
 import Data.Category.Unit
@@ -58,5 +57,5 @@
   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 s % Fix (I1 Unit) = z % Unit
+  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
@@ -13,7 +13,6 @@
   -- * Natural transformations
     (:~>)
   , Component
-  , Com(..)
   , (!)
   , o
   , natId
@@ -24,6 +23,7 @@
   , Nat(..)
   , Endo
   , Presheaves
+  , Profunctors
 
   -- * Functor isomorphisms
   , compAssoc
@@ -32,10 +32,10 @@
   , idPrecompInv
   , idPostcomp
   , idPostcompInv
-  , constPrecomp
-  , constPrecompInv
-  , constPostcomp
-  , constPostcompInv
+  , constPrecompIn
+  , constPrecompOut
+  , constPostcompIn
+  , constPostcompOut
 
   -- * Related functors
   , FunctorCompose(..)
@@ -69,10 +69,6 @@
 -- | A component for an object @z@ is an arrow from @F z@ to @G z@.
 type Component f g z = Cod f (f :% z) (g :% z)
 
--- | A newtype wrapper for components,
---   which can be useful for helper functions dealing with components.
-newtype Com f g z = Com { unCom :: Component f g z }
-
 -- | 'n ! a' returns the component for the object @a@ of a natural transformation @n@.
 --   This can be generalized to any arrow (instead of just identity arrows).
 (!) :: (Category c, Category d) => Nat c d f g -> c a b -> d (f :% a) (g :% b)
@@ -126,21 +122,17 @@
 idPostcompInv f = Nat f (Id :.: f) (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)
+constPrecompIn :: Nat j d (f :.: Const j c x) g -> Nat j d (Const j d (f :% x)) g
+constPrecompIn (Nat (f :.: Const x) g n) = Nat (Const (f % x)) g n
 
-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)
+constPrecompOut :: Nat j d f (g :.: Const j c x) -> Nat j d f (Const j d (g :% x))
+constPrecompOut (Nat f (g :.: Const x) n) = Nat f (Const (g % x)) n
 
-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)
+constPostcompIn :: Nat j d (Const k d x :.: f) g -> Nat j d (Const j d x) g
+constPostcompIn (Nat (Const x :.: _) g n) = Nat (Const x) g n
 
-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)
+constPostcompOut :: Nat j d f (Const k d x :.: g) -> Nat j d f (Const j d x)
+constPostcompOut (Nat f (Const x :.: _) n) = Nat f (Const x) n
 
 
 data FunctorCompose (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) = FunctorCompose
@@ -161,6 +153,8 @@
 
 type Presheaves k = Nat (Op k) (->)
 
+type Profunctors c d = Nat (Op d :**: c) (->)
+
 -- | @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
@@ -171,7 +165,7 @@
 --   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)
+postcompose f = FunctorCompose :.: tuple1 (natId f)
 
 
 data Wrap f h = Wrap f h
@@ -200,4 +194,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.cabal b/data-category.cabal
--- a/data-category.cabal
+++ b/data-category.cabal
@@ -1,5 +1,5 @@
 name:                data-category
-version:             0.6.2
+version:             0.7
 synopsis:            Category theory
 
 description:         Data-category is a collection of categories, and some categorical constructions on them.