diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown
--- a/CHANGELOG.markdown
+++ b/CHANGELOG.markdown
@@ -1,3 +1,13 @@
+3.5
+---
+* More combinators for `Rift`/`Lift`.
+* Added combinators for working with representable functors rather than just adjoint functors.
+* Split `Data.Functor.KanExtension` into `Data.Functor.Kan.Ran` and `Data.Functor.Kan.Lan`
+* Split `Data.Functor.KanLift` into `Data.Functor.Kan.Rift` and `Data.Functor.Kan.Lift`
+* Moved from `Data.Functor.Yoneda.Contravariant` to `Data.Functor.Yoneda.Reduction` adopting terminology from Todd Trimble.
+* Added various missing isomorphisms.
+* Greatly improved the Haddocks for this package stating laws and derivations where we can (especially for 'Rift' and 'Ran').
+
 3.3
 ---
 * Rift is now `Applicative`. Added `rap`.
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright 2011 Edward Kmett
+Copyright 2008-2013 Edward Kmett
 
 All rights reserved.
 
diff --git a/kan-extensions.cabal b/kan-extensions.cabal
--- a/kan-extensions.cabal
+++ b/kan-extensions.cabal
@@ -1,6 +1,6 @@
 name:          kan-extensions
 category:      Data Structures, Monads, Comonads, Functors
-version:       3.4
+version:       3.5
 license:       BSD3
 cabal-version: >= 1.6
 license-file:  LICENSE
@@ -9,9 +9,9 @@
 stability:     provisional
 homepage:      http://github.com/ekmett/kan-extensions/
 bug-reports:   http://github.com/ekmett/kan-extensions/issues
-copyright:     Copyright (C) 2011-2013 Edward A. Kmett
-synopsis:      Kan extensions, Kan lifts, the Yoneda lemma, and (co)density (co)monads
-description:   Kan extensions, Kan lifts, the Yoneda lemma, and (co)density (co)monads
+copyright:     Copyright (C) 2008-2013 Edward A. Kmett
+synopsis:      Kan extensions, Kan lifts, various forms of the Yoneda lemma, and (co)density (co)monads
+description:   Kan extensions, Kan lifts, various forms of the Yoneda lemma, and (co)density (co)monads
 build-type:    Simple
 
 extra-source-files:
@@ -62,10 +62,13 @@
     Control.Comonad.Density
     Control.Monad.Co
     Control.Monad.Codensity
-    Data.Functor.KanExtension
-    Data.Functor.KanLift
+    Data.Functor.Contravariant.Yoneda.Reduction
+    Data.Functor.Kan.Lan
+    Data.Functor.Kan.Lift
+    Data.Functor.Kan.Ran
+    Data.Functor.Kan.Rift
     Data.Functor.Yoneda
-    Data.Functor.Yoneda.Contravariant
+    Data.Functor.Yoneda.Reduction
 
   ghc-options: -Wall
 
diff --git a/src/Control/Comonad/Density.hs b/src/Control/Comonad/Density.hs
--- a/src/Control/Comonad/Density.hs
+++ b/src/Control/Comonad/Density.hs
@@ -13,15 +13,19 @@
 -- Stability   :  experimental
 -- Portability :  non-portable (GADTs, MPTCs)
 --
