diff --git a/category-extras.cabal b/category-extras.cabal
--- a/category-extras.cabal
+++ b/category-extras.cabal
@@ -1,6 +1,6 @@
 name:                   category-extras
 category:               Control, Monads, Comonads
-version:                0.50.3
+version:                0.51.0
 license:                BSD3
 cabal-version:          >= 1.2
 license-file:           LICENSE
@@ -19,23 +19,23 @@
                         Envelopes and Barbed Wire/.
 build-type:             Simple
 
-flag ArrowSubclassesCategory {
+flag ArrowSubclassesCategory
         description:    Indicates Control.Category is available and that the standard library has
                         its arrows subclass Control.Category.Category
         default:        True
-}
 
-flag TypeFamilies {
-       description:    Support for Type Families is available to us
-}
+flag RedefinableEitherMonad
+        description:         Indicates Control.Monad.Error isn't baked into the Prelude
 
-flag Optimize { 
+flag TypeFamilies
+        description:    Support for Type Families is available to us
+
+flag Optimize
         description:    Enable optimizations
         default:        False
-}
 
-library { 
-        build-depends:  base > 3, mtl, array
+library
+        build-depends:  mtl >= 1.1
         extensions:
                 CPP,
                 EmptyDataDecls,
@@ -77,6 +77,7 @@
                 Control.Functor.Adjunction.HigherOrder,
                 Control.Functor.Algebra,
                 Control.Functor.Algebra.Elgot,
+                Control.Functor.Categorical,
                 Control.Functor.Composition,
                 Control.Functor.Combinators.Const,
                 Control.Functor.Combinators.Lift,
@@ -98,6 +99,7 @@
                 Control.Functor.Pointed.Composition,
                 Control.Functor.Representable,
                 Control.Functor.Strong,
+                Control.Functor.Yoneda,
                 Control.Functor.Zip,
                 Control.Functor.Zap,
                 Control.Monad.Free,
@@ -119,6 +121,7 @@
                 Control.Morphism.Para,
                 Control.Morphism.Dyna,
                 Control.Morphism.Apo,
+                Control.Morphism.Universal,
                 Control.Morphism.Zygo,
                 Control.Morphism.Histo,
                 Data.Void
@@ -126,20 +129,22 @@
         hs-source-dirs:         src
         ghc-options:            -Wall 
 
-        if flag(ArrowSubclassesCategory) {
-                build-depends: ghc >= 6.9
+        if flag(ArrowSubclassesCategory)
+                build-depends: ghc >= 6.9, base > 3, array
                 cpp-options: -D__ARROW_SUBCLASSES_CATEGORY__=1
-        } else { 
-                build-depends: ghc < 6.9
-        }
+        else
+                build-depends: ghc < 6.9, base
+                hs-source-dirs: pre-6.9
+                exposed-modules: Control.Category
 
-        if flag(TypeFamilies) {
+        if flag(RedefinableEitherMonad)
+                build-depends: ghc >= 6.8 
+        else
+                cpp-options: -D__BROKEN_EITHER__=1
+
+        if flag(TypeFamilies)
                 extensions: TypeFamilies
                 cpp-options: -D__TYPE_FAMILIES__=1
-        }
 
-        if flag(Optimize) {
+        if flag(Optimize)
                 ghc-options: -funbox-strict-fields -O2
-        }
-}
-
diff --git a/pre-6.9/Control/Category.hs b/pre-6.9/Control/Category.hs
new file mode 100644
--- /dev/null
+++ b/pre-6.9/Control/Category.hs
@@ -0,0 +1,20 @@
+module Control.Category 
+	( (>>>), (<<<), Category ((.), id)
+	) where
+
+import Prelude hiding (id,(.))
+import qualified Prelude hiding (flip)
+
+class Category (~>) where
+	(.) :: (b ~> c) -> (a ~> b) -> a ~> c
+	id :: a ~> a
+
+(<<<) :: Category (~>) => (b ~> c) -> (a ~> b) -> a ~> c
+(<<<) = (.)
+
+(>>>) :: Category (~>) => (a ~> b) -> (b ~> c) -> a ~> c
+(>>>) = flip (.)
+
+instance Category (->) where
+	(.) = (Prelude..)
+	id = Prelude.id
diff --git a/src/Control/Category/Cartesian.hs b/src/Control/Category/Cartesian.hs
--- a/src/Control/Category/Cartesian.hs
+++ b/src/Control/Category/Cartesian.hs
@@ -27,7 +27,7 @@
 import Control.Category.Associative
 import Control.Category.Monoidal
 import Prelude hiding (Functor, map, (.), id, fst, snd, curry, uncurry)
-import qualified Prelude
+import qualified Prelude (fst,snd)
 import Control.Functor
 import Control.Category
 
diff --git a/src/Control/Category/Hask.hs b/src/Control/Category/Hask.hs
--- a/src/Control/Category/Hask.hs
+++ b/src/Control/Category/Hask.hs
@@ -8,9 +8,9 @@
 -- Stability	: experimental
 -- Portability	: portable
 --
+-- Make it clearer when we are dealing with the category (->) that we mean the category
+-- of haskell types via its Hom bifunctor (->)
 -------------------------------------------------------------------------------------------
-module Control.Category.Hask
-	( Hask
-	) where
+module Control.Category.Hask (Hask) where
 
 type Hask = (->) 
