diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,3 +1,7 @@
+Copyright 2008 Edward Kmett
+Copyright 2007 Iavor Diatchki
+Copyright 2004-2008 Dave Menendez
+
 All rights reserved.
 
 Redistribution and use in source and binary forms, with or without
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.51.3
+version:                0.52.0
 license:                BSD3
 cabal-version:          >= 1.2
 license-file:           LICENSE
@@ -63,6 +63,7 @@
                 Control.Comonad.Cofree,
                 Control.Comonad.Context,
                 Control.Comonad.Coideal,
+                Control.Comonad.Density,
                 Control.Comonad.Fix,
                 Control.Comonad.Indexed,
                 Control.Comonad.HigherOrder,
@@ -70,6 +71,7 @@
                 Control.Comonad.Pointer,
                 Control.Comonad.Reader,
                 Control.Comonad.Supply
+                Control.Comonad.Trans,
                 Control.Functor,
                 Control.Functor.Adjunction,
                 Control.Functor.Adjunction.HigherOrder,
@@ -92,6 +94,8 @@
                 Control.Functor.HigherOrder.Composition,
                 Control.Functor.Indexed,
                 Control.Functor.KanExtension,
+                Control.Functor.KanExtension.Interpreter,
+                Control.Functor.Lambek,
                 Control.Functor.Limit,
                 Control.Functor.Pointed,
                 Control.Functor.Pointed.Composition,
@@ -100,6 +104,8 @@
                 Control.Functor.Yoneda,
                 Control.Functor.Zip,
                 Control.Functor.Zap,
+                Control.Monad.Categorical,
+                Control.Monad.Codensity,
                 Control.Monad.Free,
                 Control.Monad.HigherOrder,
                 Control.Monad.Ideal,
@@ -111,18 +117,21 @@
                 Control.Monad.Parameterized,
                 Control.Monad.Hyper,
                 Control.Monad.Either,
-                Control.Morphism.Hylo,
-                Control.Morphism.Cata,
                 Control.Morphism.Ana,
-                Control.Morphism.Meta,
-                Control.Morphism.Futu,
+                Control.Morphism.Apo,
+                Control.Morphism.Build,
+                Control.Morphism.Cata,
                 Control.Morphism.Chrono,
-                Control.Morphism.Para,
+                Control.Morphism.Destroy,
                 Control.Morphism.Dyna,
-                Control.Morphism.Apo,
+                Control.Morphism.Futu,
+                Control.Morphism.Histo,
+                Control.Morphism.Hylo,
+                Control.Morphism.Meta,
+                Control.Morphism.Para,
+                Control.Morphism.Span,
                 Control.Morphism.Universal,
                 Control.Morphism.Zygo,
-                Control.Morphism.Histo,
                 Data.Void
 
         hs-source-dirs:         src
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,8 +12,9 @@
 ----------------------------------------------------------------------------
 module Control.Comonad.Cofree 
 	( Cofree
-	, runCofree, anaCofree, cofree
+	, runCofree, cofree
 	, ComonadCofree(outCofree)
+	, RunComonadCofree(anaCofree)
 	) where
 
 import Control.Arrow ((&&&))
@@ -28,9 +29,6 @@
 runCofree :: Cofree f a -> (a, f (Cofree f a))
 runCofree = runPCofree . outB
 
-anaCofree :: Functor f => (a -> c) -> (a -> f a) -> a -> Cofree f c
-anaCofree h t = InB . Biff . (Identity . h &&& fmap (anaCofree h t) . t)
-
 cofree :: a -> f (Cofree f a) -> Cofree f a 
 cofree a as = InB $ Biff (Identity a,as)
 
@@ -42,3 +40,9 @@
 
 instance ComonadCofree f w => ComonadCofree f (CoreaderT w e) where
 	outCofree = fmap CoreaderT . outCofree . runCoreaderT