--- The density comonad for a functor. aka the comonad generated 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
+-- The 'Density' 'Comonad' for a 'Functor' (aka the 'Comonad generated 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''.
+--
+-- The left Kan extension of a 'Functor' along itself (@'Lan' f f@) forms a 'Comonad'. This is
+-- that 'Comonad'.
 ----------------------------------------------------------------------------
 module Control.Comonad.Density
   ( Density(..)
   , liftDensity
   , densityToAdjunction, adjunctionToDensity
+  , densityToLan, lanToDensity
   ) where
 
 import Control.Applicative
@@ -30,38 +34,80 @@
 import Data.Functor.Apply
 import Data.Functor.Adjunction
 import Data.Functor.Extend
+import Data.Functor.Kan.Lan
 
 data Density k a where
   Density :: (k b -> a) -> k b -> Density k a
 
 instance Functor (Density f) where
   fmap f (Density g h) = Density (f . g) h
+  {-# INLINE fmap #-}
 
 instance Extend (Density f) where
   duplicated (Density f ws) = Density (Density f) ws
+  {-# INLINE duplicated #-}
 
 instance Comonad (Density f) where
   duplicate (Density f ws) = Density (Density f) ws
+  {-# INLINE duplicate #-}
   extract (Density f a) = f a
+  {-# INLINE extract #-}
 
 instance ComonadTrans Density where
   lower (Density f c) = extend f c
+  {-# INLINE lower #-}
 
 instance Apply f => Apply (Density f) where
   Density kxf x <.> Density kya y =
     Density (\k -> kxf (fmap fst k) (kya (fmap snd k))) ((,) <$> x <.> y)
+  {-# INLINE (<.>) #-}
 
 instance Applicative f => Applicative (Density f) where
   pure a = Density (const a) (pure ())
+  {-# INLINE pure #-}
   Density kxf x <*> Density kya y =
     Density (\k -> kxf (fmap fst k) (kya (fmap snd k))) (liftA2 (,) x y)
+  {-# INLINE (<*>) #-}
 
--- | The natural isomorphism between a comonad w and the comonad generated by w (forwards).
+-- | The natural transformation from a @'Comonad' w@ to the 'Comonad' generated by @w@ (forwards).
+--
+-- This is merely a right-inverse (section) of 'lower', rather than a full inverse.
+--
+-- @
+-- 'lower' . 'liftDensity' ≡ 'id'
+-- @
 liftDensity :: Comonad w => w a -> Density w a
 liftDensity = Density extract
+{-# INLINE liftDensity #-}
 
+-- | The Density 'Comonad' of a left adjoint is isomorphic to the 'Comonad' formed by that 'Adjunction'.
+--
+-- This isomorphism is witnessed by 'densityToAdjunction' and 'adjunctionToDensity'.
+--
+-- @
+-- 'densityToAdjunction' . 'adjunctionToDensity' ≡ 'id'
+-- 'adjunctionToDensity' . 'densityToAdjunction' ≡ 'id'
+-- @
 densityToAdjunction :: Adjunction f g => Density f a -> f (g a)
 densityToAdjunction (Density f v) = fmap (leftAdjunct f) v
+{-# INLINE densityToAdjunction #-}
 
 adjunctionToDensity :: Adjunction f g => f (g a) -> Density f a
 adjunctionToDensity = Density counit
+{-# INLINE adjunctionToDensity #-}
+
+-- | The 'Density' 'Comonad' of a 'Functor' @f@ is obtained by taking the left Kan extension
+-- ('Lan') of @f@ along itself. This isomorphism is witnessed by 'lanToDensity' and 'densityToLan'
+--
+-- @
+-- 'lanToDensity' . 'densityToLan' ≡ 'id'
+-- 'densityToLan' . 'lanToDensity' ≡ 'id'
+-- @
+lanToDensity :: Lan f f a -> Density f a
+lanToDensity (Lan f v) = Density f v
+{-# INLINE lanToDensity #-}
+
+densityToLan :: Density f a -> Lan f f a
+densityToLan (Density f v) = Lan f v
+{-# INLINE densityToLan #-}
+
diff --git a/src/Control/Monad/Co.hs b/src/Control/Monad/Co.hs
--- a/src/Control/Monad/Co.hs
+++ b/src/Control/Monad/Co.hs
@@ -23,12 +23,25 @@
 --
 -- <http://comonad.com/reader/2011/monads-from-comonads/>
 --
--- 'Co' and 'CoT' just special cases of the general notion of a
--- Right Kan lift.
+-- 'Co' can be viewed as a right Kan lift along a 'Comonad'.
 --
--- TODO: We could consider unifying the definition of 'CoT' and 'Rift', but
--- 'Rift' f f also forms a Codensity-like 'Monad', so there is a reasonable
--- case for keeping them separate.
+-- In general you can \"sandwich\" a monad in between two halves of an adjunction.
+-- That is to say, if you have an adjunction @F -| G : C -> D @ then not only does @GF@
+-- form a monad, but @GMF@ forms a monad for @M@ a monad in @D@. Therefore if we
+-- have an adjunction @F -| G : Hask -> Hask^op@ then we can lift a 'Comonad' in @Hask@
+-- which is a 'Monad' in @Hask^op@ to a 'Monad' in 'Hask'.
+--
+-- For any @r@, the 'Contravariant' functor / presheaf @(-> r)@ :: Hask^op -> Hask is adjoint to the \"same\"
+-- 'Contravariant' functor @(-> r) :: Hask -> Hask^op@. So we can sandwhich a
+-- Monad in Hask^op in the middle to obtain @w (a -> r-) -> r+@, and then take a coend over
+-- @r@ to obtain @forall r. w (a -> r) -> r@. This gives rise to 'Co'. If we observe that
+-- we didn't care what the choices we made for @r@ were to finish this construction, we can
+-- upgrade to @forall r. w (a -> m r) -> m r@ in a manner similar to how @ContT@ is constructed
+-- yielding 'CoT'.
+--
+-- We could consider unifying the definition of 'Co' and 'Rift', but
+-- there are many other arguments for which 'Rift' can form a 'Monad', and this
+-- wouldn't give rise to 'CoT'.
 ----------------------------------------------------------------------------
 module Control.Monad.Co
   (
diff --git a/src/Control/Monad/Codensity.hs b/src/Control/Monad/Codensity.hs
--- a/src/Control/Monad/Codensity.hs
+++ b/src/Control/Monad/Codensity.hs
@@ -1,5 +1,8 @@
-{-# LANGUAGE Rank2Types, FlexibleInstances, MultiParamTypeClasses, UndecidableInstances #-}
 {-# LANGUAGE CPP #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
 {-# LANGUAGE Trustworthy #-}
 #endif
@@ -10,7 +13,7 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Control.Monad.Codensity
--- Copyright   :  (C) 2008-2011 Edward Kmett
+-- Copyright   :  (C) 2008-2013 Edward Kmett
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
@@ -21,58 +24,86 @@
 module Control.Monad.Codensity
   ( Codensity(..)
   , lowerCodensity
-  , codensityToAdjunction
-  , adjunctionToCodensity
+  , codensityToAdjunction, adjunctionToCodensity
+  , codensityToRan, ranToCodensity
+  , codensityToComposedRep, composedRepToCodensity
   , improve
   ) where
 
 import Control.Applicative
+import Control.Concurrent.Speculation
+import Control.Concurrent.Speculation.Class
+import Control.Monad (ap, MonadPlus(..))
+import Control.Monad.Free
+import Control.Monad.IO.Class
 import Control.Monad.Reader.Class
 import Control.Monad.State.Class
-import Control.Monad.Free.Class
-import Control.Monad.Free
-import Control.Monad (ap, MonadPlus(..))
+import Control.Monad.Trans.Class
 import Data.Functor.Adjunction
 import Data.Functor.Apply
+import Data.Functor.Kan.Ran
 import Data.Functor.Plus
-import Control.Monad.Trans.Class
-import Control.Monad.IO.Class
-import Control.Concurrent.Speculation
-import Control.Concurrent.Speculation.Class
+import Data.Functor.Representable
+import Data.Key
 
-newtype Codensity m a = Codensity { runCodensity :: forall b. (a -> m b) -> m b }
+-- |
+-- @'Codensity' f@ is the Monad generated by taking the right Kan extension
+-- of any 'Functor' @f@ along itself (@Ran f f@).
+--
+-- This can often be more \"efficient\" to construct than @f@ itself using
+-- repeated applications of @(>>=)@.
+--
+-- See \"Asymptotic Improvement of Computations over Free Monads\" by Janis
+-- Voightländer for more information about this type.
+--
+-- <http://www.iai.uni-bonn.de/~jv/mpc08.pdf>
+newtype Codensity m a = Codensity
+  { runCodensity :: forall b. (a -> m b) -> m b
+  }
 
 instance MonadSpec (Codensity m) where
   specByM f g a = Codensity $ \k -> specBy f g k a
+  {-# INLINE specByM #-}
 #if !(MIN_VERSION_speculation(1,5,0))
   specByM' f g a = Codensity $ \k -> specBy' f g k a
+  {-# INLINE specByM' #-}
 #endif
 
 instance Functor (Codensity k) where
   fmap f (Codensity m) = Codensity (\k -> m (k . f))
+  {-# INLINE fmap #-}
 
 instance Apply (Codensity f) where
   (<.>) = ap
+  {-# INLINE (<.>) #-}
 
 instance Applicative (Codensity f) where
   pure x = Codensity (\k -> k x)
+  {-# INLINE pure #-}
   (<*>) = ap
+  {-# INLINE (<*>) #-}
 
 instance Monad (Codensity f) where
   return x = Codensity (\k -> k x)
+  {-# INLINE return #-}
   m >>= k = Codensity (\c -> runCodensity m (\a -> runCodensity (k a) c))
+  {-# INLINE (>>=) #-}
 
 instance MonadIO m => MonadIO (Codensity m) where
-  liftIO = lift . liftIO 
+  liftIO = lift . liftIO
+  {-# INLINE liftIO #-}
 
 instance MonadTrans Codensity where
   lift m = Codensity (m >>=)
+  {-# INLINE lift #-}
 
 instance Alt v => Alt (Codensity v) where
   Codensity m <!> Codensity n = Codensity (\k -> m k <!> n k)
+  {-# INLINE (<!>) #-}
 
 instance Plus v => Plus (Codensity v) where
   zero = Codensity (const zero)
+  {-# INLINE zero #-}
 
 {-
 instance Plus v => Alternative (Codensity v) where
@@ -85,32 +116,110 @@
 -}
 
 instance Alternative v => Alternative (Codensity v) where
-  empty                         = Codensity (\_ -> empty)
+  empty = Codensity (\_ -> empty)
+  {-# INLINE empty #-}
   Codensity m <|> Codensity n = Codensity (\k -> m k <|> n k)
+  {-# INLINE (<|>) #-}
 
 instance MonadPlus v => MonadPlus (Codensity v) where
-  mzero                             = Codensity (\_ -> mzero)
+  mzero = Codensity (\_ -> mzero)
+  {-# INLINE mzero #-}
   Codensity m `mplus` Codensity n = Codensity (\k -> m k `mplus` n k)
+  {-# INLINE mplus #-}
 
+-- |
+-- This serves as the *left*-inverse (retraction) of 'lift'.
+--
+--
+-- @
+-- 'lowerCodensity . lift' ≡ 'id'
+-- @
+--
+-- In general this is not a full 2-sided inverse, merely a retraction, as
+-- @'Codensity' m@ is often considerably "larger" than @m@.
+--
+-- e.g. @'Codensity' ((->) s)) a ~ forall r. (a -> s -> r) -> s -> r@
+-- could support a full complement of @'MonadState' s@ actions, while @(->) s@
+-- is limited to @'MonadReader' s@ actions.
 lowerCodensity :: Monad m => Codensity m a -> m a
 lowerCodensity a = runCodensity a return
+{-# INLINE lowerCodensity #-}
 
+-- | The 'Codensity' monad of a right adjoint is isomorphic to the
+-- monad obtained from the 'Adjunction'.
+--
+-- @
+-- 'codensityToAdjunction' . 'adjunctionToCodensity' ≡ 'id'
+-- 'adjunctionToCodensity' . 'codensityToAdjunction' ≡ 'id'
+-- @
 codensityToAdjunction :: Adjunction f g => Codensity g a -> g (f a)
 codensityToAdjunction r = runCodensity r unit
+{-# INLINE codensityToAdjunction #-}
 
 adjunctionToCodensity :: Adjunction f g => g (f a) -> Codensity g a
 adjunctionToCodensity f = Codensity (\a -> fmap (rightAdjunct a) f)
+{-# INLINE adjunctionToCodensity #-}
 
+-- | The 'Codensity' monad of a representable 'Functor' is isomorphic to the
+-- monad obtained from the 'Adjunction' for which that 'Functor' is the right
+-- adjoint.
+--
+-- @
+-- 'codensityToComposedRep' . 'composedRepToCodensity' ≡ 'id'
+-- 'composedRepToCodensity' . 'codensityToComposedRep' ≡ 'id'
+-- @
+--
+-- @
+-- codensityToComposedRep = 'ranToComposedRep' . 'codensityToRan'
+-- @
+
+codensityToComposedRep :: Representable u => Codensity u a -> u (Key u, a)
+codensityToComposedRep (Codensity f) = f (\a -> tabulate $ \e -> (e, a))
+{-# INLINE codensityToComposedRep #-}
+
+-- |
+--
+-- @
+-- 'composedRepToCodensity' = 'ranToCodensity' . 'composedRepToRan'
+-- @
+composedRepToCodensity :: (Representable u, Functor h) => u (Key u, a) -> Codensity u a
+composedRepToCodensity hfa = Codensity $ \k -> fmap (\(e, a) -> index (k a) e) hfa
+{-# INLINE composedRepToCodensity #-}
+
+-- | The 'Codensity' 'Monad' of a 'Functor' @g@ is the right Kan extension ('Ran')
+-- of @g@ along itself.
+--
+-- @
+-- 'codensityToRan' . 'ranToCodensity' ≡ 'id'
+-- 'ranToCodensity' . 'codensityToRan' ≡ 'id'
+-- @
+codensityToRan :: Codensity g a -> Ran g g a
+codensityToRan (Codensity m) = Ran m
+{-# INLINE codensityToRan #-}
+
+ranToCodensity :: Ran g g a -> Codensity g a
+ranToCodensity (Ran m) = Codensity m
+{-# INLINE ranToCodensity #-}
+
 instance (Functor f, MonadFree f m) => MonadFree f (Codensity m) where
   wrap t = Codensity (\h -> wrap (fmap (\p -> runCodensity p h) t))
+  {-# INLINE wrap #-}
 
 instance MonadReader r m => MonadState r (Codensity m) where
   get = Codensity (ask >>=)
+  {-# INLINE get #-}
   put s = Codensity (\k -> local (const s) (k ()))
+  {-# INLINE put #-}
 
 -- | Right associate all binds in a computation that generates a free monad
+--
 -- This can improve the asymptotic efficiency of the result, while preserving
 -- semantics.
+--
+-- See \"Asymptotic Improvement of Computations over Free Monads\" by Janis
+-- Voightländer for more information about this combinator.
+--
+-- <http://www.iai.uni-bonn.de/~jv/mpc08.pdf>
 improve :: Functor f => (forall m. MonadFree f m => m a) -> Free f a
 improve m = lowerCodensity m
-
+{-# INLINE improve #-}
diff --git a/src/Data/Functor/Contravariant/Yoneda/Reduction.hs b/src/Data/Functor/Contravariant/Yoneda/Reduction.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Functor/Contravariant/Yoneda/Reduction.hs
@@ -0,0 +1,70 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE UndecidableInstances #-}
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
+{-# LANGUAGE Trustworthy #-}
+#endif
+-----------------------------------------------------------------------------
+-- |
+-- Copyright   :  (C) 2013 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  provisional
+-- Portability :  GADTs, TFs, MPTCs
+--
+-- Yoneda Reduction of presheafs
+--
+-- <http://ncatlab.org/nlab/show/Yoneda+reduction>
+--
+----------------------------------------------------------------------------
+module Data.Functor.Contravariant.Yoneda.Reduction
+  ( Yoneda(..)
+  , liftYoneda
+  , lowerYoneda
+  ) where
+
+import Control.Arrow
+import Data.Functor.Contravariant
+import Data.Functor.Contravariant.Adjunction
+import Data.Functor.Contravariant.Representable
+
+type instance Value (Yoneda f) = Value f
+
+-- | A 'Contravariant' functor (aka presheaf) suitable for Yoneda reduction.
+data Yoneda f a where
+  Yoneda :: (a -> b) -> f b -> Yoneda f a
+
+instance Contravariant (Yoneda f) where
+  contramap f (Yoneda g m) = Yoneda (g.f) m
+  {-# INLINE contramap #-}
+
+instance Valued f => Valued (Yoneda f) where
+  contramapWithValue beav (Yoneda ac fc) = Yoneda (left ac . beav) (contramapWithValue id fc)
+  {-# INLINE contramapWithValue #-}
+
+instance Coindexed f => Coindexed (Yoneda f) where
+  coindex (Yoneda ab fb) a = coindex fb (ab a)
+  {-# INLINE coindex #-}
+
+instance Representable f => Representable (Yoneda f) where
+  contrarep = liftYoneda . contrarep
+  {-# INLINE contrarep #-}
+
+instance Adjunction f g => Adjunction (Yoneda f) (Yoneda g) where
+  leftAdjunct f = liftYoneda . leftAdjunct (lowerYoneda . f)
+  {-# INLINE leftAdjunct #-}
+  rightAdjunct f = liftYoneda . rightAdjunct (lowerYoneda . f)
+  {-# INLINE rightAdjunct #-}
+
+-- | Yoneda "expansion" of a presheaf
+liftYoneda :: f a -> Yoneda f a
+liftYoneda = Yoneda id
+{-# INLINE liftYoneda #-}
+
+-- | Yoneda reduction on a presheaf
+lowerYoneda :: Contravariant f => Yoneda f a -> f a
+lowerYoneda (Yoneda f m) = contramap f m
+{-# INLINE lowerYoneda #-}
diff --git a/src/Data/Functor/Kan/Lan.hs b/src/Data/Functor/Kan/Lan.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Functor/Kan/Lan.hs
@@ -0,0 +1,114 @@
+{-# LANGUAGE Rank2Types, GADTs #-}
+{-# LANGUAGE CPP #-}
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
+{-# LANGUAGE Trustworthy #-}
+#endif
+-------------------------------------------------------------------------------------------
+-- |
+-- Copyright 	: 2008-2013 Edward Kmett
+-- License	: BSD
+--
+-- Maintainer	: Edward Kmett <ekmett@gmail.com>
+-- Stability	: experimental
+-- Portability	: rank 2 types
+--
+-- Left Kan Extensions
+-------------------------------------------------------------------------------------------
+module Data.Functor.Kan.Lan
+  (
+  -- * Left Kan Extensions
+    Lan(..)
+  , toLan, fromLan
+  , glan
+  , composeLan, decomposeLan
+  , adjointToLan, lanToAdjoint
+  , composedAdjointToLan, lanToComposedAdjoint
+  ) where
+
+import Control.Applicative
+import Data.Functor.Adjunction
+import Data.Functor.Apply
+import Data.Functor.Composition
+import Data.Functor.Identity
+
+-- | The left Kan extension of a 'Functor' @h@ along a 'Functor' @g@.
+data Lan g h a where
+  Lan :: (g b -> a) -> h b -> Lan g h a
+
+instance Functor (Lan f g) where
+  fmap f (Lan g h) = Lan (f . g) h
+  {-# INLINE fmap #-}
+
+instance (Functor g, Apply h) => Apply (Lan g h) where
+  Lan kxf x <.> Lan kya y =
+    Lan (\k -> kxf (fmap fst k) (kya (fmap snd k))) ((,) <$> x <.> y)
+  {-# INLINE (<.>) #-}
+
+instance (Functor g, Applicative h) => Applicative (Lan g h) where
+  pure a = Lan (const a) (pure ())
+  {-# INLINE pure #-}
+  Lan kxf x <*> Lan kya y =
+    Lan (\k -> kxf (fmap fst k) (kya (fmap snd k))) (liftA2 (,) x y)
+  {-# INLINE (<*>) #-}
+
+-- | The universal property of a left Kan extension.
+toLan :: Functor f => (forall a. h a -> f (g a)) -> Lan g h b -> f b
+toLan s (Lan f v) = fmap f (s v)
+{-# INLINE toLan #-}
+
+-- | 'fromLan' and 'toLan' witness a (higher kinded) adjunction between @'Lan' g@ and @(`Compose` g)@
+--
+-- @
+-- 'toLan' . 'fromLan' ≡ 'id'
+-- 'fromLan' . 'toLan' ≡ 'id'
+-- @
+fromLan :: (forall a. Lan g h a -> f a) -> h b -> f (g b)
+fromLan s = s . glan
+{-# INLINE fromLan #-}
+
+-- |
+--
+-- @
+-- 'adjointToLan' . 'lanToAdjoint' ≡ 'id'
+-- 'lanToAdjoint' . 'adjointToLan' ≡ 'id'
+-- @
+adjointToLan :: Adjunction f g => g a -> Lan f Identity a
+adjointToLan = Lan counit . Identity
+{-# INLINE adjointToLan #-}
+
+lanToAdjoint :: Adjunction f g => Lan f Identity a -> g a
+lanToAdjoint (Lan f v) = leftAdjunct f (runIdentity v)
+{-# INLINE lanToAdjoint #-}
+
+-- | 'lanToComposedAdjoint' and 'composedAdjointToLan' witness the natural isomorphism between @Lan f h@ and @Compose h g@ given @f -| g@
+--
+-- @
+-- 'composedAdjointToLan' . 'lanToComposedAdjoint' ≡ 'id'
+-- 'lanToComposedAdjoint' . 'composedAdjointToLan' ≡ 'id'
+-- @
+lanToComposedAdjoint :: (Functor h, Adjunction f g) => Lan f h a -> h (g a)
+lanToComposedAdjoint (Lan f v) = fmap (leftAdjunct f) v
+{-# INLINE lanToComposedAdjoint #-}
+
+composedAdjointToLan :: Adjunction f g => h (g a) -> Lan f h a
+composedAdjointToLan = Lan counit
+{-# INLINE composedAdjointToLan #-}
+
+-- | 'composeLan' and 'decomposeLan' witness the natural isomorphism from @Lan f (Lan g h)@ and @Lan (f `o` g) h@
+--
+-- @
+-- 'composeLan' . 'decomposeLan' ≡ 'id'
+-- 'decomposeLan' . 'composeLan' ≡ 'id'
+-- @
+composeLan :: (Composition compose, Functor f) => Lan f (Lan g h) a -> Lan (compose f g) h a
+composeLan (Lan f (Lan g h)) = Lan (f . fmap g . decompose) h
+{-# INLINE composeLan #-}
+
+decomposeLan :: Composition compose => Lan (compose f g) h a -> Lan f (Lan g h) a
+decomposeLan (Lan f h) = Lan (f . compose) (Lan id h)
+{-# INLINE decomposeLan #-}
+
+-- | This is the natural transformation that defines a Left Kan extension.
+glan :: h a -> Lan g h (g a)
+glan = Lan id
+{-# INLINE glan #-}
diff --git a/src/Data/Functor/Kan/Lift.hs b/src/Data/Functor/Kan/Lift.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Functor/Kan/Lift.hs
@@ -0,0 +1,151 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE GADTs #-}
+
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
+{-# LANGUAGE Trustworthy #-}
+#endif
+-------------------------------------------------------------------------------------------
+-- |
+-- Copyright 	: 2013 Edward Kmett and Dan Doel
+-- License	: BSD
+--
+-- Maintainer	: Edward Kmett <ekmett@gmail.com>
+-- Stability	: experimental
+-- Portability	: rank N types
+--
+-- Left Kan lifts for functors over Hask, wherever they exist.
+--
+-- <http://ncatlab.org/nlab/show/Kan+lift>
+-------------------------------------------------------------------------------------------
+module Data.Functor.Kan.Lift
+  (
+  -- * Left Kan lifts
+    Lift(..)
+  , toLift, fromLift, glift
+  , composeLift, decomposeLift
+  , adjointToLift, liftToAdjoint
+  , liftToComposedAdjoint, composedAdjointToLift
+  , repToLift, liftToRep
+  , liftToComposedRep, composedRepToLift
+  ) where
+
+import Data.Copointed
+import Data.Functor.Adjunction
+import Data.Functor.Composition
+import Data.Functor.Compose
+import Data.Functor.Identity
+import Data.Functor.Representable
+import Data.Key
+
+-- * Left Kan Lift
+
+-- |
+-- > f => g . Lift g f
+-- > (forall z. f => g . z) -> Lift g f => z -- couniversal
+--
+-- Here we use the universal property directly as how we extract from our definition of 'Lift'.
+newtype Lift g f a = Lift { runLift :: forall z. Functor z => (forall x. f x -> g (z x)) -> z a }
+
+instance Functor (Lift g h) where
+  fmap f (Lift g) = Lift (fmap f . g)
+  {-# INLINE fmap #-}
+
+instance (Functor g, g ~ h) => Copointed (Lift g h) where
+  copoint x = runIdentity (runLift x (fmap Identity))
+  {-# INLINE copoint #-}
+
+-- |
+--
+-- @f => g ('Lift' g f a)@
+glift :: Adjunction l g => k a -> g (Lift g k a)
+glift = leftAdjunct (\lka -> Lift (\k2gz -> rightAdjunct k2gz lka))
+{-# INLINE glift #-}
+
+-- | The universal property of 'Lift'
+toLift :: Functor z => (forall a. f a -> g (z a)) -> Lift g f b -> z b
+toLift = flip runLift
+{-# INLINE toLift #-}
+
+-- | When the adjunction exists
+--
+-- @
+-- 'fromLift' . 'toLift' ≡ 'id'
+-- 'toLift' . 'fromLift' ≡ 'id'
+-- @
+fromLift :: Adjunction l u => (forall a. Lift u f a -> z a) -> f b -> u (z b)
+fromLift f = fmap f . glift
+{-# INLINE fromLift #-}
+
+-- |
+--
+-- @
+-- 'composeLift' . 'decomposeLift' = 'id'
+-- 'decomposeLift' . 'composeLift' = 'id'
+-- @
+composeLift :: (Composition compose, Functor f, Functor g) => Lift f (Lift g h) a -> Lift (compose g f) h a
+composeLift (Lift m) = Lift $ \h -> m $ decompose . toLift (fmap Compose . decompose . h)
+{-# INLINE composeLift #-}
+
+decomposeLift :: (Composition compose, Adjunction l g) => Lift (compose g f) h a -> Lift f (Lift g h) a
+decomposeLift (Lift m) = Lift $ \h -> m (compose . fmap h . glift)
+{-# INLINE decomposeLift #-}
+
+-- | @Lift u Identity a@ is isomorphic to the left adjoint to @u@ if one exists.
+--
+-- @
+-- 'adjointToLift' . 'liftToAdjoint' ≡ 'id'
+-- 'liftToAdjoint' . 'adjointToLift' ≡ 'id'
+-- @
+adjointToLift :: Adjunction f u => f a -> Lift u Identity a
+adjointToLift fa = Lift $ \k -> rightAdjunct (k . Identity) fa
+{-# INLINE adjointToLift #-}
+
+
+-- | @Lift u Identity a@ is isomorphic to the left adjoint to @u@ if one exists.
+liftToAdjoint :: Adjunction f u => Lift u Identity a -> f a
+liftToAdjoint = toLift (unit . runIdentity)
+{-# INLINE liftToAdjoint #-}
+
+-- |
+--
+-- @
+-- 'repToLift' . 'liftToRep' ≡ 'id'
+-- 'liftToRep' . 'repToLift' ≡ 'id'
+-- @
+repToLift :: Representable u => Key u -> a -> Lift u Identity a
+repToLift e a = Lift $ \k -> index (k (Identity a)) e
+{-# INLINE repToLift #-}
+
+liftToRep :: Representable u => Lift u Identity a -> (Key u, a)
+liftToRep (Lift m) = m $ \(Identity a) -> tabulate $ \e -> (e, a)
+{-# INLINE liftToRep #-}
+
+-- | @Lift u h a@ is isomorphic to the post-composition of the left adjoint of @u@ onto @h@ if such a left adjoint exists.
+--
+-- @
+-- 'liftToComposedAdjoint' . 'composedAdjointToLift' ≡ 'id'
+-- 'composedAdjointToLift' . 'liftToComposedAdjoint' ≡ 'id'
+-- @
+liftToComposedAdjoint :: (Adjunction f u, Functor h) => Lift u h a -> f (h a)
+liftToComposedAdjoint (Lift m) = decompose $ m (leftAdjunct Compose)
+{-# INLINE liftToComposedAdjoint #-}
+
+-- | @Lift u h a@ is isomorphic to the post-composition of the left adjoint of @u@ onto @h@ if such a left adjoint exists.
+composedAdjointToLift :: Adjunction f u => f (h a) -> Lift u h a
+composedAdjointToLift = rightAdjunct glift
+{-# INLINE composedAdjointToLift #-}
+
+-- |
+--
+-- @
+-- 'liftToComposedRep' . 'composedRepToLift' ≡ 'id'
+-- 'composedRepToLift' . 'liftToComposedRep' ≡ 'id'
+-- @
+liftToComposedRep :: (Functor h, Representable u) => Lift u h a -> (Key u, h a)
+liftToComposedRep (Lift m) = decompose $ m $ \h -> tabulate $ \e -> Compose (e, h)
+{-# INLINE liftToComposedRep #-}
+
+composedRepToLift :: Representable u => Key u -> h a -> Lift u h a
+composedRepToLift e ha = Lift $ \h2uz -> index (h2uz ha) e
+{-# INLINE composedRepToLift #-}
diff --git a/src/Data/Functor/Kan/Ran.hs b/src/Data/Functor/Kan/Ran.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Functor/Kan/Ran.hs
@@ -0,0 +1,167 @@
+{-# LANGUAGE Rank2Types, GADTs #-}
+{-# LANGUAGE CPP #-}
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
+{-# LANGUAGE Trustworthy #-}
+#endif
+-------------------------------------------------------------------------------------------
+-- |
+-- Copyright 	: 2008-2013 Edward Kmett
+-- License	: BSD
+--
+-- Maintainer	: Edward Kmett <ekmett@gmail.com>
+-- Stability	: experimental
+-- Portability	: rank 2 types
+--
+-- * Right Kan Extensions
+-------------------------------------------------------------------------------------------
+module Data.Functor.Kan.Ran
+  (
+    Ran(..)
+  , toRan, fromRan
+  , gran
+  , composeRan, decomposeRan
+  , adjointToRan, ranToAdjoint
+  , composedAdjointToRan, ranToComposedAdjoint
+  , repToRan, ranToRep
+  , composedRepToRan, ranToComposedRep
+  ) where
+
+import Data.Functor.Adjunction
+import Data.Functor.Composition
+import Data.Functor.Identity
+import Data.Functor.Representable
+import Data.Key
+
+-- | The right Kan extension of a 'Functor' h along a 'Functor' g.
+--
+-- We can define a right Kan extension in several ways. The definition here is obtained by reading off
+-- the definition in of a right Kan extension in terms of an End, but we can derive an equivalent definition
+-- from the universal property.
+--
+-- Given a 'Functor' @h : C -> D@ and a 'Functor' @g : C -> C'@, we want to find extend @h@ /back/ along @g@
+-- to give @Ran g h : C' -> C@, such that the natural transformation @'gran' :: Ran g h (g a) -> h a@ exists.
+--
+-- In some sense this is trying to approximate the inverse of @g@ by using one of
+-- its adjoints, because if the adjoint and the inverse both exist, they match!
+--
+-- > Hask -h-> Hask
+-- >   |       +
+-- >   g      /
+-- >   |    Ran g h
+-- >   v    /
+-- > Hask -'
+--
+-- The Right Kan extension is unique (up to isomorphism) by taking this as its universal property.
+--
+-- That is to say given any @K : C' -> C@ such that we have a natural transformation from @k.g@ to @h@
+-- @(forall x. k (g x) -> h x)@ there exists a canonical natural transformation from @k@ to @Ran g h@.
+-- @(forall x. k x -> Ran g h x)@.
+--
+-- We could literally read this off as a valid Rank-3 definition for 'Ran':
+--
+-- @
+-- data Ran' g h a = forall z. 'Functor' z => Ran' (forall x. z (g x) -> h x) (z a)
+-- @
+--
+-- This definition is isomorphic the simpler Rank-2 definition we use below as witnessed by the
+--
+-- @
+-- ranIso1 :: Ran g f x -> Ran' g f x
+-- ranIso1 (Ran e) = Ran' e id
+--
+-- ranIso2 :: Ran' g f x -> Ran g f x
+-- ranIso2 (Ran' h z) = Ran $ \k -> h (k <$> z)
+-- @
+--
+-- @
+-- ranIso2 (ranIso1 (Ran e)) ≡ -- by definition
+-- ranIso2 (Ran' e id) ≡       -- by definition
+-- Ran $ \k -> e (k <$> id)    -- by definition
+-- Ran $ \k -> e (k . id)      -- f . id = f
+-- Ran $ \k -> e k             -- eta reduction
+-- Ran e
+-- @
+--
+-- The other direction is left as an exercise for the reader.
+newtype Ran g h a = Ran { runRan :: forall b. (a -> g b) -> h b }
+
+instance Functor (Ran g h) where
+  fmap f m = Ran (\k -> runRan m (k . f))
+  {-# INLINE fmap #-}
+
+-- | The universal property of a right Kan extension.
+toRan :: Functor k => (forall a. k (g a) -> h a) -> k b -> Ran g h b
+toRan s t = Ran (s . flip fmap t)
+{-# INLINE toRan #-}
+
+-- | 'toRan' and 'fromRan' witness a higher kinded adjunction. from @(`'Compose'` g)@ to @'Ran' g@
+--
+-- @
+-- 'toRan' . 'fromRan' ≡ 'id'
+-- 'fromRan' . 'toRan' ≡ 'id'
+-- @
+fromRan :: (forall a. k a -> Ran g h a) -> k (g b) -> h b
+fromRan s = flip runRan id . s
+{-# INLINE fromRan #-}
+
+-- |
+-- @
+-- 'composeRan' . 'decomposeRan' ≡ 'id'
+-- 'decomposeRan' . 'composeRan' ≡ 'id'
+-- @
+composeRan :: Composition compose => Ran f (Ran g h) a -> Ran (compose f g) h a
+composeRan r = Ran (\f -> runRan (runRan r (decompose . f)) id)
+{-# INLINE composeRan #-}
+
+decomposeRan :: (Composition compose, Functor f) => Ran (compose f g) h a -> Ran f (Ran g h) a
+decomposeRan r = Ran (\f -> Ran (\g -> runRan r (compose . fmap g . f)))
+{-# INLINE decomposeRan #-}
+
+-- |
+--
+-- @
+-- 'adjointToRan' . 'ranToAdjoint' ≡ 'id'
+-- 'ranToAdjoint' . 'adjointToRan' ≡ 'id'
+-- @
+adjointToRan :: Adjunction f g => f a -> Ran g Identity a
+adjointToRan f = Ran (\a -> Identity $ rightAdjunct a f)
+{-# INLINE adjointToRan #-}
+
+ranToAdjoint :: Adjunction f g => Ran g Identity a -> f a
+ranToAdjoint r = runIdentity (runRan r unit)
+{-# INLINE ranToAdjoint #-}
+
+-- |
+--
+-- @
+-- 'composedAdjointToRan' . 'ranToComposedAdjoint' ≡ 'id'
+-- 'ranToComposedAdjoint' . 'composedAdjointToRan' ≡ 'id'
+-- @
+ranToComposedAdjoint :: Adjunction f g => Ran g h a -> h (f a)
+ranToComposedAdjoint r = runRan r unit
+{-# INLINE ranToComposedAdjoint #-}
+
+composedAdjointToRan :: (Adjunction f g, Functor h) => h (f a) -> Ran g h a
+composedAdjointToRan f = Ran (\a -> fmap (rightAdjunct a) f)
+{-# INLINE composedAdjointToRan #-}
+
+-- | This is the natural transformation that defines a Right Kan extension.
+gran :: Ran g h (g a) -> h a
+gran (Ran f) = f id
+{-# INLINE gran #-}
+
+repToRan :: Representable u => Key u -> a -> Ran u Identity a
+repToRan e a = Ran $ \k -> Identity $ index (k a) e
+{-# INLINE repToRan #-}
+
+ranToRep :: Representable u => Ran u Identity a -> (Key u, a)
+ranToRep (Ran f) = runIdentity $ f (\a -> tabulate $ \e -> (e, a))
+{-# INLINE ranToRep #-}
+
+ranToComposedRep :: Representable u => Ran u h a -> h (Key u, a)
+ranToComposedRep (Ran f) = f (\a -> tabulate $ \e -> (e, a))
+{-# INLINE ranToComposedRep #-}
+
+composedRepToRan :: (Representable u, Functor h) => h (Key u, a) -> Ran u h a
+composedRepToRan hfa = Ran $ \k -> fmap (\(e, a) -> index (k a) e) hfa
+{-# INLINE composedRepToRan #-}
diff --git a/src/Data/Functor/Kan/Rift.hs b/src/Data/Functor/Kan/Rift.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Functor/Kan/Rift.hs
@@ -0,0 +1,191 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE GADTs #-}
+
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
+{-# LANGUAGE Trustworthy #-}
+#endif
+-------------------------------------------------------------------------------------------
+-- |
+-- Copyright 	: 2013 Edward Kmett and Dan Doel
+-- License	: BSD
+--
+-- Maintainer	: Edward Kmett <ekmett@gmail.com>
+-- Stability	: experimental
+-- Portability	: rank N types
+--
+-- Right and Left Kan lifts for functors over Hask, where they exist.
+--
+-- <http://ncatlab.org/nlab/show/Kan+lift>
+-------------------------------------------------------------------------------------------
+module Data.Functor.Kan.Rift
+  (
+  -- * Right Kan lifts
+    Rift(..)
+  , toRift, fromRift, grift
+  , composeRift, decomposeRift
+  , adjointToRift, riftToAdjoint
+  , composedAdjointToRift, riftToComposedAdjoint
+  , rap
+  ) where
+
+import Control.Applicative
+import Data.Functor.Adjunction
+import Data.Functor.Composition
+import Data.Functor.Identity
+import Data.Pointed
+
+-- * Right Kan Lift
+
+-- |
+--
+-- @g . 'Rift' g f => f@
+--
+-- This could alternately be defined directly from the (co)universal propertly
+-- in which case, we'd get 'toRift' = 'UniversalRift', but then the usage would
+-- suffer.
+--
+-- @
+-- data 'UniversalRift' g f a = forall z. 'Functor' z =>
+--      'UniversalRift' (forall x. g (z x) -> f x) (z a)
+-- @
+--
+-- We can witness the isomorphism between Rift and UniversalRift using:
+--
+-- @
+-- riftIso1 :: Functor g => UniversalRift g f a -> Rift g f a
+-- riftIso1 (UniversalRift h z) = Rift $ \g -> h $ fmap (\k -> k <$> z) g
+-- @
+--
+-- @
+-- riftIso2 :: Rift g f a -> UniversalRift g f a
+-- riftIso2 (Rift e) = UniversalRift e id
+-- @
+--
+-- @
+-- riftIso1 (riftIso2 (Rift h)) =
+-- riftIso1 (UniversalRift h id) =          -- by definition
+-- Rift $ \g -> h $ fmap (\k -> k <$> id) g -- by definition
+-- Rift $ \g -> h $ fmap id g               -- <$> = (.) and (.id)
+-- Rift $ \g -> h g                         -- by functor law
+-- Rift h                                   -- eta reduction
+-- @
+--
+-- The other direction is left as an exercise for the reader.
+--
+-- There are several monads that we can form from @Rift@.
+--
+-- When @g@ is corepresentable (e.g. is a right adjoint) then there exists @x@ such that @g ~ (->) x@, then it follows that
+--
+-- @
+-- Rift g g a ~
+-- forall r. (x -> a -> r) -> x -> r ~
+-- forall r. (a -> x -> r) -> x -> r ~
+-- forall r. (a -> g r) -> g r ~
+-- Codensity g r
+-- @
+--
+-- When @f@ is a left adjoint, so that @f -| g@ then
+--
+-- @
+-- Rift f f a ~
+-- forall r. f (a -> r) -> f r ~
+-- forall r. (a -> r) -> g (f r) ~
+-- forall r. (a -> r) -> Adjoint f g r ~
+-- Yoneda (Adjoint f g r)
+-- @
+--
+-- An alternative way to view that is to note that whenever @f@ is a left adjoint then @f -| 'Rift' f 'Identity'@, and since @'Rift' f f@ is isomorphic to @'Rift' f 'Identity' (f a)@, this is the 'Monad' formed by the adjunction.
+--
+-- @'Rift' w f ~ 'Control.Monad.Co.CoT' w f@ can be a 'Monad' for any 'Comonad' @w@.
+--
+-- @'Rift' 'Identity' m@ can be a 'Monad' for any 'Monad' @m@, as it is isomorphic to @'Yoneda' m@.
+
+newtype Rift g h a =
+  Rift { runRift :: forall r. g (a -> r) -> h r }
+
+instance Functor g => Functor (Rift g h) where
+  fmap f (Rift g) = Rift (g . fmap (.f))
+  {-# INLINE fmap #-}
+
+instance (Functor g, g ~ h) => Pointed (Rift g h) where
+  point a = Rift (fmap ($a))
+  {-# INLINE point #-}
+
+instance (Functor g, g ~ h) => Applicative (Rift g h) where
+  pure a = Rift (fmap ($a))
+  {-# INLINE pure #-}
+  Rift mf <*> Rift ma = Rift (ma . mf . fmap (.))
+  {-# INLINE (<*>) #-}
+
+-- | Indexed applicative composition of right Kan lifts.
+rap :: Functor f => Rift f g (a -> b) -> Rift g h a -> Rift f h b
+rap (Rift mf) (Rift ma) = Rift (ma . mf . fmap (.))
+{-# INLINE rap #-}
+
+grift :: Adjunction f u => f (Rift f k a) -> k a
+grift = rightAdjunct (\r -> leftAdjunct (runRift r) id)
+{-# INLINE grift #-}
+
+-- | The universal property of 'Rift'
+toRift :: (Functor g, Functor k) => (forall x. g (k x) -> h x) -> k a -> Rift g h a
+toRift h z = Rift $ \g -> h $ fmap (<$> z) g
+{-# INLINE toRift #-}
+
+-- |
+-- When @f -| u@, then @f -| Rift f Identity@ and
+--
+-- @
+-- 'toRift' . 'fromRift' ≡ 'id'
+-- 'fromRift' . 'toRift' ≡ 'id'
+-- @
+fromRift :: Adjunction f u => (forall a. k a -> Rift f h a) -> f (k b) -> h b
+fromRift f = grift . fmap f
+{-# INLINE fromRift #-}
+
+-- | @Rift f Identity a@ is isomorphic to the right adjoint to @f@ if one exists.
+--
+-- @
+-- 'adjointToRift' . 'riftToAdjoint' ≡ 'id'
+-- 'riftToAdjoint' . 'adjointToRift' ≡ 'id'
+-- @
+adjointToRift :: Adjunction f u => u a -> Rift f Identity a
+adjointToRift ua = Rift (Identity . rightAdjunct (<$> ua))
+{-# INLINE adjointToRift #-}
+
+-- | @Rift f Identity a@ is isomorphic to the right adjoint to @f@ if one exists.
+riftToAdjoint :: Adjunction f u => Rift f Identity a -> u a
+riftToAdjoint (Rift m) = leftAdjunct (runIdentity . m) id
+{-# INLINE riftToAdjoint #-}
+
+-- |
+--
+-- @
+-- 'composeRift' . 'decomposeRift' ≡ 'id'
+-- 'decomposeRift' . 'composeRift' ≡ 'id'
+-- @
+composeRift :: (Composition compose, Adjunction g u) => Rift f (Rift g h) a -> Rift (compose g f) h a
+composeRift (Rift f) = Rift (grift . fmap f . decompose)
+{-# INLINE composeRift #-}
+
+decomposeRift :: (Composition compose, Functor f, Functor g) => Rift (compose g f) h a -> Rift f (Rift g h) a
+decomposeRift (Rift f) = Rift $ \far -> Rift (f . compose . fmap (\rs -> fmap (rs.) far))
+{-# INLINE decomposeRift #-}
+
+
+-- | @Rift f h a@ is isomorphic to the post-composition of the right adjoint of @f@ onto @h@ if such a right adjoint exists.
+--
+-- @
+-- 'riftToComposedAdjoint' . 'composedAdjointToRift' ≡ 'id'
+-- 'composedAdjointToRift' . 'riftToComposedAdjoint' ≡ 'id'
+-- @
+
+riftToComposedAdjoint :: Adjunction f u => Rift f h a -> u (h a)
+riftToComposedAdjoint (Rift m) = leftAdjunct m id
+{-# INLINE riftToComposedAdjoint #-}
+
+-- | @Rift f h a@ is isomorphic to the post-composition of the right adjoint of @f@ onto @h@ if such a right adjoint exists.
+composedAdjointToRift :: (Functor h, Adjunction f u) => u (h a) -> Rift f h a
+composedAdjointToRift uha = Rift $ rightAdjunct (\b -> fmap b <$> uha)
+{-# INLINE composedAdjointToRift #-}
+
diff --git a/src/Data/Functor/KanExtension.hs b/src/Data/Functor/KanExtension.hs
deleted file mode 100644
--- a/src/Data/Functor/KanExtension.hs
+++ /dev/null
@@ -1,96 +0,0 @@
-{-# LANGUAGE Rank2Types, GADTs #-}
-{-# LANGUAGE CPP #-}
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
-{-# LANGUAGE Trustworthy #-}
-#endif
--------------------------------------------------------------------------------------------
--- |
--- Module	: Data.Functor.KanExtension
--- Copyright 	: 2008-2011 Edward Kmett
--- License	: BSD
---
--- Maintainer	: Edward Kmett <ekmett@gmail.com>
--- Stability	: experimental
--- Portability	: rank 2 types
---
--------------------------------------------------------------------------------------------
-module Data.Functor.KanExtension where
-
-import Data.Functor.Identity
-import Data.Functor.Adjunction
-import Data.Functor.Composition
-import Data.Functor.Apply
-import Control.Applicative
-
-newtype Ran g h a = Ran { runRan :: forall b. (a -> g b) -> h b }
-
-instance Functor (Ran g h) where
-  fmap f m = Ran (\k -> runRan m (k . f))
-
--- | 'toRan' and 'fromRan' witness a higher kinded adjunction. from @(`'Compose'` g)@ to @'Ran' g@
-toRan :: Functor k => (forall a. k (g a) -> h a) -> k b -> Ran g h b
-toRan s t = Ran (s . flip fmap t)
-
-fromRan :: (forall a. k a -> Ran g h a) -> k (g b) -> h b
-fromRan s = flip runRan id . s
-
-composeRan :: Composition compose => Ran f (Ran g h) a -> Ran (compose f g) h a
-composeRan r = Ran (\f -> runRan (runRan r (decompose . f)) id)
-
-decomposeRan :: (Composition compose, Functor f) => Ran (compose f g) h a -> Ran f (Ran g h) a
-decomposeRan r = Ran (\f -> Ran (\g -> runRan r (compose . fmap g . f)))
-
-adjointToRan :: Adjunction f g => f a -> Ran g Identity a
-adjointToRan f = Ran (\a -> Identity $ rightAdjunct a f)
-
-ranToAdjoint :: Adjunction f g => Ran g Identity a -> f a
-ranToAdjoint r = runIdentity (runRan r unit)
-
-ranToComposedAdjoint :: Adjunction f g => Ran g h a -> h (f a)
-ranToComposedAdjoint r = runRan r unit
-
-composedAdjointToRan :: (Adjunction f g, Functor h) => h (f a) -> Ran g h a
-composedAdjointToRan f = Ran (\a -> fmap (rightAdjunct a) f)
-
-data Lan g h a where
-  Lan :: (g b -> a) -> h b -> Lan g h a
-
--- 'fromLan' and 'toLan' witness a (higher kinded) adjunction between @'Lan' g@ and @(`Compose` g)@
-toLan :: Functor f => (forall a. h a -> f (g a)) -> Lan g h b -> f b
-toLan s (Lan f v) = fmap f (s v)
-
-fromLan :: (forall a. Lan g h a -> f a) -> h b -> f (g b)
-fromLan s = s . Lan id
-
-instance Functor (Lan f g) where
-  fmap f (Lan g h) = Lan (f . g) h
-
-instance (Functor g, Apply h) => Apply (Lan g h) where
-  Lan kxf x <.> Lan kya y =
-    Lan (\k -> kxf (fmap fst k) (kya (fmap snd k))) ((,) <$> x <.> y)
-
-instance (Functor g, Applicative h) => Applicative (Lan g h) where
-  pure a = Lan (const a) (pure ())
-  Lan kxf x <*> Lan kya y =
-    Lan (\k -> kxf (fmap fst k) (kya (fmap snd k))) (liftA2 (,) x y)
-
-adjointToLan :: Adjunction f g => g a -> Lan f Identity a
-adjointToLan = Lan counit . Identity
-
-lanToAdjoint :: Adjunction f g => Lan f Identity a -> g a
-lanToAdjoint (Lan f v) = leftAdjunct f (runIdentity v)
-
--- | 'lanToComposedAdjoint' and 'composedAdjointToLan' witness the natural isomorphism between @Lan f h@ and @Compose h g@ given @f -| g@
-lanToComposedAdjoint :: (Functor h, Adjunction f g) => Lan f h a -> h (g a)
-lanToComposedAdjoint (Lan f v) = fmap (leftAdjunct f) v
-
-composedAdjointToLan :: Adjunction f g => h (g a) -> Lan f h a
-composedAdjointToLan = Lan counit
-
--- | 'composeLan' and 'decomposeLan' witness the natural isomorphism from @Lan f (Lan g h)@ and @Lan (f `o` g) h@
-composeLan :: (Composition compose, Functor f) => Lan f (Lan g h) a -> Lan (compose f g) h a
-composeLan (Lan f (Lan g h)) = Lan (f . fmap g . decompose) h
-
-decomposeLan :: Composition compose => Lan (compose f g) h a -> Lan f (Lan g h) a
-decomposeLan (Lan f h) = Lan (f . compose) (Lan id h)
-
diff --git a/src/Data/Functor/KanLift.hs b/src/Data/Functor/KanLift.hs
deleted file mode 100644
--- a/src/Data/Functor/KanLift.hs
+++ /dev/null
@@ -1,284 +0,0 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE GADTs #-}
-
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
-{-# LANGUAGE Trustworthy #-}
-#endif
--------------------------------------------------------------------------------------------
--- |
--- Copyright 	: 2013 Edward Kmett and Dan Doel
--- License	: BSD
---
--- Maintainer	: Edward Kmett <ekmett@gmail.com>
--- Stability	: experimental
--- Portability	: rank N types
---
--- Right and Left Kan lifts for functors over Hask, where they exist.
---
--- <http://ncatlab.org/nlab/show/Kan+lift>
--------------------------------------------------------------------------------------------
-module Data.Functor.KanLift
-  (
-  -- * Right Kan lifts
-    Rift(..)
-  , toRift, fromRift, grift
-  , composeRift, decomposeRift
-  , adjointToRift, riftToAdjoint
-  , composedAdjointToRift, riftToComposedAdjoint
-  , rap
-  -- * Left Kan lifts
-  , Lift(..)
-  , toLift, fromLift, glift
-  , composeLift, decomposeLift
-  , adjointToLift, liftToAdjoint
-  , liftToComposedAdjoint, composedAdjointToLift
-  ) where
-
-import Control.Applicative
-import Data.Copointed
-import Data.Functor.Adjunction
-import Data.Functor.Composition
-import Data.Functor.Compose
-import Data.Functor.Identity
-import Data.Pointed
-
--- * Right Kan Lift
-
--- |
---
--- @g . 'Rift' g f => f@
---
--- This could alternately be defined directly from the (co)universal propertly
--- in which case, we'd get 'toRift' = 'UniversalRift', but then the usage would
--- suffer.
---
--- @
--- data 'UniversalRift' g f a = forall z. 'Functor' z =>
---      'UniversalRift' (forall x. g (z x) -> f x) (z a)
--- @
---
--- We can witness the isomorphism between Rift and UniversalRift using:
---
--- @
--- riftIso1 :: Functor g => UniversalRift g f a -> Rift g f a
--- riftIso1 (UniversalRift h z) = Rift $ \g -> h $ fmap (\k -> k <$> z) g
--- @
---
--- @
--- riftIso2 :: Rift g f a -> UniversalRift g f a
--- riftIso2 (Rift e) = UniversalRift e id
--- @
---
--- @
--- riftIso1 (riftIso2 (Rift h)) =
--- riftIso1 (UniversalRift h id) =          -- by definition
--- Rift $ \g -> h $ fmap (\k -> k <$> id) g -- by definition
--- Rift $ \g -> h $ fmap id g               -- <$> = (.) and (.id)
--- Rift $ \g -> h g                         -- by functor law
--- Rift h                                   -- eta reduction
--- @
---
--- The other direction is left as an exercise for the reader.
---
--- There are several monads that we can form from @Rift@.
---
--- When @g@ is corepresentable (e.g. is a right adjoint) then there exists @x@ such that @g ~ (->) x@, then it follows that
---
--- @
--- Rift g g a ~
--- forall r. (x -> a -> r) -> x -> r ~
--- forall r. (a -> x -> r) -> x -> r ~
--- forall r. (a -> g r) -> g r ~
--- Codensity g r
--- @
---
--- When @f@ is a left adjoint, so that @f -| g@ then
---
--- @
--- Rift f f a ~
--- forall r. f (a -> r) -> f r ~
--- forall r. (a -> r) -> g (f r) ~
--- forall r. (a -> r) -> Adjoint f g r ~
--- Yoneda (Adjoint f g r)
--- @
---
--- An alternative way to view that is to note that whenever @f@ is a left adjoint then @f -| 'Rift' f 'Identity'@, and since @'Rift' f f@ is isomorphic to @'Rift' f 'Identity' (f a)@, this is the 'Monad' formed by the adjunction.
---
--- @'Rift' w f ~ 'Control.Monad.Co.CoT' w f@ can be a 'Monad' for any 'Comonad' @w@.
---
--- @'Rift' 'Identity' m@ can be a 'Monad' for any 'Monad' @m@, as it is isomorphic to @'Yoneda' m@.
-
-newtype Rift g h a =
-  Rift { runRift :: forall r. g (a -> r) -> h r }
-
-instance Functor g => Functor (Rift g h) where
-  fmap f (Rift g) = Rift (g . fmap (.f))
-  {-# INLINE fmap #-}
-
-instance (Functor g, g ~ h) => Pointed (Rift g h) where
-  point a = Rift (fmap ($a))
-  {-# INLINE point #-}
-
-instance (Functor g, g ~ h) => Applicative (Rift g h) where
-  pure a = Rift (fmap ($a))
-  {-# INLINE pure #-}
-  Rift mf <*> Rift ma = Rift (ma . mf . fmap (.))
-  {-# INLINE (<*>) #-}
-
--- | Indexed applicative composition of right Kan lifts.
-rap :: Functor f => Rift f g (a -> b) -> Rift g h a -> Rift f h b
-rap (Rift mf) (Rift ma) = Rift (ma . mf . fmap (.))
-{-# INLINE rap #-}
-
-grift :: Adjunction f u => f (Rift f k a) -> k a
-grift = rightAdjunct (\r -> leftAdjunct (runRift r) id)
-{-# INLINE grift #-}
-
--- | The universal property of 'Rift'
-toRift :: (Functor g, Functor k) => (forall x. g (k x) -> h x) -> k a -> Rift g h a
-toRift h z = Rift $ \g -> h $ fmap (<$> z) g
-{-# INLINE toRift #-}
-
--- |
--- When @f -| u@, then @f -| Rift f Identity@ and
---
--- @
--- 'toRift' . 'fromRift' ≡ 'id'
--- 'fromRift' . 'toRift' ≡ 'id'
--- @
-fromRift :: Adjunction f u => (forall a. k a -> Rift f h a) -> f (k b) -> h b
-fromRift f = grift . fmap f
-{-# INLINE fromRift #-}
-
--- | @Rift f Identity a@ is isomorphic to the right adjoint to @f@ if one exists.
---
--- @
--- 'adjointToRift' . 'riftToAdjoint' ≡ 'id'
--- 'riftToAdjoint' . 'adjointToRift' ≡ 'id'
--- @
-adjointToRift :: Adjunction f u => u a -> Rift f Identity a
-adjointToRift ua = Rift (Identity . rightAdjunct (<$> ua))
-{-# INLINE adjointToRift #-}
-
--- | @Rift f Identity a@ is isomorphic to the right adjoint to @f@ if one exists.
-riftToAdjoint :: Adjunction f u => Rift f Identity a -> u a
-riftToAdjoint (Rift m) = leftAdjunct (runIdentity . m) id
-{-# INLINE riftToAdjoint #-}
-
--- |
---
--- @
--- 'composeRift' . 'decomposeRift' ≡ 'id'
--- 'decomposeRift' . 'composeRift' ≡ 'id'
--- @
-composeRift :: (Composition compose, Adjunction g u) => Rift f (Rift g h) a -> Rift (compose g f) h a
-composeRift (Rift f) = Rift (grift . fmap f . decompose)
-{-# INLINE composeRift #-}
-
-decomposeRift :: (Composition compose, Functor f, Functor g) => Rift (compose g f) h a -> Rift f (Rift g h) a
-decomposeRift (Rift f) = Rift $ \far -> Rift (f . compose . fmap (\rs -> fmap (rs.) far))
-{-# INLINE decomposeRift #-}
-
-
--- |
--- | @Rift f h a@ is isomorphic to the post-composition of the right adjoint of @f@ onto @h@ if such a right adjoint exists.
---
--- @
--- 'riftToComposedAdjoint' . 'composedAdjointToRift' ≡ 'id'
--- 'composedAdjointToRift' . 'riftToComposedAdjoint' ≡ 'id'
--- @
-
-riftToComposedAdjoint :: Adjunction f u => Rift f h a -> u (h a)
-riftToComposedAdjoint (Rift m) = leftAdjunct m id
-{-# INLINE riftToComposedAdjoint #-}
-
--- | @Rift f h a@ is isomorphic to the post-composition of the right adjoint of @f@ onto @h@ if such a right adjoint exists.
-composedAdjointToRift :: (Functor h, Adjunction f u) => u (h a) -> Rift f h a
-composedAdjointToRift uha = Rift $ rightAdjunct (\b -> fmap b <$> uha)
-{-# INLINE composedAdjointToRift #-}
-
--- * Left Kan Lift
-
--- |
--- > f => g . Lift g f
--- > (forall z. f => g . z) -> Lift g f => z -- couniversal
---
--- Here we use the universal property directly as how we extract from our definition of 'Lift'.
-newtype Lift g f a = Lift { runLift :: forall z. Functor z => (forall x. f x -> g (z x)) -> z a }
-
-instance Functor (Lift g h) where
-  fmap f (Lift g) = Lift (fmap f . g)
-  {-# INLINE fmap #-}
-
-instance (Functor g, g ~ h) => Copointed (Lift g h) where
-  copoint x = runIdentity (runLift x (fmap Identity))
-  {-# INLINE copoint #-}
-
--- |
---
--- @f => g ('Lift' g f a)@
-glift :: Adjunction l g => k a -> g (Lift g k a)
-glift = leftAdjunct (\lka -> Lift (\k2gz -> rightAdjunct k2gz lka))
-{-# INLINE glift #-}
-
--- | The universal property of 'Lift'
-toLift :: Functor z => (forall a. f a -> g (z a)) -> Lift g f b -> z b
-toLift = flip runLift
-{-# INLINE toLift #-}
-
--- toLift decompose :: Compose f => Lift g (compose g f) a -> f a
-
--- | When the adjunction exists
---
--- @
--- 'fromLift' . 'toLift' ≡ 'id'
--- 'toLift' . 'fromLift' ≡ 'id'
--- @
-fromLift :: Adjunction l u => (forall a. Lift u f a -> z a) -> f b -> u (z b)
-fromLift f = fmap f . glift
-{-# INLINE fromLift #-}
-
--- |
---
--- @
--- 'composeLift' . 'decomposeLift' = 'id'
--- 'decomposeLift' . 'composeLift' = 'id'
--- @
-composeLift :: (Composition compose, Functor f, Functor g) => Lift f (Lift g h) a -> Lift (compose g f) h a
-composeLift (Lift m) = Lift $ \h -> m $ decompose . toLift (fmap Compose . decompose . h)
-{-# INLINE composeLift #-}
-
-decomposeLift :: (Composition compose, Adjunction l g) => Lift (compose g f) h a -> Lift f (Lift g h) a
-decomposeLift (Lift m) = Lift $ \h -> m (compose . fmap h . glift)
-{-# INLINE decomposeLift #-}
-
--- | @Lift u Identity a@ is isomorphic to the left adjoint to @u@ if one exists.
---
--- @
--- 'adjointToLift' . 'liftToAdjoint' ≡ 'id'
--- 'liftToAdjoint' . 'adjointToLift' ≡ 'id'
--- @
-adjointToLift :: Adjunction f u => f a -> Lift u Identity a
-adjointToLift fa = Lift $ \k -> rightAdjunct (k . Identity) fa
-{-# INLINE adjointToLift #-}
-
--- | @Lift u Identity a@ is isomorphic to the left adjoint to @u@ if one exists.
-liftToAdjoint :: Adjunction f u => Lift u Identity a -> f a
-liftToAdjoint = toLift (unit . runIdentity)
-{-# INLINE liftToAdjoint #-}
-
--- | @Lift u h a@ is isomorphic to the post-composition of the left adjoint of @u@ onto @h@ if such a left adjoint exists.
---
--- @
--- 'liftToComposedAdjoint' . 'composedAdjointToLift' ≡ 'id'
--- 'composedAdjointToLift' . 'liftToComposedAdjoint' ≡ 'id'
--- @
-liftToComposedAdjoint :: (Adjunction f u, Functor h) => Lift u h a -> f (h a)
-liftToComposedAdjoint (Lift m) = decompose $ m (leftAdjunct Compose)
-{-# INLINE liftToComposedAdjoint #-}
-
--- | @Lift u h a@ is isomorphic to the post-composition of the left adjoint of @u@ onto @h@ if such a left adjoint exists.
-composedAdjointToLift :: Adjunction f u => f (h a) -> Lift u h a
-composedAdjointToLift = rightAdjunct glift
-{-# INLINE composedAdjointToLift #-}
diff --git a/src/Data/Functor/Yoneda.hs b/src/Data/Functor/Yoneda.hs
--- a/src/Data/Functor/Yoneda.hs
+++ b/src/Data/Functor/Yoneda.hs
@@ -5,13 +5,20 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Functor.Yoneda
--- Copyright   :  (C) 2011 Edward Kmett
+-- Copyright   :  (C) 2011-2013 Edward Kmett
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
 -- Stability   :  provisional
 -- Portability :  MPTCs, fundeps
 --
+-- The co-Yoneda lemma states that
+--
+-- @f a@ is isomorphic to @(forall r. (a -> r) -> f a)@
+--
+-- This is described in a rather intuitive fashion by Dan Piponi in
+--
+-- <http://blog.sigfpe.com/2006/11/yoneda-lemma.html>
 ----------------------------------------------------------------------------
 
 module Data.Functor.Yoneda
diff --git a/src/Data/Functor/Yoneda/Contravariant.hs b/src/Data/Functor/Yoneda/Contravariant.hs
deleted file mode 100644
--- a/src/Data/Functor/Yoneda/Contravariant.hs
+++ /dev/null
@@ -1,171 +0,0 @@
-{-# LANGUAGE CPP, GADTs, FlexibleContexts, MultiParamTypeClasses, UndecidableInstances, TypeFamilies #-}
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
-{-# LANGUAGE Trustworthy #-}
-#endif
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Functor.Yoneda.Contravariant
--- Copyright   :  (C) 2011 Edward Kmett
--- License     :  BSD-style (see the file LICENSE)
---
--- Maintainer  :  Edward Kmett <ekmett@gmail.com>
--- Stability   :  provisional
--- Portability :  GADTs, MPTCs, fundeps
---
-----------------------------------------------------------------------------
-module Data.Functor.Yoneda.Contravariant
-  ( Yoneda(..)
-  , liftYoneda
-  , lowerYoneda
-  , lowerM
-  ) where
-
-import Control.Applicative
-import Control.Monad (MonadPlus(..), liftM)
-import Control.Monad.Fix
-import Control.Monad.Trans.Class
-import Control.Comonad
-import Control.Comonad.Trans.Class
-import Data.Distributive
-import Data.Function (on)
-import Data.Functor.Bind
-import Data.Functor.Extend
-import Data.Functor.Plus
-import Data.Functor.Adjunction
-import Data.Functor.Representable
-import Data.Key
-import Data.Foldable
-import Data.Traversable
-import Data.Semigroup.Foldable
-import Data.Semigroup.Traversable
-import Prelude hiding (sequence, lookup, zipWith)
-import Text.Read hiding (lift)
-
--- | The contravariant Yoneda lemma applied to a covariant functor
-data Yoneda f a where
-  Yoneda :: (b -> a) -> f b -> Yoneda f a
-
-liftYoneda :: f a -> Yoneda f a 
-liftYoneda = Yoneda id
-
-lowerYoneda :: Functor f => Yoneda f a -> f a
-lowerYoneda (Yoneda f m) = fmap f m
-
-lowerM :: Monad f => Yoneda f a -> f a 
-lowerM (Yoneda f m) = liftM f m
-
-instance Functor (Yoneda f) where
-  fmap f (Yoneda g v) = Yoneda (f . g) v
-
-type instance Key (Yoneda f) = Key f
-
-instance Keyed f => Keyed (Yoneda f) where
-  mapWithKey f (Yoneda k a) = Yoneda id $ mapWithKey (\x -> f x . k) a
-
-instance Apply f => Apply (Yoneda f) where
-  m <.> n = liftYoneda $ lowerYoneda m <.> lowerYoneda n
-
-instance Applicative f => Applicative (Yoneda f) where
-  pure = liftYoneda . pure
-  m <*> n = liftYoneda $ lowerYoneda m <*> lowerYoneda n
-
-instance Zip f => Zip (Yoneda f) where
-  zipWith f m n = liftYoneda $ zipWith f (lowerYoneda m) (lowerYoneda n)
-
-instance ZipWithKey f => ZipWithKey (Yoneda f) where
-  zipWithKey f m n = liftYoneda $ zipWithKey f (lowerYoneda m) (lowerYoneda n)
-
-instance Alternative f => Alternative (Yoneda f) where
-  empty = liftYoneda empty 
-  m <|> n = liftYoneda $ lowerYoneda m <|> lowerYoneda n
-
-instance Alt f => Alt (Yoneda f) where
-  m <!> n = liftYoneda $ lowerYoneda m <!> lowerYoneda n
-
-instance Plus f => Plus (Yoneda f) where
-  zero = liftYoneda zero
-
-instance Bind m => Bind (Yoneda m) where
-  Yoneda f v >>- k = liftYoneda (v >>- lowerYoneda . k . f)
-
-instance Monad m => Monad (Yoneda m) where
-  return = Yoneda id . return
-  Yoneda f v >>= k = lift (v >>= lowerM . k . f)
-
-instance MonadTrans Yoneda where
-  lift = Yoneda id
-
-instance MonadFix f => MonadFix (Yoneda f) where
-  mfix f = lift $ mfix (lowerM . f)
-
-instance MonadPlus f => MonadPlus (Yoneda f) where
-  mzero = lift mzero
-  m `mplus` n = lift $ lowerM m `mplus` lowerM n
-
-instance (Functor f, Lookup f) => Lookup (Yoneda f) where
-  lookup k f = lookup k (lowerYoneda f)
-
-instance (Functor f, Indexable f) => Indexable (Yoneda f) where
-  index = index . lowerYoneda
-
-instance Representable f => Representable (Yoneda f) where
-  tabulate = liftYoneda . tabulate
-
-instance Extend w => Extend (Yoneda w) where
-  extended k (Yoneda f v) = Yoneda id $ extended (k . Yoneda f) v
-
-instance Comonad w => Comonad (Yoneda w) where
-  extend k (Yoneda f v) = Yoneda id $ extend (k . Yoneda f) v
-  extract (Yoneda f v) = f (extract v)
-
-instance ComonadTrans Yoneda where
-  lower (Yoneda f a) = fmap f a
-
-instance Foldable f => Foldable (Yoneda f) where
-  foldMap f (Yoneda k a) = foldMap (f . k) a
-
-instance FoldableWithKey f => FoldableWithKey (Yoneda f) where
-  foldMapWithKey f (Yoneda k a) = foldMapWithKey (\x -> f x . k) a
-
-instance Foldable1 f => Foldable1 (Yoneda f) where
-  foldMap1 f (Yoneda k a) = foldMap1 (f . k) a
-
-instance FoldableWithKey1 f => FoldableWithKey1 (Yoneda f) where
-  foldMapWithKey1 f (Yoneda k a) = foldMapWithKey1 (\x -> f x . k) a
-
-instance Traversable f => Traversable (Yoneda f) where
-  traverse f (Yoneda k a) = Yoneda id <$> traverse (f . k) a
-
-instance Traversable1 f => Traversable1 (Yoneda f) where
-  traverse1 f (Yoneda k a) = Yoneda id <$> traverse1 (f . k) a
-
-instance TraversableWithKey f => TraversableWithKey (Yoneda f) where
-  traverseWithKey f (Yoneda k a) = Yoneda id <$> traverseWithKey (\x -> f x . k) a
-
-instance TraversableWithKey1 f => TraversableWithKey1 (Yoneda f) where
-  traverseWithKey1 f (Yoneda k a) = Yoneda id <$> traverseWithKey1 (\x -> f x . k) a
-
-instance Distributive f => Distributive (Yoneda f) where
-  collect f = liftYoneda . collect (lowerYoneda . f)
-
-instance (Functor f, Show (f a)) => Show (Yoneda f a) where
-  showsPrec d (Yoneda f a) = showParen (d > 10) $
-    showString "liftYoneda " . showsPrec 11 (fmap f a)
-
-#ifdef __GLASGOW_HASKELL__
-instance (Functor f, Read (f a)) => Read (Yoneda f a) where
-  readPrec = parens $ prec 10 $ do
-    Ident "liftYoneda" <- lexP
-    liftYoneda <$> step readPrec
-#endif
-
-instance (Functor f, Eq (f a)) => Eq (Yoneda f a) where
-  (==) = (==) `on` lowerYoneda
-
-instance (Functor f, Ord (f a)) => Ord (Yoneda f a) where
-  compare = compare `on` lowerYoneda
-
-instance Adjunction f g => Adjunction (Yoneda f) (Yoneda g) where
-  unit = liftYoneda . fmap liftYoneda . unit
-  counit = counit . fmap lowerYoneda . lowerYoneda
-
diff --git a/src/Data/Functor/Yoneda/Reduction.hs b/src/Data/Functor/Yoneda/Reduction.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Functor/Yoneda/Reduction.hs
@@ -0,0 +1,220 @@
+{-# LANGUAGE CPP, GADTs, FlexibleContexts, MultiParamTypeClasses, UndecidableInstances, TypeFamilies #-}
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
+{-# LANGUAGE Trustworthy #-}
+#endif
+-----------------------------------------------------------------------------
+-- |
+-- Copyright   :  (C) 2011-2013 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  provisional
+-- Portability :  GADTs, MPTCs, fundeps
+--
+-- Yoneda Reduction:
+--
+-- <http://ncatlab.org/nlab/show/Yoneda+reduction>
+--
+-- @Yoneda f@ is isomorphic to @Lan f Identity@
+----------------------------------------------------------------------------
+module Data.Functor.Yoneda.Reduction
+  ( Yoneda(..)
+  , liftYoneda
+  , lowerYoneda
+  , lowerM
+  ) where
+
+import Control.Applicative
+import Control.Monad (MonadPlus(..), liftM)
+import Control.Monad.Fix
+import Control.Monad.Trans.Class
+import Control.Comonad
+import Control.Comonad.Trans.Class
+import Data.Distributive
+import Data.Function (on)
+import Data.Functor.Bind
+import Data.Functor.Extend
+import Data.Functor.Plus
+import Data.Functor.Adjunction
+import Data.Functor.Representable
+import Data.Key
+import Data.Foldable
+import Data.Traversable
+import Data.Semigroup.Foldable
+import Data.Semigroup.Traversable
+import Prelude hiding (sequence, lookup, zipWith)
+import Text.Read hiding (lift)
+
+-- | A form suitable for Yoneda reduction
+data Yoneda f a where
+  Yoneda :: (b -> a) -> f b -> Yoneda f a
+
+-- | Yoneda "expansion"
+liftYoneda :: f a -> Yoneda f a
+liftYoneda = Yoneda id
+{-# INLINE liftYoneda #-}
+
+-- | Yoneda reduction
+lowerYoneda :: Functor f => Yoneda f a -> f a
+lowerYoneda (Yoneda f m) = fmap f m
+{-# INLINE lowerYoneda #-}
+
+-- | Yoneda reduction given a 'Monad'.
+lowerM :: Monad f => Yoneda f a -> f a
+lowerM (Yoneda f m) = liftM f m
+{-# INLINE lowerM #-}
+
+instance Functor (Yoneda f) where
+  fmap f (Yoneda g v) = Yoneda (f . g) v
+  {-# INLINE fmap #-}
+
+type instance Key (Yoneda f) = Key f
+
+instance Keyed f => Keyed (Yoneda f) where
+  mapWithKey f (Yoneda k a) = Yoneda id $ mapWithKey (\x -> f x . k) a
+  {-# INLINE mapWithKey #-}
+
+instance Apply f => Apply (Yoneda f) where
+  m <.> n = liftYoneda $ lowerYoneda m <.> lowerYoneda n
+  {-# INLINE (<.>) #-}
+
+instance Applicative f => Applicative (Yoneda f) where
+  pure = liftYoneda . pure
+  {-# INLINE pure #-}
+  m <*> n = liftYoneda $ lowerYoneda m <*> lowerYoneda n
+  {-# INLINE (<*>) #-}
+
+instance Zip f => Zip (Yoneda f) where
+  zipWith f m n = liftYoneda $ zipWith f (lowerYoneda m) (lowerYoneda n)
+  {-# INLINE zipWith #-}
+
+instance ZipWithKey f => ZipWithKey (Yoneda f) where
+  zipWithKey f m n = liftYoneda $ zipWithKey f (lowerYoneda m) (lowerYoneda n)
+  {-# INLINE zipWithKey #-}
+
+instance Alternative f => Alternative (Yoneda f) where
+  empty = liftYoneda empty
+  {-# INLINE empty #-}
+  m <|> n = liftYoneda $ lowerYoneda m <|> lowerYoneda n
+  {-# INLINE (<|>) #-}
+
+instance Alt f => Alt (Yoneda f) where
+  m <!> n = liftYoneda $ lowerYoneda m <!> lowerYoneda n
+  {-# INLINE (<!>) #-}
+
+instance Plus f => Plus (Yoneda f) where
+  zero = liftYoneda zero
+  {-# INLINE zero #-}
+
+instance Bind m => Bind (Yoneda m) where
+  Yoneda f v >>- k = liftYoneda (v >>- lowerYoneda . k . f)
+  {-# INLINE (>>-) #-}
+
+instance Monad m => Monad (Yoneda m) where
+  return = Yoneda id . return
+  {-# INLINE return #-}
+  Yoneda f v >>= k = lift (v >>= lowerM . k . f)
+  {-# INLINE (>>=) #-}
+
+instance MonadTrans Yoneda where
+  lift = Yoneda id
+  {-# INLINE lift #-}
+
+instance MonadFix f => MonadFix (Yoneda f) where
+  mfix f = lift $ mfix (lowerM . f)
+  {-# INLINE mfix #-}
+
+instance MonadPlus f => MonadPlus (Yoneda f) where
+  mzero = lift mzero
+  {-# INLINE mzero #-}
+  m `mplus` n = lift $ lowerM m `mplus` lowerM n
+  {-# INLINE mplus #-}
+
+instance (Functor f, Lookup f) => Lookup (Yoneda f) where
+  lookup k f = lookup k (lowerYoneda f)
+  {-# INLINE lookup #-}
+
+instance (Functor f, Indexable f) => Indexable (Yoneda f) where
+  index = index . lowerYoneda
+  {-# INLINE index #-}
+
+instance Representable f => Representable (Yoneda f) where
+  tabulate = liftYoneda . tabulate
+  {-# INLINE tabulate #-}
+
+instance Extend w => Extend (Yoneda w) where
+  extended k (Yoneda f v) = Yoneda id $ extended (k . Yoneda f) v
+  {-# INLINE extended #-}
+
+instance Comonad w => Comonad (Yoneda w) where
+  extend k (Yoneda f v) = Yoneda id $ extend (k . Yoneda f) v
+  {-# INLINE extend #-}
+  extract (Yoneda f v) = f (extract v)
+  {-# INLINE extract #-}
+
+instance ComonadTrans Yoneda where
+  lower (Yoneda f a) = fmap f a
+  {-# INLINE lower #-}
+
+instance Foldable f => Foldable (Yoneda f) where
+  foldMap f (Yoneda k a) = foldMap (f . k) a
+  {-# INLINE foldMap #-}
+
+instance FoldableWithKey f => FoldableWithKey (Yoneda f) where
+  foldMapWithKey f (Yoneda k a) = foldMapWithKey (\x -> f x . k) a
+  {-# INLINE foldMapWithKey #-}
+
+instance Foldable1 f => Foldable1 (Yoneda f) where
+  foldMap1 f (Yoneda k a) = foldMap1 (f . k) a
+  {-# INLINE foldMap1 #-}
+
+instance FoldableWithKey1 f => FoldableWithKey1 (Yoneda f) where
+  foldMapWithKey1 f (Yoneda k a) = foldMapWithKey1 (\x -> f x . k) a
+  {-# INLINE foldMapWithKey1 #-}
+
+instance Traversable f => Traversable (Yoneda f) where
+  traverse f (Yoneda k a) = Yoneda id <$> traverse (f . k) a
+  {-# INLINE traverse #-}
+
+instance Traversable1 f => Traversable1 (Yoneda f) where
+  traverse1 f (Yoneda k a) = Yoneda id <$> traverse1 (f . k) a
+  {-# INLINE traverse1 #-}
+
+instance TraversableWithKey f => TraversableWithKey (Yoneda f) where
+  traverseWithKey f (Yoneda k a) = Yoneda id <$> traverseWithKey (\x -> f x . k) a
+  {-# INLINE traverseWithKey #-}
+
+instance TraversableWithKey1 f => TraversableWithKey1 (Yoneda f) where
+  traverseWithKey1 f (Yoneda k a) = Yoneda id <$> traverseWithKey1 (\x -> f x . k) a
+  {-# INLINE traverseWithKey1 #-}
+
+instance Distributive f => Distributive (Yoneda f) where
+  collect f = liftYoneda . collect (lowerYoneda . f)
+  {-# INLINE collect #-}
+
+instance (Functor f, Show (f a)) => Show (Yoneda f a) where
+  showsPrec d (Yoneda f a) = showParen (d > 10) $
+    showString "liftYoneda " . showsPrec 11 (fmap f a)
+  {-# INLINE showsPrec #-}
+
+#ifdef __GLASGOW_HASKELL__
+instance (Functor f, Read (f a)) => Read (Yoneda f a) where
+  readPrec = parens $ prec 10 $ do
+    Ident "liftYoneda" <- lexP
+    liftYoneda <$> step readPrec
+  {-# INLINE readPrec #-}
+#endif
+
+instance (Functor f, Eq (f a)) => Eq (Yoneda f a) where
+  (==) = (==) `on` lowerYoneda
+  {-# INLINE (==) #-}
+
+instance (Functor f, Ord (f a)) => Ord (Yoneda f a) where
+  compare = compare `on` lowerYoneda
+  {-# INLINE compare #-}
+
+instance Adjunction f g => Adjunction (Yoneda f) (Yoneda g) where
+  unit = liftYoneda . fmap liftYoneda . unit
+  {-# INLINE unit #-}
+  counit = counit . fmap lowerYoneda . lowerYoneda
+  {-# INLINE counit #-}