diff --git a/src/Control/Comonad/Cofree.hs b/src/Control/Comonad/Cofree.hs
--- a/src/Control/Comonad/Cofree.hs
+++ b/src/Control/Comonad/Cofree.hs
@@ -12,24 +12,19 @@
 ----------------------------------------------------------------------------
 module Control.Comonad.Cofree 
 	( Cofree
-	, outCofree, runCofree, anaCofree, cofree
-	, CofreeLike(unwrap)
-	, Expensive(..)
-	, coimprove, worsen
+	, runCofree, anaCofree, cofree
+	, ComonadCofree(outCofree)
 	) where
 
 import Control.Arrow ((&&&))
 import Control.Comonad
 import Control.Functor.Fix
 import Control.Functor.Combinators.Biff
-import Control.Functor.KanExtension
 import Control.Monad.Identity
+import Control.Comonad.Reader
 
 type Cofree f = Fix (PCofree f)
 
-outCofree :: Cofree f a -> f (Cofree f a)
-outCofree = snd . runCofree
-
 runCofree :: Cofree f a -> (a, f (Cofree f a))
 runCofree = runPCofree . outB
 
@@ -39,19 +34,11 @@
 cofree :: a -> f (Cofree f a) -> Cofree f a 
 cofree a as = InB $ Biff (Identity a,as)
 
-class (Functor f, Comonad w) => CofreeLike f w | w -> f where
-        unwrap :: w a -> f (w a)
-
-instance Functor f => CofreeLike f (Cofree f) where
-        unwrap = outCofree 
-
-instance CofreeLike f w => CofreeLike f (Lan w w) where
-        unwrap (Lan f c) = fmap (Lan f) (unwrap c)
-
-data Expensive f a = forall w. CofreeLike f w => Expensive { runExpensive :: w a }
+class (Functor f, Comonad w) => ComonadCofree f w | w -> f where
+        outCofree :: w a -> f (w a)
 
-coimprove :: Functor f => Cofree f a -> Expensive f a
-coimprove m = Expensive (coabs m)
+instance Functor f => ComonadCofree f (Cofree f) where
+        outCofree = snd . runCofree
 
-worsen :: Functor f => (forall w. CofreeLike f w => w a) -> Cofree f a
-worsen m = corep m 
+instance ComonadCofree f w => ComonadCofree f (CoreaderT w e) where
+	outCofree = fmap CoreaderT . outCofree . runCoreaderT
diff --git a/src/Control/Functor/Adjunction.hs b/src/Control/Functor/Adjunction.hs
--- a/src/Control/Functor/Adjunction.hs
+++ b/src/Control/Functor/Adjunction.hs
@@ -11,16 +11,21 @@
 --
 -------------------------------------------------------------------------------------------
 
-module Control.Functor.Adjunction where
+module Control.Functor.Adjunction 
+	( Adjunction (unit, counit, leftAdjunct, rightAdjunct)
+	, ACompF(ACompF)
+	) where
 
 import Control.Functor.Composition
 import Control.Functor.Exponential
 import Control.Functor.Full
+import Control.Functor.HigherOrder
 import Control.Applicative
 import Control.Monad.Reader
-import Control.Monad.Instances
-import Control.Comonad
+import Control.Monad.State
+import Control.Monad.Identity
 import Control.Comonad.Reader
+import Control.Comonad.Context
 
 -- | An 'Adjunction' formed by the 'Functor' f and 'Functor' g. 
 
@@ -30,7 +35,7 @@
 
 -- 2. @unit@ and @counit@
 
-class (Functor f, Functor g) => Adjunction f g where
+class (Functor f, Functor g) => Adjunction f g | f -> g, g -> f where
 	unit   :: a -> g (f a)
 	counit :: f (g a) -> a
 	leftAdjunct  :: (f a -> b) -> a -> g b
@@ -41,9 +46,12 @@
 	leftAdjunct f = fmap f . unit
 	rightAdjunct f = counit . fmap f
 
+instance (Adjunction f1 g1, Adjunction f2 g2) => Adjunction (CompF f2 f1) (CompF g1 g2) where
+	counit = counit . fmap (counit . fmap decompose) . decompose
+	unit = compose . fmap (fmap compose . unit) . unit
 
 -- | Adjunction-oriented composition, yields monads and comonads from adjunctions
-newtype ACompF f g a = ACompF (CompF f g a) deriving (Functor, ExpFunctor, Full, Composition)
+newtype ACompF f g a = ACompF (CompF f g a) deriving (Functor, ExpFunctor, Full, Composition, HFunctor)
 
 instance Adjunction f g => Pointed (ACompF g f) where
         point = compose . unit
@@ -70,4 +78,10 @@
 	unit a = Reader (\e -> Coreader e a)
 	counit (Coreader x f) = runReader f x
 
--- instance Adjunction f g => Adjunction (CoreaderT e f) (ReaderT e g) where
+instance ComonadContext e ((,)e `ACompF` (->)e) where
+	getC = fst . decompose
+	modifyC f = uncurry (flip id . f) . decompose
+
+instance MonadState e ((->)e `ACompF` (,)e) where
+	get = compose $ \s -> (s,s)
+	put s = compose $ const (s,())
diff --git a/src/Control/Functor/Adjunction/HigherOrder.hs b/src/Control/Functor/Adjunction/HigherOrder.hs
--- a/src/Control/Functor/Adjunction/HigherOrder.hs
+++ b/src/Control/Functor/Adjunction/HigherOrder.hs
@@ -15,6 +15,7 @@
 	) where
 
 import Control.Functor.HigherOrder
+import Control.Functor.HigherOrder.Composition
 import Control.Functor.Extras
 
 class (HFunctor f, HFunctor g) => HAdjunction f g where