+
+class ComonadCofree f w => RunComonadCofree f w | w -> f where
+	anaCofree :: Functor f => (a -> c) -> (a -> f a) -> a -> w c
+
+instance Functor f => RunComonadCofree f (Cofree f) where
+	anaCofree h t = InB . Biff . (Identity . h &&& fmap (anaCofree h t) . t)
diff --git a/src/Control/Comonad/Density.hs b/src/Control/Comonad/Density.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Comonad/Density.hs
@@ -0,0 +1,100 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Control.Comonad.Density
+-- Copyright   :  (C) 2008 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable (rank-2 polymorphism)
+--
+-- The density comonad for a functor. aka the comonad cogenerated by a functor
+-- The ''density'' term dates back to Dubuc''s 1974 thesis. The term 
+-- ''monad genererated by a functor'' dates back to 1972 in Street''s 
+-- ''Formal Theory of Monads''.
+----------------------------------------------------------------------------
+module Control.Comonad.Density
+	( Density(..)
+	, densityToLan, lanToDensity
+	, toDensity, fromDensity
+	, liftDensity, lowerDensity
+	, densityToAdjunction, adjunctionToDensity
+	, densityToComposedAdjunction, composedAdjunctionToDensity
+	, improveCofree
+	) where
+
+import Prelude hiding (abs)
+import Control.Comonad.Context
+import Control.Comonad.Cofree
+import Control.Comonad.Trans
+import Control.Comonad.Reader
+import Control.Functor.Adjunction
+import Control.Functor.Composition
+import Control.Functor.Extras
+import Control.Functor.Pointed ()
+import Control.Functor.KanExtension
+import Control.Monad.Identity
+
+data Density k a = forall b. Density (k b -> a) (k b)
+
+densityToLan :: Density k a -> Lan k k a
+densityToLan (Density f v) = Lan f v
+
+lanToDensity :: Lan k k a -> Density k a 
+lanToDensity (Lan f v) = Density f v
+
+-- | @Nat(k, s.k)@ is isomorphic to @Nat (Density k, s)@ (forwards)
+toDensity :: Functor s => (forall a. k a -> s (k a)) -> Density k :~> s
+toDensity s (Density f v) = fmap f $ s v
+
+-- | @Nat(k, s.k)@ is isomorphic to @Nat (Density k, s)@ (backwards)
+fromDensity :: (Density k :~> s) -> k a -> s (k a)
+fromDensity s = s . Density id
+
+instance ComonadTrans Density where
+	colift = liftDensity
+
+instance Functor (Density f) where
+	fmap f (Density g h) = Density (f . g) h
+
+instance Copointed (Density f) where
+	extract (Density f a) = f a
+
+instance Comonad (Density f) where
+	duplicate (Density f ws) = Density (Density f) ws
+
+-- | The natural isomorphism between a comonad w and the comonad generated by w (forwards).
+liftDensity :: Comonad w => w a -> Density w a
+liftDensity = Density extract 
+
+-- | The natural isomorphism between a comonad w and the comonad generated by w (backwards).
+lowerDensity :: Comonad w => Density w a -> w a 
+lowerDensity (Density f c) = extend f c
+
+densityToAdjunction :: Adjunction f g => Density f a -> f (g a)
+densityToAdjunction (Density f v) = fmap (leftAdjunct f) v
+
+adjunctionToDensity :: Adjunction f g => f (g a) -> Density f a
+adjunctionToDensity = Density counit
+
+densityToComposedAdjunction :: (Composition o, Adjunction f g) => Density f :~> (f `o` g)
+densityToComposedAdjunction (Density f v) = compose (fmap (leftAdjunct f) v)
+
+composedAdjunctionToDensity :: (Composition o, Adjunction f g) => (f `o` g) :~> Density f
+composedAdjunctionToDensity = Density counit . decompose
+
+instance ComonadReader e w => ComonadReader e (Density w) where
+	askC = askC . lowerDensity
+
+instance ComonadContext e w => ComonadContext e (Density w) where
+        getC = getC . lowerDensity 
+	modifyC f = modifyC f . lowerDensity
+
+instance ComonadCofree f w => ComonadCofree f (Density w) where
+        outCofree (Density f c) = fmap (Density f) (outCofree c)
+
+instance RunComonadCofree f w => RunComonadCofree f (Density w) where
+	anaCofree l r = liftDensity . anaCofree l r
+
+improveCofree :: Functor f => (forall w. ComonadCofree f w => w a) -> Cofree f a
+improveCofree m = lowerDensity m
diff --git a/src/Control/Comonad/Trans.hs b/src/Control/Comonad/Trans.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Comonad/Trans.hs
@@ -0,0 +1,20 @@
+{-# OPTIONS_GHC -fglasgow-exts #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Control.Comonad.Trans
+-- Copyright   :  (C) 2008 Edward Kmett
+--		  (C) 2004 Dave Menendez
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  experimental
+-- Portability :  portable
+----------------------------------------------------------------------------
+module Control.Comonad.Trans
+	( ComonadTrans(colift)
+	) where
+
+import Control.Comonad
+
+class ComonadTrans t where
+	colift :: Comonad w => w a -> t w a 
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
@@ -50,6 +50,7 @@
 	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, HFunctor)
 
@@ -75,6 +76,10 @@
 	rightAdjunct f ~(e,a) = f a e
 	unit a e = (e,a)
 	counit (x,f) = f x
+
+instance Adjunction Identity Identity where
+	unit = Identity . Identity
+	counit = runIdentity . runIdentity 
 
 instance Adjunction (Coreader e) (Reader e) where
 	unit a = Reader (\e -> Coreader e a)
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
@@ -10,46 +10,44 @@
 --
 -- 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 machinery for lifting (co)monads into and lowering (co)monads out of 
--- Kan extensions.
+-- See <http://comonad.com/reader/2008/kan-extensions/>
+-- and <http://comonad.com/reader/2008/kan-extensions-ii/>
+-- for motivation.
+--
+-- NB: @Yoneda@, @CoYoneda@, @Density@, @Codensity@ have been factored
+-- out into separate modules.
 ----------------------------------------------------------------------------
 module Control.Functor.KanExtension 
 	( 
 	-- * Right Kan Extensions
 	  Ran(..)
 	, toRan, fromRan
-	, liftRan, lowerRan
 	, adjointToRan, ranToAdjoint
 	, ranToComposedAdjoint, composedAdjointToRan
 	, composeRan, decomposeRan
 	-- * Left Kan Extensions
 	, Lan(..)
 	, toLan, fromLan
-	, liftLan, lowerLan
 	, adjointToLan, lanToAdjoint
 	, composeLan, decomposeLan
 	, lanToComposedAdjoint, composedAdjointToLan
-	-- * Performance tweaks for (co)free (co)monads
-	, 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.Functor.Adjunction
-import Control.Monad.State
-import Control.Monad.Reader
 import Control.Monad.Identity
-import Control.Monad.Free
 
--- | Right Kan Extension
+
+-- | The right Kan Extension of h along g.
+-- An alternative definition in terms of Ends.
+--
+-- @newtype RanT g h a b b' { (a -> g b) -> h b' }@
+--
+-- @type Ran g h a = End (RanT g h a)@
 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)
@@ -67,13 +65,6 @@
 instance Functor (Ran g h) where
 	fmap f m = Ran (\k -> runRan m (k . f))
 
-instance Pointed (Ran f f) where
-	point x = Ran (\k -> k x)
-
-instance Monad (Ran f f) where
-	return = point
-	m >>= k = Ran (\c -> runRan m (\a -> runRan (k a) c))
-
 -- | 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)
@@ -82,31 +73,6 @@
 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)
@@ -122,6 +88,10 @@
 composedAdjointToRan f = Ran (\a -> fmap (rightAdjunct a) (decompose f))
 
 -- | Left Kan Extension
+--
+-- @newtype LanT g h a b b' { (g b -> a, h b') }@
+--
+-- @type Lan g h a = Coend (LanT g h a)@
 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)