@@ -27,3 +28,8 @@
         hcounit = hrightAdjunct id
         hleftAdjunct f = hfmap f . hunit
         hrightAdjunct f = hcounit . hfmap f
+
+
+instance (HAdjunction f1 g1, HAdjunction f2 g2) => HAdjunction (CompH f2 f1) (CompH g1 g2) where
+        hcounit = hcounit . hfmap (hcounit . hfmap hdecompose) . hdecompose
+        hunit = hcompose . hfmap (hfmap hcompose . hunit) . hunit
diff --git a/src/Control/Functor/Algebra/Elgot.hs b/src/Control/Functor/Algebra/Elgot.hs
--- a/src/Control/Functor/Algebra/Elgot.hs
+++ b/src/Control/Functor/Algebra/Elgot.hs
@@ -13,31 +13,22 @@
 --
 -- Elgot algebras given you a shortcircuitable hylomorphism where you
 -- can directly return a sub-answer to the catamorphism.
+-- 
+-- Elgot coalgebras are defined in:
+-- <http://comonad.com/reader/2008/elgot-coalgebras/>
 ----------------------------------------------------------------------------
 module Control.Functor.Algebra.Elgot
 	( elgot
 	, coelgot
---	, g_elgot
---	, g_coelgot
 	) where
 
 import Control.Arrow ((|||),(&&&))
 import Control.Functor.Algebra
--- import Control.Functor.Extras
--- import Control.Comonad
--- import Control.Monad
 
+-- | Elgot algebra
 elgot :: Functor f => Algebra f a -> (b -> Either a (f b)) -> b -> a
 elgot phi psi = h where h = (id ||| phi . fmap h) . psi
 
+-- | Elgot coalgebra
 coelgot :: Functor f => ((a, f b) -> b) -> Coalgebra f a -> a -> b
 coelgot phi psi = h where h = phi . (id &&& fmap h . psi)
-
--- ideally this would have b -> Either a (f b)
--- g_elgot :: (Comonad w, Functor f) => Dist f w -> GAlgebra f w a -> (b -> Either (w a) (f b)) -> b -> a
--- g_elgot k phi psi = extract . h where 
--- 	h = (id ||| liftW phi . k . fmap (duplicate . h)) . psi
-
--- g_coelgot :: (Monad m, Functor f) => Dist m f -> ((m a, f b) -> b) -> GCoalgebra f m a -> a -> b
--- g_coelgot k phi psi = h . return where
---	h = phi . (id &&& fmap (h . join) . k . liftM psi)
diff --git a/src/Control/Functor/Categorical.hs b/src/Control/Functor/Categorical.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Functor/Categorical.hs
@@ -0,0 +1,64 @@
+-------------------------------------------------------------------------------------------
+-- |
+-- Module	: Control.Functor.Categorical
+-- Copyright 	: 2008 Edward Kmett
+-- License	: BSD3
+--
+-- Maintainer	: Edward Kmett <ekmett@gmail.com>
+-- Stability	: experimental
+-- Portability	: non-portable (functional-dependencies)
+--
+-- A more categorical definition of Functor than endofunctors in the category Hask
+-------------------------------------------------------------------------------------------
+module Control.Functor.Categorical
+	( CFunctor (cmap)
+	) where
+
+import Prelude hiding (id,(.))
+import Control.Category
+import Control.Category.Hask
+import Control.Monad.Identity
+import Control.Monad.List
+import Control.Monad.Cont
+
+import Control.Monad.Reader
+import Control.Monad.Writer as LW
+import Control.Monad.State as LS
+
+import Control.Monad.RWS as LRWS
+#if __GLASGOW_HASKELL__ >= 608
+import Control.Monad.Writer.Strict as SW
+import Control.Monad.State.Strict as SS
+import Control.Monad.RWS.Strict as SRWS
+#endif
+
+class (Category r, Category s) => CFunctor f r s | f r -> s,  f s -> r where
+	cmap :: r a b -> s (f a) (f b)
+
+instance CFunctor ([]) Hask Hask where cmap = fmap 
+instance CFunctor Maybe Hask Hask where cmap = fmap
+instance CFunctor (Either a) Hask Hask where cmap = fmap 
+instance CFunctor Identity Hask Hask where cmap = fmap
+instance CFunctor ((,)e) Hask Hask where cmap = fmap
+instance CFunctor (Reader e) Hask Hask where cmap = fmap
+instance CFunctor (LW.Writer e) Hask Hask where cmap = fmap
+instance CFunctor (LS.State s) Hask Hask where cmap = fmap
+instance CFunctor (Cont e) Hask Hask where cmap = fmap
+instance CFunctor (LRWS.RWS r w s) Hask Hask where cmap = fmap
+instance CFunctor IO Hask Hask where cmap = fmap
+
+instance Monad m => CFunctor (ReaderT e m) Hask Hask where cmap = fmap
+instance Monad m => CFunctor (LW.WriterT e m) Hask Hask where cmap = fmap
+instance Monad m => CFunctor (LS.StateT e m) Hask Hask where cmap = fmap
+instance Monad m => CFunctor (ContT r m) Hask Hask where cmap = fmap
+instance Monad m => CFunctor (ListT m) Hask Hask where cmap = fmap
+instance Monad m => CFunctor (LRWS.RWST r w s m) Hask Hask where cmap = fmap
+
+#if __GLASGOW_HASKELL__ >= 608
+instance CFunctor (SW.Writer e) Hask Hask where cmap = fmap
+instance CFunctor (SS.State s) Hask Hask where cmap = fmap
+instance CFunctor (SRWS.RWS r w s) Hask Hask where cmap = fmap
+instance Monad m => CFunctor (SW.WriterT w m) Hask Hask where cmap = fmap
+instance Monad m => CFunctor (SS.StateT s m) Hask Hask where cmap = fmap
+instance Monad m => CFunctor (SRWS.RWST r w s m) Hask Hask where cmap = fmap
+#endif
diff --git a/src/Control/Functor/Combinators/Flip.hs b/src/Control/Functor/Combinators/Flip.hs
--- a/src/Control/Functor/Combinators/Flip.hs
+++ b/src/Control/Functor/Combinators/Flip.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE TypeFamilies #-}
 -------------------------------------------------------------------------------------------
 -- |
 -- Module	: Control.Functor.Combinators.Flip
diff --git a/src/Control/Functor/Combinators/Lift.hs b/src/Control/Functor/Combinators/Lift.hs
--- a/src/Control/Functor/Combinators/Lift.hs
+++ b/src/Control/Functor/Combinators/Lift.hs
@@ -25,6 +25,7 @@
 import Control.Functor.Contra
 import Control.Functor.Exponential
 import Control.Functor.Full
+import Control.Functor.HigherOrder
 import Control.Monad.Identity
 import Control.Functor.Pointed
 import Control.Arrow ((&&&),(|||))
@@ -49,6 +50,11 @@
 
 instance (Bifunctor p Hask Hask Hask, ExpFunctor f ,ExpFunctor g) => ExpFunctor (Lift p f g) where
         xmap f g = Lift . bimap (xmap f g) (xmap f g) . runLift
+
+instance (Bifunctor p Hask Hask Hask) => HFunctor (Ap p) where
+        ffmap f = Lift . bimap (fmap f) (fmap f) . runLift
+        hfmap f = Lift . second f . runLift
+
 
 type (f :*: g) = Lift (,) f g
 
diff --git a/src/Control/Functor/Composition.hs b/src/Control/Functor/Composition.hs
--- a/src/Control/Functor/Composition.hs
+++ b/src/Control/Functor/Composition.hs
@@ -9,7 +9,10 @@
 -- Stability	: experimental
 -- Portability	: non-portable (class-associated types)
 --
--- Generalized functor composeosition.
+-- Generalized functor composition.
+-- Since we have many reasons for which you might want to compose a functor, and many 
+-- expected results. i.e. monads via adjunctions, monads via composition with a pointed
+-- endofunctor, etc. we have to make multiple composition operators.
 -------------------------------------------------------------------------------------------
 
 module Control.Functor.Composition
@@ -27,6 +30,7 @@
 import Control.Functor
 import Control.Functor.Exponential
 import Control.Functor.Full
+import Control.Functor.HigherOrder
 import Control.Category.Hask
 import Control.Category.Braided
 
@@ -34,12 +38,18 @@
 	decompose  :: (f `o` g) x -> f (g x)
 	compose    :: f (g x) -> (f `o` g) x
 
+-- | Basic functor composition
 newtype CompF f g a = CompF { runCompF :: f (g a) }
 
 instance Composition CompF where
 	compose = CompF
 	decompose = runCompF
 
+instance Functor f => HFunctor (CompF f) where
+	ffmap = fmap
+	hfmap f = compose . fmap f . decompose
+
+-- | An infix alias for functor composition
 type (:.:) = CompF
 
 -- common functor composition traits
@@ -52,14 +62,19 @@
 instance (Full f, Full g) => Full (CompF f g) where
         premap f = premap . premap $ decompose . f . compose
 
+-- | The only reason the compositions are all the same is for type inference. This can be liberalized.
 associateComposition :: (Functor f, Composition c) => c (c f g) h a -> c f (c g h) a
 associateComposition = compose . fmap compose . decompose . decompose
 
 coassociateComposition :: (Functor f, Composition c) => c f (c g h) a -> c (c f g) h a
 coassociateComposition = compose . compose . fmap decompose . decompose
 
+
+-- | Bifunctor composition
 newtype Comp p f g a b = Comp { runComp :: p (f a b) (g a b) }
+-- | Bifunctor coproduct
 type (:++:) = Comp Either
+-- | Bifunctor product
 type (:**:) = Comp (,)
 
 instance (Bifunctor p c d Hask, PFunctor f a c, PFunctor g a d) => PFunctor (Comp p f g) a Hask where
diff --git a/src/Control/Functor/Extras.hs b/src/Control/Functor/Extras.hs
--- a/src/Control/Functor/Extras.hs
+++ b/src/Control/Functor/Extras.hs
@@ -15,9 +15,15 @@
 infixr 0 :~>, :~~> -- to match ->
 
 type Dist f g = forall a. f (g a) -> g (f a)
+
 -- A natural transformation between functors f and g.
 type f :~> g = forall a. f a -> g a
+
+-- Its bifunctorial analogue
 type f :~~> g = forall a b. f a b -> g a b
+
+-- Dinatural transformations
+type Dinatural f g = forall a. f a a -> g a a
 
 class PostFold m f where
         postFold :: f (m (f a)) -> m (f a)
diff --git a/src/Control/Functor/HigherOrder.hs b/src/Control/Functor/HigherOrder.hs
--- a/src/Control/Functor/HigherOrder.hs
+++ b/src/Control/Functor/HigherOrder.hs
@@ -22,8 +22,13 @@
 	, LowerH(..)
 	) where
 