@@ -139,20 +109,6 @@
 instance Functor (Lan f g) where
 	fmap f (Lan g h) = Lan (f . g) h
 
-instance Copointed (Lan f f) where
-	extract (Lan f a) = f a
-
-instance Comonad (Lan f f) where
-	duplicate (Lan f ws) = Lan (Lan f) ws
-
--- | 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 
-
--- | 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
@@ -167,13 +123,6 @@
 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
@@ -182,14 +131,3 @@
 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/KanExtension/Interpreter.hs b/src/Control/Functor/KanExtension/Interpreter.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Functor/KanExtension/Interpreter.hs
@@ -0,0 +1,42 @@
+{-# OPTIONS_GHC -fglasgow-exts #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Control.Functor.KanExtension.Interpreter
+-- Copyright   :  (C) 2008 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable (rank-2 polymorphism)
+--
+-- Ghani and Johann's Interp/InterpT types from ''Initial Algebra Semantics is Enough!''
+-- <http://crab.rutgers.edu/~pjohann/tlca07-rev.pdf> and its dual.
+----------------------------------------------------------------------------
+module Control.Functor.KanExtension.Interpreter
+	( Interpreter, InterpreterT
+	, interpreterAlgebra, algebraInterpreter
+	, Cointerpreter, CointerpreterT
+	, cointerpreterCoalgebra, coalgebraCointerpreter
+	) where
+
+import Control.Functor.Extras
+import Control.Functor.HigherOrder
+import Control.Functor.KanExtension
+
+type Interpreter y g h = y :~> Ran g h
+type InterpreterT f g h = forall y. Functor y => Interpreter y g h -> Interpreter (f y) g h
+
+interpreterAlgebra :: InterpreterT f g h -> HAlgebra f (Ran g h)
+interpreterAlgebra i = i id
+
+algebraInterpreter :: HFunctor f => HAlgebra f (Ran g h) -> InterpreterT f g h
+algebraInterpreter h i = h . hfmap i
+
+type Cointerpreter y g h = Lan g h :~> y
+type CointerpreterT f g h = forall y. Functor y => Cointerpreter y g h -> Cointerpreter (f y) g h
+
+cointerpreterCoalgebra :: CointerpreterT f g h -> HCoalgebra f (Lan g h)
+cointerpreterCoalgebra i = i id
+
+coalgebraCointerpreter :: HFunctor f => HCoalgebra f (Lan g h) -> CointerpreterT f g h
+coalgebraCointerpreter h i = hfmap i . h
diff --git a/src/Control/Functor/Lambek.hs b/src/Control/Functor/Lambek.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Functor/Lambek.hs
@@ -0,0 +1,41 @@
+{-# OPTIONS_GHC -fglasgow-exts #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Control.Functor.Lambek
+-- Copyright   :  (C) 2008 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable (rank-2 polymorphism)
+-- 
+----------------------------------------------------------------------------
+module Control.Functor.Lambek
+	( 
+	-- * Lambek's Lemma
+	  lambek
+	, hlambek
+	, colambek
+	, hcolambek
+	) where
+
+import Control.Functor.Algebra 
+import Control.Functor.Extras
+import Control.Functor.Fix
+import Control.Functor.HigherOrder
+import Control.Morphism.Cata
+import Control.Morphism.Ana
+
+-- Lambek's lemma
+lambek :: Functor f => Algebra f (FixF f) -> Coalgebra f (FixF f)
+lambek inF = cata (fmap inF)
+
+hlambek :: HFunctor f => HAlgebra f (FixH f) -> HCoalgebra f (FixH f)
+hlambek inH = hcata (hfmap inH)
+
+colambek :: Functor f => Coalgebra f (FixF f) -> Algebra f (FixF f)
+colambek out = ana (fmap out)
+
+hcolambek :: HFunctor f => HCoalgebra f (FixH f) -> HAlgebra f (FixH f)
+hcolambek out = hana (hfmap out)
+
diff --git a/src/Control/Functor/Limit.hs b/src/Control/Functor/Limit.hs
--- a/src/Control/Functor/Limit.hs
+++ b/src/Control/Functor/Limit.hs
@@ -10,17 +10,28 @@
 --
 ----------------------------------------------------------------------------
 module Control.Functor.Limit
-	( Lim
-	, Colim
-	, module Control.Functor.KanExtension
-	, Void
-	, Const
+	( Limit, HasLimit(limit)
+	, Colimit(..)
 	) where
 
 import Prelude hiding (abs)
-import Control.Applicative (Const)
-import Data.Void (Void)
-import Control.Functor.KanExtension
+import Data.Monoid
 
-type Lim = Ran (Const Void)
-type Colim = Lan (Const Void)
+-- | @type Limit = Ran (Const Void)@
+-- Limit { runLimit :: forall a. f a }
+type Limit f = forall a. f a 
+
+class HasLimit f where
+	limit :: f a
+
+instance HasLimit Maybe where
+	limit = Nothing
+
+instance HasLimit [] where
+	limit = []
+
+instance Monoid a => HasLimit (Either a) where
+	limit = (Left mempty)
+
+-- | @type Colimit = Lan (Const Void)@
+data Colimit f = forall b. Colimit { runColimit :: f b }
diff --git a/src/Control/Functor/Pointed.hs b/src/Control/Functor/Pointed.hs
--- a/src/Control/Functor/Pointed.hs
+++ b/src/Control/Functor/Pointed.hs
@@ -17,18 +17,19 @@
 	, PCopointed(..)
 	) where
 
-import Control.Functor
 import Control.Category
 import Control.Category.Hask
+import Control.Functor
+-- import Control.Functor.Algebra
 import Control.Monad.Identity
 import Prelude hiding ((.),id)
 
 -- return
 class Functor f => Pointed f where
-        point :: a -> f a
+        point :: a -> f a -- Coalgebra f a
 
 class Functor f => Copointed f where
-        extract :: f a -> a
+        extract :: f a -> a -- Algebra f a
 
 {-# RULES
 "extract/point" extract . point = id
diff --git a/src/Control/Functor/Representable.hs b/src/Control/Functor/Representable.hs
--- a/src/Control/Functor/Representable.hs
+++ b/src/Control/Functor/Representable.hs
@@ -13,6 +13,8 @@
 
 module Control.Functor.Representable where
 
+import Control.Monad.Identity
+
 class Functor f => Representable f x where
 	rep :: (x -> a) -> f a
 	unrep :: f a -> (x -> a)
@@ -31,3 +33,19 @@
         rep f = EitherF (f . Left) (f . Right)
         unrep (EitherF l r) = either l r
 
+instance Representable Identity () where
+	rep f = Identity (f ())
+	unrep (Identity a) = const a
+
+data Both a = Both a a 
+
+instance Functor Both where
+	fmap f (Both a b) = Both (f a) (f b)
+
+instance Representable Both Bool where
+	rep f = Both (f False) (f True)
+	unrep (Both x _) False = x
+	unrep (Both _ y) True = y
+
+-- instance Adjunction f g => Representable g (f ()) where
+-- instance Representable (Cofree Identity) (Free Identity ()) where
diff --git a/src/Control/Functor/Yoneda.hs b/src/Control/Functor/Yoneda.hs
--- a/src/Control/Functor/Yoneda.hs
+++ b/src/Control/Functor/Yoneda.hs
@@ -8,27 +8,220 @@
 -- Stability	: experimental
 -- Portability	: portable
 --
--- The Yoneda lemma materialized as a Kan extension, and hence as a higher order functor
+-- The Yoneda lemma can be realized as the Kan extension along Identity
+-- However, having this special instance allows us to define Yoneda f as a monad, 
+-- comonad, etc. based on whatever properties the base functor has, without
+-- limiting ourselves to what Ran f f can manage.
+--
+-- Performance wise, Yoneda may make your monad more efficient at handling a bunch of 
+-- fmaps, while CoYoneda may do the same for a comonad assuming you require a greater than
+-- linear amount of time to fmap over your structure. You can apply each in either role
+-- but the asymptotics will probably not be in your favor.
+--
 -------------------------------------------------------------------------------------------
 
 module Control.Functor.Yoneda
-	( Yoneda
-	, toYoneda, fromYoneda
+	( Yoneda(Yoneda,runYoneda), ranToYoneda, yonedaToRan, lowerYoneda
+	, CoYoneda(CoYoneda), lanToCoYoneda, coYonedaToLan, liftCoYoneda
 	) where
 
-import Control.Functor.KanExtension
+import Control.Applicative
+import Control.Comonad.HigherOrder
+import Control.Comonad.Cofree
+import Control.Comonad.Context
+import Control.Comonad.Reader
+import Control.Comonad.Trans
 import Control.Functor.Extras
+import Control.Functor.KanExtension
+import Control.Functor.Pointed
+import Control.Functor.HigherOrder
 import Control.Monad.Identity
+import Control.Monad.HigherOrder
+import Control.Monad.Free
+import Control.Monad.Trans
+import Control.Monad.Reader.Class
+import Control.Monad.State.Class
+import Control.Monad.Writer.Class
 
-type Yoneda = Ran Identity
+-- Yoneda ~ Ran Identity
+newtype Yoneda f a = Yoneda { runYoneda :: forall b. ((a -> b) -> f b) } 
 
-toYoneda :: Functor f => f :~> Yoneda f
-toYoneda a = Ran (\f -> fmap (runIdentity . f) a)
+ranToYoneda :: Ran Identity f :~> Yoneda f
+ranToYoneda r = Yoneda (\f -> runRan r (Identity . f))
 
-fromYoneda :: Yoneda f :~> f 
-fromYoneda t = runRan t Identity
+yonedaToRan :: Yoneda f :~> Ran Identity f
+yonedaToRan y = Ran (\f -> runYoneda y (runIdentity . f))
 
--- 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)
+lowerYoneda :: Yoneda f :~> f 
+lowerYoneda m = runYoneda m id
+
+instance Functor (Yoneda f) where
+	fmap f m = Yoneda (\k -> runYoneda m (k . f))
+
+instance Pointed f => Pointed (Yoneda f) where
+	point a = Yoneda (\f -> point (f a))
+
+instance Applicative f => Applicative (Yoneda f) where
+	pure a = Yoneda (\f -> pure (f a))
+	m <*> n = Yoneda (\f -> runYoneda m (f .) <*> runYoneda n id)
+
+instance Monad f => Monad (Yoneda f) where
+	return a = Yoneda (\f -> return (f a))
+	m >>= k = Yoneda (\f -> runYoneda m id >>= \a -> runYoneda (k a) f)
+
+instance HFunctor Yoneda where
+	ffmap = fmap
+	hfmap f y = Yoneda (f . runYoneda y)
+
+-- f a -> Yoneda f a 
+instance HPointed Yoneda where
+	hreturn a = Yoneda (\f -> fmap f a) 
+
+-- exists because Monad doesn't require Functor!
+instance MonadTrans Yoneda where
+	lift a = Yoneda (\f -> liftM f a)
+
+instance ComonadTrans Yoneda where
+	colift = hreturn
+
+-- Yoneda f a -> f a
+instance HCopointed Yoneda where
+	hextract t = runYoneda t id
+
+instance HMonad Yoneda where
+	hbind f = f . hextract 
+
+instance HComonad Yoneda where
+	hextend f = hreturn . f
+
+instance Copointed f => Copointed (Yoneda f) where
+	extract = extract . hextract
+
+instance Comonad f => Comonad (Yoneda f) where
+	extend k m = Yoneda (\f -> extend (f . k . hreturn) (hextract m))
+
+instance MonadState e m => MonadState e (Yoneda m) where
+	get = lift get
+	put = lift . put
+
+instance MonadReader e m => MonadReader e (Yoneda m) where
+	ask = lift ask
+	local r = lift . local r . lowerYoneda
+
+instance MonadWriter e m => MonadWriter e (Yoneda m) where
+	tell = lift . tell
+	listen = lift . listen . flip runYoneda id 
+	pass = lift . pass . lowerYoneda
+
+instance MonadFree f m => MonadFree f (Yoneda m) where
+	inFree = lift . inFree . fmap lowerYoneda
+
+instance RunMonadFree f m => RunMonadFree f (Yoneda m) where
+	cataFree l r = cataFree l r . lowerYoneda
+
+instance ComonadCofree f m => ComonadCofree f (Yoneda m) where
+	outCofree = fmap colift . outCofree . lowerYoneda
+
+instance RunComonadCofree f m => RunComonadCofree f (Yoneda m) where
+	anaCofree l r = colift . anaCofree l r
+
+instance ComonadContext e m => ComonadContext e (Yoneda m) where
+	getC = getC . lowerYoneda
+	modifyC s = modifyC s . lowerYoneda
+
+instance ComonadReader e m => ComonadReader e (Yoneda m) where
+	askC = askC . lowerYoneda
+	
+
+-- | Left Kan Extensions
+-- CoYoneda ~ Lan Identity
+data CoYoneda f a = forall b. CoYoneda (b -> a) (f b)
+
+lanToCoYoneda :: Lan Identity f :~> CoYoneda f 
+lanToCoYoneda (Lan f v) = CoYoneda (f . Identity) v
+
+coYonedaToLan :: CoYoneda f :~> Lan Identity f
+coYonedaToLan (CoYoneda f v) = Lan (f . runIdentity) v
+
+instance Functor (CoYoneda f) where
+	fmap f (CoYoneda g v) = CoYoneda (f . g) v
+
+instance Pointed f => Pointed (CoYoneda f) where
+	point = hreturn . point
+
+instance Applicative f => Applicative (CoYoneda f) where
+	pure = hreturn . pure
+	m <*> n = CoYoneda id (hextract m <*> hextract n)
+
+instance Monad m => Monad (CoYoneda m) where
+	return = CoYoneda id . return
+	CoYoneda f v >>= k = CoYoneda id (v >>= (\(CoYoneda f' v') -> liftM f' v') . k . f)
+
+instance HFunctor CoYoneda where
+	ffmap = fmap 
+	hfmap f (CoYoneda g v) = CoYoneda g (f v)
+
+instance HPointed CoYoneda where
+	hreturn = CoYoneda id
+
+instance HMonad CoYoneda where
+	hbind f = f . hextract
+
+instance HComonad CoYoneda where
+	hextend f = hreturn . f
+
+instance HCopointed CoYoneda where
+	hextract (CoYoneda f v) = fmap f v
+
+liftCoYoneda :: f :~> CoYoneda f
+liftCoYoneda = CoYoneda id
+
+-- | Just a conceptual nicety for monads since they aren't functors in Haskell. this is otherwise just hextract
+lowerCoYoneda :: Monad f => CoYoneda f :~> f 
+lowerCoYoneda (CoYoneda f v) = liftM f v 
+
+instance Copointed w => Copointed (CoYoneda w) where
+	extract (CoYoneda f v) = f (extract v)
+
+instance Comonad w => Comonad (CoYoneda w) where
+	extend k (CoYoneda f v) = CoYoneda id $ extend (k . CoYoneda f) v
+
+instance MonadTrans CoYoneda where
+	lift = CoYoneda id
+
+instance ComonadTrans CoYoneda where
+	colift = CoYoneda id
+
+-- All the (Co)monadFoo CoYoneda instances
+
+instance ComonadCofree f m => ComonadCofree f (CoYoneda m) where
+	outCofree = fmap colift . outCofree . hextract
+
+instance RunComonadCofree f m => RunComonadCofree f (CoYoneda m) where
+	anaCofree l r = colift . anaCofree l r
+
+instance ComonadContext e m => ComonadContext e (CoYoneda m) where
+	getC = getC . hextract
+	modifyC s = modifyC s . hextract
+
+instance ComonadReader e m => ComonadReader e (CoYoneda m) where
+	askC = askC . hextract
+	
+instance MonadState e m => MonadState e (CoYoneda m) where
+	get = lift get
+	put = lift . put
+
+instance MonadReader e m => MonadReader e (CoYoneda m) where
+	ask = lift ask
+	local r = lift . local r . lowerCoYoneda
+
+instance MonadWriter e m => MonadWriter e (CoYoneda m) where
+	tell = lift . tell
+	listen = lift . listen . lowerCoYoneda
+	pass = lift . pass . lowerCoYoneda
+
+instance MonadFree f m => MonadFree f (CoYoneda m) where
+	inFree = lift . inFree . fmap lowerCoYoneda
+
+instance RunMonadFree f m => RunMonadFree f (CoYoneda m) where
+	cataFree l r = cataFree l r . lowerCoYoneda
diff --git a/src/Control/Functor/Zap.hs b/src/Control/Functor/Zap.hs
--- a/src/Control/Functor/Zap.hs
+++ b/src/Control/Functor/Zap.hs
@@ -23,6 +23,12 @@
 
 {- | Minimum definition: zapWith -}
 
+-- zapWith :: Adjunction f g => (a -> b -> c) -> f a -> g b -> c
+-- zapWith f a b = uncurry (flip f) . counit . fmap (uncurry (flip strength)) $ strength a b
+
+-- zap :: Adjunction f g => f (a -> b) -> g a -> b
+-- zap = zapWith id
+
 class Zap f g | f -> g, g -> f where
 	zapWith :: (a -> b -> c) -> f a -> g b -> c
 	zap :: f (a -> b) -> g a -> b
diff --git a/src/Control/Monad/Categorical.hs b/src/Control/Monad/Categorical.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Categorical.hs
@@ -0,0 +1,17 @@
+module Control.Monad.Categorical where
+import Prelude hiding (id,(.))
+import Control.Category
+import Control.Functor.Categorical
+
+class CFunctor m c d => CPointed m c d where
+	creturn :: d a (m a)
+
+-- class CPointed m (~>) => CApplicative m (~>) where
+--	cap :: m (a ~> b) ~> m a ~> m b
+
+class CPointed m (~>) (~>) => CMonad m (~>) where
+	cbind :: (a ~> m b) -> m a ~> m b
+	cjoin :: m (m a) ~> m a 
+
+	cbind f = cjoin . cmap f 
+	cjoin = cbind id 
diff --git a/src/Control/Monad/Codensity.hs b/src/Control/Monad/Codensity.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Codensity.hs
@@ -0,0 +1,86 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Control.Monad.Codensity
+-- Copyright   :  (C) 2008 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable (rank-2 polymorphism)
+--
+----------------------------------------------------------------------------
+module Control.Monad.Codensity
+	( Codensity, liftCodensity, lowerCodensity
+	, codensityToRan, ranToCodensity
+	, toCodensity, fromCodensity
+	, codensityToAdjunction
+	, adjunctionToCodensity
+	, improveFree
+	) where
+
+import Prelude hiding (abs)
+import Control.Comonad.Context
+import Control.Functor.Extras
+import Control.Functor.Pointed ()
+import Control.Functor.Adjunction
+import Control.Functor.KanExtension
+import Control.Monad.State
+import Control.Monad.Reader
+import Control.Monad.Identity
+import Control.Monad.Free
+
+newtype Codensity m a = Codensity { runCodensity :: forall b. (a -> m b) -> m b }
+
+codensityToRan :: Codensity m :~> Ran m m
+codensityToRan x = Ran (runCodensity x)
+
+ranToCodensity :: Ran m m :~> Codensity m
+ranToCodensity x = Codensity (runRan x)
+
+liftCodensity :: Monad m => m :~> Codensity m
+liftCodensity m = Codensity (m >>=)
+
+lowerCodensity :: Monad m => Codensity m :~> m
+lowerCodensity a = runCodensity a return
+
+toCodensity :: Functor s => (forall a. s (k a) -> k a) -> s :~> Codensity k
+toCodensity s t = Codensity (s . flip fmap t)
+
+fromCodensity :: (s :~> Codensity k) -> s (k a) -> k a
+fromCodensity s = flip runCodensity id . s
+
+instance Functor (Codensity k) where
+	fmap f m = Codensity (\k -> runCodensity m (k . f))
+
+instance Pointed (Codensity f) where
+	point x = Codensity (\k -> k x)
+
+instance Monad (Codensity f) where
+	return = point
+	m >>= k = Codensity (\c -> runCodensity m (\a -> runCodensity (k a) c))
+
+instance MonadReader r m => MonadReader r (Codensity m) where
+	ask = liftCodensity ask
+	local f m = Codensity (\c -> ask >>= \r -> local f (runCodensity m (local (const r) . c)))
+
+instance MonadIO m => MonadIO (Codensity m) where
+	liftIO = liftCodensity . liftIO 
+
+instance MonadState s m => MonadState s (Codensity m) where
+	get = liftCodensity get
+	put = liftCodensity . put
+
+instance MonadFree f m => MonadFree f (Codensity m) where
+        inFree t = Codensity (inFree . flip fmap t . flip runCodensity)
+
+instance RunMonadFree f m => RunMonadFree f (Codensity m) where
+	cataFree l r = cataFree l r . lowerCodensity
+
+codensityToAdjunction :: Adjunction f g => Codensity g a -> g (f a)
+codensityToAdjunction r = runCodensity r unit
+
+adjunctionToCodensity :: Adjunction f g => g (f a) -> Codensity g a
+adjunctionToCodensity f = Codensity (\a -> fmap (rightAdjunct a) f)
+
+improveFree :: Functor f => (forall m. MonadFree f m => m a) -> Free f a
+improveFree m = lowerCodensity m
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
@@ -20,15 +20,16 @@
 	, PFree
 	, Free
 	, runFree
-	, cataFree
 	, free
 	, MonadFree(inFree)
+	, RunMonadFree(cataFree)
 	) where
 
 import Prelude hiding ((.),id)
 import Control.Category
 import Control.Category.Cartesian
 import Control.Functor
+import Control.Functor.Algebra
 import Control.Functor.Combinators.Biff
 import Control.Functor.Fix
 import Control.Monad.Parameterized
@@ -40,11 +41,14 @@
 runFree :: Free f a -> Either a (f (Free f a))
 runFree = first runIdentity . runBiff . outB
 
-cataFree :: Functor f => (c -> a) -> (f a -> a) -> Free f c -> a
-cataFree l r = (l . runIdentity ||| r . fmap (cataFree l r)) . runBiff . outB
-
 free :: Either a (f (Free f a)) -> Free f a
 free = InB . Biff . first Identity
+
+class MonadFree f m => RunMonadFree f m | m -> f where
+	cataFree :: (c -> a) -> Algebra f a -> m c -> a
+
+instance Functor f => RunMonadFree f (Free f) where
+	cataFree l r = (l . runIdentity ||| r . fmap (cataFree l r)) . runBiff . outB
 
 class (Functor f, Monad m) => MonadFree f m | m -> f where
         inFree :: f (m a) -> m a
diff --git a/src/Control/Morphism/Ana.hs b/src/Control/Morphism/Ana.hs
--- a/src/Control/Morphism/Ana.hs
+++ b/src/Control/Morphism/Ana.hs
@@ -10,7 +10,12 @@
 -- Portability :  non-portable (rank-2 polymorphism)
 -- 
 ----------------------------------------------------------------------------
-module Control.Morphism.Ana where
+module Control.Morphism.Ana 
+	( ana, g_ana, distAna
+	, biana, g_biana
+	, hana
+	, kana, runkana
+	) where
 
 import Control.Category.Hask
 import Control.Functor
@@ -18,6 +23,8 @@
 import Control.Functor.Extras
 import Control.Functor.Fix
 import Control.Functor.HigherOrder
+import Control.Functor.KanExtension
+import Control.Functor.KanExtension.Interpreter
 import Control.Comonad ()
 import Control.Monad.Identity
 
@@ -44,3 +51,9 @@
 -- | A higher-order anamorphism for constructing higher order functors.
 hana :: HFunctor f => HCoalgebra f a -> a :~> FixH f
 hana g = InH . hfmap (hana g) . g
+
+kana :: HFunctor f => CointerpreterT f g h -> Lan g h :~> FixH f
+kana i = hana (cointerpreterCoalgebra i)
+
+runkana :: HFunctor f => CointerpreterT f g h -> (g b -> a) -> h b -> FixH f a 
+runkana i f v = kana i (Lan f v)
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
@@ -52,4 +52,3 @@
 
 distApoT :: (Functor f, Monad m) => Dist m f -> Dist (ApoT f m) f
 distApoT = distGApoT (liftCoalgebra outF)
-
diff --git a/src/Control/Morphism/Build.hs b/src/Control/Morphism/Build.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Morphism/Build.hs
@@ -0,0 +1,31 @@
+{-# OPTIONS_GHC -fglasgow-exts #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Control.Morphism.Build
+-- Copyright   :  (C) 2008 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable (rank-2 polymorphism)
+-- 
+----------------------------------------------------------------------------
+module Control.Morphism.Build where
+
+import Control.Functor.Extras
+import Control.Functor.HigherOrder
+import Control.Functor.KanExtension
+-- import Control.Functor.KanExtension.Interpreter
+-- import Control.Morphism.Cata
+
+-- | @forall h g.  hcata h . hbuild g = g h@ cannot be realized as a RULE because
+-- h and g are not monotypes.
+-- Kan extended build, gbuild in Ghani/Johann parlance, but g_foo currently denotes
+-- generalized in the 'has a parameterizing (co)monad' sense.
+hbuild :: (HFunctor f, Functor c) => (forall x. HAlgebra f x -> c :~> x) -> c :~> FixH f
+hbuild g = g InH
+
+-- | @ forall h g. kcata h . kbuild g = g (interpreterAlgebra h)@ cannot be realized as 
+-- a RULE because h and g are not monotypes.
+kbuild :: HFunctor f => (forall x. HAlgebra f x -> Lan g h :~> x) -> Lan g h :~> FixH f
+kbuild = hbuild
diff --git a/src/Control/Morphism/Cata.hs b/src/Control/Morphism/Cata.hs
--- a/src/Control/Morphism/Cata.hs
+++ b/src/Control/Morphism/Cata.hs
@@ -10,16 +10,23 @@
 -- Portability :  non-portable (rank-2 polymorphism)
 -- 
 ----------------------------------------------------------------------------
-module Control.Morphism.Cata where
+module Control.Morphism.Cata 
+	( cata, g_cata, distCata
+	, bicata, g_bicata
+	, hcata
+	, kcata, runkcata
+	) where
 
 import Control.Comonad
 import Control.Category.Hask
 import Control.Functor
 import Control.Functor.Pointed
 import Control.Functor.Algebra 
-import Control.Functor.HigherOrder
 import Control.Functor.Extras
 import Control.Functor.Fix
+import Control.Functor.HigherOrder
+import Control.Functor.KanExtension
+import Control.Functor.KanExtension.Interpreter
 import Control.Monad.Identity
 
 cata :: Functor f => Algebra f a -> FixF f -> a
@@ -41,3 +48,9 @@
 
 hcata :: HFunctor f => HAlgebra f a -> FixH f :~> a
 hcata f = f . hfmap (hcata f) . outH
+
+kcata :: HFunctor f => InterpreterT f g h -> FixH f :~> Ran g h
+kcata i = hcata (interpreterAlgebra i)
+
+runkcata :: HFunctor f => InterpreterT f g h -> FixH f a -> (a -> g b) -> h b
+runkcata i = runRan . kcata i
diff --git a/src/Control/Morphism/Chrono.hs b/src/Control/Morphism/Chrono.hs
--- a/src/Control/Morphism/Chrono.hs
+++ b/src/Control/Morphism/Chrono.hs
@@ -21,9 +21,9 @@
 import Control.Morphism.Futu
 import Control.Morphism.Histo
 
-chrono :: (Functor f, Functor g) => GAlgebra g (Cofree g) b -> (f :~> g) -> GCoalgebra f (Free f) a -> a -> b
+chrono :: (RunMonadFree f m, RunComonadCofree g w) => GAlgebra g w b -> (f :~> g) -> GCoalgebra f m a -> a -> b
 chrono = g_hylo (distHisto id) (distFutu id)
 
-g_chrono :: (Functor f, Functor g, Functor h, Functor j) => 
-	    Dist g h -> Dist j f -> GAlgebra g (Cofree h) b -> (f :~> g) -> GCoalgebra f (Free j) a -> a -> b
+g_chrono :: (Functor f, Functor g, RunComonadCofree h w, RunMonadFree j m) => 
+	    Dist g h -> Dist j f -> GAlgebra g w b -> (f :~> g) -> GCoalgebra f m a -> a -> b
 g_chrono h f = g_hylo (distHisto h) (distFutu f)
diff --git a/src/Control/Morphism/Destroy.hs b/src/Control/Morphism/Destroy.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Morphism/Destroy.hs
@@ -0,0 +1,26 @@
+{-# OPTIONS_GHC -fglasgow-exts #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Control.Morphism.Destroy
+-- Copyright   :  (C) 2008 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable (rank-2 polymorphism)
+-- 
+----------------------------------------------------------------------------
+module Control.Morphism.Destroy where
+
+import Control.Functor.Extras
+import Control.Functor.HigherOrder
+import Control.Functor.KanExtension
+-- import Control.Morphism.Ana
+
+-- | @forall h g . hdestroy g . hana h = g h@ cannot be realized as a RULE.
+hdestroy :: (HFunctor f, Functor c) => (forall g. HCoalgebra f g -> g :~> c) -> FixH f :~> c
+hdestroy g = g outH
+
+-- | @forall h g . kdestroy g . kana h = g (cointerpreterCoalgebra h)@ cannot be realized as a RULE
+kdestroy :: HFunctor f => (forall x. HCoalgebra f x -> x :~> Ran g h) -> FixH f :~> Ran g h
+kdestroy = kdestroy
diff --git a/src/Control/Morphism/Dyna.hs b/src/Control/Morphism/Dyna.hs
--- a/src/Control/Morphism/Dyna.hs
+++ b/src/Control/Morphism/Dyna.hs
@@ -19,5 +19,5 @@
 import Control.Morphism.Histo
 import Control.Morphism.Ana
 
-dyna :: (Functor f, Functor g) => GAlgebra g (Cofree g) b -> (f :~> g) -> Coalgebra f a -> a -> b
+dyna :: (Functor f, RunComonadCofree g w) => GAlgebra g w b -> (f :~> g) -> Coalgebra f a -> a -> b
 dyna f e g = g_hylo (distHisto id) distAna f e (liftCoalgebra g)
diff --git a/src/Control/Morphism/Futu.hs b/src/Control/Morphism/Futu.hs
--- a/src/Control/Morphism/Futu.hs
+++ b/src/Control/Morphism/Futu.hs
@@ -20,12 +20,13 @@
 import Control.Monad.Free
 import Control.Morphism.Ana
 
-futu :: Functor f => GCoalgebra f (Free f) a -> a -> FixF f
+-- futu :: Functor f => GCoalgebra f (Free f) a -> a -> FixF f
+futu :: (RunMonadFree f m) => GCoalgebra f m a -> a -> FixF f
 futu = g_ana (distFutu id)
 
-g_futu :: (Functor f, Functor h) => Dist h f -> GCoalgebra f (Free h) a -> a -> FixF f
+g_futu :: (Functor f, RunMonadFree h m) => Dist h f -> GCoalgebra f m a -> a -> FixF f
 g_futu k = g_ana (distFutu k)
 
-distFutu :: (Functor f, Functor h) => Dist h f -> Dist (Free h) f
+distFutu :: (Functor f, RunMonadFree h m) => Dist h f -> Dist m f
 distFutu k = cataFree (fmap return) (fmap inFree . k)
 
diff --git a/src/Control/Morphism/Histo.hs b/src/Control/Morphism/Histo.hs
--- a/src/Control/Morphism/Histo.hs
+++ b/src/Control/Morphism/Histo.hs
@@ -20,11 +20,11 @@
 import Control.Comonad.Cofree
 import Control.Morphism.Cata
 
-histo :: Functor f => GAlgebra f (Cofree f) a -> FixF f -> a
+histo :: (RunComonadCofree f w) => GAlgebra f w a -> FixF f -> a
 histo = g_cata (distHisto id)
 
-g_histo :: (Functor f, Functor h) => Dist f h -> GAlgebra f (Cofree h) a -> FixF f -> a
+g_histo :: (RunComonadCofree h w, Functor f) => Dist f h -> GAlgebra f w a -> FixF f -> a
 g_histo k = g_cata (distHisto k)
 
-distHisto :: (Functor f, Functor h) => Dist f h -> Dist f (Cofree h)
+distHisto :: (RunComonadCofree h w, Functor f) => Dist f h -> Dist f w
 distHisto k = anaCofree (fmap extract) (k . fmap outCofree)
diff --git a/src/Control/Morphism/Hylo.hs b/src/Control/Morphism/Hylo.hs
--- a/src/Control/Morphism/Hylo.hs
+++ b/src/Control/Morphism/Hylo.hs
@@ -23,11 +23,12 @@
 import Control.Functor.Extras
 import Control.Functor.HigherOrder
 
+-- | hylo :: (g b -> b) -> (forall c. f c -> g c) -> (a -> f b) -> a -> b
 hylo :: Functor f => Algebra g b -> (f :~> g) -> Coalgebra f a -> a -> b
 hylo f e g = f . e . fmap (hylo f e g). g 
 
-g_hylo :: (Comonad w, Functor f, Monad m) =>
-          Dist g w -> Dist m f -> GAlgebra g w b -> (f :~> g) -> GCoalgebra f m a -> a -> b
+-- | g_hylo :: (Comonad w, Functor f, Monad m) => (forall d. g (w d) -> w (g d)) -> (forall e. m (f e) -> f (m e)) -> (g (w b) -> b) -> (forall c. f c -> g c) -> a -> f (m a) -> a -> b
+g_hylo :: (Comonad w, Functor f, Monad m) => Dist g w -> Dist m f -> GAlgebra g w b -> (f :~> g) -> GCoalgebra f m a -> a -> b
 g_hylo w m f e g = extract . h . return where h = liftW f . w . e . fmap (duplicate . h . join) . m . liftM g
 
 -- The Jeremy Gibbons-style bifunctor-based version has the same expressive power, but may fuse with bimaps better
diff --git a/src/Control/Morphism/Span.hs b/src/Control/Morphism/Span.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Morphism/Span.hs
@@ -0,0 +1,21 @@
+{-# OPTIONS_GHC -fglasgow-exts #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Control.Morphism.Span
+-- Copyright   :  (C) 2008 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable (rank-2 polymorphism)
+--
+-- Spans and Cospans
+-- <http://en.wikipedia.org/wiki/Span_(category_theory)>
+----------------------------------------------------------------------------
+module Control.Morphism.Span 
+	( Span(..)
+	, Cospan(..)
+	) where
+
+newtype Span (~>) x y z = Span { runSpan :: (y ~> x, y ~> z) }
+newtype Cospan (~>) x y z = Cospan { runCospan :: (x ~> y, z ~> y) }