+import Control.Functor
 import Control.Functor.Pointed
 import Control.Functor.Extras
+import Control.Monad.Reader
+import Control.Monad.State.Lazy
+import Control.Monad.Writer.Lazy
+import Control.Monad.List
 
 type HAlgebra f g = f g :~> g
 type HCoalgebra f g = g :~> f g
@@ -53,6 +58,34 @@
 
 instance (HCopointed h, Copointed f) => Copointed (LowerH h f) where
 	extract = extract . hextract . liftH
+
+instance HFunctor (ReaderT e) where
+	ffmap f g = ReaderT (fmap f . runReaderT g) 
+	hfmap f g = ReaderT (f . runReaderT g)
+
+instance HPointed (ReaderT e) where
+	hreturn = ReaderT . const
+
+instance HFunctor (StateT e) where
+	ffmap f (StateT g) = StateT (fmap (first f) . g)
+	hfmap f (StateT g) = StateT (f . g)
+
+instance HPointed (StateT e) where
+	hreturn m = StateT (\s -> fmap (\a -> (a,s)) m) 
+
+instance HFunctor (WriterT e) where
+	ffmap f = WriterT . fmap (first f) . runWriterT 
+	hfmap f = WriterT . f . runWriterT
+
+instance Monoid e => HPointed (WriterT e) where
+	hreturn = WriterT . fmap (\a -> (a,mempty))
+
+instance HFunctor ListT where
+	ffmap f = ListT . fmap (fmap f) . runListT 
+	hfmap f = ListT . f . runListT
+
+instance HPointed ListT where
+	hreturn = ListT . fmap return
 
 {-# RULES
 "hextract/hreturn" hextract . hreturn = id
diff --git a/src/Control/Functor/KanExtension.hs b/src/Control/Functor/KanExtension.hs
--- a/src/Control/Functor/KanExtension.hs
+++ b/src/Control/Functor/KanExtension.hs
@@ -11,31 +11,52 @@
 -- Left and right Kan extensions, expressed as higher order functors
 --
 -- Included is the 'monad generated by a functor' @Ran f f@
--- and the comonad cogenerated by a functor @Lan f f@.
+-- and the comonad cogenerated by a functor @Lan f f@
+-- and machinery for lifting (co)monads into and lowering (co)monads out of 
+-- Kan extensions.
 ----------------------------------------------------------------------------
 module Control.Functor.KanExtension 
-	( Ran(..)
+	( 
+	-- * Right Kan Extensions
+	  Ran(..)
 	, toRan, fromRan
+	, liftRan, lowerRan
+	, adjointToRan, ranToAdjoint
+	, ranToComposedAdjoint, composedAdjointToRan
+	, composeRan, decomposeRan
+	-- * Left Kan Extensions
 	, Lan(..)
 	, toLan, fromLan
-	, rep, abs
-	, corep, coabs
+	, liftLan, lowerLan
+	, adjointToLan, lanToAdjoint
+	, composeLan, decomposeLan
+	, lanToComposedAdjoint, composedAdjointToLan
+	-- * Performance tweaks for (co)free comonads
+	, improveFree
+	, worsenCofree
 	) where
 
 import Prelude hiding (abs)
+import Control.Comonad.Context
+import Control.Comonad.Cofree
 import Control.Functor.Composition
 import Control.Functor.Extras
 import Control.Functor.Pointed ()
 import Control.Functor.HigherOrder
-import Control.Comonad
-import Control.Monad.Cont
+import Control.Functor.Adjunction
+import Control.Monad.State
+import Control.Monad.Reader
+import Control.Monad.Identity
+import Control.Monad.Free
 
 -- | Right Kan Extension
 newtype Ran g h a = Ran { runRan :: forall b. (a -> g b) -> h b }
 
+-- | Nat(k `o` g, h) is isomorphic to Nat(k, Ran g h) (forwards)
 toRan :: (Composition o, Functor k) => (k `o` g :~> h) -> k :~> Ran g h
 toRan s t = Ran (s . compose . flip fmap t)
 
+-- | Nat(k `o` g, h) is isomorphic to Nat(k, Ran g h) (backwards)
 fromRan :: Composition o => (k :~> Ran g h) -> (k `o` g) :~> h
 fromRan s = flip runRan id . s . decompose
 
@@ -53,19 +74,61 @@
 	return = point
 	m >>= k = Ran (\c -> runRan m (\a -> runRan (k a) c))
 
--- | See <http://wwwtcs.inf.tu-dresden.de/%7Evoigt/mpc08.pdf>
-rep :: Monad m => m a -> Ran m m a
-rep m = Ran (m >>=)
+-- | The natural isomorphism from @Ran f (Ran g h)@ to @Ran (f `o` g) h@ (forwards)
+composeRan :: Composition o => Ran f (Ran g h) :~> Ran (f `o` g) h
+composeRan r = Ran (\f -> runRan (runRan r (decompose . f)) id)
 
-abs :: Monad m => Ran m m a -> m a 
-abs a = runRan a return
+-- | The natural isomorphism from @Ran f (Ran g h)@ to @Ran (f `o` g) h@ (backwards)
+decomposeRan :: (Functor f, Composition o) => Ran (f `o` g) h :~> Ran f (Ran g h)
+decomposeRan r = Ran (\f -> Ran (\g -> runRan r (compose . fmap g . f)))
 
+-- | Lift a monad into its right Kan extension along itself. This is the same operation
+-- as is performed by Voightlaender's rep in <http://wwwtcs.inf.tu-dresden.de/%7Evoigt/mpc08.pdf>
+-- and the ContT monad's lift operation. This is also viewable as the forward half of the 
+-- natural isomorphism between a monad m and the monad generated by m.
+liftRan :: Monad m => m a -> Ran m m a
+liftRan m = Ran (m >>=)
+
+-- | The natural isomorphism between a monad m and the monad generated by m (backwards)
+lowerRan :: Monad m => Ran m m a -> m a 
+lowerRan a = runRan a return
+
+instance MonadReader r m => MonadReader r (Ran m m) where
+	ask = liftRan ask
+	local f m = Ran (\c -> ask >>= \r -> local f (runRan m (local (const r) . c)))
+
+instance MonadIO m => MonadIO (Ran m m) where
+	liftIO = liftRan . liftIO 
+
+instance MonadState s m => MonadState s (Ran m m) where
+	get = liftRan get
+	put = liftRan . put
+
+instance MonadFree f m => MonadFree f (Ran m m) where
+        inFree t = Ran (inFree . flip fmap t . flip runRan)
+
+-- | @f -| g@ iff @Ran g Identity@ exists (forward)
+adjointToRan :: Adjunction f g => f :~> Ran g Identity
+adjointToRan f = Ran (\a -> Identity $ rightAdjunct a f)
+
+-- | @f -| g@ iff @Ran g Identity@ exists (backwards)
+ranToAdjoint :: Adjunction f g => Ran g Identity :~> f
+ranToAdjoint r = runIdentity (runRan r unit)
+
+ranToComposedAdjoint :: (Composition o, Adjunction f g) => Ran g h :~> (h `o` f)
+ranToComposedAdjoint r = compose (runRan r unit)
+
+composedAdjointToRan :: (Functor h, Composition o, Adjunction f g) => (h `o` f) :~> Ran g h
+composedAdjointToRan f = Ran (\a -> fmap (rightAdjunct a) (decompose f))
+
 -- | Left Kan Extension
 data Lan g h a = forall b. Lan (g b -> a) (h b)
 
+-- | @Nat(h, f.g)@ is isomorphic to @Nat (Lan g h, f)@ (forwards)
 toLan :: (Composition o, Functor f) => (h :~> (f `o` g)) -> Lan g h :~> f
 toLan s (Lan f v) = fmap f . decompose $ s v
 
+-- | @Nat(h, f.g)@ is isomorphic to @Nat (Lan g h, f)@ (backwards)
 fromLan :: Composition o => (Lan g h :~> f) -> h :~> (f `o` g)
 fromLan s = compose . s . Lan id
 
@@ -82,9 +145,51 @@
 instance Comonad (Lan f f) where
 	duplicate (Lan f ws) = Lan (Lan f) ws
 
-coabs :: Comonad w => w a -> Lan w w a
-coabs = Lan extract 
+-- | The natural isomorphism between a comonad w and the comonad generated by w (forwards).
+liftLan :: Comonad w => w a -> Lan w w a
+liftLan = Lan extract 
 
-corep :: Comonad w => Lan w w a -> w a 
-corep (Lan f c) = extend f c
+-- | The natural isomorphism between a comonad w and the comonad generated by w (backwards).
+lowerLan :: Comonad w => Lan w w a -> w a 
+lowerLan (Lan f c) = extend f c
 
+-- | f -| g iff Lan f Identity is inhabited (forwards)
+adjointToLan :: Adjunction f g => g :~> Lan f Identity
+adjointToLan = Lan counit . Identity
+
+-- | f -| g iff Lan f Identity is inhabited (backwards)
+lanToAdjoint :: Adjunction f g => Lan f Identity :~> g
+lanToAdjoint (Lan f v) = leftAdjunct f (runIdentity v)
+
+lanToComposedAdjoint :: (Functor h, Composition o, Adjunction f g) => Lan f h :~> (h `o` g)
+lanToComposedAdjoint (Lan f v) = compose (fmap (leftAdjunct f) v)
+
+composedAdjointToLan :: (Composition o, Adjunction f g) => (h `o` g) :~> Lan f h 
+composedAdjointToLan = Lan counit . decompose
+
+instance ComonadContext e m => ComonadContext e (Lan m m) where
+        getC = getC . lowerLan 
+	modifyC f = modifyC f . lowerLan
+
+instance ComonadCofree f w => ComonadCofree f (Lan w w) where
+        outCofree (Lan f c) = fmap (Lan f) (outCofree c)
+
+-- | the natural isomorphism from @Lan f (Lan g h)@ to @Lan (f `o` g) h@ (forwards)
+composeLan :: (Functor f, Composition o) => Lan f (Lan g h) :~> Lan (f `o` g) h
+composeLan (Lan f (Lan g h)) = Lan (f . fmap g . decompose) h
+
+-- | the natural isomorphism from @Lan f (Lan g h)@ to @Lan (f `o` g) h@ (backwards)
+decomposeLan :: Composition o => Lan (f `o` g) h :~> Lan f (Lan g h)
+decomposeLan (Lan f h) = Lan (f . compose) (Lan id h)
+
+
+-- | Voigtlaender's asymptotic performance improvement for free monads
+improveFree :: Functor f => (forall m. MonadFree f m => m a) -> Free f a
+improveFree m = lowerRan m
+
+worsenCofree :: Functor f => (forall w. ComonadCofree f w => w a) -> Cofree f a
+worsenCofree m = lowerLan m
+
+-- data AnyCofree f a = forall w. ComonadCofree f w => AnyCofree { runAnyCofree :: w a }
+-- coimprove :: Functor f => Cofree f a -> AnyCofree f a
+-- coimprove m = AnyCofree (liftLan m)
diff --git a/src/Control/Functor/Strong.hs b/src/Control/Functor/Strong.hs
--- a/src/Control/Functor/Strong.hs
+++ b/src/Control/Functor/Strong.hs
@@ -13,12 +13,12 @@
 
 module Control.Functor.Strong where
 
-import Prelude hiding (sequence)
+import Prelude hiding (sequence,Either)
 import Data.Traversable
-import Control.Monad.Either ()
+import Control.Monad.Either (Either(..))
 
-strength :: Functor f => f a -> b -> f (a,b)
-strength fa b = fmap (\a -> (a,b)) fa
+strength :: Functor f => a -> f b -> f (a,b)
+strength a fb = fmap ((,)a) fb
 
 costrength :: Traversable f => f (Either a b) -> Either a (f b)
 costrength = sequence
diff --git a/src/Control/Functor/Yoneda.hs b/src/Control/Functor/Yoneda.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Functor/Yoneda.hs
@@ -0,0 +1,34 @@
+-------------------------------------------------------------------------------------------
+-- |
+-- Module	: Control.Functor.Yoneda
+-- Copyright 	: 2008 Edward Kmett
+-- License	: BSD
+--
+-- Maintainer	: Edward Kmett <ekmett@gmail.com>
+-- Stability	: experimental
+-- Portability	: portable
+--
+-- The Yoneda lemma materialized as a Kan extension, and hence as a higher order functor
+-------------------------------------------------------------------------------------------
+
+module Control.Functor.Yoneda
+	( Yoneda
+	, toYoneda, fromYoneda
+	) where
+
+import Control.Functor.KanExtension
+import Control.Functor.Extras
+import Control.Monad.Identity
+
+type Yoneda = Ran Identity
+
+toYoneda :: Functor f => f :~> Yoneda f
+toYoneda a = Ran (\f -> fmap (runIdentity . f) a)
+
+fromYoneda :: Yoneda f :~> f 
+fromYoneda t = runRan t Identity
+
+-- newtype Yoneda f a = Yoneda { runYoneda :: forall b. (a -> b) -> f b } 
+-- instance HFunctor Yoneda where
+--	ffmap f (Yoneda t) = check (t f)
+--	hfmap f (Yoneda t) = Yoneda (f . t)
diff --git a/src/Control/Monad/Either.hs b/src/Control/Monad/Either.hs
--- a/src/Control/Monad/Either.hs
+++ b/src/Control/Monad/Either.hs
@@ -14,36 +14,42 @@
 -- therefore incompatible with Control.Monad.Error
 ----------------------------------------------------------------------------
 module Control.Monad.Either 
-	( Either(..)
-	, EitherT(..)
+	( Either(Left,Right)
+	, EitherT(EitherT,runEitherT)
 	) where
 
-import Data.Either
+import Control.Functor.Pointed
 import Control.Applicative
-import Control.Monad
 import Control.Monad.Fix
-import Control.Functor.Pointed
 
-newtype EitherT a m b = EitherT { runEitherT :: m (Either a b) }
+#if __BROKEN_EITHER__
+import Prelude hiding (Either(Left,Right))
+#endif
 
-{-
+-- we have to define our own because the Control.Monad.Error instance is 
+-- baked into the prelude on old versions.
+#if __BROKEN_EITHER__
+data Either a b = Left a | Right b
 instance Functor (Either e) where
 	fmap _ (Left a) = Left a
 	fmap f (Right a) = Right (f a)
+#endif
 
-instance Pointed (Either e) where
-	point = Right
--}
+newtype EitherT a m b = EitherT { runEitherT :: m (Either a b) }
 
-instance Applicative (Either e) where
-	pure = Right
-	(<*>) = ap
+-- defined in Control.Functor.Pointed
+--instance Pointed (Either e) where
+--	point = Right
 
 instance Monad (Either e) where
         return = Right
         Right m >>= k = k m
         Left e  >>= _ = Left e
 
+instance Applicative (Either e) where
+	pure = Right
+	a <*> b = do x <- a; y <- b; return (x y)
+
 instance MonadFix (Either e) where
 	mfix f = let 
 		a = f $ case a of
@@ -52,7 +58,7 @@
 		in a
 
 instance Functor f => Functor (EitherT a f) where
-        fmap f = EitherT . fmap (fmap f) . runEitherT
+	fmap f = EitherT . fmap (fmap f) . runEitherT
 
 instance Pointed f => Pointed (EitherT a f) where
 	point = EitherT . point . Right
diff --git a/src/Control/Monad/Free.hs b/src/Control/Monad/Free.hs
--- a/src/Control/Monad/Free.hs
+++ b/src/Control/Monad/Free.hs
@@ -19,30 +19,24 @@
 	( module Control.Monad.Parameterized
 	, PFree
 	, Free
-	, inFree
 	, runFree
 	, cataFree
 	, free
-	-- * Improving asymptotic performance with right Kan extensions
-	, FreeLike(wrap)
-	, improve
+	, MonadFree(inFree)
 	) where
 
-import Prelude hiding ((.),id,abs)
+import Prelude hiding ((.),id)
 import Control.Category
 import Control.Category.Cartesian
 import Control.Functor
 import Control.Functor.Combinators.Biff
-import Control.Functor.KanExtension
 import Control.Functor.Fix
 import Control.Monad.Parameterized
 import Control.Monad.Identity
+import Control.Monad.Reader
 
 type Free f = Fix (PFree f)
 
-inFree :: f (Free f a) -> Free f a
-inFree = InB . Biff . Right
-
 runFree :: Free f a -> Either a (f (Free f a))
 runFree = first runIdentity . runBiff . outB
 
@@ -52,14 +46,13 @@
 free :: Either a (f (Free f a)) -> Free f a
 free = InB . Biff . first Identity
 
-class (Functor f, Monad m) => FreeLike f m where
-        wrap :: f (m a) -> m a
+class (Functor f, Monad m) => MonadFree f m | m -> f where
+        inFree :: f (m a) -> m a
 
-instance FreeLike f m => FreeLike f (Ran m m) where
-        wrap t = Ran (wrap . flip fmap t . flip runRan)
+instance Functor f => MonadFree f (Free f) where
+        inFree = InB . Biff . Right
 
-instance Functor f => FreeLike f (Free f) where
-        wrap = inFree
+instance MonadFree f m => MonadFree f (ReaderT e m) where
+	inFree fma = ReaderT (\e -> inFree $ fmap (flip runReaderT e) fma)
 
-improve :: Functor f => (forall m. FreeLike f m => m a) -> Free f a
-improve m = abs m 
+-- instance (MonadFree f m, Traversable f) => MonadFree f (StateT e m) where
diff --git a/src/Control/Monad/Indexed/Cont.hs b/src/Control/Monad/Indexed/Cont.hs
--- a/src/Control/Monad/Indexed/Cont.hs
+++ b/src/Control/Monad/Indexed/Cont.hs
@@ -7,20 +7,25 @@
 --
 -- Maintainer	: Edward Kmett <ekmett@gmail.com>
 -- Stability	: experimental
--- Portability	: Rank-2 Types
---
+-- Portability	: rank-2 Types required for correctness of shift, but they can be removed
 -------------------------------------------------------------------------------------------
 
-module Control.Monad.Indexed.Cont where
+module Control.Monad.Indexed.Cont 
+	( IxMonadCont(reset, shift)
+	, IxContT(IxContT, runIxContT)
+	, runIxContT_
+	, IxCont(IxCont)
+	, runIxCont
+	, runIxCont_
+	) where
 
 import Control.Applicative
 import Control.Functor.Pointed
 import Control.Monad.Trans
 import Control.Monad.Identity
 import Control.Monad.Indexed
--- import Control.Monad.Cont.Class
-import Control.Monad.State.Class
-import Control.Monad.Reader.Class
+import Control.Monad.State
+import Control.Monad.Reader
 import Control.Monad.Indexed.Trans
 
 class IxMonad m => IxMonadCont m where
diff --git a/src/Control/Monad/Indexed/State.hs b/src/Control/Monad/Indexed/State.hs
--- a/src/Control/Monad/Indexed/State.hs
+++ b/src/Control/Monad/Indexed/State.hs
@@ -26,11 +26,10 @@
 import Control.Monad.Indexed.Trans
 import Control.Monad.Indexed.Fix
 import Control.Monad.State
-import Control.Monad.Writer.Class
-import Control.Monad.Reader.Class
-import Control.Monad.Cont.Class
+import Control.Monad.Writer
+import Control.Monad.Reader
+import Control.Monad.Cont
 import Control.Monad.Error.Class
-
 
 class IxMonad m => IxMonadState m where
 	iget :: m i i i
diff --git a/src/Control/Morphism/Apo.hs b/src/Control/Morphism/Apo.hs
--- a/src/Control/Morphism/Apo.hs
+++ b/src/Control/Morphism/Apo.hs
@@ -20,12 +20,11 @@
 	, distGApo, distGApoT
 	) where
 
-
 import Control.Functor.Algebra
 import Control.Functor.Extras
 import Control.Functor.Fix
 import Control.Monad
-import Control.Monad.Either
+import Control.Monad.Either 
 import Control.Morphism.Ana
 import Control.Arrow ((|||))
 
diff --git a/src/Control/Morphism/Universal.hs b/src/Control/Morphism/Universal.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Morphism/Universal.hs
@@ -0,0 +1,35 @@
+-------------------------------------------------------------------------------------------
+-- |
+-- Module	: Control.Morphism.Universal
+-- Copyright 	: 2008 Edward Kmett
+-- License	: BSD3
+--
+-- Maintainer	: Edward Kmett <ekmett@gmail.com>
+-- Stability	: experimental
+-- Portability	: portable
+--
+-- Note the choice of which is universal and which is couniversal is chosen to 
+-- make the definitions consistent with limits and colimits.
+
+-------------------------------------------------------------------------------------------
+
+module Control.Morphism.Universal
+	( Couniversal(..), extractCouniversal, universalize
+	, Universal(..), extractUniversal, couniversalize
+	) where
+
+data Couniversal a f x = Couniversal (a -> f x) (forall z. (a -> f z) -> x -> z)
+
+extractCouniversal :: Couniversal a f x -> a -> f x
+extractCouniversal (Couniversal f _) = f
+
+couniversalize :: (a -> f z) -> Couniversal a f x -> x -> z
+couniversalize f (Couniversal _ s) = s f
+
+data Universal a f x = Universal (f x -> a) (forall z. (f z -> a) -> z -> x)
+
+extractUniversal :: Universal a f x -> f x -> a
+extractUniversal (Universal f _) = f
+
+universalize :: Universal a f x -> (f z -> a) -> z -> x
+universalize (Universal _ s) f = s f