diff --git a/Control/MFunctor.hs b/Control/MFunctor.hs
deleted file mode 100644
--- a/Control/MFunctor.hs
+++ /dev/null
@@ -1,90 +0,0 @@
--- | This module temporarily holds this class until it can find a better home.
-
-{-# LANGUAGE Rank2Types #-}
-
-module Control.MFunctor (
-    -- * Functors over Monads
-    MFunctor(..),
-    hoistK,
-    raise,
-    raiseK
-    ) where
-
-import Control.Monad.Trans.Class (MonadTrans(lift))
-import Control.Monad.Trans.Identity (IdentityT, mapIdentityT)
-import Control.Monad.Trans.Maybe (MaybeT, mapMaybeT)
-import Control.Monad.Trans.Reader (ReaderT, mapReaderT)
-import Control.Monad.Trans.RWS (RWST, mapRWST)
-import qualified Control.Monad.Trans.State.Strict as StateStrict
-import qualified Control.Monad.Trans.State.Lazy   as StateLazy 
-import qualified Control.Monad.Trans.Writer.Strict as WriterStrict
-import qualified Control.Monad.Trans.Writer.Lazy   as WriterLazy
-
-{- | A functor in the category of monads
-
-> hoist f . hoist g = hoist (f . g)
->
-> hoist id = id
-
-    If @f@ is a monad morphism, then @hoist f@ is a monad morphism, meaning that
-    @hoistK f = (hoist f .)@ defines a functor between Kleisli categories:
-
-> hoistK f k1 >=> hoistK f k2 = hoistK f (k1 >=> k2)
->
-> hoistK f return = return
--}
-class MFunctor t where
-    {-| Lift a monad morphism from @m@ to @n@ into a monad morphism from
-        @(t m)@ to @(t n)@ -}
-    hoist
-     :: (Monad m)
-     => (forall a . m a -> n a)  -- ^ Monad morphism
-     -> t m b -> t n b
-
-instance MFunctor IdentityT where
-    hoist nat = mapIdentityT nat
-
-instance MFunctor MaybeT where
-    hoist nat = mapMaybeT nat
-
-instance MFunctor (ReaderT r) where
-    hoist nat = mapReaderT nat
-
-instance MFunctor (RWST r w s) where
-    hoist nat = mapRWST nat
-
-instance MFunctor (StateStrict.StateT s) where
-    hoist nat = StateStrict.mapStateT nat
-
-instance MFunctor (StateLazy.StateT s) where
-    hoist nat = StateLazy.mapStateT nat
-
-instance MFunctor (WriterStrict.WriterT w) where
-    hoist nat = WriterStrict.mapWriterT nat
-
-instance MFunctor (WriterLazy.WriterT w) where
-    hoist nat = WriterLazy.mapWriterT nat
-
--- | Convenience function equivalent to @(hoist f .)@
-hoistK
- :: (Monad m, MFunctor t)
- => (forall a . m a -> n a)  -- ^ Monad morphism
- -> (b' -> t m b)            -- ^ Kleisli arrow
- -> (b' -> t n b)
-hoistK k p a' = hoist k (p a')
--- hoistK k = (hoist k .)
-
-{-| Lift the base monad
-
-> raise = hoist lift
--}
-raise :: (Monad m, MFunctor t1, MonadTrans t2) => t1 m r -> t1 (t2 m) r
-raise = hoist lift
-
-{-| Lift the base monad of a \'@K@\'leisli arrow
-
-> raiseK = hoistK lift
--}
-raiseK
- :: (Monad m, MFunctor t1, MonadTrans t2) => (q -> t1 m r) -> (q -> t1 (t2 m) r)
-raiseK = (hoist lift .)
diff --git a/Control/PFunctor.hs b/Control/PFunctor.hs
deleted file mode 100644
--- a/Control/PFunctor.hs
+++ /dev/null
@@ -1,89 +0,0 @@
--- | This module defines functors in the category of proxies
-
-{-# LANGUAGE KindSignatures, Rank2Types #-}
-
-module Control.PFunctor (
-    -- * Functors over Proxies
-    PFunctor(..),
-    hoistPK,
-    raiseP,
-    raisePK,
-    ) where
-
-import Control.Proxy.Class (Proxy)
-import Control.Proxy.Trans (ProxyTrans(liftP))
-
-{-| A functor in the category of proxies
-
-> hoistP f . hoistP g = hoistP (f . g)
->
-> hoistP id = id
-
-    If @f@ is a proxy morphism, then @hoistP f@ is a proxy morphism, meaning
-    that @hoistPK f = (hoistP f .)@ defines a functor between five categories.
-
-    Functor between Kleisli categories:
-
-> hoistPK f p1 >=> hoistPK f p2 = hoistPK f (p1 >=> p2)
->
-> hoistPK f return = return
-
-    Functor between 'P.Proxy' categories:
-
-> hoistPK f p1 >-> hoistPK f p2 = hoistPK f (p1 >-> p2)
->
-> hoistPK f idT = idT
-
-> hoistPK f p1 >~> hoistPK f p2 = hoistPK f (p1 >~> p2)
->
-> hoistPK f coidT = coidT
-
-    Functor between \"request\" categories:
-
-> hoistPK f p1 \>\ hoistPK f p2 = hoistPK f (p2 \>\ p2)
->
-> hoistPK f request = request
-
-    Functor between \"respond\" categories:
-
-> hoistPK f p1 />/ hoistPK f p2 = hoistPK f (p2 />/ p2)
->
-> hoistPK f respond = respond
--}
-class PFunctor (t
-    :: (* -> * -> * -> * -> (* -> *) -> * -> *)
-    ->  * -> * -> * -> * -> (* -> *) -> * -> * ) where
-    {-| Lift a proxy morphism from @p1@ to @p2@ into a proxy morphism from
-        @(t p1)@ to @(t p2)@ -}
-    hoistP
-     :: (Monad m, Proxy p1)
-     => (forall r1 . p1 a' a b' b m r1 ->   p2 a' a b' b n r1) -- ^ Proxy morphism
-     -> (          t p1 a' a b' b m r2 -> t p2 a' a b' b n r2)
-
--- | Convenience function equivalent to @(hoistP f .)@
-hoistPK
- :: (Monad m, Proxy p1, PFunctor t)
- => (forall r1 . p1 a' a b' b m r1 -> p2 a' a b' b n r1) -- ^ Proxy morphism
- -> (q -> t p1 a' a b' b m r2) -- ^ Proxy Kleisli arrow
- -> (q -> t p2 a' a b' b n r2)
-hoistPK f = (hoistP f .)
-
-{-| Lift the base proxy
-
-> raiseP = hoistP liftP
--}
-raiseP
- :: (Monad m, Proxy p, PFunctor t1, ProxyTrans t2)
- => t1 p a' a b' b m r -- ^ Proxy
- -> t1 (t2 p) a' a b' b m r
-raiseP = hoistP liftP
-
-{-| Lift the base proxy of a \'@K@\'leisli arrow
-
-> raisePK = hoistPK liftP
--}
-raisePK
- :: (Monad m, Proxy p, PFunctor t1, ProxyTrans t2)
- => (q -> t1 p a' a b' b m r) -- ^ Proxy Kleisli arrow
- -> (q -> t1 (t2 p) a' a b' b m r)
-raisePK = hoistPK liftP
diff --git a/Control/Pipe.hs b/Control/Pipe.hs
--- a/Control/Pipe.hs
+++ b/Control/Pipe.hs
@@ -4,8 +4,8 @@
     implementation.
 
     The 'Pipe' type is a monad transformer that enriches the base monad with the
-    ability to 'await' or 'yield' data to and from other 'Pipe's. -}
-
+    ability to 'await' or 'yield' data to and from other 'Pipe's.
+-}
 module Control.Pipe (
     -- * Types
     -- $types
@@ -13,17 +13,20 @@
     Producer,
     Consumer,
     Pipeline,
+
     -- * Create Pipes
     -- $create
     await,
     yield,
     pipe,
+
     -- * Compose Pipes
     -- $category
     (<+<),
     (>+>),
     idP,
     PipeC(..),
+
     -- * Run Pipes
     runPipe
     ) where
@@ -52,17 +55,16 @@
     * @r@ - The type of the return value
 -}
 data Pipe a b m r
-  = Await (a -> Pipe a b m r)
-  | Yield b    (Pipe a b m r)
-  | M       (m (Pipe a b m r))
-  | Pure r
-{-
-Technically, the correct implementation that satisfies the monad transformer
-laws is:
-
-type PipeF a b x = Await (a -> x) | Yield b x deriving (Functor)
+     = Await (a -> Pipe a b m r)
+     | Yield  b   (Pipe a b m r)
+     | M     (m   (Pipe a b m r))
+     | Pure r
+{- Technically, the correct implementation that satisfies the monad transformer
+   laws is:
 
-type Pipe a b = FreeT (PipeF a b)
+> data PipeF a b x = Await (a -> x) | Yield b x deriving (Functor)
+> 
+> type Pipe a b = FreeT (PipeF a b)
 -}
 
 instance (Monad m) => Functor (Pipe a b m) where
@@ -119,24 +121,21 @@
 >     when ok (yield x)
 -}
 
-{-|
-    Wait for input from upstream.
+{-| Wait for input from upstream.
 
     'await' blocks until input is available from upstream.
 -}
 await :: Pipe a b m a
 await = Await Pure
 
-{-|
-    Deliver output downstream.
+{-| Deliver output downstream.
 
     'yield' restores control back upstream and binds its value to 'await'.
 -}
 yield :: b -> Pipe a b m ()
 yield b = Yield b (Pure ())
 
-{-|
-    Convert a pure function into a pipe
+{-| Convert a pure function into a pipe
 
 > pipe f = forever $ do
 >     x <- await
@@ -182,8 +181,8 @@
 (>+>) :: (Monad m) => Pipe a b m r -> Pipe b c m r -> Pipe a c m r
 p2 >+> p1 = p1 <+< p2
 
-infixr 8 <+<
-infixl 8 >+>
+infixr 7 <+<
+infixl 7 >+>
 
 -- | Corresponds to 'id' from @Control.Category@
 idP :: (Monad m) => Pipe a a m r
diff --git a/Control/Proxy.hs b/Control/Proxy.hs
--- a/Control/Proxy.hs
+++ b/Control/Proxy.hs
@@ -1,6 +1,7 @@
 {-| Recommended entry import for this library
 
-    Read "Control.Proxy.Tutorial" for an extended proxy tutorial. -}
+    Read "Control.Proxy.Tutorial" for an extended proxy tutorial.
+-}
 
 module Control.Proxy (
     -- * Modules
diff --git a/Control/Proxy/Class.hs b/Control/Proxy/Class.hs
--- a/Control/Proxy/Class.hs
+++ b/Control/Proxy/Class.hs
@@ -1,42 +1,35 @@
 {-| The 'Proxy' class defines the library's core API.  Everything else in this
-    library builds exclusively on top of the 'Proxy' type class so that all
-    proxy implementations and extensions can share the same standard library.
-
-    Several of these type classes duplicate methods from familiar type-classes
-    (such as ('?>=') duplicating ('>>=')).  You do NOT need to use these
-    duplicate methods.  Instead, read the \"Polymorphic proxies\" section below
-    which explains their purpose and how they help clean up type signatures. -}
+    library builds on top of the 'Proxy' type class so that all proxy
+    implementations and extensions can share the same standard library.
+-}
 
 {-# LANGUAGE Rank2Types #-}
 
 module Control.Proxy.Class (
     -- * Core proxy class
     Proxy(..),
+    (>->),
     idT,
+    (>~>),
     coidT,
+
+    -- ** Flipped operators
     (<-<),
     (<~<),
-
-    -- * request/respond substitution
-    Interact(..),
-    (/</),
-    (\<\),
+    (<<-),
+    (~<<),
 
     -- * Laws
     -- $laws
 
     -- * Polymorphic proxies
     -- $poly
-    MonadPlusP(..),
-    MonadIOP(..)
+    ProxyInternal(..),
+    MonadPlusP(..)
     ) where
 
 import Control.Monad.IO.Class (MonadIO)
 
--- Documentation imports
-import Control.Monad.Trans.Class (lift)
-import Control.MFunctor(hoist)
-
 {- * I make educated guesses about which associativy is most efficient for each
      operator.
    * Keep proxy composition lower in precedence than function composition, which
@@ -46,27 +39,20 @@
 >
 > hoist f . k >-> p
 -}
-infixr 7 <-<
-infixl 7 >->
-infixr 8 /</
-infixl 8 \>\
-infixl 8 \<\
-infixr 8 />/
-infixl 1 ?>= -- This should match the fixity of >>=
-
-{-| The core API for the @pipes@ library
-
-    You should only use 'request', 'respond', and ('>->')
+infixr 7 <-<, ->>
+infixl 7 >->, <<-
+infixr 7 >~>, ~<<
+infixl 7 <~<, >>~
+infixl 1 ?>=  -- This should match the fixity of >>=
 
-    I only provide ('>~>') for theoretical symmetry, and the remaining methods
-    just implement internal type class plumbing.
--}
-class Proxy p where
+-- | The core API for the @pipes@ library
+class (ProxyInternal p) => Proxy p where
     {-| 'request' input from upstream, passing an argument with the request
 
         @request a'@ passes @a'@ as a parameter to upstream that upstream may
         use to decide what response to return.  'request' binds the upstream's
-        response of type @a@ to its own return value. -}
+        response of type @a@ to its own return value.
+    -}
     request :: (Monad m) => a' -> p a' a b' b m a
 
     {-| 'respond' with an output for downstream and bind downstream's next
@@ -74,52 +60,47 @@
           
         @respond b@ satisfies a downstream 'request' by supplying the value @b@.
         'respond' blocks until downstream 'request's a new value and binds the
-        argument of type @b'@ from the next 'request' as its return value. -}
+        argument of type @b'@ from the next 'request' as its return value.
+    -}
     respond :: (Monad m) => b -> p a' a b' b m b'
 
-    {-| Compose two proxies blocked on a 'respond', generating a new proxy
-        blocked on a 'respond'
-
-        Begins from the downstream end and satisfies every 'request' with a
-        'respond' -}
-    (>->)
-     :: (Monad m)
-     => (b' -> p a' a b' b m r)
-     -> (c' -> p b' b c' c m r)
-     -> (c' -> p a' a c' c m r)
+    {-| Connect an upstream 'Proxy' that handles all 'request's
 
-    {-| Compose two proxies blocked on a 'request', generating a new proxy
-        blocked on a 'request'
+        Point-ful version of ('>->')
+    -}
+    (->>)
+        :: (Monad m)
+        => (b'  -> p a' a b' b m r)
+        ->         p b' b c' c m r
+        ->         p a' a c' c m r
 
-        Begins from the upstream end and satisfies every 'respond' with a
-        'request' -}
-    (>~>)
-     :: (Monad m)
-     => (a -> p a' a b' b m r)
-     -> (b -> p b' b c' c m r)
-     -> (a -> p a' a c' c m r)
+    {-| Connect a downstream 'Proxy' that handles all 'respond's
 
-    {-| 'return_P' is identical to 'return', except with a more polymorphic
-        constraint. -}
-    return_P :: (Monad m) => r -> p a' a b' b m r
+        Point-ful version of ('>~>')
+    -}
+    (>>~)
+        :: (Monad m)
+        =>        p a' a b' b m r
+        -> (b  -> p b' b c' c m r)
+        ->        p a' a c' c m r
 
-    {-| ('?>=') is identical to ('>>='), except with a more polymorphic
-        constraint. -}
-    (?>=)
-     :: (Monad m)
-     => p a' a b' b m r -> (r -> p a' a b' b m r') -> p a' a b' b m r'
+{-| Pull-based composition
 
-    {-| 'lift_P' is identical to 'lift', except with a more polymorphic
-        constraint. -}
-    lift_P :: (Monad m) => m r -> p a' a b' b m r
+    Compose two proxies blocked on a 'respond', generating a new proxy blocked
+    on a 'respond'.  Begins from the downstream end and satisfies every
+    'request' with a 'respond'.
+-}
+(>->)
+    :: (Monad m, Proxy p)
+    => (b'  -> p a' a b' b m r)
+    -> (c'_ -> p b' b c' c m r)
+    -> (c'_ -> p a' a c' c m r)
+k1 >-> k2 = \c' -> k1 ->> k2 c'
+{-# INLINABLE (>->) #-}
 
-    {-| 'hoist_P' is identical to 'hoist', except with a more polymorphic
-        constraint. -}
-    hoist_P
-     :: (Monad m)
-     => (forall r . m r  -> n r) -> (p a' a b' b m r' -> p a' a b' b n r')
+{-| Pull-based identity
 
-{-| 'idT' forwards requests followed by responses
+    'idT' forwards requests followed by responses
 
 > idT = request >=> respond >=> idT
 -}
@@ -130,9 +111,26 @@
         respond a  ?>= \a'2 ->
         go a'2
 -- idT = foreverK $ request >=> respond
+{-# INLINABLE idT #-}
 
-{-| 'coidT' forwards responses followed by requests
+{-| Push-based composition
 
+    Compose two proxies blocked on a 'request', generating a new proxy blocked
+    on a 'request'.  Begins from the upstream end and satisfies every 'respond'
+    with a 'request'
+-}
+(>~>)
+    :: (Monad m, Proxy p)
+    => (a_ -> p a' a b' b m r)
+    -> (b  -> p b' b c' c m r)
+    -> (a_ -> p a' a c' c m r)
+k1 >~> k2 = \a -> k1 a >>~ k2
+{-# INLINABLE (>~>) #-}
+
+{-| Push-based identity
+
+    'coidT' forwards responses followed by requests
+
 > coidT = respond >=> request >=> coidT
 -}
 coidT :: (Monad m, Proxy p) => a -> p a' a a' a m r
@@ -142,59 +140,43 @@
         request a' ?>= \a2 ->
         go a2
 -- coidT = foreverK $ respond >=> request
-
-{-| Compose two proxies blocked on a 'respond', generating a new proxy blocked
-    on a 'respond'
+{-# INLINABLE coidT #-}
 
-    Begins from the downstream end and satisfies every 'request' with a
-    'respond' -}
+-- | Equivalent to ('>->') with the arguments flipped
 (<-<)
- :: (Monad m, Proxy p)
- => (c' -> p b' b c' c m r)
- -> (b' -> p a' a b' b m r)
- -> (c' -> p a' a c' c m r)
+    :: (Monad m, Proxy p)
+    => (c' -> p b' b c' c m r)
+    -> (b' -> p a' a b' b m r)
+    -> (c' -> p a' a c' c m r)
 p1 <-< p2 = p2 >-> p1
-
-{-| Compose two proxies blocked on a 'request', generating a new proxy blocked
-    on a 'request'
-
-    Begins from the upstream end and satisfies every 'respond' with a 'request'
+{-# INLINABLE (<-<) #-}
 
-    You don't need to use this.  I include it only for symmetry. -}
+-- | Equivalent to ('>~>') with the arguments flipped
 (<~<)
- :: (Monad m, Proxy p)
- => (b -> p b' b c' c m r)
- -> (a -> p a' a b' b m r)
- -> (a -> p a' a c' c m r)
+    :: (Monad m, Proxy p)
+    => (b -> p b' b c' c m r)
+    -> (a -> p a' a b' b m r)
+    -> (a -> p a' a c' c m r)
 p1 <~< p2 = p2 >~> p1
-
--- | Two extra Proxy categories of theoretical interest
-class Interact p where
-    -- | @f \\>\\ g@ replaces all 'request's in 'g' with 'f'.
-    (\>\) :: (Monad m)
-          => (b' -> p a' a x' x m b)
-          -> (c' -> p b' b x' x m c)
-          -> (c' -> p a' a x' x m c)
-
-    -- | @f \/>\/ g@ replaces all 'respond's in 'f' with 'g'.
-    (/>/) :: (Monad m)
-          => (a -> p x' x b' b m a')
-          -> (b -> p x' x c' c m b')
-          -> (a -> p x' x c' c m a')
+{-# INLINABLE (<~<) #-}
 
--- | @f \/<\/ g@ replaces all 'request's in 'f' with 'g'.
-(/</) :: (Monad m, Interact p)
-      => (c' -> p b' b x' x m c)
-      -> (b' -> p a' a x' x m b)
-      -> (c' -> p a' a x' x m c)
-p1 /</ p2 = p2 \>\ p1
+-- | Equivalent to ('->>') with the arguments flipped
+(<<-)
+    :: (Monad m, Proxy p)
+    =>         p b' b c' c m r
+    -> (b'  -> p a' a b' b m r)
+    ->         p a' a c' c m r
+k <<- p = p ->> k
+{-# INLINABLE (<<-) #-}
 
--- | @f \\<\\ g@ replaces all 'respond's in 'g' with 'f'.
-(\<\) :: (Monad m, Interact p)
-      => (b -> p x' x c' c m b')
-      -> (a -> p x' x b' b m a')
-      -> (a -> p x' x c' c m a')
-p1 \<\ p2 = p2 />/ p1
+-- | Equivalent to ('>>~') with the arguments flipped
+(~<<)
+    :: (Monad m, Proxy p)
+    => (b  -> p b' b c' c m r)
+    ->        p a' a b' b m r
+    ->        p a' a c' c m r
+k ~<< p = p >>~ k
+{-# INLINABLE (~<<) #-}
 
 {- $laws
     The 'Proxy' class defines an interface to all core proxy capabilities that
@@ -216,32 +198,21 @@
     begins from the downstream end, whereas ('>~>') accepts proxies blocked on
     'request' and begins from the upstream end.
 
-    Second, all proxies are monads, defined by:
-
-    * 'return_P'
-
-    * ('?>=')
-
-    These must satify the monad laws using @(>>=) = (?>=)@ and
-    @return = return_P@.
-
-    Third, all proxies are monad transformers, defined by:
-
-    * 'lift_P'
-
-    This must satisfy the monad transformer laws, using @lift = lift_P@.
-
-    Fourth, all proxies are functors in the category of monads, defined by:
+    Second, all proxies are monads and must satify the monad laws using
+    @(>>=) = (?>=)@ and @return = return_P@.
 
-    * 'hoist_P'
+    Third, all proxies are monad transformers and must satisfy the monad
+    transformer laws, using @lift = lift_P@.
 
-    This must satisfy the functor laws, using @hoist = hoist_P@.
+    Fourth, all proxies are functors in the category of monads and must satisfy
+    the functor laws, using @hoist = hoist_P@.
 
-    All 'Proxy' instances must satisfy these additional laws:
+    Fifth, all proxies form two streaming categories:
 
-    * ('>->') and 'idT' form a category:
+    * ('>->') and 'idT' form the \"pull-based\" category:
 
 > Define: idT = request >=> respond >=> idT
+> Define: k1 >-> k2 = \c' -> k1 ->> k2 c'
 >
 > idT >-> p = p
 >
@@ -249,9 +220,10 @@
 >
 > (p1 >-> p2) >-> p3 = p1 >-> (p2 >-> p3)
 
-    * ('>~>') and 'coidT' form a category:
+    * ('>~>') and 'coidT' form the \"push-based\" category:
 
 > Define: coidT = respond >=> request >=> coidT
+> Define: k1 >~> k2 = \a -> k1 a >>~ k2
 >
 > coidT >~> p = p
 >
@@ -282,50 +254,11 @@
 >
 > (liftK f >=> respond >=> p1) >~> (liftK g >=> respond >=> p2)
 >     = liftK (f >=> g) >=> (p1 >-> p2)
-
-    The 'Interact' class exists primarily for theoretical interest and to
-    justify some of the functor laws for the 'ProxyTrans' type class.  You will
-    probably never use it.
-
-    The 'Interact' class defines the ability to:
-    
-    * Replace existing 'request' commands using ('\>\')
-
-    * Replace existing 'respond' commands using ('/>/')
-    
-    Laws:
-
-    * ('\>\') and 'request' form a category:
-
-> request \>\ f = f
->
-> f \>\ request = f
->
-> (f \>\ g) \>\ h = f \>\ (g \>\ h)
-
-    * ('/>/') and 'respond' form a category:
-
-> respond />/ f = f
->
-> f />/ respond = f
->
-> (f />/ g) />/ h = f />/ (g />/ h)
-
-    Additionally, ('\>\') and ('/>/') distribute in one direction over Kleisli
-    composition:
-
-> a \>\ (b >=> c) = (a \>\ b) >=> (a \>\ c)
->
-> a \>\ return = return
-
-> (b >=> c) />/ a = (b />/ a) >=> (c />/ a)
->
-> return />/ a = return
 -}
 
 {- $poly
-    Many of these type classes contain methods which copy methods from more
-    familiar type classes.  These duplicate methods serve two purposes.
+    The 'ProxyInternal' and 'MonadPlusP' type classes duplicate methods from
+    more familiar type classes.  These duplicate methods serve two purposes.
 
     First, this library requires type class instances that would otherwise be
     impossible to define without providing higher-kinded constraints.  Rather
@@ -333,9 +266,9 @@
 
 > instance (forall a' a b' b . MonadTrans (p a' a b' b)) => ...
 
-      ... the instance can instead use the following Haskell98 constraint:
+    ... the instance can instead use the following Haskell98 constraint:
 
-> instance (MonadTransP p) => ...
+> instance (Proxy p) => ...
 
     Second, these type classes don't require the @FlexibleContexts@ extension
     to use and substantially clean up constraints in type signatures.  They
@@ -345,14 +278,15 @@
 
       .. into cleaner and more general constraints like this:
 
-> P :: (Proxy p) => ...
+> p :: (Proxy p) => ...
 
-    These type classes exist solely for internal plumbing and you should never
-    directly use the duplicate methods from them.  Instead, you can use all the
-    original type classes as long as you embed your proxy code within at least
-    one proxy transformer (or 'IdentityP' if don't use any transformers).  The
-    type-class machinery will then automatically convert the messier and less
-    polymorphic constraints to the simpler and more general constraints.
+    'ProxyInternal' and 'MonadPlusP' exist solely for internal type class
+    plumbing and I discourage you from using the methods in these classes
+    unless you enjoy making your code less readable.  Instead, you can use all
+    the original type classes as long as you embed your proxy code within at
+    least one proxy transformer (or 'IdentityP' if don't use any transformers).
+    The type-class machinery will then automatically convert the messier and
+    less polymorphic constraints to the simpler and more general constraints.
 
     For example, consider the following almost-correct definition for @mapMD@
     (from "Control.Proxy.Prelude.Base"):
@@ -423,18 +357,36 @@
 >     respond c
 -}
 
-{-| The @(MonadPlusP p)@ constraint is equivalent to the following constraint:
+{-| The @(ProxyInternal p)@ constraint is (basically) equivalent to the
+    following polymorphic constraint:
 
+> (forall a' a b' b m . (Monad m)
+>     => Monad      (p a' a b' b m)
+>     ,  MonadTrans (p a' a b' b  )
+>     ,  MFunctor   (p a' a b' b m)
+>     ,  MonadIO    (p a' a b' b m)
+>     ) => ...
+-}
+class ProxyInternal p where
+    return_P :: (Monad m) => r -> p a' a b' b m r
+    (?>=)
+        :: (Monad m)
+        => p a' a b' b m r -> (r -> p a' a b' b m r') -> p a' a b' b m r'
+
+    lift_P :: (Monad m) => m r -> p a' a b' b m r
+
+    hoist_P
+        :: (Monad m)
+        => (forall r . m r  -> n r) -> (p a' a b' b m r' -> p a' a b' b n r')
+
+    liftIO_P :: (MonadIO m) => IO r -> p a' a b' b m r
+
+{-| The @(MonadPlusP p)@ constraint is equivalent to the following polymorphic
+    constraint:
+
 > (forall a' a b' b m . (Monad m) => MonadPlus (p a' a b' b m)) => ...
 -}
 class (Proxy p) => MonadPlusP p where
     mzero_P :: (Monad m) => p a' a b' b m r
     mplus_P
-     :: (Monad m) => p a' a b' b m r -> p a' a b' b m r -> p a' a b' b m r
-
-{-| The @(MonadIOP p)@ constraint is equivalent to the following constraint:
-
-> (forall a' a b' b m . (MonadIO m) => MonadIO (p a' a b' b m)) => ...
--}
-class (Proxy p) => MonadIOP p where
-    liftIO_P :: (MonadIO m) => IO r -> p a' a b' b m r
+        :: (Monad m) => p a' a b' b m r -> p a' a b' b m r -> p a' a b' b m r
diff --git a/Control/Proxy/Core.hs b/Control/Proxy/Core.hs
--- a/Control/Proxy/Core.hs
+++ b/Control/Proxy/Core.hs
@@ -8,21 +8,23 @@
     module Control.Proxy.Prelude,
     module Control.Proxy.Trans,
     module Control.Proxy.Trans.Identity,
+    module Control.Proxy.ListT,
+    module Control.Proxy.Morph,
     module Control.Monad,
     module Control.Monad.Trans.Class,
-    module Control.MFunctor,
-    module Control.PFunctor
+    module Control.Monad.Morph,
     ) where
 
-import Control.MFunctor
+import Control.Monad.Morph (MFunctor(hoist))
 import Control.Monad (forever, (>=>), (<=<))
 import Control.Monad.Trans.Class (MonadTrans(lift))
 import Control.Proxy.Class
+import Control.Proxy.ListT
+import Control.Proxy.Morph
 import Control.Proxy.Synonym
 import Control.Proxy.Trans
 import Control.Proxy.Trans.Identity
 import Control.Proxy.Prelude
-import Control.PFunctor
 
 {- $modules
     "Control.Proxy.Class" defines the 'Proxy' type class that lets you program
@@ -39,11 +41,14 @@
     "Control.Proxy.Trans.Identity" exports 'runIdentityP', which substantially
     eases writing completely polymorphic proxies.
 
+    "Control.Proxy.ListT" defines a generalized @ListT@ monad transformer that
+    can interconvert with proxies.
+
+    "Control.Proxy.Morph" exports 'hoistP'.
+
     "Control.Monad" exports 'forever', ('>=>'), and ('<=<').
 
     "Control.Monad.Trans.Class" exports 'lift'.
 
-    "Control.MFunctor" exports 'hoist'.
-
-    "Control.PFunctor" exports 'hoistP'.
+    "Control.Monad.Morph" exports 'hoist'.
 -}
diff --git a/Control/Proxy/Core/Correct.hs b/Control/Proxy/Core/Correct.hs
--- a/Control/Proxy/Core/Correct.hs
+++ b/Control/Proxy/Core/Correct.hs
@@ -4,8 +4,8 @@
 
     However, I advise that you stick to the 'Proxy' type class API rather than
     import this module so that your code works with both 'Proxy' implementations
-    and also works with all proxy transformers. -}
-
+    and also works with all proxy transformers.
+-}
 module Control.Proxy.Core.Correct (
     -- * Types
     ProxyCorrect(..),
@@ -20,10 +20,12 @@
 
 import Control.Applicative (Applicative(pure, (<*>)))
 import Control.Monad.IO.Class (MonadIO(liftIO))
+import Control.Monad.Morph (MFunctor(hoist))
 import Control.Monad.Trans.Class (MonadTrans(lift))
-import Control.MFunctor (MFunctor(hoist))
-import Control.Proxy.Class
-import Control.Proxy.Synonym (C)
+import Control.Proxy.Class (
+    Proxy(request, respond, (->>), (>>~)),
+    ProxyInternal(return_P, (?>=), lift_P, liftIO_P, hoist_P) )
+import Control.Proxy.ListT (ListT((//>), (>\\)))
 
 {-| A 'ProxyCorrect' communicates with an upstream interface and a downstream
     interface.
@@ -41,15 +43,16 @@
 
     * @m     @ - The base monad
 
-    * @r     @ - The final return value -}
+    * @r     @ - The final return value
+-}
 data ProxyCorrect a' a b' b m  r =
     Proxy { unProxy :: m (ProxyF a' a b' b r (ProxyCorrect a' a b' b m r)) }
 
 -- | The base functor for the 'ProxyCorrect' type
 data ProxyF a' a b' b r x
-  = Request a' (a  -> x)
-  | Respond b  (b' -> x)
-  | Pure    r
+    = Request a' (a  -> x)
+    | Respond b  (b' -> x)
+    | Pure    r
 
 instance (Monad m) => Functor (ProxyCorrect a' a b' b m) where
     fmap f p0 = go p0 where
@@ -81,79 +84,65 @@
                 Pure       r   -> unProxy (f r) )
 
 instance MonadTrans (ProxyCorrect a' a b' b) where
-    lift = lift_P
+    lift m = Proxy (m >>= \r -> return (Pure r))
 
+instance MFunctor (ProxyCorrect a' a b' b) where
+    hoist nat p0 = go p0 where
+        go p = Proxy (nat (do
+            x <- unProxy p
+            return (case x of
+                Request a' fa  -> Request a' (\a  -> go (fa  a ))
+                Respond b  fb' -> Respond b  (\b' -> go (fb' b'))
+                Pure       r   -> Pure r )))
+
 instance (MonadIO m) => MonadIO (ProxyCorrect a' a b' b m) where
     liftIO m = Proxy (liftIO (m >>= \r -> return (Pure r)))
- -- liftIO = Proxy . liftIO . liftM Pure
 
-instance MonadIOP ProxyCorrect where
-    liftIO_P = liftIO
-
-instance Proxy ProxyCorrect where
-    fb'_0 >-> fc' = \c' -> fb'_0 >-| fc' c' where
-        fb' >-| p1 = Proxy (do
-            x <- unProxy p1
-            case x of
-                Request b' fb  -> unProxy (fb' b' |-> fb)
-                Respond c  fc' -> return (Respond c (\c' -> fb' >-| fc' c'))
-                Pure       r   -> return (Pure r) )
-        p2 |-> fb = Proxy (do
-            x <- unProxy p2
-            case x of
-                Request a' fa  -> return (Request a' (\a -> fa a |-> fb))
-                Respond b  fb' -> unProxy (fb' >-| fb b)
-                Pure       r   -> return (Pure r) )
+instance ProxyInternal ProxyCorrect where
+    return_P = return
+    (?>=)    = (>>=)
 
-    fa_0 >~> fb_0 = \a -> fa_0 a |-> fb_0 where
-        fb' >-| p1 = Proxy (do
-            x <- unProxy p1
-            case x of
-                Request b' fb  -> unProxy (fb' b' |-> fb)
-                Respond c  fc' -> return (Respond c (\c' -> fb' >-| fc' c'))
-                Pure       r   -> return (Pure r) )
-        p2 |-> fb = Proxy (do
-            x <- unProxy p2
-            case x of
-                Request a' fa  -> return (Request a' (\a -> fa a |-> fb))
-                Respond b  fb' -> unProxy (fb' >-| fb b)
-                Pure       r   -> return (Pure r) )
+    lift_P   = lift
 
-    request a' = Proxy (return (Request a' (\a  -> Proxy (return (Pure a )))))
-    respond b  = Proxy (return (Respond b  (\b' -> Proxy (return (Pure b')))))
+    hoist_P  = hoist
 
-    return_P = return
-    (?>=)   = (>>=)
+    liftIO_P = liftIO
 
-    lift_P m = Proxy (m >>= \r -> return (Pure r))
+instance Proxy ProxyCorrect where
+    fb' ->> p = Proxy (do
+        x <- unProxy p
+        case x of
+            Request b' fb  -> unProxy (fb' b' >>~ fb)
+            Respond c  fc' -> return (Respond c (\c' -> fb' ->> fc' c'))
+            Pure       r   -> return (Pure r) )
+    p >>~ fb = Proxy (do
+        x <- unProxy p
+        case x of
+            Request a' fa  -> return (Request a' (\a -> fa a >>~ fb))
+            Respond b  fb' -> unProxy (fb' ->> fb b)
+            Pure       r   -> return (Pure r) )
 
-    hoist_P = hoist
+    request = \a' -> Proxy (return (Request a' (\a  ->
+        Proxy (return (Pure a )))))
+    respond = \b  -> Proxy (return (Respond b  (\b' ->
+        Proxy (return (Pure b')))))
 
-instance Interact ProxyCorrect where
-    k2 \>\ k1 = \a' -> go (k1 a') where
+instance ListT ProxyCorrect where
+    fb' >\\ p0 = go p0 where
         go p = Proxy (do
             x <- unProxy p
             case x of
-                Request b' fb  -> unProxy (k2 b' >>= \b -> go (fb b))
+                Request b' fb  -> unProxy (fb' b' >>= \b -> go (fb b))
                 Respond x  fx' -> return (Respond x (\x' -> go (fx' x')))
                 Pure       a   -> return (Pure a) )
-    k2 />/ k1 = \a' -> go (k2 a') where
+    p0 //> fb = go p0 where
         go p = Proxy (do
             x <- unProxy p
             case x of
                 Request x' fx  -> return (Request x' (\x -> go (fx x)))
-                Respond b  fb' -> unProxy (k1 b >>= \b' -> go (fb' b'))
+                Respond b  fb' -> unProxy (fb b >>= \b' -> go (fb' b'))
                 Pure       a   -> return (Pure a) )
 
-instance MFunctor (ProxyCorrect a' a b' b) where
-    hoist nat p0 = go p0 where
-        go p = Proxy (nat (do
-            x <- unProxy p
-            return (case x of
-                Request a' fa  -> Request a' (\a  -> go (fa  a ))
-                Respond b  fb' -> Respond b  (\b' -> go (fb' b'))
-                Pure       r   -> Pure r )))
-
 {- $run
     The following commands run self-sufficient proxies, converting them back to
     the base monad.
@@ -163,10 +152,12 @@
 
     Use 'runProxyK' if you are running proxies nested within proxies.  It
     provides a Kleisli arrow as its result that you can pass to another
-    'runProxy' / 'runProxyK' command. -}
+    'runProxy' / 'runProxyK' command.
+-}
 
 {-| Run a self-sufficient 'ProxyCorrect' Kleisli arrow, converting it back to
-    the base monad -}
+    the base monad
+-}
 runProxy :: (Monad m) => (() -> ProxyCorrect a' () () b m r) -> m r
 runProxy k = go (k ()) where
     go p = do
@@ -175,12 +166,16 @@
             Request _ fa  -> go (fa  ())
             Respond _ fb' -> go (fb' ())
             Pure      r   -> return r
+{-# INLINABLE runProxy #-}
 
 {-| Run a self-sufficient 'ProxyCorrect' Kleisli arrow, converting it back to a
-    Kleisli arrow in the base monad -}
+    Kleisli arrow in the base monad
+-}
 runProxyK :: (Monad m) => (() -> ProxyCorrect a' () () b m r) -> (() -> m r)
 runProxyK p = \() -> runProxy p
+{-# INLINABLE runProxyK #-}
 
 -- | Run the 'Pipe' monad transformer, converting it back to the base monad
 runPipe :: (Monad m) => ProxyCorrect a' () () b m r -> m r
 runPipe p = runProxy (\_ -> p)
+{-# INLINABLE runPipe #-}
diff --git a/Control/Proxy/Core/Fast.hs b/Control/Proxy/Core/Fast.hs
--- a/Control/Proxy/Core/Fast.hs
+++ b/Control/Proxy/Core/Fast.hs
@@ -19,11 +19,15 @@
     concrete type and instead you should stick to the 'Proxy' type class API.
     This not only ensures that your code does not violate the monad transformer
     laws, but also guarantees that it works with the other proxy implementations
-    and with any proxy transformers. -}
+    and with any proxy transformers.
+-}
 
 {-# LANGUAGE Trustworthy #-}
-{- The rewrite RULES require the 'TrustWorthy' annotation.  I've supplied the
-   correctness proof for each rewrite rule immediately below each rule. -}
+{- The rewrite RULES require the 'TrustWorthy' annotation.  Their proofs are
+   pretty trivial since they are just inlining the definition of their
+   respective operators.  GHC doesn't do this inlining automatically because the
+   @go@ helper function is recursive.
+-}
 
 module Control.Proxy.Core.Fast (
     -- * Types
@@ -41,10 +45,12 @@
 
 import Control.Applicative (Applicative(pure, (<*>)))
 import Control.Monad.IO.Class (MonadIO(liftIO))
+import Control.Monad.Morph (MFunctor(hoist))
 import Control.Monad.Trans.Class (MonadTrans(lift))
-import Control.MFunctor (MFunctor(hoist))
-import Control.Proxy.Class
-import Control.Proxy.Synonym (C)
+import Control.Proxy.Class (
+    Proxy(request, respond, (->>), (>>~)),
+    ProxyInternal(return_P, (?>=), lift_P, liftIO_P, hoist_P))
+import Control.Proxy.ListT (ListT((//>), (>\\)))
 
 {-| A 'ProxyFast' communicates with an upstream interface and a downstream
     interface.
@@ -61,12 +67,13 @@
 
     * @m     @ - The base monad
 
-    * @r     @ - The final return value -}
+    * @r     @ - The final return value
+-}
 data ProxyFast a' a b' b m r
-  = Request a' (a  -> ProxyFast a' a b' b m r )
-  | Respond b  (b' -> ProxyFast a' a b' b m r )
-  | M          (m    (ProxyFast a' a b' b m r))
-  | Pure    r
+    = Request a' (a  -> ProxyFast a' a b' b m r )
+    | Respond b  (b' -> ProxyFast a' a b' b m r )
+    | M          (m    (ProxyFast a' a b' b m r))
+    | Pure    r
 
 instance (Monad m) => Functor (ProxyFast a' a b' b m) where
     fmap f p0 = go p0 where
@@ -90,141 +97,117 @@
     (>>=)  = _bind
 
 _bind
- :: (Monad m)
- => ProxyFast a' a b' b m r
- -> (r -> ProxyFast a' a b' b m r')
- -> ProxyFast a' a b' b m r'
+    :: (Monad m)
+    => ProxyFast a' a b' b m r
+    -> (r -> ProxyFast a' a b' b m r')
+    -> ProxyFast a' a b' b m r'
 p0 `_bind` f = go p0 where
     go p = case p of
-        Request a' fa  -> Request a' (\a  -> go (fa  a))
+        Request a' fa  -> Request a' (\a  -> go (fa  a ))
         Respond b  fb' -> Respond b  (\b' -> go (fb' b'))
         M          m   -> M (m >>= \p' -> return (go p'))
         Pure       r   -> f r
 
 {-# RULES
-    "_bind (Request a' Pure) f" forall a' f .
-        _bind (Request a' Pure) f = Request a' f;
-    "_bind (Respond b  Pure) f" forall b  f .
-        _bind (Respond b  Pure) f = Respond b  f
+    "_bind (Request a' k) f" forall a' k f .
+        _bind (Request a' k) f = Request a' (\a  -> _bind (k a)  f);
+    "_bind (Respond b  k) f" forall b  k f .
+        _bind (Respond b  k) f = Respond b  (\b' -> _bind (k b') f);
+    "_bind (M          m) f" forall m    f .
+        _bind (M          m) f = M (m >>= \p -> return (_bind p f));
+    "_bind (Pure    r   ) f" forall r    f .
+        _bind (Pure       r) f = f r;
   #-}
-{- Proof that the rewrite rules are Trustworthy:
 
-  _bind (Request a' Pure) f
-= go (Request a' Pure) where
-    go p = case p of
-        Request a' fa  -> Request a' (\a  -> go (fa  a))
-        Respond b  fb' -> Respond b  (\b' -> go (fb' b'))
-        M          m   -> M (m >>= \p' -> return (go p'))
-        Pure       r   -> f r
-= Request a' (\a -> go (Pure a))
-= Request a' (\a -> f a)
-= Request a' f
-
-  _bind (Respond b Pure) f
-= go (Respond b Pure) where
-    go p = case p of
-        Request a' fa  -> Request a' (\a  -> go (fa  a))
-        Respond b  fb' -> Respond b  (\b' -> go (fb' b'))
-        M          m   -> M (m >>= \p' -> return (go p'))
-        Pure       r   -> f r
-= Respond b (\b' -> go (Pure b'))
-= Respond b (\b' -> f b')
-= Respond b f
--}
-
--- | Only satisfies laws modulo 'observe'
+-- | Only satisfies monad transformer laws modulo 'observe'
 instance MonadTrans (ProxyFast a' a b' b) where
-    lift = _lift
-
-_lift :: (Monad m) => m r -> ProxyFast a' a b' b m r
-_lift m = M (m >>= \r -> return (Pure r))
--- _lift = M . liftM Pure
-
-{- These never fire, for some reason, but keep them until I figure out how to
-   get them to work. -}
-{-# RULES
-    "_lift m ?>= f" forall m f .
-        _bind (_lift m) f = M (m >>= \r -> return (f r))
-  #-}
-{- Proof that the rewrite rule is Trustworthy:
+    lift m = M (m >>= \r -> return (Pure r))
 
-  _bind (_lift m) f
-= _bind (M (m >>= \r -> return (Pure r))) f
-= go (M (m >>= \r -> return (Pure r))) where
-    go p = case p of
-        Request a' fa  -> Request a' (\a  -> go (fa  a))
-        Respond b  fb' -> Respond b  (\b' -> go (fb' b'))
-        M          m   -> M (m >>= \p' -> return (go p'))
-        Pure       r   -> f r
-= M ((m >>= \r -> return (Pure r)) >>= \p' -> return (go p'))
-= M (m >>= \r -> (return (Pure r) >>= \p' -> return (go p')))
-= M (m >>= \r -> return (go (Pure r)))
-= M (m >>= \r -> return (f r))
--}
+instance MFunctor (ProxyFast a' a b' b) where
+    hoist nat p0 = go (observe p0) where
+        go p = case p of
+            Request a' fa  -> Request a' (\a  -> go (fa  a ))
+            Respond b  fb' -> Respond b  (\b' -> go (fb' b'))
+            M          m   -> M (nat (m >>= \p' -> return (go p')))
+            Pure       r   -> Pure r
 
 instance (MonadIO m) => MonadIO (ProxyFast a' a b' b m) where
     liftIO m = M (liftIO (m >>= \r -> return (Pure r)))
- -- liftIO = M . liftIO . liftM Pure
 
-instance MonadIOP ProxyFast where
+instance ProxyInternal ProxyFast where
+    return_P = Pure
+    (?>=)    = _bind
+
+    lift_P   = lift
+
     liftIO_P = liftIO
 
-instance Proxy ProxyFast where
-    fb'_0 >-> fc'_0 = \c' -> fb'_0 >-| fc'_0 c' where
-        p1 |-> fb = case p1 of
-            Request a' fa  -> Request a' (\a -> fa a |-> fb)
-            Respond b  fb' -> fb' >-| fb b
-            M          m   -> M (m >>= \p1' -> return (p1' |-> fb))
-            Pure       r   -> Pure r
-        fb' >-| p2 = case p2 of
-            Request b' fb  -> fb' b' |-> fb
-            Respond c  fc' -> Respond c (\c' -> fb' >-| fc' c')
-            M          m   -> M (m >>= \p2' -> return (fb' >-| p2'))
-            Pure       r   -> Pure r
+    hoist_P  = hoist
 
-    fa_0 >~> fb_0 = \a -> fa_0 a |-> fb_0 where
-        p1 |-> fb = case p1 of
-            Request a' fa  -> Request a' (\a -> fa a |-> fb)
-            Respond b  fb' -> fb' >-| fb b
-            M          m   -> M (m >>= \p1' -> return (p1' |-> fb))
-            Pure       r   -> Pure r
-        fb' >-| p2 = case p2 of
-            Request b' fb  -> fb' b' |-> fb
-            Respond c  fc' -> Respond c (\c' -> fb' >-| fc' c')
-            M          m   -> M (m >>= \p2' -> return (fb' >-| p2'))
-            Pure       r   -> Pure r
+instance Proxy ProxyFast where
+    fb' ->> p = case p of
+        Request b' fb  -> fb' b' >>~ fb
+        Respond c  fc' -> Respond c (\c' -> fb' ->> fc' c')
+        M          m   -> M (m >>= \p' -> return (fb' ->> p'))
+        Pure       r   -> Pure r
+    p >>~ fb = case p of
+        Request a' fa  -> Request a' (\a -> fa a >>~ fb)
+        Respond b  fb' -> fb' ->> fb b
+        M          m   -> M (m >>= \p' -> return (p' >>~ fb))
+        Pure       r   -> Pure r
 
-    request a' = Request a' Pure
-    respond b  = Respond b  Pure
+    request = \a' -> Request a' Pure
+    respond = \b  -> Respond b  Pure
 
-    return_P = return
-    (?>=)   = _bind
+instance ListT ProxyFast where
+    (>\\) = _req
+    (//>) = _resp
 
-    lift_P = _lift
+_req
+    :: (Monad m)
+    => (b' -> ProxyFast a' a x' x m b)
+    -> ProxyFast b' b x' x m c
+    -> ProxyFast a' a x' x m c
+fb' `_req` p0 = go p0 where
+    go p = case p of
+        Request b' fb  -> fb' b' >>= \b -> go (fb b)
+        Respond x  fx' -> Respond x (\x' -> go (fx' x'))
+        M          m   -> M (m >>= \p' -> return (go p'))
+        Pure       a   -> Pure a
 
-    hoist_P = hoist
+{-# RULES
+    "_req fb' (Request b' fb )" forall fb' b' fb  .
+        _req fb' (Request b' fb ) = _bind (fb' b') (\b -> _req fb' (fb b));
+    "_req fb' (Respond x  fx')" forall fb' x  fx' .
+        _req fb' (Respond x  fx') = Respond x (\x' -> _req fb' (fx' x'));
+    "_req fb' (M          m  )" forall fb'    m   .
+        _req fb' (M          m  ) = M (m >>= \p' -> return (_req fb' p'));
+    "_req fb' (Pure    a     )" forall fb' a      .
+        _req fb' (Pure    a     ) = Pure a;
+  #-}
 
-instance Interact ProxyFast where
-    k2 \>\ k1 = \a' -> go (k1 a') where
-        go p = case p of
-            Request b' fb  -> k2 b' >>= \b -> go (fb b)
-            Respond x  fx' -> Respond x (\x' -> go (fx' x'))
-            M          m   -> M (m >>= \p' -> return (go p'))
-            Pure       a   -> Pure a
-    k2 />/ k1 = \a' -> go (k2 a') where
-        go p = case p of
-            Request x' fx  -> Request x' (\x -> go (fx x))
-            Respond b  fb' -> k1 b >>= \b' -> go (fb' b')
-            M          m   -> M (m >>= \p' -> return (go p'))
-            Pure       a   -> Pure a
+_resp
+    :: (Monad m)
+    => ProxyFast x' x b' b m a'
+    -> (b -> ProxyFast x' x c' c m b')
+    -> ProxyFast x' x c' c m a'
+p0 `_resp` fb = go p0 where
+    go p = case p of
+        Request x' fx  -> Request x' (\x -> go (fx x))
+        Respond b  fb' -> fb b >>= \b' -> go (fb' b')
+        M          m   -> M (m >>= \p' -> return (go p'))
+        Pure       a   -> Pure a
 
-instance MFunctor (ProxyFast a' a b' b) where
-    hoist nat p0 = go (observe p0) where
-        go p = case p of
-            Request a' fa  -> Request a' (\a  -> go (fa  a ))
-            Respond b  fb' -> Respond b  (\b' -> go (fb' b'))
-            M          m   -> M (nat (m >>= \p' -> return (go p')))
-            Pure       r   -> Pure r
+{-# RULES
+    "_resp (Request x' fx ) fb" forall x' fx  fb .
+        _resp (Request x' fx ) fb = Request x' (\x -> _resp (fx  x) fb);
+    "_resp (Respond b  fb') fb" forall b  fb' fb .
+        _resp (Respond b  fb') fb = _bind (fb b) (\b' -> _resp (fb' b') fb);
+    "_resp (M          m  ) fb" forall    m   fb .
+        _resp (M          m  ) fb = M (m >>= \p' -> return (_resp p' fb));
+    "_resp (Pure    a     ) fb" forall a      fb .
+        _resp (Pure    a     ) fb = Pure a;
+  #-}
 
 {- $run
     The following commands run self-sufficient proxies, converting them back to
@@ -235,10 +218,12 @@
 
     Use 'runProxyK' if you are running proxies nested within proxies.  It
     provides a Kleisli arrow as its result that you can pass to another
-    'runProxy' / 'runProxyK' command. -}
+    'runProxy' / 'runProxyK' command.
+-}
 
 {-| Run a self-sufficient 'ProxyFast' Kleisli arrow, converting it back to the
-    base monad -}
+    base monad
+-}
 runProxy :: (Monad m) => (() -> ProxyFast a' () () b m r) -> m r
 runProxy k = go (k ()) where
     go p = case p of
@@ -246,15 +231,19 @@
         Respond _ fb' -> go (fb' ())
         M         m   -> m >>= go
         Pure      r   -> return r
+{-# INLINABLE runProxy #-}
 
 {-| Run a self-sufficient 'ProxyFast' Kleisli arrow, converting it back to a
-    Kleisli arrow in the base monad -}
+    Kleisli arrow in the base monad
+-}
 runProxyK :: (Monad m) => (() -> ProxyFast a' () () b m r) -> (() -> m r)
 runProxyK p = \() -> runProxy p
+{-# INLINABLE runProxyK #-}
 
 -- | Run the 'Pipe' monad transformer, converting it back to the base monad
 runPipe :: (Monad m) => ProxyFast a' () () b m r -> m r
 runPipe p = runProxy (\_ -> p)
+{-# INLINABLE runPipe #-}
 
 {-| The monad transformer laws are correct when viewed through the 'observe'
     function:
@@ -278,3 +267,4 @@
         Pure       r   -> return (Pure r)
         Request a' fa  -> return (Request a' (\a  -> observe (fa  a )))
         Respond b  fb' -> return (Respond b  (\b' -> observe (fb' b')))
+{-# INLINABLE observe #-}
diff --git a/Control/Proxy/ListT.hs b/Control/Proxy/ListT.hs
new file mode 100644
--- /dev/null
+++ b/Control/Proxy/ListT.hs
@@ -0,0 +1,281 @@
+{-| This module implements \"ListT done right\" in terms of proxies.
+
+    The 'RespondT' monad transformer is the 'ListT' monad transformer over the
+    downstream output type.  Each 'respond' corresponds to an element of the
+    list.  The monad bind operation non-deterministically selects one of the
+    previous 'respond's as input.  The 'RespondT' Kleisli category corresponds
+    to the \"respond\" category of the 'ListT' class.
+
+    Symmetrically, the 'RequestT' monad transformer is the 'ListT' monad
+    transformer over the upstream output type.  Each 'request' corresponds to an
+    element of the list.  The monad bind operation non-deterministically selects
+    one of the previous 'request's as input.  The 'RequestT' Kleisli category
+    corresponds to the \"request\" category of the 'ListT' class.
+
+    Unlike 'ListT' from @transformers@, these monad transformers are correct by
+    construction and always satisfy the monad and monad transformer laws.
+-}
+
+{-# LANGUAGE KindSignatures #-}
+
+module Control.Proxy.ListT (
+    -- * Respond Monad Transformer
+    RespondT(..),
+    runRespondK,
+    ProduceT,
+
+    -- * Request Monad Transformer
+    RequestT(..),
+    runRequestK,
+    CoProduceT,
+
+    -- * ListT
+    ListT(..),
+    (\>\),
+    (/>/),
+
+    -- ** Flipped operators
+    (/</),
+    (\<\),
+    (//<),
+    (<\\)
+
+    -- * Laws
+    -- $laws
+    ) where
+
+import Control.Applicative (Applicative(pure, (<*>)), Alternative(empty, (<|>)))
+import Control.Monad (MonadPlus(mzero, mplus))
+import Control.Monad.IO.Class (MonadIO(liftIO))
+import Control.Monad.Trans.Class (MonadTrans(lift))
+import Control.Proxy.Class (Proxy(request, respond), return_P, (?>=), lift_P)
+import Control.Proxy.Synonym (C)
+import Data.Monoid (Monoid(mempty, mappend))
+
+-- For documentation
+import Control.Monad ((>=>), (<=<))
+
+-- | A monad transformer over a proxy's downstream output
+newtype RespondT (p :: * -> * -> * -> * -> (* -> *) -> * -> *) a' a b' m b =
+    RespondT { runRespondT :: p a' a b' b m b' }
+
+instance (Monad m, ListT p) => Functor (RespondT p a' a b' m) where
+    fmap f p = RespondT (runRespondT p //> \a -> respond (f a))
+
+instance (Monad m, ListT p) => Applicative (RespondT p a' a b' m) where
+    pure a = RespondT (respond a)
+    mf <*> mx = RespondT (
+        runRespondT mf //> \f ->
+        runRespondT mx //> \x ->
+        respond (f x) )
+
+instance (Monad m, ListT p) => Monad (RespondT p a' a b' m) where
+    return a = RespondT (respond a)
+    m >>= f  = RespondT (runRespondT m //> \a -> runRespondT (f a))
+
+instance (ListT p) => MonadTrans (RespondT p a' a b') where
+    lift m = RespondT (lift_P m ?>= \a -> respond a)
+
+instance (MonadIO m, ListT p) => MonadIO (RespondT p a' a b' m) where
+    liftIO m = lift (liftIO m)
+
+instance (Monad m, ListT p, Monoid b')
+       => Alternative (RespondT p a' a b' m) where
+    empty = RespondT (return_P mempty)
+    p1 <|> p2 = RespondT (
+        runRespondT p1 ?>= \r1 ->
+        runRespondT p2 ?>= \r2 ->
+        return_P (mappend r1 r2) )
+
+instance (Monad m, ListT p, Monoid b') => MonadPlus (RespondT p a' a b' m) where
+    mzero = empty
+    mplus = (<|>)
+
+-- | Convert a 'RespondT' \'@K@\'leisli arrow into a proxy
+runRespondK :: (q -> RespondT p a' a b' m b) -> (q -> p a' a b' b m b')
+runRespondK k q = runRespondT (k q)
+{-# INLINABLE runRespondK #-}
+
+-- | 'ProduceT' is isomorphic to \"ListT done right\"
+type ProduceT p = RespondT p C () ()
+
+-- | A monad transformer over a proxy's upstream output
+newtype RequestT (p :: * -> * -> * -> * -> (* -> *) -> * -> *) a b' b m a' =
+    RequestT { runRequestT :: p a' a b' b m a }
+
+instance (Monad m, ListT p) => Functor (RequestT p a b' b m) where
+    fmap f p = RequestT (runRequestT p //< \a -> request (f a))
+
+instance (Monad m, ListT p) => Applicative (RequestT p a b' b m) where
+    pure a = RequestT (request a)
+    mf <*> mx = RequestT (
+        runRequestT mf //< \f ->
+        runRequestT mx //< \x ->
+        request (f x) )
+
+instance (Monad m, ListT p) => Monad (RequestT p a b' b m) where
+    return a = RequestT (request a)
+    m >>= f  = RequestT (runRequestT m //< \a -> runRequestT (f a))
+
+instance (ListT p) => MonadTrans (RequestT p a' a b') where
+    lift m = RequestT (lift_P m ?>= \a -> request a)
+
+instance (MonadIO m, ListT p) => MonadIO (RequestT p a b' b m) where
+    liftIO m = lift (liftIO m)
+
+instance (Monad m, ListT p, Monoid a)
+       => Alternative (RequestT p a b' b m) where
+    empty = RequestT (return_P mempty)
+    p1 <|> p2 = RequestT (
+        runRequestT p1 ?>= \r1 ->
+        runRequestT p2 ?>= \r2 ->
+        return_P (mappend r1 r2) )
+
+instance (Monad m, ListT p, Monoid a) => MonadPlus (RequestT p a b' b m) where
+    mzero = empty
+    mplus = (<|>)
+
+-- | Convert a 'RequestT' \'@K@\'leisli arrow into a proxy
+runRequestK :: (q -> RequestT p a b' b m a') -> (q -> p a' a b' b m a)
+runRequestK k q = runRequestT (k q)
+{-# INLINABLE runRequestK #-}
+
+-- | 'CoProduceT' is isomorphic to \"ListT done right\"
+type CoProduceT p = RequestT p () () C
+
+{- * I make educated guesses about which associativy is most efficient for each
+     operator.
+   * Keep composition lower in precedence than function composition, which
+     is 9 at the time of of this comment, so that users can write things like:
+
+> lift . k />/ p
+>
+> hoist f . k />/ p
+-}
+infixr 8 /</, >\\
+infixl 8 \>\, //<
+infixl 8 \<\, //>
+infixr 8 />/, <\\
+
+-- | The two generalized \"ListT\" categories
+class (Proxy p) => ListT p where
+    {-| @f >\\\\ p@ replaces all 'request's in @p@ with @f@.
+
+        Equivalent to to ('=<<') for 'RequestT'
+
+        Point-ful version of ('\>\')
+    -}
+    (>\\)
+        :: (Monad m)
+        => (b' -> p a' a x' x m b)
+        ->        p b' b x' x m c
+        ->        p a' a x' x m c
+
+    {-| @p \/\/> f@ replaces all 'respond's in @p@ with @f@.
+
+        Equivalent to ('>>=') for 'RespondT'
+
+        Point-ful version of ('/>/')
+    -}
+    (//>)
+        :: (Monad m)
+        =>       p x' x b' b m a'
+        -> (b -> p x' x c' c m b')
+        ->       p x' x c' c m a'
+
+{-| @f \\>\\ g@ replaces all 'request's in 'g' with 'f'.
+
+    Equivalent to ('<=<') for 'RequestT'
+
+    Point-free version of ('>\\')
+-}
+(\>\)
+    :: (Monad m, ListT p)
+    => ( b' -> p a' a x' x m b)
+    -> (_c' -> p b' b x' x m c)
+    -> (_c' -> p a' a x' x m c)
+f \>\ g = \c' -> f >\\ g c'
+{-# INLINABLE (\>\) #-}
+
+{-| @f \/>\/ g@ replaces all 'respond's in 'f' with 'g'.
+
+    Equivalent to ('>=>') for 'RespondT'
+
+    Point-free version of ('//>')
+-}
+(/>/)
+    :: (Monad m, ListT p)
+    => (_a -> p x' x b' b m a')
+    -> ( b -> p x' x c' c m b')
+    -> (_a -> p x' x c' c m a')
+f />/ g = \a -> f a //> g
+{-# INLINABLE (/>/) #-}
+
+-- | Equivalent to ('\>\') with the arguments flipped
+(/</)
+    :: (Monad m, ListT p)
+    => (_c' -> p b' b x' x m c)
+    -> ( b' -> p a' a x' x m b)
+    -> (_c' -> p a' a x' x m c)
+p1 /</ p2 = p2 \>\ p1
+{-# INLINABLE (/</) #-}
+
+-- | Equivalent to ('/>/') with the arguments flipped
+(\<\)
+    :: (Monad m, ListT p)
+    => ( b -> p x' x c' c m b')
+    -> (_a -> p x' x b' b m a')
+    -> (_a -> p x' x c' c m a')
+p1 \<\ p2 = p2 />/ p1
+{-# INLINABLE (\<\) #-}
+
+-- | Equivalent to ('>\\') with the arguments flipped
+(//<)
+    :: (Monad m, ListT p)
+    =>        p b' b x' x m c
+    -> (b' -> p a' a x' x m b)
+    ->        p a' a x' x m c
+p //< f = f >\\ p
+{-# INLINABLE (//<) #-}
+
+-- | Equivalent to ('//>') with the arguments flipped
+(<\\)
+    :: (Monad m, ListT p)
+    => (b -> p x' x c' c m b')
+    ->       p x' x b' b m a'
+    ->       p x' x c' c m a'
+f <\\ p = p //> f
+{-# INLINABLE (<\\) #-}
+
+{- $laws
+    The 'ListT' class defines the ability to:
+    
+    * Replace existing 'request' commands using ('\>\')
+
+    * Replace existing 'respond' commands using ('/>/')
+    
+    Laws:
+
+    * ('/>/') and 'respond' form a ListT Kleisli category:
+
+> return = respond
+>
+> (>=>) = (//>)
+
+    * ('\>\') and 'request' also form a ListT Kleisli category:
+
+> return = request
+>
+> (>>=) = (//<)
+
+    Additionally, ('\>\') and ('/>/') both define functors between Proxy Kleisli
+    categories:
+
+> a \>\ (b >=> c) = (a \>\ b) >=> (a \>\ c)
+>
+> a \>\ return = return
+
+> (b >=> c) />/ a = (b />/ a) >=> (c />/ a)
+>
+> return />/ a = return
+-}
diff --git a/Control/Proxy/Morph.hs b/Control/Proxy/Morph.hs
new file mode 100644
--- /dev/null
+++ b/Control/Proxy/Morph.hs
@@ -0,0 +1,117 @@
+{-| A proxy morphism is a natural transformation:
+
+> morph :: forall r . p a' a b' b m r -> q a' a b' b n r
+
+    ... that defines a functor between five categories:
+
+    * Functor between Kleisli categories:
+
+> morph p1 >=> morph p2 = morph (p1 >=> p2)
+>
+> morph return = return
+
+    * Functor between 'P.Proxy' composition categories:
+
+> morph p1 >-> morph p2 = morph (p1 >-> p2)
+>
+> morph idT = idT
+
+> morph p1 >~> morph p2 = morph (p1 >~> p2)
+>
+> morph coidT = coidT
+
+    * Functor between 'ListT' Kleisli categories:
+
+> morph p1 \>\ morph p2 = morph (p2 \>\ p2)
+>
+> morph request = request
+
+> morph p1 />/ morph p2 = morph (p2 />/ p2)
+>
+> morph respond = respond
+
+    Examples of proxy morphisms include:
+
+    * 'liftP' (from 'ProxyTrans')
+
+    * 'squashP' (See below)
+
+    * @'hoistP' f@ (See below) if @f@ is a proxy morphism
+
+    * @(f . g)@, if @f@ and @g@ are both proxy morphisms
+
+    * 'id'
+
+    Proxy morphisms commonly arise when manipulating existing proxy transformer
+    code for compatibility purposes.  The 'PFUnctor', 'ProxyTrans', and 'PMonad'
+    classes define standard ways to change proxy transformer stacks:
+
+    * 'liftP' introduces a new proxy transformer layer of any type:.
+
+    * 'squashP' flattens two identical monad transformer layers into a single
+      layer of the same type.
+
+    * 'hoistP' maps proxy morphisms to modify deeper layers of the proxy
+      transformer stack.
+-}
+
+{-# LANGUAGE KindSignatures, Rank2Types #-}
+
+module Control.Proxy.Morph (
+    -- * Functors over Proxies
+    PFunctor(..),
+
+    -- * Monads over Proxies
+    PMonad(..),
+    squashP
+    ) where
+
+import Control.Proxy.Class (Proxy)
+import Control.Proxy.Trans (ProxyTrans(liftP))
+
+{-| A functor in the category of proxies, using 'hoistP' as the analog of
+    'fmap':
+
+> hoistP f . hoistP g = hoistP (f . g)
+>
+> hoistP id = id
+-}
+class PFunctor (t
+    :: (* -> * -> * -> * -> (* -> *) -> * -> *)
+    ->  * -> * -> * -> * -> (* -> *) -> * -> * ) where
+    {-| Lift a proxy morphism from @p1@ to @p2@ into a proxy morphism from
+        @(t p1)@ to @(t p2)@
+    -}
+    hoistP
+        :: (Monad m, Proxy p1)
+        => (forall r1 . p1 a' a b' b m r1 ->   p2 a' a b' b n r1) -- ^ Proxy morphism
+        -> (          t p1 a' a b' b m r2 -> t p2 a' a b' b n r2)
+
+{-| A monad in the category of monads, using 'liftP' from 'ProxyTrans' as the
+    analog of 'return' and 'embedP' as the analog of ('=<<'):
+
+> embedP liftP = id
+>
+> embedP f (liftP p) = f p
+>
+> embed g (embed f t) = embed (\p -> embed g (f p)) t
+-}
+class (PFunctor t, ProxyTrans t) => PMonad t where
+    {-| Embed a newly created 'PMonad' layer within an existing layer
+
+        'embedP' is analogous to ('=<<')
+    -}
+    embedP
+        :: (Monad n, Proxy p2)
+        => (forall r1 . p1 a' a b' b m r1 -> t p2 a' a b' b n r1)
+        -> (          t p1 a' a b' b m r2 -> t p2 a' a b' b n r2)
+
+{-| Squash to 'PMonad' layers into a single layer
+
+    'squashP' is analogous to 'join'
+-}
+squashP
+    :: (Monad m, Proxy p, PMonad t)
+    => t (t p) a' a b' b m r -> t p a' a b' b m r
+squashP = embedP id
+{-# INLINABLE squashP #-}
diff --git a/Control/Proxy/Pipe.hs b/Control/Proxy/Pipe.hs
--- a/Control/Proxy/Pipe.hs
+++ b/Control/Proxy/Pipe.hs
@@ -3,8 +3,8 @@
 
     This module differs slightly from "Control.Pipe" in order to promote
     seamless interoperability with both pipes and proxies.  See the \"Upgrade
-    Pipes to Proxies\" section below for details. -}
-
+    Pipes to Proxies\" section below for details.
+-}
 {-# LANGUAGE KindSignatures #-}
 
 module Control.Proxy.Pipe (
@@ -29,52 +29,65 @@
     ) where
 
 import Control.Monad (forever)
-import Control.Proxy.Class (Proxy(request, respond, (>->), (?>=)))
+import Control.Proxy.Class (Proxy, respond, request, (->>))
 import Control.Proxy.Synonym (Pipe, Consumer, Producer, C)
 import Control.Proxy.Trans.Identity (runIdentityP)
 
 {-| Wait for input from upstream
 
-    'await' blocks until input is available from upstream. -}
+    'await' blocks until input is available from upstream.
+-}
 await :: (Monad m, Proxy p) => Pipe p a b m a
 await = request ()
+{-# INLINABLE await #-}
 
 {-| Deliver output downstream
 
-    'yield' restores control back downstream and binds its value to 'await'. -}
-yield :: (Monad m, Proxy p) => b -> p a' a () b m ()
-yield b = runIdentityP $ do
-    respond b
-    return ()
+    'yield' restores control back downstream and binds its value to 'await'.
+-}
+yield :: (Monad m, Proxy p) => b -> p a' a b' b m b'
+yield = respond
+{-# INLINABLE yield #-}
 
 -- | Convert a pure function into a pipe
 pipe :: (Monad m, Proxy p) => (a -> b) -> Pipe p a b m r
 pipe f = runIdentityP $ forever $ do
     a <- request ()
     respond (f a)
+{-# INLINABLE pipe #-}
 
-infixr 9 <+<
-infixl 9 >+>
+infixr 7 <+<
+infixl 7 >+>
 
 -- | Corresponds to ('<<<')/('.') from @Control.Category@
 (<+<)
- :: (Monad m, Proxy p) => Pipe p b c m r -> Pipe p a b m r -> Pipe p a c m r
+    :: (Monad m, Proxy p)
+    => p b' b c' c m r
+    -> p a' a b' b m r
+    -> p a' a c' c m r
 p1 <+< p2 = p2 >+> p1
+{-# INLINABLE (<+<) #-}
 
 -- | Corresponds to ('>>>') from @Control.Category@
 (>+>)
- :: (Monad m, Proxy p) => Pipe p a b m r -> Pipe p b c m r -> Pipe p a c m r
-p1 >+> p2 = ((\() -> p1) >-> (\() -> p2)) ()
+    :: (Monad m, Proxy p)
+    => p a' a b' b m r
+    -> p b' b c' c m r
+    -> p a' a c' c m r
+p1 >+> p2 = (\_ -> p1) ->> p2
+{-# INLINABLE (>+>) #-}
 
 -- | Corresponds to 'id' from @Control.Category@
 idP :: (Monad m, Proxy p) => Pipe p a a m r
 idP = runIdentityP $ forever $ do
     a <- request ()
     respond a
+{-# INLINABLE idP #-}
 
 {-| A self-contained 'Pipeline' that is ready to be run
 
-    'Pipeline's never 'request' nor 'respond'. -}
+    'Pipeline's never 'request' nor 'respond'.
+-}
 type Pipeline (p :: * -> * -> * -> * -> (* -> *) -> * -> *) = p C () () C
 
 {- $run
@@ -84,7 +97,8 @@
 
     Each implementation must supply its own 'runPipe' function since it is
     the only non-polymorphic 'Pipe' function and the compiler uses it to
-    select which underlying proxy implementation to use. -}
+    select which underlying proxy implementation to use.
+-}
 
 {- $upgrade
     You can upgrade classic 'Pipe' code to work with the proxy ecosystem in
@@ -113,7 +127,7 @@
     The change ensures that all your code now works in the 'ProxyFast' monad,
     which is the faster of the two proxy implementations.
 
-    Second, modify all your 'Pipe's to take an empty '()' as their final
+    Second, modify all your 'Pipe's to take an empty @()@ as their final
     argument, and translate the following functions:
 
     * ('<+<') to ('<-<')
@@ -194,5 +208,4 @@
 >     if (n == 0)
 >         then E.throw "Error: received 0"
 >         else lift $ print n
-
 -}
diff --git a/Control/Proxy/Prelude.hs b/Control/Proxy/Prelude.hs
--- a/Control/Proxy/Prelude.hs
+++ b/Control/Proxy/Prelude.hs
@@ -18,4 +18,5 @@
     "Control.Proxy.Prelude.IO" provides proxies for simple 'IO'.
 
     "Control.Proxy.Prelude.Kleisli" provides convenience functions for working
-    with Kleisli arrows. -}
+    with Kleisli arrows.
+-}
diff --git a/Control/Proxy/Prelude/Base.hs b/Control/Proxy/Prelude/Base.hs
--- a/Control/Proxy/Prelude/Base.hs
+++ b/Control/Proxy/Prelude/Base.hs
@@ -37,6 +37,12 @@
     enumFromToS,
     enumFromToC,
 
+    -- * ListT
+    eachS,
+    eachC,
+    rangeS,
+    rangeC,
+
     -- * Folds
     foldD,
     foldU,
@@ -67,6 +73,13 @@
     foldlD',
     foldlU',
 
+    -- * ArrowChoice
+    -- $choice
+    leftD,
+    rightD,
+    leftU,
+    rightU,
+
     -- * Zips and Merges
     zipD,
     mergeD,
@@ -79,20 +92,34 @@
     -- * Modules
     -- $modules
     module Control.Monad.Trans.State.Strict,
-    module W,
+    module Control.Monad.Trans.Writer.Lazy,
     module Data.Monoid
     ) where
 
-import Control.MFunctor (hoist)
+import Control.Monad.Morph (hoist)
 import Control.Monad.Trans.Class (lift)
-import Control.Monad.Trans.Writer.Lazy as W (
-    WriterT(runWriterT), execWriterT, runWriter )
-import Control.Monad.Trans.Writer.Lazy (tell)
+import Control.Monad.Trans.Writer.Lazy (
+    WriterT(runWriterT), execWriterT, runWriter, execWriter )
+import qualified Control.Monad.Trans.Writer.Lazy as W (tell)
 import Control.Monad.Trans.State.Strict (
-    StateT(StateT, runStateT), execStateT, runState, execState )
+    StateT(StateT, runStateT),
+    execStateT,
+    evalStateT,
+    runState,
+    execState,
+    evalState )
 import Control.Proxy.Class
-import Control.Proxy.Synonym
-import Control.Proxy.Trans.Identity (runIdentityP, runIdentityK)
+import Control.Proxy.ListT (
+    ListT,
+    (\>\),
+    (/>/),
+    RespondT(RespondT),
+    RequestT(RequestT),
+    ProduceT,
+    CoProduceT )
+import Control.Proxy.Prelude.Kleisli (replicateK, foreverK)
+import Control.Proxy.Synonym (Producer, Consumer, Pipe, CoProducer, CoPipe)
+import Control.Proxy.Trans.Identity (runIdentityP, runIdentityK, identityK)
 import Data.Monoid (
     Monoid,
     Endo(Endo, appEndo),
@@ -115,7 +142,8 @@
         a  <- request x
         x2 <- respond (f a)
         go x2
--- mapD f = foreverK $ request >=> respond . f
+-- mapD f = runIdentityK $ foreverK $ request >=> respond . f
+{-# INLINABLE mapD #-}
 
 {-| @(mapU g)@ applies @g@ to all values going \'@U@\'pstream.
 
@@ -130,6 +158,7 @@
         b'2 <- respond x
         go b'2
 -- mapU g = foreverK $ (request . g) >=> respond
+{-# INLINABLE mapU #-}
 
 {-| @(mapB f g)@ applies @f@ to all values going downstream and @g@ to all
     values going upstream.
@@ -147,6 +176,7 @@
         b'2 <- respond (f a )
         go b'2
 -- mapB f g = foreverK $ request . g >=> respond . f
+{-# INLINABLE mapB #-}
 
 {-| @(mapMD f)@ applies the monadic function @f@ to all values going downstream
 
@@ -162,6 +192,7 @@
         x2 <- respond b
         go x2
 -- mapMD f = foreverK $ request >=> lift . f >=> respond
+{-# INLINABLE mapMD #-}
 
 {-| @(mapMU g)@ applies the monadic function @g@ to all values going upstream
 
@@ -177,6 +208,7 @@
         b'2 <- respond x
         go b'2
 -- mapMU g = foreverK $ lift . g >=> request >=> respond
+{-# INLINABLE mapMU #-}
 
 {-| @(mapMB f g)@ applies the monadic function @f@ to all values going
     downstream and the monadic function @g@ to all values going upstream.
@@ -186,7 +218,7 @@
 > mapMB return return = idT
 -}
 mapMB
- :: (Monad m, Proxy p) => (a -> m b) -> (b' -> m a') -> b' -> p a' a b' b m r
+    :: (Monad m, Proxy p) => (a -> m b) -> (b' -> m a') -> b' -> p a' a b' b m r
 mapMB f g = runIdentityK go where
     go b' = do
         a'  <- lift (g b')
@@ -195,6 +227,7 @@
         b'2 <- respond b
         go b'2
 -- mapMB f g = foreverK $ lift . g >=> request >=> lift . f >=> respond
+{-# INLINABLE mapMB #-}
 
 {-| @(useD f)@ executes the monadic function @f@ on all values flowing
     \'@D@\'ownstream
@@ -210,6 +243,7 @@
         lift $ f a
         x2 <- respond a
         go x2
+{-# INLINABLE useD #-}
 
 {-| @(useU g)@ executes the monadic function @g@ on all values flowing
     \'@U@\'pstream
@@ -225,6 +259,7 @@
         x   <- request a'
         a'2 <- respond x
         go a'2
+{-# INLINABLE useU #-}
 
 {-| @(useB f g)@ executes the monadic function @f@ on all values flowing
     downstream and the monadic function @g@ on all values flowing upstream
@@ -234,7 +269,8 @@
 > useB (\_ -> return ()) (\_ -> return ()) = idT
 -}
 useB
- :: (Monad m, Proxy p) => (a -> m r1) -> (a' -> m r2) -> a' -> p a' a a' a m r
+    :: (Monad m, Proxy p)
+    => (a -> m r1) -> (a' -> m r2) -> a' -> p a' a a' a m r
 useB f g = runIdentityK go where
     go a' = do
         lift $ g a'
@@ -242,6 +278,7 @@
         lift $ f a
         a'2 <- respond a
         go a'2
+{-# INLINABLE useB #-}
 
 {-| @(execD md)@ executes @md@ every time values flow downstream through it.
 
@@ -260,6 +297,7 @@
     a <- request a'
     lift md
     respond a -}
+{-# INLINABLE execD #-}
 
 {-| @(execU mu)@ executes @mu@ every time values flow upstream through it.
 
@@ -278,6 +316,7 @@
     lift mu
     a <- request a'
     respond a -}
+{-# INLINABLE execU #-}
 
 {-| @(execB md mu)@ executes @mu@ every time values flow upstream through it,
     and executes @md@ every time values flow downstream through it.
@@ -299,6 +338,7 @@
     a <- request a'
     lift md
     respond a -}
+{-# INLINABLE execB #-}
 
 {-| @(takeB n)@ allows @n@ upstream/downstream roundtrips to pass through
 
@@ -314,7 +354,8 @@
              a   <- request a'
              a'2 <- respond a
              go (n - 1) a'2
--- takeB n = replicateK n $ request >=> respond
+-- takeB n = runIdentityK $ replicateK n $ request >=> respond
+{-# INLINABLE takeB #-}
 
 -- | 'takeB_' is 'takeB' with a @()@ return value, convenient for composing
 takeB_ :: (Monad m, Proxy p) => Int -> a' -> p a' a a' a m ()
@@ -326,6 +367,7 @@
             a'2 <- respond a
             go (n - 1) a'2
 -- takeB_ n = fmap void (takeB n)
+{-# INLINABLE takeB_ #-}
 
 {-| @(takeWhileD p)@ allows values to pass downstream so long as they satisfy
     the predicate @p@.
@@ -347,6 +389,7 @@
                 a'2 <- respond a
                 go a'2
             else return ()
+{-# INLINABLE takeWhileD #-}
 
 {-| @(takeWhileU p)@ allows values to pass upstream so long as they satisfy the
     predicate @p@.
@@ -364,6 +407,7 @@
                 a'2 <- respond a
                 go a'2
             else return_P ()
+{-# INLINABLE takeWhileU #-}
 
 {-| @(dropD n)@ discards @n@ values going downstream
 
@@ -381,6 +425,7 @@
 {- dropD n () = do
     replicateM_ n $ request ()
     idT () -}
+{-# INLINABLE dropD #-}
 
 {-| @(dropU n)@ discards @n@ values going upstream
 
@@ -395,6 +440,7 @@
         | otherwise = \_ -> do
             a' <- respond ()
             go (n - 1) a'
+{-# INLINABLE dropU #-}
 
 {-| @(dropWhileD p)@ discards values going downstream until one violates the
     predicate @p@.
@@ -416,6 +462,7 @@
             else do
                 x <- respond a
                 idT x
+{-# INLINABLE dropWhileD #-}
 
 {-| @(dropWhileU p)@ discards values going upstream until one violates the
     predicate @p@.
@@ -432,6 +479,7 @@
                 a2 <- respond ()
                 go a2
             else idT a'
+{-# INLINABLE dropWhileU #-}
 
 {-| @(filterD p)@ discards values going downstream if they fail the predicate
     @p@
@@ -453,6 +501,7 @@
                 respond a
                 go
             else go
+{-# INLINABLE filterD #-}
 
 {-| @(filterU p)@ discards values going upstream if they fail the predicate @p@
 
@@ -471,6 +520,7 @@
         else do
             a'2 <- respond ()
             go a'2
+{-# INLINABLE filterU #-}
 
 {-| Convert a list into a 'Producer'
 
@@ -481,6 +531,7 @@
 fromListS :: (Monad m, Proxy p) => [b] -> () -> Producer p b m ()
 fromListS xs = \_ -> foldr (\e a -> respond e ?>= \_ -> a) (return_P ()) xs
 -- fromListS xs _ = mapM_ respond xs
+{-# INLINABLE fromListS #-}
 
 {-| Convert a list into a 'CoProducer'
 
@@ -491,42 +542,78 @@
 fromListC :: (Monad m, Proxy p) => [a'] -> () -> CoProducer p a' m ()
 fromListC xs = \_ -> foldr (\e a -> request e ?>= \_ -> a) (return_P ()) xs
 -- fromListC xs _ = mapM_ request xs
+{-# INLINABLE fromListC #-}
 
 -- | 'Producer' version of 'enumFrom'
 enumFromS :: (Enum b, Monad m, Proxy p) => b -> () -> Producer p b m r
 enumFromS b0 = \_ -> runIdentityP (go b0) where
     go b = do
         respond b
-        go (succ b)
+        go $! succ b
+{-# INLINABLE enumFromS #-}
 
 -- | 'CoProducer' version of 'enumFrom'
 enumFromC :: (Enum a', Monad m, Proxy p) => a' -> () -> CoProducer p a' m r
 enumFromC a'0 = \_ -> runIdentityP (go a'0) where
     go a' = do
         request a'
-        go (succ a')
+        go $! succ a'
+{-# INLINABLE enumFromC #-}
 
 -- | 'Producer' version of 'enumFromTo'
 enumFromToS
- :: (Enum b, Ord b, Monad m, Proxy p) => b -> b -> () -> Producer p b m ()
+    :: (Enum b, Ord b, Monad m, Proxy p) => b -> b -> () -> Producer p b m ()
 enumFromToS b1 b2 _ = runIdentityP (go b1) where
     go b
         | b > b2    = return ()
         | otherwise = do
             respond b
-            go (succ b)
+            go $! succ b
+{-# INLINABLE enumFromToS #-}
 
 -- | 'CoProducer' version of 'enumFromTo'
 enumFromToC
- :: (Enum a', Ord a', Monad m, Proxy p)
- => a' -> a' -> () -> CoProducer p a' m ()
+    :: (Enum a', Ord a', Monad m, Proxy p)
+    => a' -> a' -> () -> CoProducer p a' m ()
 enumFromToC a1 a2 _ = runIdentityP (go a1) where
     go n
         | n > a2 = return ()
         | otherwise = do
             request n
-            go (succ n)
+            go $! succ n
+{-# INLINABLE enumFromToC #-}
 
+{-| Non-deterministically choose from all values in the given list
+
+> mappend <$> eachS xs <*> eachS ys = eachS (mappend <$> xs <*> ys)
+>
+> eachS (pure mempty) = pure mempty
+-}
+eachS :: (Monad m, ListT p) => [b] -> ProduceT p m b
+eachS bs = RespondT (fromListS bs ())
+{-# INLINABLE eachS #-}
+
+{-| Non-deterministically choose from all values in the given list
+
+> mappend <$> eachC xs <*> eachC ys = eachC (mappend <$> xs <*> ys)
+>
+> eachC (pure mempty) = pure mempty
+-}
+eachC :: (Monad m, ListT p) => [a'] -> CoProduceT p m a'
+eachC a's = RequestT (fromListC a's ())
+{-# INLINABLE eachC #-}
+
+-- | Non-deterministically choose from all values in the given range
+rangeS :: (Enum b, Ord b, Monad m, ListT p) => b -> b -> ProduceT p m b
+rangeS b1 b2 = RespondT (enumFromToS b1 b2 ())
+{-# INLINABLE rangeS #-}
+
+-- | Non-deterministically choose from all values in the given range
+rangeC
+    :: (Enum a', Ord a', Monad m, ListT p) => a' -> a' -> CoProduceT p m a'
+rangeC a'1 a'2 = RequestT (enumFromToC a'1 a'2 ())
+{-# INLINABLE rangeC #-}
+
 {-| Fold values flowing \'@D@\'ownstream
 
 > foldD f >-> foldD g = foldD (f <> g)
@@ -534,13 +621,15 @@
 > foldD mempty = idT
 -}
 foldD
- :: (Monad m, Proxy p, Monoid w) => (a -> w) -> x -> p x a x a (WriterT w m) r
+    :: (Monad m, Proxy p, Monoid w)
+    => (a -> w) -> x -> p x a x a (WriterT w m) r
 foldD f = runIdentityK go where
     go x = do
         a <- request x
-        lift $ tell $ f a
+        lift $ W.tell $ f a
         x2 <- respond a
         go x2
+{-# INLINABLE foldD #-}
 
 {-| Fold values flowing \'@U@\'pstream
 
@@ -549,30 +638,36 @@
 > foldU mempty = idT
 -}
 foldU
- :: (Monad m, Proxy p, Monoid w)
- => (a' -> w) -> a' -> p a' x a' x (WriterT w m) r
+    :: (Monad m, Proxy p, Monoid w)
+    => (a' -> w) -> a' -> p a' x a' x (WriterT w m) r
 foldU f = runIdentityK go where
     go a' = do
-        lift $ tell $ f a'
+        lift $ W.tell $ f a'
         x <- request a'
         a'2 <- respond x
         go a'2
+{-# INLINABLE foldU #-}
 
 {-| Fold that returns whether 'All' values flowing \'@D@\'ownstream satisfy the
-    predicate -}
+    predicate
+-}
 allD :: (Monad m, Proxy p) => (a -> Bool) -> x -> p x a x a (WriterT All m) r
 allD pred = foldD (All . pred)
+{-# INLINABLE allD #-}
 
 {-| Fold that returns whether 'All' values flowing \'@U@\'pstream satisfy the
-    predicate -}
+    predicate
+-}
 allU
- :: (Monad m, Proxy p) => (a' -> Bool) -> a' -> p a' x a' x (WriterT All m) r
+    :: (Monad m, Proxy p) => (a' -> Bool) -> a' -> p a' x a' x (WriterT All m) r
 allU pred = foldU (All . pred)
+{-# INLINABLE allU #-}
 
 {-| Fold that returns whether 'All' values flowing \'@D@\'ownstream satisfy the
     predicate
 
-    'allD_' terminates on the first value that fails the predicate -}
+    'allD_' terminates on the first value that fails the predicate
+-}
 allD_ :: (Monad m, Proxy p) => (a -> Bool) -> x -> p x a x a (WriterT All m) ()
 allD_ pred = runIdentityK go where
     go x = do
@@ -581,14 +676,17 @@
             then do
                 x2 <- respond a
                 go x2
-            else lift $ tell $ All False
+            else lift $ W.tell $ All False
+{-# INLINABLE allD_ #-}
 
 {-| Fold that returns whether 'All' values flowing \'@U@\'pstream satisfy the
     predicate
 
-    'allU_' terminates on the first value that fails the predicate -}
+    'allU_' terminates on the first value that fails the predicate
+-}
 allU_
- :: (Monad m, Proxy p) => (a' -> Bool) -> a' -> p a' x a' x (WriterT All m) ()
+    :: (Monad m, Proxy p)
+    => (a' -> Bool) -> a' -> p a' x a' x (WriterT All m) ()
 allU_ pred = runIdentityK go where
     go a' =
         if (pred a')
@@ -596,111 +694,138 @@
                 x   <- request a'
                 a'2 <- respond x
                 go a'2
-            else lift $ tell $ All False
+            else lift $ W.tell $ All False
+{-# INLINABLE allU_ #-}
 
 {-| Fold that returns whether 'Any' value flowing \'@D@\'ownstream satisfies
-    the predicate -}
+    the predicate
+-}
 anyD :: (Monad m, Proxy p) => (a -> Bool) -> x -> p x a x a (WriterT Any m) r
 anyD pred = foldD (Any . pred)
+{-# INLINABLE anyD #-}
 
 {-| Fold that returns whether 'Any' value flowing \'@U@\'pstream satisfies
-    the predicate -}
+    the predicate
+-}
 anyU
- :: (Monad m, Proxy p) => (a' -> Bool) -> a' -> p a' x a' x (WriterT Any m) r
+    :: (Monad m, Proxy p) => (a' -> Bool) -> a' -> p a' x a' x (WriterT Any m) r
 anyU pred = foldU (Any . pred)
+{-# INLINABLE anyU #-}
 
 {-| Fold that returns whether 'Any' value flowing \'@D@\'ownstream satisfies the
     predicate
 
-    'anyD_' terminates on the first value that satisfies the predicate -}
+    'anyD_' terminates on the first value that satisfies the predicate
+-}
 anyD_ :: (Monad m, Proxy p) => (a -> Bool) -> x -> p x a x a (WriterT Any m) ()
 anyD_ pred = runIdentityK go where
     go x = do
         a <- request x
         if (pred a)
-            then lift $ tell $ Any True
+            then lift $ W.tell $ Any True
             else do
                 x2 <- respond a
                 go x2
+{-# INLINABLE anyD_ #-}
 
 {-| Fold that returns whether 'Any' value flowing \'@U@\'pstream satisfies the
     predicate
 
-    'anyU_' terminates on the first value that satisfies the predicate -}
+    'anyU_' terminates on the first value that satisfies the predicate
+-}
 anyU_
- :: (Monad m, Proxy p) => (a' -> Bool) -> a' -> p a' x a' x (WriterT Any m) ()
+    :: (Monad m, Proxy p)
+    => (a' -> Bool) -> a' -> p a' x a' x (WriterT Any m) ()
 anyU_ pred = runIdentityK go where
     go a' =
         if (pred a')
-            then lift $ tell $ Any True
+            then lift $ W.tell $ Any True
             else do
                 x   <- request a'
                 a'2 <- respond x
                 go a'2
+{-# INLINABLE anyU_ #-}
 
 -- | Compute the 'Sum' of all values that flow \'@D@\'ownstream
 sumD :: (Monad m, Proxy p, Num a) => x -> p x a x a (WriterT (Sum a) m) r
 sumD = foldD Sum
+{-# INLINABLE sumD #-}
 
 -- | Compute the 'Sum' of all values that flow \'@U@\'pstream
 sumU :: (Monad m, Proxy p, Num a') => a' -> p a' x a' x (WriterT (Sum a') m) r
 sumU = foldU Sum
+{-# INLINABLE sumU #-}
 
 -- | Compute the 'Product' of all values that flow \'@D@\'ownstream
 productD
- :: (Monad m, Proxy p, Num a) => x -> p x a x a (WriterT (Product a) m) r
+    :: (Monad m, Proxy p, Num a) => x -> p x a x a (WriterT (Product a) m) r
 productD = foldD Product
+{-# INLINABLE productD #-}
 
 -- | Compute the 'Product' of all values that flow \'@U@\'pstream
 productU
- :: (Monad m, Proxy p, Num a') => a' -> p a' x a' x (WriterT (Product a') m) r
+    :: (Monad m, Proxy p, Num a')
+    => a' -> p a' x a' x (WriterT (Product a') m) r
 productU = foldU Product
+{-# INLINABLE productU #-}
 
 -- | Count how many values flow \'@D@\'ownstream
 lengthD :: (Monad m, Proxy p) => x -> p x a x a (WriterT (Sum Int) m) r
 lengthD = foldD (\_ -> Sum 1)
+{-# INLINABLE lengthD #-}
 
 -- | Count how many values flow \'@U@\'pstream
 lengthU :: (Monad m, Proxy p) => a' -> p a' x a' x (WriterT (Sum Int) m) r
 lengthU = foldU (\_ -> Sum 1)
+{-# INLINABLE lengthU #-}
 
 -- | Retrieve the first value going \'@D@\'ownstream
 headD :: (Monad m, Proxy p) => x -> p x a x a (WriterT (First a) m) r
 headD = foldD (First . Just)
+{-# INLINABLE headD #-}
 
 {-| Retrieve the first value going \'@D@\'ownstream
 
-    'headD_' terminates on the first value it receives -}
+    'headD_' terminates on the first value it receives
+-}
 headD_ :: (Monad m, Proxy p) => x -> p x a x a (WriterT (First a) m) ()
 headD_ x = runIdentityP $ do
     a <- request x
-    lift $ tell $ First (Just a)
+    lift $ W.tell $ First (Just a)
+{-# INLINABLE headD_ #-}
 
 -- | Retrieve the first value going \'@U@\'pstream
 headU :: (Monad m, Proxy p) => a' -> p a' x a' x (WriterT (First a') m) r
 headU = foldU (First . Just)
+{-# INLINABLE headU #-}
 
 {-| Retrieve the first value going \'@U@\'pstream
 
-    'headU_' terminates on the first value it receives -}
+    'headU_' terminates on the first value it receives
+-}
 headU_ :: (Monad m, Proxy p) => a' -> p a' x a' x (WriterT (First a') m) ()
-headU_ a' = runIdentityP $ lift $ tell $ First (Just a')
+headU_ a' = runIdentityP $ lift $ W.tell $ First (Just a')
+{-# INLINABLE headU_ #-}
 
 -- | Retrieve the last value going \'@D@\'ownstream
 lastD :: (Monad m, Proxy p) => x -> p x a x a (WriterT (Last a) m) r
 lastD = foldD (Last . Just)
+{-# INLINABLE lastD #-}
 
 -- | Retrieve the last value going \'@U@\'pstream
 lastU :: (Monad m, Proxy p) => a' -> p a' x a' x (WriterT (Last a') m) r
 lastU = foldU (Last . Just)
+{-# INLINABLE lastU #-}
 
 -- | Fold the values flowing \'@D@\'ownstream into a list
 toListD :: (Monad m, Proxy p) => x -> p x a x a (WriterT [a] m) r
 toListD = foldD (\x -> [x])
+{-# INLINABLE toListD #-}
 
 -- | Fold the values flowing \'@U@\'pstream into a list
 toListU :: (Monad m, Proxy p) => a' -> p a' x a' x (WriterT [a'] m) r
 toListU = foldU (\x -> [x])
+{-# INLINABLE toListU #-}
 
 {-| Fold equivalent to 'foldr'
 
@@ -709,39 +834,122 @@
 > foldr :: (a -> b -> b) -> [a] -> Endo b
 -}
 foldrD
- :: (Monad m, Proxy p) => (a -> b -> b) -> x -> p x a x a (WriterT (Endo b) m) r
+    :: (Monad m, Proxy p)
+    => (a -> b -> b) -> x -> p x a x a (WriterT (Endo b) m) r
 foldrD step = foldD (Endo . step)
+{-# INLINABLE foldrD #-}
 
 -- | Fold equivalent to 'foldr'
 foldrU
- :: (Monad m, Proxy p)
- => (a' -> b -> b) -> a' -> p a' x a' x (WriterT (Endo b) m) r
+    :: (Monad m, Proxy p)
+    => (a' -> b -> b) -> a' -> p a' x a' x (WriterT (Endo b) m) r
 foldrU step = foldU (Endo . step)
+{-# INLINABLE foldrU #-}
 
 -- | Left strict fold over \'@D@\'ownstream values
 foldlD'
- :: (Monad m, Proxy p) => (b -> a -> b) -> x -> p x a x a (StateT b m) r
+    :: (Monad m, Proxy p) => (b -> a -> b) -> x -> p x a x a (StateT b m) r
 foldlD' f = runIdentityK go where
     go x = do
         a  <- request x
         lift $ StateT $ \b -> let b' = f b a in b' `seq` return ((), b')
         x2 <- respond a
         go x2
+{-# INLINABLE foldlD' #-}
 
 -- | Left strict fold over \'@U@\'pstream values
 foldlU'
- :: (Monad m, Proxy p) => (b -> a' -> b) -> a' -> p a' x a' x (StateT b m) r
+    :: (Monad m, Proxy p) => (b -> a' -> b) -> a' -> p a' x a' x (StateT b m) r
 foldlU' f = runIdentityK go where
     go a' = do
         lift $ StateT $ \b -> let b' = f b a' in b' `seq` return ((), b')
         x   <- request a'
         a'2 <- respond x
         go a'2
+{-# INLINABLE foldlU' #-}
 
+{- $choice
+    'leftD' and 'rightD' satisfy the 'ArrowChoice' laws using @arr = mapD@.
+
+    'leftU' and 'rightU' satisfy the 'ArrowChoice' laws using @arr = mapU@.
+-}
+
+{-| Lift a proxy to operate only on 'Left' values flowing \'@D@\'ownstream and
+    forward 'Right' values
+-}
+leftD
+    :: (Monad m, ListT p)
+    => (q -> p x a x b m r) -> (q -> p x (Either a e) x (Either b e) m r)
+leftD k = runIdentityK (up \>\ (identityK k />/ dn))
+  where
+    dn b = respond (Left b)
+    up x = do
+        ma <- request x
+        case ma of
+            Left  a -> return a
+            Right e -> do
+                x2 <- respond (Right e)
+                up x2 
+{-# INLINABLE leftD #-}
+
+{-| Lift a proxy to operate only on 'Right' values flowing \'@D@\'ownstream and
+    forward 'Left' values
+-}
+rightD
+    :: (Monad m, ListT p)
+    => (q -> p x a x b m r) -> (q -> p x (Either e a) x (Either e b) m r)
+rightD k = runIdentityK (up \>\ (identityK k />/ dn))
+  where
+    dn b = respond (Right b)
+    up x = do
+        ma <- request x
+        case ma of
+            Left  e -> do
+                x2 <- respond (Left e)
+                up x2 
+            Right a -> return a
+{-# INLINABLE rightD #-}
+
+{-| Lift a proxy to operate only on 'Left' values flowing \'@U@\'pstream and
+    forward 'Right' values
+-}
+leftU
+    :: (Monad m, ListT p)
+    => (q -> p a' x b' x m r) -> (q -> p (Either a' e) x (Either b' e) x m r)
+leftU k = runIdentityK ((up \>\ identityK k) />/ dn)
+  where
+    up a' = request (Left a')
+    dn x = do
+        mb' <- respond x
+        case mb' of
+            Left  b' -> return b'
+            Right e  -> do
+                x2 <- request (Right e)
+                dn x2 
+{-# INLINABLE leftU #-}
+
+{-| Lift a proxy to operate only on 'Right' values flowing \'@D@\'ownstream and
+    forward 'Left' values
+-}
+rightU
+    :: (Monad m, ListT p)
+    => (q -> p a' x b' x m r) -> (q -> p (Either e a') x (Either e b') x m r)
+rightU k = runIdentityK ((up \>\ identityK k) />/ dn)
+  where
+    up a' = request (Right a')
+    dn x = do
+        mb' <- respond x
+        case mb' of
+            Left  e  -> do
+                x2 <- request (Left e)
+                dn x2 
+            Right b' -> return b'
+{-# INLINABLE rightU #-}
+
 -- | Zip values flowing downstream
 zipD
- :: (Monad m, Proxy p1, Proxy p2, Proxy p3)
- => () -> Consumer p1 a (Consumer p2 b (Producer p3 (a, b) m)) r
+    :: (Monad m, Proxy p1, Proxy p2, Proxy p3)
+    => () -> Consumer p1 a (Consumer p2 b (Producer p3 (a, b) m)) r
 zipD () = runIdentityP $ hoist (runIdentityP . hoist runIdentityP) go where
     go = do
         a <- request ()
@@ -749,11 +957,12 @@
             b <- request ()
             lift $ respond (a, b)
         go
+{-# INLINABLE zipD #-}
 
 -- | Interleave values flowing downstream using simple alternation
 mergeD
- :: (Monad m, Proxy p1, Proxy p2, Proxy p3)
- => () -> Consumer p1 a (Consumer p2 a (Producer p3 a m)) r
+    :: (Monad m, Proxy p1, Proxy p2, Proxy p3)
+    => () -> Consumer p1 a (Consumer p2 a (Producer p3 a m)) r
 mergeD () = runIdentityP $ hoist (runIdentityP . hoist runIdentityP) go where
     go = do
         a1 <- request ()
@@ -762,6 +971,7 @@
             a2 <- request ()
             lift $ respond a2
         go
+{-# INLINABLE mergeD #-}
 
 {- $open
     Use the @unit@ functions when you need to embed a proxy with a closed end
@@ -783,18 +993,20 @@
 -}
 
 -- | Compose 'unitD' with a closed upstream end to create a polymorphic end
-unitD :: (Monad m, Proxy p) => y' -> p x' x y' () m r
+unitD :: (Monad m, Proxy p) => q -> p x' x y' () m r
 unitD _ = runIdentityP go where
     go = do
         respond ()
         go
+{-# INLINABLE unitD #-}
 
 -- | Compose 'unitU' with a closed downstream end to create a polymorphic end
-unitU :: (Monad m, Proxy p) => y' -> p () x y' y m r
+unitU :: (Monad m, Proxy p) => q -> p () x y' y m r
 unitU _ = runIdentityP go where
     go = do
         request ()
         go
+{-# INLINABLE unitU #-}
 
 {- $modules
     These modules help you build, run, and extract folds
diff --git a/Control/Proxy/Prelude/IO.hs b/Control/Proxy/Prelude/IO.hs
--- a/Control/Proxy/Prelude/IO.hs
+++ b/Control/Proxy/Prelude/IO.hs
@@ -3,36 +3,41 @@
     Note that 'String's are very inefficient, and I will release future separate
     packages with 'ByteString' and 'Text' operations.  I only provide these to
     allow users to test simple I/O without requiring additional library
-    dependencies. -}
-
+    dependencies.
+-}
 module Control.Proxy.Prelude.IO (
     -- * Standard I/O
+
     -- ** Input
+    stdinS,
     getLineS,
     getLineC,
     readLnS,
     readLnC,
+
     -- ** Output
-    printB,
-    printD,
-    printU,
-    putStrLnB,
+    stdoutD,
     putStrLnD,
     putStrLnU,
-    -- ** Interaction
-    promptS,
-    promptC,
+    putStrLnB,
+    printD,
+    printU,
+    printB,
+
     -- * Handle I/O
+
     -- ** Input
+
     hGetLineS,
     hGetLineC,
+
     -- ** Output
-    hPrintB,
     hPrintD,
     hPrintU,
-    hPutStrLnB,
+    hPrintB,
     hPutStrLnD,
     hPutStrLnU,
+    hPutStrLnB,
     ) where
 
 import Control.Monad (forever)
@@ -40,47 +45,78 @@
 import Control.Proxy.Prelude.Kleisli (foreverK)
 import Control.Proxy.Class (Proxy(request, respond))
 import Control.Proxy.Trans.Identity (runIdentityP, runIdentityK)
-import Control.Proxy.Synonym (Client, Server, Producer, CoProducer)
+import Control.Proxy.Synonym (Producer, CoProducer)
 import qualified System.IO as IO
 
+-- | Synonym for 'getLineS'
+stdinS :: (Proxy p) => () -> Producer p String IO r
+stdinS = getLineS
+{-# INLINABLE stdinS #-}
+
 -- | A 'Producer' that sends lines from 'stdin' downstream
 getLineS :: (Proxy p) => () -> Producer p String IO r
 getLineS () = runIdentityP $ forever $ do
     str <- lift getLine
     respond str
+{-# INLINABLE getLineS #-}
 
 -- | A 'CoProducer' that sends lines from 'stdin' upstream
 getLineC :: (Proxy p) => () -> CoProducer p String IO r
 getLineC () = runIdentityP $ forever $ do
     str <- lift getLine
     request str
+{-# INLINABLE getLineC #-}
 
 -- | 'read' input from 'stdin' one line at a time and send \'@D@\'ownstream
 readLnS :: (Read b, Proxy p) => () -> Producer p b IO r
 readLnS () = runIdentityP $ forever $ do
     a <- lift readLn
     respond a
+{-# INLINABLE readLnS #-}
 
 -- | 'read' input from 'stdin' one line at a time and send \'@U@\'pstream
 readLnC :: (Read a', Proxy p) => () -> CoProducer p a' IO r
 readLnC () = runIdentityP $ forever $ do
     a <- lift readLn
     request a
+{-# INLINABLE readLnC #-}
 
-{-| 'print's all values flowing through it to 'stdout'
+-- | Synonym for 'putStrLnD'
+stdoutD :: (Proxy p) => x -> p x String x String IO r
+stdoutD = putStrLnD
+{-# INLINABLE stdoutD #-}
 
+-- | 'putStrLn's all values flowing \'@D@\'ownstream to 'stdout'
+putStrLnD :: (Proxy p) => x -> p x String x String IO r
+putStrLnD = runIdentityK $ foreverK $ \x -> do
+    a <- request x
+    lift $ putStrLn a
+    respond a
+{-# INLINABLE putStrLnD #-}
+
+-- | 'putStrLn's all values flowing \'@U@\'pstream to 'stdout'
+putStrLnU :: (Proxy p) => String -> p String x String x IO r
+putStrLnU = runIdentityK $ foreverK $ \a' -> do
+    lift $ putStrLn a'
+    x <- request a'
+    respond x
+{-# INLINABLE putStrLnU #-}
+
+{-| 'putStrLn's all values flowing through it to 'stdout'
+
     Prefixes upstream values with \"@U: @\" and downstream values with \"@D: @\"
 -}
-printB :: (Show a', Show a, Proxy p) => a' -> p a' a a' a IO r
-printB = runIdentityK $ foreverK $ \a' -> do
+putStrLnB :: (Proxy p) => String -> p String String String String IO r
+putStrLnB = runIdentityK $ foreverK $ \a' -> do
     lift $ do
         putStr "U: "
-        print a'
+        putStrLn a'
     a <- request a'
     lift $ do
         putStr "D: "
-        print a
+        putStrLn a
     respond a
+{-# INLINABLE putStrLnB #-}
 
 -- | 'print's all values flowing \'@D@\'ownstream to 'stdout'
 printD :: (Show a, Proxy p) => x -> p x a x a IO r
@@ -88,6 +124,7 @@
     a <- request x
     lift $ print a
     respond a
+{-# INLINABLE printD #-}
 
 -- | 'print's all values flowing \'@U@\'pstream to 'stdout'
 printU :: (Show a', Proxy p) => a' -> p a' x a' x IO r
@@ -95,50 +132,23 @@
     lift $ print a'
     x <- request a'
     respond x
+{-# INLINABLE printU #-}
 
-{-| 'putStrLn's all values flowing through it to 'stdout'
+{-| 'print's all values flowing through it to 'stdout'
 
     Prefixes upstream values with \"@U: @\" and downstream values with \"@D: @\"
 -}
-putStrLnB :: (Proxy p) => String -> p String String String String IO r
-putStrLnB = runIdentityK $ foreverK $ \a' -> do
+printB :: (Show a', Show a, Proxy p) => a' -> p a' a a' a IO r
+printB = runIdentityK $ foreverK $ \a' -> do
     lift $ do
         putStr "U: "
-        putStrLn a'
+        print a'
     a <- request a'
     lift $ do
         putStr "D: "
-        putStrLn a
-    respond a
-
--- | 'putStrLn's all values flowing \'@D@\'ownstream to 'stdout'
-putStrLnD :: (Proxy p) => x -> p x String x String IO r
-putStrLnD = runIdentityK $ foreverK $ \x -> do
-    a <- request x
-    lift $ putStrLn a
+        print a
     respond a
-
--- | 'putStrLn's all values flowing \'@U@\'pstream to 'stdout'
-putStrLnU :: (Proxy p) => String -> p String x String x IO r
-putStrLnU = runIdentityK $ foreverK $ \a' -> do
-    lift $ putStrLn a'
-    x <- request a'
-    respond x
-
--- | Convert 'stdin'/'stdout' into a line-based 'Server'
-promptS :: (Proxy p) => String -> Server p String String IO r
-promptS = runIdentityK $ foreverK $ \send -> do
-    recv <- lift $ do
-        putStrLn send
-        getLine
-    respond recv
-
--- | Convert 'stdin'/'stdout' into a line-based 'Client'
-promptC :: (Proxy p) => () -> Client p String String IO r
-promptC () = runIdentityP $ forever $ do
-    send <- lift getLine
-    recv <- request send
-    lift $ putStrLn recv
+{-# INLINABLE printB #-}
 
 -- | A 'Producer' that sends lines from a handle downstream
 hGetLineS :: (Proxy p) => IO.Handle -> () -> Producer p String IO ()
@@ -151,6 +161,7 @@
                 str <- lift $ IO.hGetLine h
                 respond str
                 go
+{-# INLINABLE hGetLineS #-}
 
 -- | A 'CoProducer' that sends lines from a 'Handle' upstream
 hGetLineC :: (Proxy p) => IO.Handle -> () -> CoProducer p String IO ()
@@ -163,21 +174,7 @@
                 str <- lift $ IO.hGetLine h
                 request str
                 go
-
-{-| 'print's all values flowing through it to a 'Handle'
-
-    Prefixes upstream values with \"@U: @\" and downstream values with \"@D: @\"
--}
-hPrintB :: (Show a, Show a', Proxy p) => IO.Handle -> a' -> p a' a a' a IO r
-hPrintB h = runIdentityK $ foreverK $ \a' -> do
-    lift $ do
-        IO.hPutStr h "U: "
-        IO.hPrint h a'
-    a <- request a'
-    lift $ do
-        IO.hPutStr h "D: "
-        IO.hPrint h a
-    respond a
+{-# INLINABLE hGetLineC #-}
 
 -- | 'print's all values flowing \'@D@\'ownstream to a 'Handle'
 hPrintD :: (Show a, Proxy p) => IO.Handle -> x -> p x a x a IO r
@@ -185,6 +182,7 @@
     a <- request x
     lift $ IO.hPrint h a
     respond a
+{-# INLINABLE hPrintD #-}
 
 -- | 'print's all values flowing \'@U@\'pstream to a 'Handle'
 hPrintU :: (Show a', Proxy p) => IO.Handle -> a' -> p a' x a' x IO r
@@ -192,22 +190,23 @@
     lift $ IO.hPrint h a'
     x <- request a'
     respond x
+{-# INLINABLE hPrintU #-}
 
-{-| 'putStrLn's all values flowing through it to a 'Handle'
+{-| 'print's all values flowing through it to a 'Handle'
 
     Prefixes upstream values with \"@U: @\" and downstream values with \"@D: @\"
 -}
-hPutStrLnB
- :: (Proxy p) => IO.Handle -> String -> p String String String String IO r
-hPutStrLnB h = runIdentityK $ foreverK $ \a' -> do
+hPrintB :: (Show a, Show a', Proxy p) => IO.Handle -> a' -> p a' a a' a IO r
+hPrintB h = runIdentityK $ foreverK $ \a' -> do
     lift $ do
         IO.hPutStr h "U: "
-        IO.hPutStrLn h a'
+        IO.hPrint h a'
     a <- request a'
     lift $ do
         IO.hPutStr h "D: "
-        IO.hPutStrLn h a
+        IO.hPrint h a
     respond a
+{-# INLINABLE hPrintB #-}
 
 -- | 'putStrLn's all values flowing \'@D@\'ownstream to a 'Handle'
 hPutStrLnD :: (Proxy p) => IO.Handle -> x -> p x String x String IO r
@@ -215,6 +214,7 @@
     a <- request x
     lift $ IO.hPutStrLn h a
     respond a
+{-# INLINABLE hPutStrLnD #-}
 
 -- | 'putStrLn's all values flowing \'@U@\'pstream to a 'Handle'
 hPutStrLnU :: (Proxy p) => IO.Handle -> String -> p String x String x IO r
@@ -222,3 +222,21 @@
     lift $ IO.hPutStrLn h a'
     x <- request a'
     respond x
+{-# INLINABLE hPutStrLnU #-}
+
+{-| 'putStrLn's all values flowing through it to a 'Handle'
+
+    Prefixes upstream values with \"@U: @\" and downstream values with \"@D: @\"
+-}
+hPutStrLnB
+    :: (Proxy p) => IO.Handle -> String -> p String String String String IO r
+hPutStrLnB h = runIdentityK $ foreverK $ \a' -> do
+    lift $ do
+        IO.hPutStr h "U: "
+        IO.hPutStrLn h a'
+    a <- request a'
+    lift $ do
+        IO.hPutStr h "D: "
+        IO.hPutStrLn h a
+    respond a
+{-# INLINABLE hPutStrLnB #-}
diff --git a/Control/Proxy/Prelude/Kleisli.hs b/Control/Proxy/Prelude/Kleisli.hs
--- a/Control/Proxy/Prelude/Kleisli.hs
+++ b/Control/Proxy/Prelude/Kleisli.hs
@@ -7,10 +7,19 @@
     foreverK,
     replicateK,
     liftK,
+    hoistK,
+    raise,
+    raiseK,
+    hoistPK,
+    raiseP,
+    raisePK
     ) where
 
-import Control.MFunctor (MFunctor(hoist))
+import Control.Monad.Morph (MFunctor(hoist))
 import Control.Monad.Trans.Class (MonadTrans(lift))
+import Control.Proxy.Class (Proxy)
+import Control.Proxy.Morph (PFunctor(hoistP))
+import Control.Proxy.Trans (ProxyTrans(liftP))
 
 {-| Compose a \'@K@\'leisli arrow with itself forever
 
@@ -30,7 +39,9 @@
 foreverK :: (Monad m) => (a -> m a) -> (a -> m b)
 foreverK k = let r = \a -> k a >>= r in r
 {- foreverK uses 'let' to avoid a space leak.
-   See: http://hackage.haskell.org/trac/ghc/ticket/5205 -}
+   See: http://hackage.haskell.org/trac/ghc/ticket/5205
+-}
+{-# INLINABLE foreverK #-}
 
 -- | Repeat a \'@K@\'leisli arrow multiple times
 replicateK :: (Monad m) => Int -> (a -> m a) -> (a -> m a)
@@ -39,6 +50,7 @@
         | n < 1     = return
         | n == 1    = k
         | otherwise = \a -> k a >>= go (n - 1)
+{-# INLINABLE replicateK #-}
 
 {-| Convenience function equivalent to @(lift .)@
 
@@ -49,3 +61,63 @@
 liftK :: (Monad m, MonadTrans t) => (a -> m b) -> (a -> t m b)
 liftK k a = lift (k a)
 -- liftK = (lift .)
+{-# INLINABLE liftK #-}
+
+-- | Convenience function equivalent to @(hoist f .)@
+hoistK
+    :: (Monad m, MFunctor t)
+    => (forall a . m a -> n a)  -- ^ Monad morphism
+    -> (b' -> t m b)            -- ^ Kleisli arrow
+    -> (b' -> t n b)
+hoistK k p a' = hoist k (p a')
+-- hoistK k = (hoist k .)
+{-# INLINABLE hoistK #-}
+
+{-| Lift the base monad
+
+> raise = hoist lift
+-}
+raise :: (Monad m, MFunctor t1, MonadTrans t2) => t1 m r -> t1 (t2 m) r
+raise = hoist lift
+{-# INLINABLE raise #-}
+
+{-| Lift the base monad of a \'@K@\'leisli arrow
+
+> raiseK = hoistK lift
+-}
+raiseK
+    :: (Monad m, MFunctor t1, MonadTrans t2)
+    => (q -> t1 m r) -> (q -> t1 (t2 m) r)
+raiseK = (hoist lift .)
+{-# INLINABLE raiseK #-}
+
+-- | Convenience function equivalent to @(hoistP f .)@
+hoistPK
+    :: (Monad m, Proxy p1, PFunctor t)
+    => (forall r1 . p1 a' a b' b m r1 -> p2 a' a b' b n r1) -- ^ Proxy morphism
+    -> (q -> t p1 a' a b' b m r2) -- ^ Proxy Kleisli arrow
+    -> (q -> t p2 a' a b' b n r2)
+hoistPK f = (hoistP f .)
+{-# INLINABLE hoistPK #-}
+
+{-| Lift the base proxy
+
+> raiseP = hoistP liftP
+-}
+raiseP
+    :: (Monad m, Proxy p, PFunctor t1, ProxyTrans t2)
+    => t1 p a' a b' b m r -- ^ Proxy
+    -> t1 (t2 p) a' a b' b m r
+raiseP = hoistP liftP
+{-# INLINABLE raiseP #-}
+
+{-| Lift the base proxy of a \'@K@\'leisli arrow
+
+> raisePK = hoistPK liftP
+-}
+raisePK
+    :: (Monad m, Proxy p, PFunctor t1, ProxyTrans t2)
+    => (q -> t1 p a' a b' b m r) -- ^ Proxy Kleisli arrow
+    -> (q -> t1 (t2 p) a' a b' b m r)
+raisePK = hoistPK liftP
+{-# INLINABLE raisePK #-}
diff --git a/Control/Proxy/Synonym.hs b/Control/Proxy/Synonym.hs
--- a/Control/Proxy/Synonym.hs
+++ b/Control/Proxy/Synonym.hs
@@ -1,9 +1,12 @@
 {-| These type synonyms simplify type signatures when proxies do not use all
-    their type variables. -}
-
+    their type variables.
+-}
 {-# LANGUAGE KindSignatures #-}
 
 module Control.Proxy.Synonym (
+    -- * Closed
+    C,
+
     -- * Synonyms
     Pipe,
     Producer,
@@ -13,23 +16,25 @@
     CoConsumer,
     Client,
     Server,
-    Session,
-
-    -- * Closed
-    C
+    Session
     ) where
 
+-- | The empty type, denoting a \'@C@\'losed end
+data C = C -- Constructor not exported, but I include it to avoid EmptyDataDecls
+
 -- | A unidirectional 'Proxy'.
 type Pipe (p :: * -> * -> * -> * -> (* -> *) -> * -> *) a b = p () a () b
 
 {-| A 'Pipe' that produces values
 
-    'Producer's never 'request'. -}
+    'Producer's never 'request'.
+-}
 type Producer (p :: * -> * -> * -> * -> (* -> *) -> * -> *) b = p C () () b
 
 {-| A 'Pipe' that consumes values
 
-    'Consumer's never 'respond'. -}
+    'Consumer's never 'respond'.
+-}
 type Consumer (p :: * -> * -> * -> * -> (* -> *) -> * -> *) a = p () a () C
 
 -- | A 'Pipe' where everything flows upstream
@@ -37,30 +42,32 @@
 
 {-| A 'CoPipe' that produces values flowing upstream
 
-    'CoProducer's never 'respond'. -}
+    'CoProducer's never 'respond'.
+-}
 type CoProducer (p :: * -> * -> * -> * -> (* -> *) -> * -> *) a' = p a' () () C
 
 {-| A 'CoConsumer' that consumes values flowing upstream
 
-    'CoConsumer's never 'request'. -}
+    'CoConsumer's never 'request'.
+-}
 type CoConsumer (p :: * -> * -> * -> * -> (* -> *) -> * -> *) b' = p C () b' ()
 
 {-| @Server b' b@ receives requests of type @b'@ and sends responses of type
     @b@.
 
-    'Server's never 'request'. -}
+    'Server's never 'request'.
+-}
 type Server (p :: * -> * -> * -> * -> (* -> *) -> * -> *) b' b = p C () b' b
 
 {-| @Client a' a@ sends requests of type @a'@ and receives responses of
     type @a@.
 
-    'Client's never 'respond'. -}
+    'Client's never 'respond'.
+-}
 type Client (p :: * -> * -> * -> * -> (* -> *) -> * -> *) a' a = p a' a () C
 
-{-| A self-contained 'Session', ready to be run by 'runSession'
+{-| A self-contained 'Session', ready to be run by 'runProxy'
 
-    'Session's never 'request' or 'respond'. -}
+    'Session's never 'request' or 'respond'.
+-}
 type Session (p :: * -> * -> * -> * -> (* -> *) -> * -> *) = p C () () C
-
--- | The empty type, denoting a \'@C@\'losed end
-data C = C -- Constructor not exported, but I include it to avoid EmptyDataDecls
diff --git a/Control/Proxy/Trans.hs b/Control/Proxy/Trans.hs
--- a/Control/Proxy/Trans.hs
+++ b/Control/Proxy/Trans.hs
@@ -14,7 +14,7 @@
     -- $laws
     ) where
 
-import Control.Proxy.Class
+import Control.Proxy.Class (Proxy)
 
 -- | Uniform interface to lifting proxies
 class ProxyTrans t where
@@ -27,6 +27,7 @@
 mapP :: (Monad m, Proxy p, ProxyTrans t)
      => (q -> p a' a b' b m r) -> (q -> t p a' a b' b m r)
 mapP = (liftP .)
+{-# INLINABLE mapP #-}
 
 {- $laws
      'mapP' defines a functor that preserves five categories:
diff --git a/Control/Proxy/Trans/Codensity.hs b/Control/Proxy/Trans/Codensity.hs
new file mode 100644
--- /dev/null
+++ b/Control/Proxy/Trans/Codensity.hs
@@ -0,0 +1,158 @@
+{-| This module provides the proxy transformer equivalent of 'CodensityT'.
+
+    The base 'Proxy' implementations suffer a quadratic time complexity if
+    you repeatedly left-associate the monad bind operation.  You can recover
+    linear time complexity just by adding 'runCodensityK' right after
+    'runProxy', which transforms the base 'Proxy' implementation to use
+    continuation-passing style:
+
+> -- Before:
+> runProxy $ ...
+>
+> -- After:
+> runProxy $ runCodensityK $ ...
+
+    Everything will still type-check if you you wrote your code to be
+    polymorphic over the base 'Proxy'.
+
+    Note that even though 'CodensityP' has better time complexity for
+    left-associated binds, it has worse constant factors for everything else
+    (about 6x slower on pure benchmarks), because:
+
+    * You cannot optimize it using rewrite rules
+
+    * It has a slower composition operation
+
+    So only use it if you actually need it, which is typically only the case if
+    you left associate your monad binds on the order of hundreds of times.  Even
+    better: only wrap the problematic portions of the pipeline in
+    'runCodensityK' so that the performance of the rest of the pipeline does not
+    suffer.
+-}
+
+{-# LANGUAGE KindSignatures, PolymorphicComponents #-}
+
+module Control.Proxy.Trans.Codensity (
+    -- * Codensity Proxy Transformer
+    CodensityP,
+    runCodensityP,
+    runCodensityK
+    ) where
+
+import Control.Applicative (Applicative(pure, (<*>)), Alternative(empty, (<|>)))
+import Control.Monad (MonadPlus(mzero, mplus))
+import Control.Monad.IO.Class (MonadIO(liftIO))
+import Control.Monad.Morph (MFunctor(hoist))
+import Control.Monad.Trans.Class (MonadTrans(lift))
+import Control.Proxy.Class (
+    Proxy(request, respond, (->>), (>>~)),
+    ProxyInternal(return_P, (?>=), lift_P, liftIO_P, hoist_P),
+    MonadPlusP(mzero_P, mplus_P) )
+import Control.Proxy.Morph (PFunctor(hoistP))
+import Control.Proxy.ListT (ListT((>\\), (//>)))
+import Control.Proxy.Trans (ProxyTrans(liftP))
+
+-- | The 'Codensity' proxy transformer
+newtype CodensityP p a' a b' b (m :: * -> *) r
+    = CodensityP { unCodensityP
+        :: forall x . (Monad m, Proxy p)
+         => (r -> p a' a b' b m x) -> p a' a b' b m x }
+{- The type class instances only satisfy their laws if you hide the constructor
+   for 'CodensityP'.
+
+   Normally you would not have to hide it and you could rely on parametricity to
+   guarantee that 'CodensityP p' is isomorphic to 'p'.  However, the 'MFunctor'
+   and 'PFunctor' type classes require including class constraints within the
+   constructor, which breaks parametricity and makes it possible to define
+   'CodensityP' values which break the laws for the following type class
+   instances.
+-}
+
+instance (Proxy p, Monad m) => Functor (CodensityP p a' a b' b m) where
+    fmap f p = CodensityP (\k ->
+        unCodensityP p    (\a ->
+        k (f a)) )
+
+instance (Proxy p, Monad m) => Applicative (CodensityP p a' a b' b m) where
+    pure = return
+    fp <*> xp = CodensityP (\k ->
+        unCodensityP fp    (\f ->
+        unCodensityP xp    (\x ->
+        k (f x) ) ) )
+
+instance (Proxy p, Monad m) => Monad (CodensityP p a' a b' b m) where
+    return = return_P
+    (>>=)  = (?>=)
+
+instance (Proxy p) => MonadTrans (CodensityP p a' a b' b) where
+    lift = lift_P
+
+instance (Proxy p) => MFunctor (CodensityP p a' a b' b) where
+    hoist = hoist_P
+
+instance (Proxy p, MonadIO m) => MonadIO (CodensityP p a' a b' b m) where
+    liftIO = liftIO_P
+
+instance (MonadPlusP p, Monad m) => Alternative (CodensityP p a' a b' b m) where
+    empty = mzero
+    (<|>) = mplus
+
+instance (MonadPlusP p, Monad m) => MonadPlus (CodensityP p a' a b' b m) where
+    mzero = mzero_P
+    mplus = mplus_P
+
+instance (Proxy p) => ProxyInternal (CodensityP p) where
+    return_P = \r -> CodensityP (\k -> k r)
+    m ?>= f  = CodensityP  (\k ->
+        unCodensityP  m    (\a ->
+        unCodensityP (f a)   k ) )
+
+    lift_P m = CodensityP (\k -> lift_P m ?>= k)
+
+    hoist_P nat p = CodensityP (\k ->
+        hoist_P nat (unCodensityP p return_P) ?>= k)
+
+    liftIO_P m = CodensityP (\k -> liftIO_P m ?>= k)
+
+instance (MonadPlusP p) => MonadPlusP (CodensityP p) where
+    mzero_P       = CodensityP (\_ -> mzero_P)
+    mplus_P m1 m2 = CodensityP (\k ->
+        mplus_P (unCodensityP m1 k) (unCodensityP m2 k) )
+
+instance (Proxy p) => Proxy (CodensityP p) where
+    fb' ->> p = CodensityP (\k ->
+        ((\b' -> unCodensityP (fb' b') return_P) ->> unCodensityP p return_P)
+            ?>= k )
+    p >>~ fb  = CodensityP (\k ->
+        (unCodensityP p return_P >>~ (\b -> unCodensityP (fb b) return_P))
+            ?>= k )
+    request = \a' -> CodensityP (\k -> request a' ?>= k)
+    respond = \b  -> CodensityP (\k -> respond b  ?>= k)
+
+instance (ListT p) => ListT (CodensityP p) where
+    fb' >\\ p = CodensityP (\k ->
+        ((\b' -> unCodensityP (fb' b') return_P) >\\ unCodensityP p return_P)
+            ?>= k )
+    p //> fb  = CodensityP (\k ->
+        (unCodensityP p return_P //> (\b -> unCodensityP (fb b) return_P))
+            ?>= k )
+
+instance ProxyTrans CodensityP where
+    liftP p = CodensityP (\k -> p ?>= k)
+
+instance PFunctor CodensityP where
+    hoistP nat p = CodensityP (\k -> nat (unCodensityP p return_P) ?>= k)
+
+-- | Run a 'CodensityP' proxy, converting, converting it back to the base proxy
+runCodensityP
+    :: (Monad m, Proxy p) => CodensityP p a' a b' b m r -> p a' a b' b m r
+runCodensityP p = unCodensityP p return_P
+{-# INLINABLE runCodensityP #-}
+
+{-| Run a 'CodensityP' \'@K@\'leisli arrow, converting it back to the base proxy
+-}
+runCodensityK
+    :: (Monad m, Proxy p)
+    => (q -> CodensityP p a' a b' b m r) -> (q -> p a' a b' b m r)
+runCodensityK k q = runCodensityP (k q)
+{-# INLINABLE runCodensityK #-}
diff --git a/Control/Proxy/Trans/Either.hs b/Control/Proxy/Trans/Either.hs
--- a/Control/Proxy/Trans/Either.hs
+++ b/Control/Proxy/Trans/Either.hs
@@ -6,45 +6,49 @@
     -- * EitherP
     EitherP(..),
     runEitherK,
+
     -- * Either operations
     left,
     right,
+
     -- * Symmetric monad
     -- $symmetry
     throw,
     catch,
-    handle
+    handle,
+    fmapL
     ) where
 
 import Control.Applicative (Applicative(pure, (<*>)), Alternative(empty, (<|>)))
 import Control.Monad (MonadPlus(mzero, mplus))
 import Control.Monad.IO.Class (MonadIO(liftIO))
+import Control.Monad.Morph (MFunctor(hoist))
 import Control.Monad.Trans.Class (MonadTrans(lift))
-import Control.MFunctor (MFunctor(hoist))
-import Control.PFunctor (PFunctor(hoistP))
-import Control.Proxy.Class
+import Control.Proxy.Class (
+    Proxy(request, respond, (->>), (>>~)),
+    ProxyInternal(return_P, (?>=), lift_P, liftIO_P, hoist_P),
+    MonadPlusP(mzero_P, mplus_P) )
+import Control.Proxy.Morph (PFunctor(hoistP), PMonad(embedP))
 import Control.Proxy.Trans (ProxyTrans(liftP))
 #if MIN_VERSION_base(4,6,0)
 #else
 import Prelude hiding (catch)
 #endif
+import Data.Monoid (Monoid(mempty, mappend))
 
 -- | The 'Either' proxy transformer
 newtype EitherP e p a' a b' b (m :: * -> *) r
-  = EitherP { runEitherP :: p a' a b' b m (Either e r) }
+    = EitherP { runEitherP :: p a' a b' b m (Either e r) }
 
-instance (Proxy              p, Monad m)
-       => Functor (EitherP e p a' a b' b m) where
+instance (Proxy p, Monad m) => Functor (EitherP e p a' a b' b m) where
     fmap f p = EitherP (
         runEitherP p ?>= \e ->
         return_P (case e of
             Left  l -> Left l
             Right r -> Right (f r) ) )
- -- fmap f = EitherP . liftM (fmap f) . runEitherP
 
-instance (Proxy                  p, Monad m)
-       => Applicative (EitherP e p a' a b' b m) where
-    pure = return
+instance (Proxy p, Monad m) => Applicative (EitherP e p a' a b' b m) where
+    pure      = return
     fp <*> xp = EitherP (
         runEitherP fp ?>= \e1 ->
         case e1 of
@@ -54,93 +58,91 @@
                  return_P (case e2 of
                       Left l  -> Left  l
                       Right x -> Right (f x) ) )
- -- fp <*> xp = EitherP ((<*>) <$> (runEitherP fp) <*> (runEitherP xp))
 
-instance (Proxy            p, Monad m)
-       => Monad (EitherP e p a' a b' b m) where
+instance (Proxy p, Monad m) => Monad (EitherP e p a' a b' b m) where
     return = return_P
-    (>>=) = (?>=)
+    (>>=)  = (?>=)
 
-instance (MonadPlusP             p, Monad m)
+instance (Proxy p) => MonadTrans (EitherP e p a' a b' b) where
+    lift = lift_P
+
+instance (Proxy p) => MFunctor (EitherP e p a' a b' b) where
+    hoist = hoist_P
+
+instance (Proxy p, MonadIO m) => MonadIO (EitherP e p a' a b' b m) where
+    liftIO = liftIO_P
+
+instance (Proxy p, Monad m, Monoid e)
        => Alternative (EitherP e p a' a b' b m) where
     empty = mzero
     (<|>) = mplus
 
-instance (MonadPlusP            p )
-       => MonadPlusP (EitherP e p) where
-    mzero_P = EitherP mzero_P
-    mplus_P m1 m2 = EitherP (mplus_P (runEitherP m1) (runEitherP m2))
-
-instance (MonadPlusP           p, Monad m)
+instance (Proxy p, Monad m, Monoid e)
        => MonadPlus (EitherP e p a' a b' b m) where
     mzero = mzero_P
     mplus = mplus_P
 
-instance (Proxy                 p )
-       => MonadTrans (EitherP e p a' a b' b) where
-    lift = lift_P
-
-instance (MonadIOP            p )
-       => MonadIOP (EitherP e p) where
-    liftIO_P m = EitherP (liftIO_P (m >>= \x -> return (Right x)))
- -- liftIO = EitherP . liftIO . liftM Right
-
-instance (MonadIOP           p, MonadIO m)
-       => MonadIO (EitherP e p a' a b' b m) where
-    liftIO = liftIO_P
+instance (Proxy p) => ProxyInternal (EitherP e p) where
+    return_P = \r -> EitherP (return_P (Right r))
+    m ?>= f = EitherP (
+        runEitherP m ?>= \e ->
+        case e of
+            Left  l -> return_P (Left l)
+            Right r -> runEitherP (f r) )
 
-instance (Proxy               p )
-       => MFunctor (EitherP e p a' a b' b) where
-    hoist = hoist_P
+    lift_P m = EitherP (lift_P (m >>= \x -> return (Right x)))
 
-instance (Proxy            p )
-       => Proxy (EitherP e p) where
-    p1 >-> p2 = \c'1 -> EitherP (
-        ((\b' -> runEitherP (p1 b')) >-> (\c'2 -> runEitherP (p2 c'2))) c'1 )
- -- p1 >-> p2 = (EitherP .) $ runEitherP . p1 >-> runEitherP . p2
+    hoist_P nat p = EitherP (hoist_P nat (runEitherP p))
 
-    p1 >~> p2 = \c'1 -> EitherP (
-        ((\b' -> runEitherP (p1 b')) >~> (\c'2 -> runEitherP (p2 c'2))) c'1 )
- -- p1 >~> p2 = (EitherP .) $ runEitherP . p1 >~> runEitherP . p2
+    liftIO_P m = EitherP (liftIO_P (m >>= \x -> return (Right x)))
 
+instance (Proxy p) => Proxy (EitherP e p) where
+    fb' ->> p = EitherP ((\b' -> runEitherP (fb' b')) ->> runEitherP p)
+    p >>~ fb  = EitherP (runEitherP p >>~ (\b -> runEitherP (fb b)))
     request = \a' -> EitherP (request a' ?>= \a  -> return_P (Right a ))
     respond = \b  -> EitherP (respond b  ?>= \b' -> return_P (Right b'))
 
-    return_P = right
-    m ?>= f = EitherP (
-        runEitherP m ?>= \e ->
-        runEitherP (case e of
-            Left  l -> left l
-            Right r -> f    r ) )
-
-    lift_P m = EitherP (lift_P (m >>= \x -> return (Right x)))
- -- lift = EitherP . lift . liftM Right
-
-    hoist_P nat p = EitherP (hoist_P nat (runEitherP p))
- -- hoist nat = EitherP . hoist nat . runEitherP
+instance (Proxy p, Monoid e) => MonadPlusP (EitherP e p) where
+    mzero_P = EitherP (return_P (Left mempty))
+    mplus_P p1 p2 = EitherP (
+        runEitherP p1 ?>= \e1 ->
+        case e1 of
+            Right r  -> return_P (Right r)
+            Left  l1 ->
+                runEitherP p2 ?>= \e2 ->
+                case e2 of
+                    Right r  -> return_P (Right r)
+                    Left  l2 -> return_P (Left (mappend l1 l2)) )
 
 instance ProxyTrans (EitherP e) where
     liftP p = EitherP (p ?>= \x -> return_P (Right x))
- -- liftP = EitherP . liftM Right
 
 instance PFunctor (EitherP e) where
-    hoistP nat = EitherP . nat . runEitherP
+    hoistP nat p = EitherP (nat (runEitherP p))
 
+instance PMonad (EitherP e) where
+    embedP nat p = EitherP (
+        runEitherP (nat (runEitherP p)) ?>= \x ->
+        return_P (case x of
+            Left         e  -> Left e
+            Right (Left  e) -> Left e
+            Right (Right a) -> Right a ) )
+
 -- | Run an 'EitherP' \'@K@\'leisi arrow, returning either a 'Left' or 'Right'
 runEitherK
- :: (q -> EitherP e p a' a b' b m r) -> (q -> p a' a b' b m (Either e r))
+    :: (q -> EitherP e p a' a b' b m r) -> (q -> p a' a b' b m (Either e r))
 runEitherK p q = runEitherP (p q)
--- runEitherK = (runEitherP .)
+{-# INLINABLE runEitherK #-}
 
 -- | Abort the computation and return a 'Left' result
 left :: (Monad m, Proxy p) => e -> EitherP e p a' a b' b m r
 left e = EitherP (return_P (Left e))
--- left = EitherP . return . Left
+{-# INLINABLE left #-}
 
 -- | Synonym for 'return'
 right :: (Monad m, Proxy p) => r -> EitherP e p a' a b' b m r
 right r = EitherP (return_P (Right r))
--- right = EitherP . return . Right
+{-# INLINABLE right #-}
 
 {- $symmetry
     'EitherP' forms a second symmetric monad over the left type variable.
@@ -161,24 +163,33 @@
 -- | Synonym for 'left'
 throw :: (Monad m, Proxy p) => e -> EitherP e p a' a b' b m r
 throw = left
+{-# INLINABLE throw #-}
 
 -- | Resume from an aborted operation
 catch
- :: (Monad m, Proxy p)
- => EitherP e p a' a b' b m r        -- ^ Original computation
- -> (e -> EitherP f p a' a b' b m r) -- ^ Handler
- -> EitherP f p a' a b' b m r        -- ^ Handled computation
+    :: (Monad m, Proxy p)
+    => EitherP e p a' a b' b m r        -- ^ Original computation
+    -> (e -> EitherP f p a' a b' b m r) -- ^ Handler
+    -> EitherP f p a' a b' b m r        -- ^ Handled computation
 catch m f = EitherP (
     runEitherP m ?>= \e ->
     runEitherP (case e of
         Left  l -> f     l
         Right r -> right r ))
+{-# INLINABLE catch #-}
 
 -- | 'catch' with the arguments flipped
 handle
- :: (Monad m, Proxy p)
- => (e -> EitherP f p a' a b' b m r) -- ^ Handler
- -> EitherP e p a' a b' b m r        -- ^ Original computation
- -> EitherP f p a' a b' b m r        -- ^ Handled computation
+    :: (Monad m, Proxy p)
+    => (e -> EitherP f p a' a b' b m r) -- ^ Handler
+    -> EitherP e p a' a b' b m r        -- ^ Original computation
+    -> EitherP f p a' a b' b m r        -- ^ Handled computation
 handle f m = catch m f
--- handle = flip catch
+{-# INLINABLE handle #-}
+
+-- | 'fmap' over the \'@L@\'eft variable
+fmapL
+    :: (Monad m, Proxy p)
+    => (e -> f) -> EitherP e p a' a b' b m r -> EitherP f p a' a b' b m r
+fmapL f p = catch p (\e -> throw (f e))
+{-# INLINABLE fmapL #-}
diff --git a/Control/Proxy/Trans/Identity.hs b/Control/Proxy/Trans/Identity.hs
--- a/Control/Proxy/Trans/Identity.hs
+++ b/Control/Proxy/Trans/Identity.hs
@@ -12,125 +12,94 @@
 import Control.Applicative (Applicative(pure, (<*>)), Alternative(empty, (<|>)))
 import Control.Monad (MonadPlus(mzero, mplus))
 import Control.Monad.IO.Class (MonadIO(liftIO))
+import Control.Monad.Morph (MFunctor(hoist))
 import Control.Monad.Trans.Class (MonadTrans(lift))
-import Control.MFunctor (MFunctor(hoist))
-import Control.PFunctor (PFunctor(hoistP))
-import Control.Proxy.Class
+import Control.Proxy.Class (
+    Proxy(request, respond, (->>), (>>~)),
+    ProxyInternal(return_P, (?>=), lift_P, liftIO_P, hoist_P),
+    MonadPlusP(mzero_P, mplus_P) )
+import Control.Proxy.Morph (PFunctor(hoistP), PMonad(embedP))
+import Control.Proxy.ListT (ListT((>\\), (//>)))
 import Control.Proxy.Trans (ProxyTrans(liftP))
 
 -- | The 'Identity' proxy transformer
-newtype IdentityP p a' a b' b (m :: * -> *) r =
-    IdentityP { runIdentityP :: p a' a b' b m r }
-
-instance (Proxy              p, Monad m)
-       => Functor (IdentityP p a' a b' b m) where
+newtype IdentityP p a' a b' b (m :: * -> *) r
+    = IdentityP { runIdentityP :: p a' a b' b m r } 
+instance (Proxy p, Monad m) => Functor (IdentityP p a' a b' b m) where
     fmap f p = IdentityP (
         runIdentityP p ?>= \x ->
         return_P (f x) )
- -- fmap = liftM
 
-instance (Proxy                  p, Monad m)
-       => Applicative (IdentityP p a' a b' b m) where
-    pure = return
-
+instance (Proxy p, Monad m) => Applicative (IdentityP p a' a b' b m) where
+    pure      = return
     fp <*> xp = IdentityP (
         runIdentityP fp ?>= \f ->
         runIdentityP xp ?>= \x ->
         return_P (f x) )
- -- fp <*> xp = ap
 
-instance (Proxy            p, Monad m)
-       => Monad (IdentityP p a' a b' b m) where
+instance (Proxy p, Monad m) => Monad (IdentityP p a' a b' b m) where
     return = return_P
-    (>>=) = (?>=)
-
-instance (MonadPlusP             p, Monad m)
-       => Alternative (IdentityP p a' a b' b m) where
-    empty = mzero
-    (<|>) = mplus
-
-instance (MonadPlusP            p )
-       => MonadPlusP (IdentityP p) where
-    mzero_P = IdentityP mzero_P
-    mplus_P m1 m2 = IdentityP (mplus_P (runIdentityP m1) (runIdentityP m2))
-
-instance (MonadPlusP           p, Monad m)
-       => MonadPlus (IdentityP p a' a b' b m) where
-    mzero = mzero_P
-    mplus = mplus_P
+    (>>=)  = (?>=)
 
-instance (Proxy                 p )
-       => MonadTrans (IdentityP p a' a b' b) where
+instance (Proxy p) => MonadTrans (IdentityP p a' a b' b) where
     lift = lift_P
 
-instance (MonadIOP            p )
-       => MonadIOP (IdentityP p) where
-    liftIO_P m = IdentityP (liftIO_P m)
- -- liftIO = IdentityP . liftIO
-
-instance (MonadIOP           p, MonadIO m)
-       => MonadIO (IdentityP p a' a b' b m) where
-    liftIO = liftIO_P
-
-instance (Proxy               p )
-       => MFunctor (IdentityP p a' a b' b) where
+instance (Proxy p) => MFunctor (IdentityP p a' a b' b) where
     hoist = hoist_P
 
-instance (Proxy            p )
-       => Proxy (IdentityP p) where
-    p1 >-> p2 = \c'1 -> IdentityP (
-        ((\c'2 -> runIdentityP (p1 c'2))
-     >-> (\b'  -> runIdentityP (p2 b' )) ) c'1 )
- -- p1 >-> p2 = (IdentityP .) $ runIdentityP . p1 >-> runIdentityP . p2
-
-    p1 >~> p2 = \c'1 -> IdentityP (
-        ((\c'2 -> runIdentityP (p1 c'2))
-     >~> (\b'  -> runIdentityP (p2 b' )) ) c'1 )
- -- p1 >~> p2 = (IdentityP .) $ runIdentityP . p1 >~> runIdentityP . p2
+instance (Proxy p, MonadIO m) => MonadIO (IdentityP p a' a b' b m) where
+    liftIO = liftIO_P
 
-    request = \a' -> IdentityP (request a')
- -- request = P . request
+instance (MonadPlusP p, Monad m) => Alternative (IdentityP p a' a b' b m) where
+    empty = mzero
+    (<|>) = mplus
 
-    respond = \b -> IdentityP (respond b)
- -- respond = P . respond
+instance (MonadPlusP p, Monad m) => MonadPlus (IdentityP p a' a b' b m) where
+    mzero = mzero_P
+    mplus = mplus_P
 
+instance (Proxy p) => ProxyInternal (IdentityP p) where
     return_P = \r -> IdentityP (return_P r)
- -- return = P . return
-
-    m ?>= f = IdentityP (
+    m ?>= f  = IdentityP (
         runIdentityP m ?>= \x ->
         runIdentityP (f x) )
 
     lift_P m = IdentityP (lift_P m)
- -- lift = P . lift
 
     hoist_P nat p = IdentityP (hoist_P nat (runIdentityP p))
- -- hoist nat = IdentityP . hoist nat . runIdentityP
 
-instance (Interact            p )
-      =>  Interact (IdentityP p) where
-    p1 \>\ p2 = \c'1 -> IdentityP (
-        ((\b'  -> runIdentityP (p1 b' ))
-     \>\ (\c'2 -> runIdentityP (p2 c'2)) ) c'1 )
- -- p1 \>\ p2 = (IdentityP .) $ runIdentityP . p1 \>\ runIdentityP . p2
+    liftIO_P m = IdentityP (liftIO_P m)
 
-    p1 />/ p2 = \a1 -> IdentityP (
-        ((\a2 -> runIdentityP (p1 a2))
-     />/ (\b  -> runIdentityP (p2 b )) ) a1 )
- -- p1 />/ p2 = (IdentityP .) $ runIdentityP . p1 />/ runIdentityP . p2
+instance (Proxy p) => Proxy (IdentityP p) where
+    fb' ->> p = IdentityP ((\b' -> runIdentityP (fb' b')) ->> runIdentityP p)
+    p >>~ fb  = IdentityP (runIdentityP p >>~ (\b -> runIdentityP (fb b)))
 
+    request = \a' -> IdentityP (request a')
+    respond = \b  -> IdentityP (respond b )
+
+instance (ListT p) => ListT (IdentityP p) where
+    fb' >\\ p = IdentityP ((\b' -> runIdentityP (fb' b')) >\\ runIdentityP p)
+    p //> fb  = IdentityP (runIdentityP p //> (\b -> runIdentityP (fb b)))
+
+instance (MonadPlusP p) => MonadPlusP (IdentityP p) where
+    mzero_P       = IdentityP  mzero_P
+    mplus_P m1 m2 = IdentityP (mplus_P (runIdentityP m1) (runIdentityP m2))
+
 instance ProxyTrans IdentityP where
     liftP = IdentityP
 
 instance PFunctor IdentityP where
-    hoistP nat = IdentityP . nat . runIdentityP
+    hoistP nat p = IdentityP (nat (runIdentityP p))
 
+instance PMonad IdentityP where
+    embedP nat p = nat (runIdentityP p)
+
 -- | Wrap a \'@K@\'leisli arrow in 'IdentityP'
 identityK :: (q -> p a' a b' b m r) -> (q -> IdentityP p a' a b' b m r)
 identityK k q = IdentityP (k q)
--- identityK = (IdentityP .)
+{-# INLINABLE identityK #-}
 
 -- | Run an 'P' \'@K@\'leisli arrow
 runIdentityK :: (q -> IdentityP p a' a b' b m r) -> (q -> p a' a b' b m r)
 runIdentityK k q = runIdentityP (k q)
--- runIdentityK = (runIdentityP .)
+{-# INLINABLE runIdentityK #-}
diff --git a/Control/Proxy/Trans/Maybe.hs b/Control/Proxy/Trans/Maybe.hs
--- a/Control/Proxy/Trans/Maybe.hs
+++ b/Control/Proxy/Trans/Maybe.hs
@@ -6,6 +6,7 @@
     -- * MaybeP
     MaybeP(..),
     runMaybeK,
+
     -- * Maybe operations
     nothing,
     just
@@ -14,29 +15,28 @@
 import Control.Applicative (Applicative(pure, (<*>)), Alternative(empty, (<|>)))
 import Control.Monad (MonadPlus(mzero, mplus))
 import Control.Monad.IO.Class (MonadIO(liftIO))
+import Control.Monad.Morph (MFunctor(hoist))
 import Control.Monad.Trans.Class (MonadTrans(lift))
-import Control.MFunctor (MFunctor(hoist))
-import Control.PFunctor (PFunctor(hoistP))
-import Control.Proxy.Class
+import Control.Proxy.Class (
+    Proxy(request, respond, (->>), (>>~)),
+    ProxyInternal(return_P, (?>=), lift_P, liftIO_P, hoist_P),
+    MonadPlusP(mzero_P, mplus_P) )
+import Control.Proxy.Morph (PFunctor(hoistP), PMonad(embedP))
 import Control.Proxy.Trans (ProxyTrans(liftP))
 
 -- | The 'Maybe' proxy transformer
 newtype MaybeP p a' a b' b (m :: * -> *) r
-  = MaybeP { runMaybeP :: p a' a b' b m (Maybe r) }
+    = MaybeP { runMaybeP :: p a' a b' b m (Maybe r) }
 
-instance (Proxy           p, Monad m)
-       => Functor (MaybeP p a' a b' b m) where
+instance (Proxy p, Monad m) => Functor (MaybeP p a' a b' b m) where
     fmap f p = MaybeP (
         runMaybeP p ?>= \m ->
         return_P (case m of
             Nothing -> Nothing
             Just x  -> Just (f x) ) )
- -- fmap f = MaybeP . fmap (fmap f) . runMaybeP
 
-instance (Proxy               p, Monad m)
-       => Applicative (MaybeP p a' a b' b m) where
-    pure = return
-
+instance (Proxy p, Monad m) => Applicative (MaybeP p a' a b' b m) where
+    pure      = return
     fp <*> xp = MaybeP (
         runMaybeP fp ?>= \m1 ->
         case m1 of
@@ -44,93 +44,83 @@
             Just f  ->
                 runMaybeP xp ?>= \m2 ->
                 case m2 of
-                    Nothing -> return_P Nothing
+                    Nothing -> return_P  Nothing
                     Just x  -> return_P (Just (f x)) )
- -- fp <*> xp = MaybeP ((<*>) <$> (runMaybeP fp) <*> (runMaybeP xp))
 
-instance (Proxy         p, Monad m)
-       => Monad (MaybeP p a' a b' b m) where
+instance (Proxy p, Monad m) => Monad (MaybeP p a' a b' b m) where
     return = return_P
     (>>=)  = (?>=)
 
-instance (Proxy               p, Monad m)
-       => Alternative (MaybeP p a' a b' b m) where
-    empty = mzero
-    (<|>) = mplus
-
-instance (Proxy              p )
-       => MonadPlusP (MaybeP p) where
-    mzero_P = nothing
-    mplus_P m1 m2 = MaybeP (
-        runMaybeP m1 ?>= \ma ->
-        runMaybeP (case ma of
-            Nothing -> m2
-            Just a  -> just a ) )
-
-instance (Proxy             p, Monad m)
-       => MonadPlus (MaybeP p a' a b' b m) where
-    mzero = mzero_P
-    mplus = mplus_P
-
-instance (Proxy              p )
-       => MonadTrans (MaybeP p a' a b' b) where
+instance (Proxy p) => MonadTrans (MaybeP p a' a b' b) where
     lift = lift_P
 
-instance (MonadIOP         p )
-       => MonadIOP (MaybeP p) where
-    liftIO_P m = MaybeP (liftIO_P (m >>= \x -> return (Just x)))
- -- liftIO = MaybeP . liftIO . liftM Just
-
-instance (MonadIOP        p, MonadIO m)
-       => MonadIO (MaybeP p a' a b' b m) where
-    liftIO = liftIO_P
-
-instance (Proxy            p )
-       => MFunctor (MaybeP p a' a b' b) where
+instance (Proxy p) => MFunctor (MaybeP p a' a b' b) where
     hoist = hoist_P
 
-instance (Proxy         p )
-       => Proxy (MaybeP p) where
-    p1 >-> p2 = \c'1 -> MaybeP (
-        ((\b' -> runMaybeP (p1 b')) >-> (\c'2 -> runMaybeP (p2 c'2))) c'1 )
- -- p1 >-> p2 = (MaybeP .) $ runMaybeP . p1 >-> runMaybeP . p2
+instance (Proxy p, MonadIO m) => MonadIO (MaybeP p a' a b' b m) where
+    liftIO = liftIO_P
 
-    p1 >~> p2 = \c'1 -> MaybeP (
-        ((\b' -> runMaybeP (p1 b')) >~> (\c'2 -> runMaybeP (p2 c'2))) c'1 )
- -- p1 >~> p2 = (MaybeP .) $ runMaybeP . p1 >~> runMaybeP . p2
+instance (Proxy p, Monad m) => Alternative (MaybeP p a' a b' b m) where
+    empty = mzero
+    (<|>) = mplus
 
-    request = \a' -> MaybeP (request a' ?>= \a  -> return_P (Just a ))
-    respond = \b  -> MaybeP (respond b  ?>= \b' -> return_P (Just b'))
+instance (Proxy p, Monad m) => MonadPlus (MaybeP p a' a b' b m) where
+    mzero = mzero_P
+    mplus = mplus_P
 
-    return_P = just
-    m ?>= f = MaybeP (
+instance (Proxy p) => ProxyInternal (MaybeP p) where
+    return_P = \r -> MaybeP (return_P (Just r))
+    m ?>= f  = MaybeP (
         runMaybeP m ?>= \ma ->
         runMaybeP (case ma of
-            Nothing -> nothing
+            Nothing -> MaybeP (return_P Nothing)
             Just a  -> f a ) )
 
     lift_P m = MaybeP (lift_P (m >>= \x -> return (Just x)))
- -- lift = MaybeP . lift . liftM Just
 
     hoist_P nat p = MaybeP (hoist_P nat (runMaybeP p))
- -- hoist nat = MaybeP . hoist nat . runMaybeP
 
+    liftIO_P m = MaybeP (liftIO_P (m >>= \x -> return (Just x)))
+
+instance (Proxy p) => Proxy (MaybeP p) where
+    fb' ->> p = MaybeP ((\b' -> runMaybeP (fb' b')) ->> runMaybeP p)
+    p >>~ fb  = MaybeP (runMaybeP p >>~ (\b -> runMaybeP (fb b)))
+    request = \a' -> MaybeP (request a' ?>= \a  -> return_P (Just a ))
+    respond = \b  -> MaybeP (respond b  ?>= \b' -> return_P (Just b'))
+
+instance (Proxy p) => MonadPlusP (MaybeP p) where
+    mzero_P       = MaybeP (return_P Nothing)
+    mplus_P m1 m2 = MaybeP (
+        runMaybeP m1 ?>= \ma ->
+        case ma of
+            Nothing -> runMaybeP m2
+            Just a  -> return_P (Just a) )
+
 instance ProxyTrans MaybeP where
     liftP p = MaybeP (p ?>= \x -> return_P (Just x))
- -- liftP = MaybeP . liftM Just
 
 instance PFunctor MaybeP where
-    hoistP nat = MaybeP . nat . runMaybeP
+    hoistP nat p = MaybeP (nat (runMaybeP p))
 
+instance PMonad MaybeP where
+    embedP nat p = MaybeP (
+        runMaybeP (nat (runMaybeP p)) ?>= \x ->
+        return_P (case x of
+            Nothing       -> Nothing
+            Just Nothing  -> Nothing
+            Just (Just a) -> Just a ) )
+
 -- | Run a 'MaybeP' \'@K@\'leisli arrow, returning the result or 'Nothing'
 runMaybeK :: (q -> MaybeP p a' a b' b m r) -> (q -> p a' a b' b m (Maybe r))
 runMaybeK p q = runMaybeP (p q)
--- runMaybeK = (runMaybeP .)
+{-# INLINABLE runMaybeK #-}
 
 -- | A synonym for 'mzero'
 nothing :: (Monad m, Proxy p) => MaybeP p a' a b' b m r
 nothing = MaybeP (return_P Nothing)
+{-# INLINABLE nothing #-}
 
 -- | A synonym for 'return'
 just :: (Monad m, Proxy p) => r -> MaybeP p a' a b' b m r
 just r = MaybeP (return_P (Just r))
+{-# INLINABLE just #-}
diff --git a/Control/Proxy/Trans/Reader.hs b/Control/Proxy/Trans/Reader.hs
--- a/Control/Proxy/Trans/Reader.hs
+++ b/Control/Proxy/Trans/Reader.hs
@@ -7,6 +7,7 @@
     ReaderP(..),
     runReaderP,
     runReaderK,
+
     -- * Reader operations
     ask,
     asks,
@@ -17,137 +18,115 @@
 import Control.Applicative (Applicative(pure, (<*>)), Alternative(empty, (<|>)))
 import Control.Monad (MonadPlus(mzero, mplus))
 import Control.Monad.IO.Class (MonadIO(liftIO))
+import Control.Monad.Morph (MFunctor(hoist))
 import Control.Monad.Trans.Class (MonadTrans(lift))
-import Control.MFunctor (MFunctor(hoist))
-import Control.PFunctor (PFunctor(hoistP))
-import Control.Proxy.Class
+import Control.Proxy.Class (
+    Proxy(request, respond, (->>), (>>~)),
+    ProxyInternal(return_P, (?>=), lift_P, liftIO_P, hoist_P),
+    MonadPlusP(mzero_P, mplus_P) )
+import Control.Proxy.Morph (PFunctor(hoistP), PMonad(embedP))
+import Control.Proxy.ListT (ListT((>\\), (//>)))
 import Control.Proxy.Trans (ProxyTrans(liftP))
 
 -- | The 'Reader' proxy transformer
 newtype ReaderP i p a' a b' b (m :: * -> *) r
-  = ReaderP { unReaderP :: i -> p a' a b' b m r }
+    = ReaderP { unReaderP :: i -> p a' a b' b m r }
 
-instance (Proxy              p, Monad m)
-       => Functor (ReaderP i p a' a b' b m) where
+instance (Proxy p, Monad m) => Functor (ReaderP i p a' a b' b m) where
     fmap f p = ReaderP (\i ->
         unReaderP p i ?>= \x ->
         return_P (f x) )
 
-instance (Proxy                  p, Monad m)
-       => Applicative (ReaderP i p a' a b' b m) where
+instance (Proxy p, Monad m) => Applicative (ReaderP i p a' a b' b m) where
     pure = return
     p1 <*> p2 = ReaderP (\i ->
         unReaderP p1 i ?>= \f -> 
         unReaderP p2 i ?>= \x -> 
         return_P (f x) )
 
-instance (Proxy            p, Monad m)
-       => Monad (ReaderP i p a' a b' b m) where
+instance (Proxy p, Monad m) => Monad (ReaderP i p a' a b' b m) where
     return = return_P
-    (>>=) = (?>=)
-
-instance (MonadPlusP             p, Monad m)
-       => Alternative (ReaderP i p a' a b' b m) where
-    empty = mzero
-    (<|>) = mplus
-
-instance (MonadPlusP           p )
-       => MonadPlusP (ReaderP i p) where
-    mzero_P = ReaderP (\_ -> mzero_P)
-    mplus_P m1 m2 = ReaderP (\i -> mplus_P (unReaderP m1 i) (unReaderP m2 i))
-
-instance (MonadPlusP           p, Monad m)
-       => MonadPlus (ReaderP i p a' a b' b m) where
-    mzero = mzero_P
-    mplus = mplus_P
+    (>>=)  = (?>=)
 
-instance (Proxy                 p )
-       => MonadTrans (ReaderP i p a' a b' b) where
+instance (Proxy p) => MonadTrans (ReaderP i p a' a b' b) where
     lift = lift_P
 
-instance (MonadIOP            p )
-       => MonadIOP (ReaderP i p) where
-    liftIO_P m = ReaderP (\_ -> liftIO_P m)
+instance (Proxy p) => MFunctor (ReaderP i p a' a b' b) where
+    hoist = hoist_P
 
-instance (MonadIOP           p, MonadIO m)
-       => MonadIO (ReaderP i p a' a b' b m) where
+instance (Proxy p, MonadIO m) => MonadIO (ReaderP i p a' a b' b m) where
     liftIO = liftIO_P
 
-instance (Proxy               p )
-       => MFunctor (ReaderP i p a' a b' b) where
-    hoist = hoist_P
-
-instance (Proxy            p  )
-       => Proxy (ReaderP i p) where
-    p1 >-> p2 = \c'1 -> ReaderP (\i ->
-        ((\b'  -> unReaderP (p1 b' ) i)
-     >-> (\c'2 -> unReaderP (p2 c'2) i) ) c'1 )
- {- p1 >-> p2 = \c' -> ReaderP $ \i ->
-        ((`unReaderP` i) . p1 >-> (`unReaderP` i) . p2) c' -}
+instance (MonadPlusP p, Monad m) => Alternative (ReaderP i p a' a b' b m) where
+    empty = mzero
+    (<|>) = mplus
 
-    p1 >~> p2 = \c'1 -> ReaderP (\i ->
-        ((\b'  -> unReaderP (p1 b' ) i)
-     >~> (\c'2 -> unReaderP (p2 c'2) i) ) c'1 )
- {- p1 >~> p2 = \c' -> ReaderP $ \i ->
-        ((`unReaderP` i) . p1 >~> (`unReaderP` i) . p2) c' -}
+instance (MonadPlusP p, Monad m) => MonadPlus (ReaderP i p a' a b' b m) where
+    mzero = mzero_P
+    mplus = mplus_P
 
+instance (Proxy p) => ProxyInternal (ReaderP i p) where
     return_P = \r -> ReaderP (\_ -> return_P r)
     m ?>= f  = ReaderP (\i ->
         unReaderP m i ?>= \a -> 
         unReaderP (f a) i )
 
-    request = \a -> ReaderP (\_ -> request a)
-    respond = \a -> ReaderP (\_ -> respond a)
-
     lift_P m = ReaderP (\_ -> lift_P m)
 
     hoist_P nat p = ReaderP (\i -> hoist_P nat (unReaderP p i))
- -- hoist_P nat = ReaderP . fmap (hoist_P nat) . unReaderP
 
-instance (Interact            p)
-       => Interact (ReaderP i p) where
-    p1 \>\ p2 = \c'1 -> ReaderP (\i ->
-        ((\b'  -> unReaderP (p1 b' ) i)
-     \>\ (\c'2 -> unReaderP (p2 c'2) i) ) c'1 )
- {- p1 \>\ p2 = \c' -> ReaderP $ \i ->
-        ((`unReaderP` i) . p1 \>\ (`unReaderP` i) . p2) c' -}
+    liftIO_P m = ReaderP (\_ -> liftIO_P m)
 
-    p1 />/ p2 = \a1 -> ReaderP (\i ->
-        ((\b  -> unReaderP (p1 b ) i)
-     />/ (\a2 -> unReaderP (p2 a2) i) ) a1 )
- {- p1 />/ p2 = \a -> ReaderP $ \i ->
-        ((`unReaderP` i) . p1 />/ (`unReaderP` i) . p2) a -}
+instance (Proxy p) => Proxy (ReaderP i p) where
+    fb' ->> p = ReaderP (\i -> (\b' -> unReaderP (fb' b') i) ->> unReaderP p i)
+    p >>~ fb  = ReaderP (\i -> unReaderP p i >>~ (\b -> unReaderP (fb b) i))
+    request = \a -> ReaderP (\_ -> request a)
+    respond = \a -> ReaderP (\_ -> respond a)
 
+instance (ListT p) => ListT (ReaderP i p) where
+    fb' >\\ p = ReaderP (\i -> (\b' -> unReaderP (fb' b') i) >\\ unReaderP p i)
+    p //> fb  = ReaderP (\i -> unReaderP p i //> (\b -> unReaderP (fb b) i))
+
+instance (MonadPlusP p) => MonadPlusP (ReaderP i p) where
+    mzero_P       = ReaderP (\_ -> mzero_P)
+    mplus_P m1 m2 = ReaderP (\i -> mplus_P (unReaderP m1 i) (unReaderP m2 i))
+
 instance ProxyTrans (ReaderP i) where
     liftP m = ReaderP (\_ -> m)
 
 instance PFunctor (ReaderP i) where
-    hoistP nat = ReaderP . (nat .) . unReaderP
+    hoistP nat p = ReaderP (\i -> nat (unReaderP p i))
 
+instance PMonad (ReaderP i) where
+    embedP nat p = ReaderP (\i -> unReaderP (nat (unReaderP p i)) i)
+
 -- | Run a 'ReaderP' computation, supplying the environment
 runReaderP :: i -> ReaderP i p a' a b' b m r -> p a' a b' b m r
 runReaderP i m = unReaderP m i
+{-# INLINABLE runReaderP #-}
 
 -- | Run a 'ReaderP' \'@K@\'leisli arrow, supplying the environment
 runReaderK :: i -> (q -> ReaderP i p a' a b' b m r) -> (q -> p a' a b' b m r)
 runReaderK i p q = runReaderP i (p q)
--- runReaderK i = (runReaderP i .)
+{-# INLINABLE runReaderK #-}
 
 -- | Get the environment
 ask :: (Proxy p, Monad m) => ReaderP i p a' a b' b m i
 ask = ReaderP return_P
+{-# INLINABLE ask #-}
 
 -- | Get a function of the environment
 asks :: (Proxy p, Monad m) => (i -> r) -> ReaderP i p a' a b' b m r
 asks f = ReaderP (\i -> return_P (f i))
+{-# INLINABLE asks #-}
 
 -- | Modify a computation's environment (a specialization of 'withReaderP')
-local
- :: (i -> i) -> ReaderP i p a' a b' b m r -> ReaderP i p a' a b' b m r
+local :: (i -> i) -> ReaderP i p a' a b' b m r -> ReaderP i p a' a b' b m r
 local = withReaderP
+{-# INLINABLE local #-}
 
 -- | Modify a computation's environment (a more general version of 'local')
 withReaderP
- :: (j -> i) -> ReaderP i p a' a b' b m r -> ReaderP j p a' a b' b m r
+    :: (j -> i) -> ReaderP i p a' a b' b m r -> ReaderP j p a' a b' b m r
 withReaderP f p = ReaderP (\i -> unReaderP p (f i))
--- withReaderP f p = ReaderP $ unReaderP p . f
+{-# INLINABLE withReaderP #-}
diff --git a/Control/Proxy/Trans/State.hs b/Control/Proxy/Trans/State.hs
--- a/Control/Proxy/Trans/State.hs
+++ b/Control/Proxy/Trans/State.hs
@@ -11,6 +11,7 @@
     evalStateK,
     execStateP,
     execStateK,
+
     -- * State operations
     get,
     put,
@@ -21,83 +22,53 @@
 import Control.Applicative (Applicative(pure, (<*>)), Alternative(empty, (<|>)))
 import Control.Monad (MonadPlus(mzero, mplus))
 import Control.Monad.IO.Class (MonadIO(liftIO))
+import Control.Monad.Morph (MFunctor(hoist))
 import Control.Monad.Trans.Class (MonadTrans(lift))
-import Control.MFunctor (MFunctor(hoist))
-import Control.PFunctor (PFunctor(hoistP))
-import Control.Proxy.Class
+import Control.Proxy.Class (
+    Proxy(request, respond, (->>), (>>~)),
+    ProxyInternal(return_P, (?>=), lift_P, liftIO_P, hoist_P),
+    MonadPlusP(mzero_P, mplus_P) )
+import Control.Proxy.Morph (PFunctor(hoistP))
 import Control.Proxy.Trans (ProxyTrans(liftP))
 
 -- | The 'State' proxy transformer
 newtype StateP s p a' a b' b (m :: * -> *) r
-  = StateP { unStateP :: s -> p a' a b' b m (r, s) }
+    = StateP { unStateP :: s -> p a' a b' b m (r, s) }
 
-instance (Proxy             p, Monad m)
-       => Functor (StateP s p a' a b' b m) where
+instance (Proxy p, Monad m) => Functor (StateP s p a' a b' b m) where
        fmap f p = StateP (\s0 ->
            unStateP p s0 ?>= \(x, s1) ->
            return_P (f x, s1) )
 
-{- As far as I can tell, there is no way to write this using an Applicative
-   context -}
-instance (Proxy                 p, Monad m)
-       => Applicative (StateP s p a' a b' b m) where
-    pure = return
+instance (Proxy p, Monad m) => Applicative (StateP s p a' a b' b m) where
+    pure      = return
     p1 <*> p2 = StateP (\s0 ->
         unStateP p1 s0 ?>= \(f, s1) ->
         unStateP p2 s1 ?>= \(x, s2) ->
         return_P (f x, s2) )
 
-instance (Proxy           p, Monad m)
-       => Monad (StateP s p a' a b' b m) where
+instance (Proxy p, Monad m) => Monad (StateP s p a' a b' b m) where
     return = return_P
     (>>=)  = (?>=)
 
-instance (MonadPlusP            p, Monad m)
-       => Alternative (StateP s p a' a b' b m) where
-    empty = mzero
-    (<|>) = mplus
-
-instance (MonadPlusP           p )
-       => MonadPlusP (StateP s p) where
-    mzero_P       = StateP (\_ -> mzero_P)
-    mplus_P m1 m2 = StateP (\s -> mplus_P (unStateP m1 s) (unStateP m2 s))
-
-instance (MonadPlusP          p, Monad m)
-       => MonadPlus (StateP s p a' a b' b m) where
-    mzero = mzero_P
-    mplus = mplus_P
-
-instance (Proxy                p )
-       => MonadTrans (StateP s p a' a b' b) where
+instance (Proxy p) => MonadTrans (StateP s p a' a b' b) where
     lift = lift_P
 
-instance (MonadIOP           p )
-       => MonadIOP (StateP s p) where
-    liftIO_P m = StateP (\s -> liftIO_P (m >>= \r -> return (r, s)))
-
-instance (MonadIOP          p, MonadIO m)
-       => MonadIO (StateP s p a' a b' b m) where
-    liftIO = liftIO_P
-
-instance (Proxy              p )
-       => MFunctor (StateP s p a' a b' b) where
+instance (Proxy p) => MFunctor (StateP s p a' a b' b) where
     hoist = hoist_P
 
-instance (Proxy           p )
-       => Proxy (StateP s p) where
-    p1 >-> p2 = \c'1 -> StateP (\s ->
-        ((\b' -> unStateP (p1 b') s) >-> (\c'2 -> unStateP (p2 c'2) s)) c'1 )
- {- (p1 >-> p2) = \c' -> StateP $ \s ->
-        ((`unStateP` s) . p1 >-> (`unStateP` s) . p2) c' -}
+instance (Proxy p, MonadIO m) => MonadIO (StateP s p a' a b' b m) where
+    liftIO = liftIO_P
 
-    p1 >~> p2 = \c'1 -> StateP (\s ->
-        ((\b' -> unStateP (p1 b') s) >~> (\c'2 -> unStateP (p2 c'2) s)) c'1 )
- {- (p1 >~> p2) = \c' -> StateP $ \s ->
-        ((`unStateP` s) . p1 >~> (`unStateP` s) . p2) c' -}
+instance (MonadPlusP p, Monad m) => Alternative (StateP s p a' a b' b m) where
+    empty = mzero
+    (<|>) = mplus
 
-    request = \a' -> StateP (\s -> request a' ?>= \a  -> return_P (a , s))
-    respond = \b  -> StateP (\s -> respond b  ?>= \b' -> return_P (b', s))
+instance (MonadPlusP p, Monad m) => MonadPlus (StateP s p a' a b' b m) where
+    mzero = mzero_P
+    mplus = mplus_P
 
+instance (Proxy p) => ProxyInternal (StateP s p) where
     return_P = \r -> StateP (\s -> return_P (r, s))
     m ?>= f  = StateP (\s ->
         unStateP m s ?>= \(a, s') ->
@@ -106,61 +77,77 @@
     lift_P m = StateP (\s -> lift_P (m >>= \r -> return (r, s)))
 
     hoist_P nat p = StateP (\s -> hoist_P nat (unStateP p s))
- -- hoist nat = StateP . fmap (hoist nat) . unStateP
 
+    liftIO_P m = StateP (\s -> liftIO_P (m >>= \r -> return (r, s)))
+
+instance (Proxy p) => Proxy (StateP s p) where
+    fb' ->> p = StateP (\s -> (\b' -> unStateP (fb' b') s) ->> unStateP p s)
+    p >>~ fb  = StateP (\s -> unStateP p s >>~ (\b -> unStateP (fb b) s))
+    request = \a' -> StateP (\s -> request a' ?>= \a  -> return_P (a , s))
+    respond = \b  -> StateP (\s -> respond b  ?>= \b' -> return_P (b', s))
+
+instance (MonadPlusP p) => MonadPlusP (StateP s p) where
+    mzero_P       = StateP (\_ -> mzero_P)
+    mplus_P m1 m2 = StateP (\s -> mplus_P (unStateP m1 s) (unStateP m2 s))
+
 instance ProxyTrans (StateP s) where
     liftP m = StateP (\s -> m ?>= \r -> return_P (r, s))
 
 instance PFunctor (StateP s) where
-    hoistP nat = StateP . (nat .) . unStateP
+    hoistP nat p = StateP (\s -> nat (unStateP p s))
 
 -- | Run a 'StateP' computation, producing the final result and state
 runStateP :: s -> StateP s p a' a b' b m r -> p a' a b' b m (r, s)
 runStateP s m = unStateP m s
+{-# INLINABLE runStateP #-}
 
 -- | Run a 'StateP' \'@K@\'leisli arrow, procuding the final result and state
 runStateK :: s -> (q -> StateP s p a' a b' b m r) -> (q -> p a' a b' b m (r, s))
 runStateK s k q = unStateP (k q) s
--- runStateK s = (runStateP s .)
+{-# INLINABLE runStateK #-}
 
 -- | Evaluate a 'StateP' computation, but discard the final state
 evalStateP
- :: (Proxy p, Monad m) => s -> StateP s p a' a b' b m r -> p a' a b' b m r
+    :: (Proxy p, Monad m) => s -> StateP s p a' a b' b m r -> p a' a b' b m r
 evalStateP s p = unStateP p s ?>= \x -> return_P (fst x)
--- evalStateP s = liftM fst . runStateP s
+{-# INLINABLE evalStateP #-}
 
 -- | Evaluate a 'StateP' \'@K@\'leisli arrow, but discard the final state
 evalStateK
- :: (Proxy p, Monad m)
- => s -> (q -> StateP s p a' a b' b m r) -> (q -> p a' a b' b m r)
+    :: (Proxy p, Monad m)
+    => s -> (q -> StateP s p a' a b' b m r) -> (q -> p a' a b' b m r)
 evalStateK s k q = evalStateP s (k q)
--- evalStateK s = (evalStateP s .)
+{-# INLINABLE evalStateK #-}
 
 -- | Evaluate a 'StateP' computation, but discard the final result
 execStateP
- :: (Proxy p, Monad m) => s -> StateP s p a' a b' b m r -> p a' a b' b m s
+    :: (Proxy p, Monad m) => s -> StateP s p a' a b' b m r -> p a' a b' b m s
 execStateP s p = unStateP p s ?>= \x -> return_P (snd x)
--- execStateP s = liftM snd . runStateP s
+{-# INLINABLE execStateP #-}
 
 -- | Evaluate a 'StateP' \'@K@\'leisli arrow, but discard the final result
 execStateK
- :: (Proxy p, Monad m)
- => s -> (q -> StateP s p a' a b' b m r) -> (q -> p a' a b' b m s)
+    :: (Proxy p, Monad m)
+    => s -> (q -> StateP s p a' a b' b m r) -> (q -> p a' a b' b m s)
 execStateK s k q = execStateP s (k q)
--- execStateK s = (execStateP s .)
+{-# INLINABLE execStateK #-}
 
 -- | Get the current state
 get :: (Proxy p, Monad m) => StateP s p a' a b' b m s
 get = StateP (\s -> return_P (s, s))
+{-# INLINABLE get #-}
 
 -- | Set the current state
 put :: (Proxy p, Monad m) => s -> StateP s p a' a b' b m ()
 put s = StateP (\_ -> return_P ((), s))
+{-# INLINABLE put #-}
 
 -- | Modify the current state using a function
 modify :: (Proxy p, Monad m) => (s -> s) -> StateP s p a' a b' b m ()
 modify f = StateP (\s -> return_P ((), f s))
+{-# INLINABLE modify #-}
 
 -- | Get the state filtered through a function
 gets :: (Proxy p, Monad m) => (s -> r) -> StateP s p a' a b' b m r
 gets f = StateP (\s -> return_P (f s, s))
+{-# INLINABLE gets #-}
diff --git a/Control/Proxy/Trans/Writer.hs b/Control/Proxy/Trans/Writer.hs
--- a/Control/Proxy/Trans/Writer.hs
+++ b/Control/Proxy/Trans/Writer.hs
@@ -4,17 +4,20 @@
     being strict in the accumulated monoid. 
 
     The underlying implementation uses the state monad to avoid quadratic blowup
-    from left-associative binds. -}
+    from left-associative binds.
+-}
 
 {-# LANGUAGE KindSignatures #-}
 
 module Control.Proxy.Trans.Writer (
     -- * WriterP
-    WriterP(..),
+    WriterP,
+    writerP,
     runWriterP,
     runWriterK,
     execWriterP,
     execWriterK,
+
     -- * Writer operations
     tell,
     censor
@@ -23,83 +26,54 @@
 import Control.Applicative (Applicative(pure, (<*>)), Alternative(empty, (<|>)))
 import Control.Monad (MonadPlus(mzero, mplus))
 import Control.Monad.IO.Class (MonadIO(liftIO))
+import Control.Monad.Morph (MFunctor(hoist))
 import Control.Monad.Trans.Class (MonadTrans(lift))
-import Control.MFunctor (MFunctor(hoist))
-import Control.PFunctor (PFunctor(hoistP))
-import Control.Proxy.Class
+import Control.Proxy.Class (
+    Proxy(request, respond, (->>), (>>~)),
+    ProxyInternal(return_P, (?>=), lift_P, liftIO_P, hoist_P),
+    MonadPlusP(mzero_P, mplus_P) )
+import Control.Proxy.Morph (PFunctor(hoistP), PMonad(embedP))
 import Control.Proxy.Trans (ProxyTrans(liftP))
 import Data.Monoid (Monoid(mempty, mappend))
 
 -- | The strict 'Writer' proxy transformer
 newtype WriterP w p a' a b' b (m :: * -> *) r
-  = WriterP { unWriterP :: w -> p a' a b' b m (r, w) }
+    = WriterP { unWriterP :: w -> p a' a b' b m (r, w) }
 
-instance (Proxy              p, Monad m)
-       => Functor (WriterP w p a' a b' b m) where
+instance (Proxy p, Monad m) => Functor (WriterP w p a' a b' b m) where
     fmap f p = WriterP (\w0 ->
         unWriterP p w0 ?>= \(x, w1) ->
         return_P (f x, w1) )
 
-instance (Proxy                  p, Monad m)
-       => Applicative (WriterP w p a' a b' b m) where
-    pure = return
+instance (Proxy p, Monad m) => Applicative (WriterP w p a' a b' b m) where
+    pure      = return
     fp <*> xp = WriterP (\w0 ->
         unWriterP fp w0 ?>= \(f, w1) ->
         unWriterP xp w1 ?>= \(x, w2) ->
         return_P (f x, w2) )
- -- (<*>) = ap
 
-instance (Proxy            p, Monad m)
-       => Monad (WriterP w p a' a b' b m) where
+instance (Proxy p, Monad m) => Monad (WriterP w p a' a b' b m) where
     return = return_P
-    (>>=) = (?>=)
-
-instance (MonadPlusP             p, Monad m)
-       => Alternative (WriterP w p a' a b' b m) where
-    empty = mzero
-    (<|>) = mplus
-
-instance (MonadPlusP            p )
-       => MonadPlusP (WriterP w p) where
-    mzero_P       = WriterP (\_ -> mzero_P)
-    mplus_P m1 m2 = WriterP (\w -> mplus_P (unWriterP m1 w) (unWriterP m2 w))
-
-instance (MonadPlusP           p, Monad m)
-       => MonadPlus (WriterP w p a' a b' b m) where
-    mzero = mzero_P
-    mplus = mplus_P
+    (>>=)  = (?>=)
 
-instance (Proxy                 p )
-       => MonadTrans (WriterP w p a' a b' b) where
+instance (Proxy p) => MonadTrans (WriterP w p a' a b' b) where
     lift = lift_P
 
-instance (MonadIOP            p )
-       => MonadIOP (WriterP w p) where
-    liftIO_P m = WriterP (\w -> liftIO_P (m >>= \r -> return (r, w)))
-
-instance (MonadIOP           p, MonadIO m)
-       => MonadIO (WriterP w p a' a b' b m) where
-    liftIO = liftIO_P
-
-instance (Proxy               p )
-       => MFunctor (WriterP w p a' a b' b) where
+instance (Proxy p) => MFunctor (WriterP w p a' a b' b) where
     hoist = hoist_P
 
-instance (Proxy            p )
-       => Proxy (WriterP w p) where
-    p1 >-> p2 = \c'1 -> WriterP (\w ->
-        ((\b' -> unWriterP (p1 b') w) >-> (\c'2 -> unWriterP (p2 c'2) w)) c'1 )
- {- p1 >-> p2 = \c' -> WriterP $ \w ->
-        ((`unWriterP` w) . p1 >-> (`unWriterP` w) . p2) c' -}
+instance (Proxy p, MonadIO m) => MonadIO (WriterP w p a' a b' b m) where
+    liftIO = liftIO_P
 
-    p1 >~> p2 = \c'1 -> WriterP (\w ->
-        ((\b' -> unWriterP (p1 b') w) >~> (\c'2 -> unWriterP (p2 c'2) w)) c'1 )
- {- p1 >~> p2 = \c' -> WriterP $ \w ->
-        ((`unWriterP` w) . p1 >~> (`unWriterP` w) . p2) c' -}
+instance (MonadPlusP p, Monad m) => Alternative (WriterP w p a' a b' b m) where
+    empty = mzero
+    (<|>) = mplus
 
-    request = \a' -> WriterP (\w -> request a' ?>= \a  -> return_P (a,  w))
-    respond = \b  -> WriterP (\w -> respond b  ?>= \b' -> return_P (b', w))
+instance (MonadPlusP p, Monad m) => MonadPlus (WriterP w p a' a b' b m) where
+    mzero = mzero_P
+    mplus = mplus_P
 
+instance (Proxy p) => ProxyInternal (WriterP w p) where
     return_P = \r -> WriterP (\w -> return_P (r, w))
     m ?>= f  = WriterP (\w ->
         unWriterP m w ?>= \(a, w') ->
@@ -108,47 +82,76 @@
     lift_P m = WriterP (\w -> lift_P (m >>= \r -> return (r, w)))
 
     hoist_P nat p = WriterP (\w -> hoist_P nat (unWriterP p w))
- -- hoist_P nat = WriterP . fmap (hoist_P nat) . unWriterP
 
+    liftIO_P m = WriterP (\w -> liftIO_P (m >>= \r -> return (r, w)))
+
+instance (Proxy p) => Proxy (WriterP w p) where
+    fb' ->> p = WriterP (\w -> (\b' -> unWriterP (fb' b') w) ->> unWriterP p w)
+    p >>~ fb  = WriterP (\w -> unWriterP p w >>~ (\b -> unWriterP (fb b) w))
+    request = \a' -> WriterP (\w -> request a' ?>= \a  -> return_P (a,  w))
+    respond = \b  -> WriterP (\w -> respond b  ?>= \b' -> return_P (b', w))
+
+instance (MonadPlusP p) => MonadPlusP (WriterP w p) where
+    mzero_P       = WriterP (\_ -> mzero_P)
+    mplus_P m1 m2 = WriterP (\w -> mplus_P (unWriterP m1 w) (unWriterP m2 w))
+
 instance ProxyTrans (WriterP w) where
     liftP m = WriterP (\w -> m ?>= \r -> return_P (r, w))
 
 instance PFunctor (WriterP w) where
-    hoistP nat = WriterP . (nat .) . unWriterP
+    hoistP nat p = WriterP (\s -> nat (unWriterP p s))
 
+instance (Monoid w) => PMonad (WriterP w) where
+    embedP nat p = writerP (
+        runWriterP (nat (runWriterP p)) ?>= \((r, w1), w2) ->
+        return_P (r, mappend w1 w2) )
+
+-- | Create a 'WriterP' from a proxy that generates a result and a monoid
+writerP
+    :: (Monad m, Proxy p, Monoid w)
+    => p a' a b' b m (r, w) -> WriterP w p a' a b' b m r
+writerP p = WriterP (\w ->
+    p ?>= \(r, w') ->
+    let w'' = mappend w w'
+    in w'' `seq` return_P (r, w'') )
+{-# INLINABLE writerP #-}
+
 -- | Run a 'WriterP' computation, producing the final result and monoid
 runWriterP :: (Monoid w) => WriterP w p a' a b' b m r -> p a' a b' b m (r, w)
 runWriterP p = unWriterP p mempty
+{-# INLINABLE runWriterP #-}
 
 -- | Run a 'WriterP' \'@K@\'leisli arrow, producing the final result and monoid
 runWriterK
- :: (Monoid w)
- => (q -> WriterP w p a' a b' b m r) -> (q -> p a' a b' b m (r, w))
+    :: (Monoid w)
+    => (q -> WriterP w p a' a b' b m r) -> (q -> p a' a b' b m (r, w))
 runWriterK k q = runWriterP (k q)
--- runWriterK = (runWriterP . )
+{-# INLINABLE runWriterK #-}
 
 -- | Evaluate a 'WriterP' computation, but discard the final result
 execWriterP
- :: (Proxy p, Monad m, Monoid w)
- => WriterP w p a' a b' b m r -> p a' a b' b m w
+    :: (Proxy p, Monad m, Monoid w)
+    => WriterP w p a' a b' b m r -> p a' a b' b m w
 execWriterP m = runWriterP m ?>= \(_, w) -> return_P w
--- execWriterP m = liftM snd $ runWriterP m
+{-# INLINABLE execWriterP #-}
 
 -- | Evaluate a 'WriterP' \'@K@\'leisli arrow, but discard the final result
 execWriterK
- :: (Proxy p, Monad m, Monoid w)
- => (q -> WriterP w p a' a b' b m r) -> (q -> p a' a b' b m w)
+    :: (Proxy p, Monad m, Monoid w)
+    => (q -> WriterP w p a' a b' b m r) -> (q -> p a' a b' b m w)
 execWriterK k q= execWriterP (k q)
+{-# INLINABLE execWriterK #-}
 
 -- | Add a value to the monoid
 tell :: (Proxy p, Monad m, Monoid w) => w -> WriterP w p a' a b' b m ()
 tell w' = WriterP (\w -> let w'' = mappend w w' in w'' `seq` return_P ((), w''))
+{-# INLINABLE tell #-}
 
 -- | Modify the result of a writer computation
 censor
- :: (Proxy p, Monad m, Monoid w)
- => (w -> w) -> WriterP w p a' a b' b m r -> WriterP w p a' a b' b m r
+    :: (Proxy p, Monad m, Monoid w)
+    => (w -> w) -> WriterP w p a' a b' b m r -> WriterP w p a' a b' b m r
 censor f p = WriterP (\w0 ->
     unWriterP p w0 ?>= \(r, w1) ->
     return_P (r, f w1) )
--- censor f = WriterP . fmap (liftM (\(r, w) -> (r, f w))) . unWriterP
+{-# INLINABLE censor #-}
diff --git a/Control/Proxy/Tutorial.hs b/Control/Proxy/Tutorial.hs
--- a/Control/Proxy/Tutorial.hs
+++ b/Control/Proxy/Tutorial.hs
@@ -1,5 +1,8 @@
 {-| This module provides a brief introductory tutorial in the \"Introduction\"
     section followed by a lengthy discussion of the library's design and idioms.
+
+    I've condensed all the code examples into a self-contained code block in the
+    Appendix section that you can use to follow along.
 -}
 
 module Control.Proxy.Tutorial (
@@ -33,6 +36,9 @@
     -- * Mix Monads and Composition
     -- $mixmonadcomp
 
+    -- * ListT
+    -- $listT
+
     -- * Folds
     -- $folds
 
@@ -54,16 +60,25 @@
     -- * Proxy Transformers
     -- $proxytrans
 
+    -- * Proxy Morphism Laws
+    -- $proxymorph
+
+    -- * Functors on Proxies
+    -- $proxyfunctor
+
     -- * Conclusion
     -- $conclusion
+
+    -- * Appendix
+    -- $appendix
     ) where
 
 -- For documentation
-import Control.Category
-import Control.Monad.Trans.Class
-import Control.MFunctor
-import Control.PFunctor
+import Control.Category (Category)
+import Control.Monad.Morph (MFunctor(hoist))
+import Control.Monad.Trans.Class (MonadTrans(lift))
 import Control.Proxy
+import Control.Proxy.Morph
 import Control.Proxy.Core.Correct (ProxyCorrect)
 import Control.Proxy.Trans.Either
 
@@ -71,13 +86,13 @@
     The @pipes@ library replaces lazy 'IO' with a safe, elegant, and
     theoretically principled alternative.  Use this library if you:
 
-    * want to write high-performance streaming programs
+    * want to write high-performance streaming programs,
 
-    * believe that lazy 'IO' was a bad idea
+    * believe that lazy 'IO' was a bad idea,
 
-    * enjoy composing modular and reusable components
+    * enjoy composing modular and reusable components, or
 
-    * love theory and elegant code
+    * love theory and elegant code.
 
     This library unifies many kinds of streaming abstractions, all of which are
     special cases of \"proxies\" (The @pipes@ name is a legacy of one such
@@ -184,9 +199,9 @@
     intermediate 'Proxy' that behaves like a verbose 'take'.  I will call it a
     'Pipe' (this library's namesake) since values flow through it:
 
->                           'a's flow in ---+ +--- 'a's flow out
->                                           | |
->                                           v v
+> --                        'a's flow in ---+ +--- 'a's flow out
+> --                                        | |
+> --                                        v v
 > take' :: (Proxy p) => Int -> () -> Pipe p a a IO ()
 > take' n () = runIdentityP $ do
 >     replicateM_ n $ do
@@ -241,14 +256,14 @@
     sends three 'request's upstream, each of which provides an 'Int' @argument@
     and expects a 'Bool' @result@:
 
->                      Sends out 'Int's ---+   +-- Receives back 'Bool's
->                                          |   |
->                                          v   v
+> --                   Sends out 'Int's ---+   +-- Receives back 'Bool's
+> --                                       |   |
+> --                                       v   v
 > threeReqs :: (Proxy p) => () -> Client p Int Bool IO ()
 > threeReqs () = runIdentityP $ forM_ [1, 3, 1] $ \argument -> do
->     lift $ putStrLn $ "Client Sends:   " ++ show (argument :: Int)
+>     lift $ putStrLn $ "Client Sends:    " ++ show (argument :: Int)
 >     result <- request argument
->     lift $ putStrLn $ "Client Receives:" ++ show (result :: Bool)
+>     lift $ putStrLn $ "Client Receives: " ++ show (result :: Bool)
 >     lift $ putStrLn "*"
 
     Notice how 'Client's use \"@request argument@\" instead of
@@ -256,18 +271,18 @@
     'request'.
 
     'Server's similarly generalize 'Producer's because they receive arguments
-    other than @()@.  The following 'Server' receives 'Int' 'request's and
-    'respond's with 'Bool' values:
+    other than @()@.  The following 'Server' receives 'Int' requests and 
+    responds with 'Bool's:
 
->                       Receives 'Int's ---+   +--- Replies with 'Bool's
->                                          |   |
->                                          v   v
+> --                    Receives 'Int's ---+   +--- Replies with 'Bool's
+> --                                       |   |
+> --                                       v   v
 > comparer :: (Proxy p) => Int -> Server p Int Bool IO r
 > comparer = runIdentityK loop where
 >     loop argument = do
->         lift $ putStrLn $ "Server Receives:" ++ show (argument :: Int)
+>         lift $ putStrLn $ "Server Receives: " ++ show (argument :: Int)
 >         let result = argument > 2
->         lift $ putStrLn $ "Server Sends:   " ++ show (result :: Bool)
+>         lift $ putStrLn $ "Server Sends:    " ++ show (result :: Bool)
 >         nextArgument <- respond result
 >         loop nextArgument
 
@@ -287,9 +302,9 @@
     We can use this to simplify the @comparer@ 'Server':
 
 > comparer = runIdentityK $ foreverK $ \argument -> do
->     lift $ putStrLn $ "Server Receives:" ++ show argument
+>     lift $ putStrLn $ "Server Receives: " ++ show argument
 >     let result = argument > 2
->     lift $ putStrLn $ "Server Sends:   " ++ show result
+>     lift $ putStrLn $ "Server Sends:    " ++ show result
 >     respond result
 
     ... which looks just like the way you might write a server's main loop in
@@ -440,8 +455,8 @@
 >
 > type Pipe p a b m r = p () a () b m r
 
-    When we compose proxies, the type system ensures sure that their input and
-    output types match:
+    When we compose proxies, the type system ensures that their input and output
+    types match:
 
 >       promptInt    >->    take' 2    >->    printer
 >
@@ -588,19 +603,19 @@
 >      |   These    |
 >      +---Match----+
 
-    This is why 'Producer's, 'Consumer's, and 'Client's all take @()@ as their
-    initial argument, because their corresponding 'respond' commands all have a
-    return value of @()@.
+    This is why 'Producer's, 'Consumer's, 'Pipe's and 'Client's all take @()@
+    as their initial argument, because their corresponding 'respond' commands
+    all have a return value of @()@.
 
     This library also provides ('>~>'), which is the dual of the ('>->')
     composition operator.  ('>~>') composes two 'Proxy's blocked on a 'request'
     and returns a new 'Proxy' blocked on a 'request':
 
 > (>~>)
->  :: (Monad m, Proxy p)
->  => (a -> p a' a b' b m r)
->  -> (b -> p b' b c' c m r)
->  -> (a -> p a' a c' c m r)
+>     :: (Monad m, Proxy p)
+>     => (a -> p a' a b' b m r)
+>     -> (b -> p b' b c' c m r)
+>     -> (a -> p a' a c' c m r)
 
     Conceptually, ('>->') composes pull-based systems and ('>~>') composes
     push-based systems.
@@ -608,7 +623,7 @@
     In fact, if you went back through the previous code and systematically
     replaced every:
 
-    * ('>->') with ('>~>'),
+    * ('>->') with ('<~<'),
 
     * 'respond' with 'request', and
 
@@ -632,10 +647,11 @@
     interface matches @p2@'s upstream interface.  This follows from the type of
     ('>->'):
 
-> (>->) :: (Monad m, Proxy p)
->  => (b' -> p a' a b' b m r)
->  -> (c' -> p b' b c' c m r)
->  -> (c' -> p a' a c' c m r)
+> (>->)
+>     :: (Monad m, Proxy p)
+>     => (b' -> p a' a b' b m r)
+>     -> (c' -> p b' b c' c m r)
+>     -> (c' -> p a' a c' c m r)
 
     Diagramatically, this looks like:
 
@@ -710,24 +726,28 @@
     These 'Category' laws guarantee the following important properties:
 
     * You can reason about each proxy's behavior independently of other proxies
+      (otherwise composition wouldn't be associative)
 
     * You don't encounter weird behavior at the interface between two components
-
-    * You don't encounter corner cases at the 'Server' or 'Client' ends of a
-     'Session'
+      or at the 'Server' or 'Client' ends of a 'Session' (otherwise 'idT'
+      wouldn't be an identity)
 -}
 
 {- $class
     All the proxy code we wrote was generic over the 'Proxy' type class, which
-    defines the three central operations of this library's API:
+    defines the four central operations of this library's API:
 
-    * ('>->'): Proxy composition
+    * ('->>'): \"Pointful\" pull-based composition, from which the point-free
+      ('>->') operator derives
 
+    * ('>>~'): \"Pointful\" push-based composition, from which the point-free
+      ('>~>') operator derives
+
     * 'request': Request input from upstream
 
     * 'respond': Respond with output to downstream
 
-    @pipes@ defines everything in terms of these three operations, which is
+    @pipes@ defines everything in terms of these four operations, which is
     why all the library's utilities are polymorphic over the 'Proxy' type class.
 
     Let's look at some example instances of the 'Proxy' type class:
@@ -789,7 +809,7 @@
 >     n <- lift readLn
 >     respond n
 
->>> :t promptInt -- I've substantially cleaned up the inferred type
+>>> :t promptInt  -- I've cleaned up the inferred type
 promptInt
   :: (Monad (Producer p Int IO), MonadTrans (Producer p Int), Proxy p) =>
      () -> Producer p Int IO r
@@ -821,7 +841,7 @@
 > upstream :: (Proxy p) => () -> Producer p () IO ()
 > upstream () = runIdentityP $ do
 >     lift $ print 2
->     respond () -- Switch to downstraem
+>     respond () -- Switch to downstream
 >     lift $ print 4
 
      "Control.Proxy.Class" enumerates the 'Proxy' laws, which equationally
@@ -899,8 +919,8 @@
     match.  For instance, I might try to modify @promptInt@ to use
     @EitherT String@ to report the error instead of using exceptions:
 
-> import Control.Monad.Trans.Either -- from the "either" package
-> import Safe (readMay)
+> import Control.Monad.Trans.Either  -- from the "either" package
+> import Safe (readMay)              -- from the "safe"   package
 >
 > promptInt2 :: (Proxy p) => () -> Producer p Int (EitherT String IO) r
 > promptInt2 () = runIdentityP $ forever $ do
@@ -908,7 +928,7 @@
 >         putStrLn "Enter an Integer:"
 >         getLine
 >     case readMay str of
->         Nothing -> lift $ left "Could not read Integer"
+>         Nothing -> lift $ left "Could not read an Integer"
 >         Just n  -> respond n
 
     However, if I try to compose it with @printer@, I receive a type error:
@@ -920,22 +940,19 @@
     ...
 
     The type error says that @promptInt2@ uses @(EitherT String IO)@ for its
-    base monad, but @printer@ uses 'IO' for its base monad, so composition can't
+    base monad, but @printer@ uses @IO@ for its base monad, so composition can't
     interleave their effects.
 
-    You can easily fix this using the 'hoist' function from the 'MFunctor' type
-    class in "Control.MFunctor", which transforms the base monad of any monad
-    transformer, including the 'Proxy' monad transformer.  "Control.MFunctor"
-    really belongs in the @transformers@ package, however it currently resides
-    here because it requires the @Rank2Types@ extension.
-
-    You will commonly use 'hoist' to 'lift' one proxy's base monad to match
-    another proxy's base monad, like so:
+    You can easily fix this using the 'hoist' function from the @mmorph@
+    package, which transforms the base monad of any monad transformer that
+    implements 'MFunctor'.  Since all proxies implement 'MFunctor' you can use
+    'hoist' from 'MFunctor' to 'lift' one proxy's base monad to match another
+    proxy's base monad, like so:
 
 >>> runEitherT $ runProxy $ promptInt2 >-> (hoist lift . printer)
 Enter an Integer:
 Hello<Enter>
-Left "Could not read Integer"
+Left "Could not read an Integer"
 
     This library provides three syntactic conveniences for making this easier to
     write.
@@ -946,16 +963,16 @@
 >>> runEitherT $ runProxy $ promptInt2 >-> hoist lift . printer
 ...
 
-    Second, "lift" is such a common argument to 'hoist' that "Control.MFunctor"
-    provides the 'raise' function:
+    Second, 'lift' is such a common argument to 'hoist' that I provide the
+    'raise' function:
 
 > raise = hoist lift
 
 >>> runEitherT $ runProxy $ promptInt2 >-> raise . printer
 ...
 
-    Third, "Control.Proxy.Prelude.Kleisli" provides the 'hoistK' and 'raiseK'
-    functions in case you think composition looks ugly:
+    Third, I provide the 'hoistK' and 'raiseK' functions in case you think
+    composition looks ugly:
 
 > hoistK f = (hoist f .)
 >
@@ -964,24 +981,8 @@
 >>> runEitherT $ runProxy $ promptInt2 >-> raiseK printer
 ...
 
-    Note that "Control.MFunctor" also provides 'MFunctor' instances for all the
-    monad transformers in the @transformers@ package.  This means that you can
-    fix any incompatibility between two monad transformer stacks just using
-    various combinations of 'hoist' and 'lift'.
-
-    To see how, consider the following contrived pathological example where I
-    want to mix two very different monad transformer stacks:
-
-> m1 :: StateT s (ReaderT i IO) r
-> m2 :: MaybeT   (WriterT w IO) r
-
-    I can interleave their transformers through judicious use of 'hoist' and
-    'lift'
-
-> mBoth :: StateT s (MaybeT (ReaderT i (WriterT w IO))) r
-> mBoth = do
->     hoist (lift . hoist lift) m1
->     lift (hoist lift m2)
+    For more information on using 'MFunctor', consult the tutorial in the
+    @Control.Monad.Morph@ module from the @mmorph@ package.
 -}
 
 {- $utilities
@@ -989,11 +990,12 @@
     for common tasks.  We can redefine the previous example functions just by
     composing these utilities.
 
-    For example, 'readLnS' reads values from user input, so we can read 'Int's
-    just by specializing its type:
+    For example, 'readLnS' reads values from user input:
 
 > readLnS :: (Proxy p, Read a) => () -> Producer p a IO r
->
+
+    ... so we can read 'Int's just by specializing its type:
+
 > readIntS :: (Proxy p) => () -> Producer p Int IO r
 > readIntS = readLnS
 
@@ -1054,7 +1056,7 @@
 
     Similarly, we can build our old @take'@ on top of 'takeB_':
 
-> take' :: (Proxy p) => Int -> a' -> p a' a a' a m ()
+> take' :: (Proxy p) => Int -> a' -> p a' a a' a IO ()
 > take' n a' = runIdentityP $ do  -- Remember, we need 'runIdentityP' if
 >     takeB_ n a'                 -- we use 'do' notation or 'lift'
 >     lift $ putStrLn "You shall not pass!"
@@ -1065,15 +1067,15 @@
     Or perhaps I want to skip user input for testing and mock @promptInt@ by
     replacing it with a predefined set of values:
 
->>> runProxy $ fromListS [4, 37, 1] >-> take'2 >-> printer
+>>> runProxy $ fromListS [4, 37, 1] >-> take' 2 >-> printer
 Received a value:
 4
 Received a value:
 37
 
-    What about our original @lines'@ function?  That's just 'hGetLineS':
+    What about our original @lines'@ function?  That's just 'stdinS':
 
-> hGetLineS :: (Proxy p) => Handle -> () -> Producer p String IO ()
+> stdinS :: (Proxy p) => () -> Producer p String IO ()
 
     You could hand-write loops that accomplish these same tasks, but proxies let
     you:
@@ -1149,8 +1151,8 @@
 
     You can also concatenate sinks, too:
 
-> sink1 :: (Proxy p) => () -> Consumer p Int IO ()
-> sink1 () = do
+> sink1 :: (Proxy p) => () -> Pipe p Int Int IO ()
+> sink1 () = runIdentityP $ do
 >     (takeB_ 3         >-> printD) () -- Sink 1
 >     (takeWhileD (< 4) >-> printD) () -- Sink 2
 >
@@ -1168,11 +1170,11 @@
     ... but the above example is gratuitous because you can simply concatenate
     the intermediate stages:
 
-> sink2 :: (Proxy p) => () -> Consumer p Int IO ()
-> sink2 () = intermediate >-> printD where
->     intermediate () = do
->         takeB_ 3 ()       -- Intermediate stage 1
->         takeWhileD (< 4)  -- Intermediate stage 2
+> sink2 :: (Proxy p) => () -> Pipe p Int Int IO ()
+> sink2 = intermediate >-> printD where
+>     intermediate () = runIdentityP $ do
+>         takeB_ 3 ()          -- Intermediate stage 1
+>         takeWhileD (< 4) ()  -- Intermediate stage 2
 >
 > -- or: sink2 = (takeB_ 3 >=> takeWhileD (< 4)) >-> printD
 
@@ -1189,6 +1191,165 @@
     two categories.
 -}
 
+{- $listT
+    Proxies generalize lists by allowing you to interleave effects between list
+    elements, but you might be surprised to learn that they also generalize the
+    list monad, too!  "Control.Proxy.ListT" provides the machinery necessary to
+    convert back and forth between proxies and a @ListT@-like monad transformer
+    that binds proxy outputs.
+
+    For example, let's say that we want to select elements from two separate
+    lists, except interleaving side effects, too:
+
+> --                          +-- ListT that will compile to a 'Producer'
+> --                          |
+> --                          v
+> pairs :: (ListT p) => () -> ProduceT p IO (Int, Int)
+> pairs () = do
+>     x <- rangeS 1 3     -- Select a number betwen 1 and 3
+>     lift $ putStrLn $ "Currently using: " ++ show x
+>     y <- eachS [4,6,8]  -- Select one of 4, 6, or 8
+>     return (x, y)
+
+    We can compile the above 'ProduceT' code to a 'Producer' using
+    'runRespondK':
+
+> -- runRespondK's type is actually more general
+> runRespondK :: (() -> ProduceT p m b) -> () -> Producer p b m ()
+>
+> runRespondK pairs :: (ListT p) => () -> Producer p (Int, Int) IO ()
+
+    The return value of the 'ProduceT' becomes the output of the corresponding
+    'Producer', which produces one output for each permutation of elements that
+    we could have selected:
+
+>>> runProxy $ runRespondK pairs >-> printD
+Currently using: 1
+(1,4)
+(1,6)
+(1,8)
+Currently using: 2
+(2,4)
+(2,6)
+(2,8)
+Currently using: 3
+(3,4)
+(3,6)
+(3,8)
+
+    This works the other way around, too!  You can wrap any 'Producer' in the
+    'RespondT' newtype to bind its output in the 'ProduceT' monad:
+
+> pairs2 :: (ListT p) => () -> ProduceT p IO (Int, Int)
+> pairs2 () = do
+>     x <- RespondT $ runIdentityP $ do
+>         respond 1
+>         lift $ putStrLn "Here"
+>         respond 2
+>     y <- RespondT $ runIdentityP $ do
+>         respond 3
+>         lift $ putStrLn "There"
+>         respond 4
+>     return (x, y)
+
+>>> runProxy $ runRespondK pairs2 >-> printD
+(1,3)
+There
+(1,4)
+Here
+(2,3)
+There
+(2,4)
+
+    In fact, this is how 'eachS' and 'rangeS' are implemented:
+
+> eachS :: (Monad m, ListT p) => [b] -> ProduceT p m b
+> eachS xs = RespondT (fromList xs ())
+>
+> rangeS :: (Enum b, Monad m, Ord b, ListT p) => b -> b -> ProduceT p m b
+> rangeS n1 n2 = RespondT (enumFromS n1 n2 ())
+
+    'ProduceT' is actually a special case of 'RespondT', related by the
+    following type synonym:
+
+> type ProduceT p = RespondT p C () ()
+
+    Moreover, you can bind anything within 'RespondT', not just 'Producer's.
+    For example, you can bind 'Pipe's within the more general 'RespondT' monad:
+
+> pairs3 :: (ListT p) => () -> RespondT p () Int () IO (Int, Int)
+> pairs3 () = do
+>     x <- RespondT $ runIdentityP $ replicateM_ 2 $ do
+>         a <- request ()
+>         lift $ putStrLn $ "Received " ++ show a
+>         respond a
+>     y <- RespondT $ runIdentityP $ replicateM_ 3 $ do
+>         a <- request ()
+>         lift $ putStrLn $ "Received " ++ show a
+>         respond a
+>     return (x, y)
+
+    ... and you will get a 'Pipe' back when you 'runRespondK' the final result:
+
+> runRespondK pairs3 :: ListT p => () -> Pipe p Int (Int, Int) IO ()
+
+>>> runProxy $ enumFromS 1 >-> runRespondK pairs3 >-> printD
+Received 1
+Received 2
+(1,2)
+Received 3
+(1,3)
+Received 4
+(1,4)
+Received 5
+Received 6
+(5,6)
+Received 7
+(5,7)
+Received 8
+(5,8)
+
+    Proxies actually form two symmetric 'ListT'-like monad transformers: one
+    binds elements output from the proxy's downstream interface and one binds
+    elements output from the proxy's upstream interface.  To distinguish them,
+    I call the downstream one 'RespondT' and the upstream one 'RequestT'.
+
+    "Control.Proxy.ListT" contains the 'ListT' class, which provides the the
+    underlying operators for both 'RespondT' and 'RequestT':
+
+    * ('>\\'): Equivalent to ('=<<') for 'RequestT'
+
+    * ('//>'): Equivalent to ('>>=') for 'RespondT'
+
+    You don't need to use these operators directly, since you can instead just
+    wrap your proxies in the 'RespondT' or 'RequestT' monad transformers and
+    they will translate the binds in those monads to the above operators under
+    the hood.
+
+    If those are the bind operators, though, then where are the corresponding
+    'return' equivalents?  Why, they are just 'respond' and 'request'!
+
+> -- return for 'RespondT'
+> return b  = RespondT (respond b)
+
+> -- return for 'RequestT'
+> return a' = RequestT (request a')
+
+    Therefore, we can use the monad laws to reason about how 'respond' interacts
+    with 'RespondT' (and, dually, how 'request' interacts with 'RequestT'):
+
+> do x' <- RespondT (respond x)  =  do f x
+>    f x'
+>
+> do x <- m                      =  do m
+>    RespondT (respond x)
+
+    'RequestT' and 'RespondT' are correct by construction, meaning that they
+    always satisfy the monad and monad transformer without exception, unlike
+    @ListT@ from @transformers@.  In other words, they behave like two
+    symmetric implementations of \"ListT done right\".
+-}
+
 {- $folds
     You can fold a stream of values in two ways, both of which use the base
     monad:
@@ -1227,12 +1388,14 @@
     * 'foldlD'': Strictly fold values flowing downstream
 
 > foldlD'
->  :: (Monad m, Proxy p) => (b -> a -> b) -> x -> p x a x a (StateT b m) r
+>     :: (Monad m, Proxy p)
+>     => (b -> a -> b) -> x -> p x a x a (StateT b m) r
 
     * 'foldlU'': Strictly fold values flowing upstream
 
 > foldU'
->  :: (Monad m, Proxy p) => (b -> a' -> b) -> a' -> p a' x a' x (StateT b m) r
+>     :: (Monad m, Proxy p)
+>     => (b -> a' -> b) -> a' -> p a' x a' x (StateT b m) r
 
     Now, let's try these folds out and see if we can build a list from user
     input:
@@ -1244,7 +1407,7 @@
 66<Enter>
 Enter an Integer:
 5<Enter>
-((), [1, 66, 5])
+((),[1,66,5])
 
     Notice that @promptInt@ uses 'IO' as its base monad, but 'toListD' uses
     @(WriterT [Int] m)@ as its base monad, so I use 'raiseK' to get the base
@@ -1257,13 +1420,13 @@
 5
 7
 4
-((), Sum 3)
+((),Sum {getSum = 3})
 
     You can also run multiple folds at the same time just by adding more
     'WriterT' layers to your base monad:
 
 >>> runWriterT $ runWriterT $ runProxy $ fromListS [9, 10] >-> anyD even >-> raiseK sumD
-(((), Any {getAny = True},Sum {getSum = 19})
+(((),Any {getAny = True}),Sum {getSum = 19}
 
     I designed certain special folds to terminate the 'Session' early if they
     can compute their result prematurely, in order to draw as little input as
@@ -1274,7 +1437,7 @@
 
 >>> runWriterT $ runProxy $ fromListS [3, 4, 9] >-> raiseK printD >-> headD_
 3
-((), First {getFirst = Just 3})
+((),First {getFirst = Just 3})
 
     Compare this to 'headD' without underscore, which folds the entire input:
 
@@ -1282,7 +1445,7 @@
 3
 4
 9
-((), First {getFirst = Just 3})
+((),First {getFirst = Just 3})
 
     Use the versions that don't prematurely terminate if you are running
     multiple folds or if you want to continue to use the rest of the input when
@@ -1297,7 +1460,7 @@
     and write a streaming utility that lazily opens a file only in response to
     a 'request', such as the following 'Producer':
 
-> readFileS :: FilePath -> () -> Producer p String IO
+> readFileS :: () -> FilePath -> () -> Producer p String IO ()
 > readFileS file () = runIdentityP $ do
 >     h <- lift $ openFile file ReadMode
 >     lift $ putStrLn "Opening file"
@@ -1339,18 +1502,16 @@
     * It is backwards compatible with \"unmanaged\" ordinary proxies
 
     Backwards compatibility means that you don't need to buy in to the
-    @pipes-safe@ way of doing things.  For example, another common approach is
-    to just open all resources before running the session and close
-    them all afterward.  For example, if I wanted to emulate the Unix @cp@
+    @pipes-safe@ way of doing things.  This matters because another common
+    approach is to just open all resources before running the session and close
+    them all afterward.  For example,, if I wanted to emulate the Unix @cp@
     command, streaming one line at a time, I might write:
 
-> import System.IO
->
 > cp :: FilePath -> FilePath -> IO ()
 > cp inFile outFile =
->     withFile file1 ReadMode  $ \hIn  ->
->     withFile file2 WriteMode $ \hOut ->
->     runProxy $ hGetLineS hIn >-> hPutLineS hOut
+>     withFile inFile  ReadMode  $ \hIn  ->
+>     withFile outFile WriteMode $ \hOut ->
+>     runProxy $ hGetLineS hIn >-> hPutStrLnD hOut
 
     Some people prefer that approach because it:
 
@@ -1402,7 +1563,7 @@
 >         putStrLn "Enter an Integer:"
 >         getLine
 >     case readMay str of
->         Nothing -> lift $ left "Could not read Integer"
+>         Nothing -> lift $ left "Could not read an Integer"
 >         Just n  -> respond n
 
     There is no way to recover from the error and resume streaming data.  You
@@ -1426,8 +1587,8 @@
 >         putStrLn "Enter an Integer:"
 >         getLine
 >     case readMay str of
->         Nothing -> E.throw "Could not read Integer"
->         Just n' -> respond n
+>         Nothing -> E.throw "Could not read an Integer"
+>         Just n  -> respond n
 
     This example does not need 'runIdentityP' (nor would that type-check)
     because the 'EitherP' proxy transformer gives the compiler enough
@@ -1437,12 +1598,12 @@
     first to unwrap the 'EitherP' followed by 'runProxy'.
 
 > runEitherK
->  :: (q -> EitherP p a' a b' b m r) -> (q -> p a' a b' b m (Either e r))
+>     :: (q -> EitherP p a' a b' b m r) -> (q -> p a' a b' b m (Either e r))
 
->>> runProxy $ runEitherK $ promptInt3 >-> printer :: IO (Either String r)
+>>> runProxy $ E.runEitherK $ promptInt3 >-> printer :: IO (Either String r)
 Enter an Integer:
 Hello<Enter>
-Left "Could not read Integer"
+Left "Could not read an Integer"
 
     Notice how we can directly compose @printer@ with @promptInt@.
     This works because @printer@'s base proxy type is completely polymorphic
@@ -1462,9 +1623,9 @@
     a given proxy each time it raises an error:
 
 > heartbeat
->  :: (Proxy p)
->  => E.EitherP String p a' a b' b IO r
->  -> E.EitherP String p a' a b' b IO r
+>     :: (Proxy p)
+>     => E.EitherP String p a' a b' b IO r
+>     -> E.EitherP String p a' a b' b IO r
 > heartbeat p = p `E.catch` \err -> do
 >     lift $ putStrLn err  -- Print the error
 >     heartbeat p          -- Restart 'p'
@@ -1475,7 +1636,7 @@
 >>> runProxy $ E.runEitherK $ (heartbeat . promptInt3) >-> takeB_ 2 >-> printer
 Enter an Integer:
 Hello<Enter>
-Could not read Integer
+Could not read an Integer
 Enter an Integer
 8
 Received a value:
@@ -1486,9 +1647,9 @@
 0
 
     It's very easy to prove that 'EitherP' has only a local effect.  In fact,
-    we can run it entirely locally like so:
+    we can run it locally on a subset of the pipeline like so:
 
->>> runProxy $ (E.runEitherK $ heartbeat . promptInt3) >-> takeB_ 2 >-> printer
+>>> runProxy $ (E.runEitherK $ heartbeat . promptInt3 >-> takeB_ 2) >-> printer
 
     Proxy transformers do not use the base monad at all, so you can use them to
     isolate effects from other proxies, as the next section demonstrates.
@@ -1554,8 +1715,8 @@
     triply nested proxy:
 
 > zipD
->  :: (Monad m, Proxy p1, Proxy p2, Proxy p3)
->  => () -> Consumer p1 a (Consumer p2 b (Producer p3 (a, b) m)) r
+>     :: (Monad m, Proxy p1, Proxy p2, Proxy p3)
+>     => () -> Consumer p1 a (Consumer p2 b (Producer p3 (a, b) m)) r
 > zipD () =
 >     runIdentityP . hoist (runIdentityP . hoist runIdentityP) $ forever $ do
 >     -- Yes, this 'runIdentityP' mess is necessary.  Sorry!
@@ -1577,15 +1738,15 @@
 > p3 = runProxy $ printD <-< p2
 
 >>> p3
-(1, 4)
-(2, 5)
-(3, 6)
+(1,4)
+(2,5)
+(3,6)
 
     You can use this trick to fork output, too:
 
 > fork
->  :: (Monad m, Proxy p1, Proxy p2, Proxy p3)
->  => () -> Consumer p1 a (Producer p2 a (Producer p3 a m)) r
+>     :: (Monad m, Proxy p1, Proxy p2, Proxy p3)
+>     => () -> Consumer p1 a (Producer p2 a (Producer p3 a m)) r
 > fork () =
 >     runIdentityP . hoist (runIdentityP . hoist runIdentityP) $ forever $ do
 >         a <- request ()          -- Request output from the 'Consumer'
@@ -1645,10 +1806,10 @@
       following form:
 
 > zip'  -- You can't define this
->  :: (Monad m, Proxy p)
->  => (() -> Producer p a      m r)
->  -> (() -> Producer p b      m r)
->  -> (() -> Producer p (a, b) m r)
+>     :: (Monad m, Proxy p)
+>     => (() -> Producer p a      m r)
+>     -> (() -> Producer p b      m r)
+>     -> (() -> Producer p (a, b) m r)
 
     Partial application requires selecting a 'Proxy' instance, which is why you
     cannot define @zip'@.  You /can/ define a @zip'@ specialized to a concrete
@@ -1680,9 +1841,9 @@
 
     For example, we might want to mix @promptInt3@ and @increment2@:
 
-> promptInt3 :: (Proxy p) => () -> Producer (E.EitherP String p) Int IO r
+> promptInt3 :: (Proxy p) => () -> Producer (EitherP String p) Int IO r
 >
-> increment2 :: (Proxy p) => () -> Consumer (S.StateP Int p) Int IO r
+> increment2 :: (Proxy p) => () -> Consumer (StateP Int p) Int IO r
 
     Unfortunately, they use two different feature sets so neither one is fully
     polymorphic over the 'Proxy' class and we cannot directly compose them.
@@ -1692,22 +1853,34 @@
 
 > class ProxyTrans t where
 >     liftP
->       :: (Monad m, Proxy p)
->       => p a' a b' b m r -> t p a' a b' b m r
+>          :: (Monad m, Proxy p)
+>          => p a' a b' b m r -> t p a' a b' b m r
 >
 > -- mapP is slightly more elegant
 > mapP
->  :: (Monad m, Proxy p, ProxyTrans t)
->  => (q -> p a' a b' b m r) -> (q -> t p a' a b' b m r)
-> mapP = (liftP . )
+>     :: (Monad m, Proxy p, ProxyTrans t)
+>     => (q -> p a' a b' b m r) -> (q -> t p a' a b' b m r)
+> mapP = (liftP .)
 
     It's very easy to use.  Just use 'mapP' to lift one proxy transformer to
     match another one.  For example, we can 'mapP' @increment2@ to match
     @promptInt3@:
 
+> promptInt3
+>     :: (Proxy stateP)
+>     => () -> Producer (EitherP String  stateP       ) Int IO r
+>
+> mapP increment2
+>     :: (Proxy p, ProxyTrans eitherP)
+>     => () -> Consumer (eitherP        (StateP Int p)) Int IO r
+>
 > promptInt3 >-> mapP increment2
->  :: (Proxy p) => () -> Session (EitherP String (StateP Int p)) IO r
+>     :: (Proxy p)
+>     => () -> Session  (EitherP String (StateP Int p))     IO r
 
+    'mapP' creates a new 'ProxyTrans' layer that type-checks as 'EitherP', and
+    @StateP Int p@ type-checks as the 'Proxy' in @promptInt3@'s signature.
+
 >>> runProxy $ S.evalStateK 0 $ E.runEitherK $ promptInt3 >-> mapP increment2
 Enter an Integer:
 4<Enter>
@@ -1717,14 +1890,26 @@
 (5, 2)
 Enter an Integer:
 Hello<Enter>
-Left "Could not read Integer"
+Left "Could not read an Integer"
 
     ... or we could instead 'mapP' @promptInt3@ to match @increment2@ and switch
     the order of the two proxy transformers:
 
+> mapP promptInt3
+>     :: (Proxy p, ProxyTrans stateP)
+>     => () -> Producer (stateP     (EitherP String p)) Int IO r
+>
+> increment2
+>     :: (Proxy eitherP)
+>     => () -> Consumer (StateP Int  eitherP          ) Int IO r
+>
 > mapP promptInt3 >-> increment2
->  :: (Proxy p) => () -> Session (StateP Int (EitherP String p)) IO r
+>     :: (Proxy p)
+>     => () -> Session  (StateP Int (EitherP String p))     IO r
 
+    'mapP' creates a new 'ProxyTrans' layer that type-checks as 'StateP', and
+    @EitherP Int p@ type-checks as the 'Proxy' in @increment2@'s signature.
+
 >>> runProxy $ E.runEitherK $ S.evalStateK 0 $ mapP promptInt3 >-> increment2
 Enter an Integer:
 4<Enter>
@@ -1734,22 +1919,37 @@
 (5, 2)
 Enter an Integer:
 Hello<Enter>
-Left "Could not read Integer"
+Left "Could not read an Integer"
 
     Like monad transformers, proxy transformers lift a base 'Monad' instance
-    to an extended 'Monad' instance.  'liftP' exactly mirrors the 'lift'
+    to an extended 'Monad' instance and 'liftP' exactly mirrors the 'lift'
     function from 'MonadTrans'.  'liftP' takes some base proxy, @p@, that
     implements 'Monad' and \"lift\"s it to an extended proxy, @(t p)@, that also
     implements 'Monad'.
 
-    So for example, I could do something like:
+    This means you can seamlessly mix effects from different proxy transformer
+    layers just by using 'liftP' to access inner layers:
 
-> do liftP $ actionInBaseProxy
->    actionInExtendedProxy
+> twoLayers
+>     :: (Proxy p)
+>     => () -> Consumer (E.EitherP String (S.StateP Int p)) Int IO r
+> twoLayers () = forever $ do
+>     a <- request ()
+>     if (a >= 0)
+>         then liftP $ S.modify (+ a)
+>         else E.throw "Negative number"
 
-    Monad transformers impose certain laws to ensure that this lifting is
-    correct.  These are known as the monad transformer laws;
+>>> runProxy $ S.runStateK 0 $ E.runEitherK $ fromListS [1, 2, -4] >-> twoLayers
+(Left "Negative number",3)
 
+    This exactly resembles how you use 'lift' to access inner layers of a monad
+    transformer stack.
+-}
+
+{- $proxymorph
+    Monad transformers impose certain laws to ensure that 'lift' behaves
+    correctly.  These are known as the \"monad morphism laws\":
+
 > (lift .) (f >=> g) = (lift .) f >=> (lift .) g
 >
 > (lift .) return = return
@@ -1794,7 +1994,7 @@
 
     But we're not even done, because proxies actually form three other
     categories, only one of which I have mentioned so far, and proxy
-    transformers lift these three other categories, too:
+    transformers lift these three other categories correctly, too:
 
 > -- The push-based category
 >
@@ -1802,22 +2002,19 @@
 >
 > mapP coidT = coidT
 
-> -- The "request" category
+> -- The upstream ListT Kleisli category
 >
 > mapP (f \>\ g) = mapP f \>\ mapP g
 >
 > mapP request = request
 
-> -- The "respond" category
+> -- The downstream ListT Kleisli category
 >
 > mapP (f />/ g) = mapP f />/ mapP g
 >
 > mapP respond = respond
 
-    I never even mentioned those last two categories because they are more
-    exotic and you probably never need to use them.  However, even if we never
-    use those categories they still guarantee two really important laws that we
-    should remember:
+    I want to highlight two of the above laws:
 
 > mapP request = request
 >
@@ -1834,34 +2031,46 @@
 
     All the proxy transformers in this library obey the proxy morphism laws,
     which ensure that 'liftP' / 'mapP' always do \"the right thing\".
+-}
 
+{- $proxyfunctor
     Proxy transformers also implement 'hoistP' from the 'PFunctor' class in
-    "Control.PFunctor".  This exactly parallels 'hoist' for monad transformers.
+    "Control.Proxy.Morph".  This exactly parallels 'hoist' from
+    @Control.Monad.Morph@.
 
-    Just like monad transformers, we can mix two completely exotic proxy
-    transformer stacks using a combination of 'liftP' and 'hoistP'.  Here's the
-    proxy transformer equivalent of the previous example I gave:
+    You will most commonly use 'hoistP' to insert arbitrary proxy transformer
+    layers to get two mismatched proxy transformer stacks to type-check.
 
-> p1 :: (Proxy p) => a' -> StateP s (ReaderP i p) a' a a' a m r
-> p2 :: (Proxy p) => a' -> MaybeP   (WriterP w p) a' a a' a m r
+    For example, consider the following two very different proxy transformer
+    stacks:
 
-    As before, I can interleave their proxy transformers through judicious use
-    of 'hoistP' and 'liftP'
+> p1 :: (Monad m, Proxy p) => a' -> StateP s (ReaderP i p) a' a a' a m a'
+> p2 :: (Monad m, Proxy p) => a' -> MaybeP   (WriterP w p) a' a a' a m a'
 
-> pSequence
->  :: (Proxy p) => StateP s (MaybeP (ReaderP i (WriterP w p))) a' a a' a r
-> pSequence a' = do
->     hoistP (liftP . hoistP liftP) (p1 a')
->     liftP (hoistP liftP (p2 a'))
+    I can normalize them to use same proxy transformer stack by judiciously
+    inserting extra proxy transformer layers using a combination of 'hoistP'
+    and 'liftP':
 
-    ... but unlike ordinary monad transformers I could instead mix them by
-    composition, too!
+> p1' :: (Monad m, Proxy p)
+>     => a' -> StateP s (MaybeP (ReaderP i (WriterP w p))) a' a a' a m a'
+> p1' = hoistP liftP . p1
+> 
+> p2' :: (Monad m, Proxy p)
+>     => a' -> StateP s (MaybeP (ReaderP i (WriterP w p))) a' a a' a m a'
+> p2' = liftP . hoistP liftP . p2
 
+    Now that I've made them agree on a common proxy transformer stack, I can
+    sequence them or compose them:
+
+> pSequence
+>     :: (Proxy p)
+>     => a' -> StateP s (MaybeP (ReaderP i (WriterP w p))) a' a a' a m a'
+> pSequence = p1' >=> p2'
+>
 > pCompose
->  :: (Proxy p) => StateP s (MaybeP (ReaderP i (WriterP w p))) a' a a' a r
-> pCompose =
->      hoistP (liftP . hoistP liftP) . p1
->  >-> liftP . hoistP liftP . p2
+>     :: (Proxy p)
+>     => a' -> StateP s (MaybeP (ReaderP i (WriterP w p))) a' a a' a m a'
+> pCompose  = p1' >-> p2'
 -}
 
 {- $conclusion
@@ -1883,3 +2092,248 @@
     tutorial's length.  So if you don't know how to implement something using
     @pipes@, just ask me and I will be happy to help.
 -}
+
+-- $appendix
+-- I've provided the full code for the above examples here so you can easily
+-- play with the examples yourself:
+-- 
+-- > import Control.Monad
+-- > import Control.Proxy hiding (zipD)
+-- > import System.IO
+-- > import qualified Data.Map as M
+-- > import Control.Monad.Trans.Either
+-- > import Safe (readMay)
+-- > import qualified Control.Proxy.Trans.Either as E
+-- > import qualified Control.Proxy.Trans.State as S
+-- > 
+-- > lines' :: (Proxy p) => Handle -> () -> Producer p String IO ()
+-- > lines' h () = runIdentityP loop where
+-- >     loop = do
+-- >         eof <- lift $ hIsEOF h
+-- >         if eof
+-- >         then return ()
+-- >         else do
+-- >             str <- lift $ hGetLine h
+-- >             respond str  -- Produce the string
+-- >             loop
+-- > 
+-- > promptInt :: (Proxy p) => () -> Producer p Int IO r
+-- > promptInt () = runIdentityP $ forever $ do
+-- >     lift $ putStrLn "Enter an Integer:"
+-- >     n <- lift readLn  -- 'lift' invokes an action in the base monad
+-- >     respond n
+-- > {-
+-- > promptInt = readLnS >-> execU (putStrLn "Enter an Integer:")
+-- > -}
+-- > 
+-- > printer :: (Proxy p, Show a) => () -> Consumer p a IO r
+-- > printer () = runIdentityP $ forever $ do
+-- >     a <- request ()  -- Consume a value
+-- >     lift $ putStrLn "Received a value:"
+-- >     lift $ print a
+-- > {-
+-- > printer :: (Proxy p, Show a) => x -> p x a x a IO r
+-- > printer = execD (putStrLn "Received a value:") >-> printD
+-- > -}
+-- > 
+-- > take' :: (Proxy p) => Int -> () -> Pipe p a a IO ()
+-- > take' n a' = runIdentityP $ do  -- Remember, we need 'runIdentityP' if
+-- >     takeB_ n a'                 -- we use 'do' notation or 'lift'
+-- >     lift $ putStrLn "You shall not pass!"
+-- > 
+-- > threeReqs :: (Proxy p) => () -> Client p Int Bool IO ()
+-- > threeReqs () = runIdentityP $ forM_ [1, 3, 1] $ \argument -> do
+-- >     lift $ putStrLn $ "Client Sends:    " ++ show (argument :: Int)
+-- >     result <- request argument
+-- >     lift $ putStrLn $ "Client Receives: " ++ show (result :: Bool)
+-- >     lift $ putStrLn "*"
+-- > 
+-- > comparer :: (Proxy p) => Int -> Server p Int Bool IO r
+-- > comparer = runIdentityK $ foreverK $ \argument -> do
+-- >     lift $ putStrLn $ "Server Receives: " ++ show argument
+-- >     let result = argument > 2
+-- >     lift $ putStrLn $ "Server Sends:    " ++ show result
+-- >     respond result
+-- > 
+-- > cache :: (Proxy p, Ord key) => key -> p key val key val IO r
+-- > cache = runIdentityK (loop M.empty) where
+-- >     loop _map key = case M.lookup key _map of
+-- >         Nothing -> do
+-- >             val  <- request key
+-- >             key2 <- respond val
+-- >             loop (M.insert key val _map) key2
+-- >         Just val -> do
+-- >             lift $ putStrLn "Used cache!"
+-- >             key2 <- respond val
+-- >             loop _map key2
+-- > 
+-- > downstream :: (Proxy p) => () -> Consumer p () IO ()
+-- > downstream () = runIdentityP $ do
+-- >     lift $ print 1
+-- >     request ()  -- Switch to upstream
+-- >     lift $ print 3
+-- >     request ()  -- Switch to upstream
+-- > 
+-- > upstream :: (Proxy p) => () -> Producer p () IO ()
+-- > upstream () = runIdentityP $ do
+-- >     lift $ print 2
+-- >     respond () -- Switch to downstream
+-- >     lift $ print 4
+-- > 
+-- > promptInt2 :: (Proxy p) => () -> Producer p Int (EitherT String IO) r
+-- > promptInt2 () = runIdentityP $ forever $ do
+-- >     str <- lift $ lift $ do
+-- >         putStrLn "Enter an Integer:"
+-- >         getLine
+-- >     case readMay str of
+-- >         Nothing -> lift $ left "Could not read an Integer"
+-- >         Just n  -> respond n
+-- > 
+-- > readIntS :: (Proxy p) => () -> Producer p Int IO r
+-- > readIntS = readLnS
+-- > 
+-- > source1 :: (Proxy p) => () -> Producer p Int IO r
+-- > source1 () = runIdentityP $ do
+-- >     fromListS [4, 4] ()  -- Source 1
+-- >     readLnS ()           -- Source 2
+-- > 
+-- > source2 :: (Proxy p) => () -> Producer p Int IO ()
+-- > source2 () = runIdentityP $ do
+-- >     fromListS [4, 4] ()
+-- >     (readLnS >-> takeB_ 3) () -- You can compose inside a do block!
+-- > 
+-- > sink1 :: (Proxy p) => () -> Pipe p Int Int IO ()
+-- > sink1 () = runIdentityP $ do
+-- >     (takeB_ 3         >-> printD) () -- Sink 1
+-- >     (takeWhileD (< 4) >-> printD) () -- Sink 2
+-- > 
+-- > sink2 :: (Proxy p) => () -> Pipe p Int Int IO ()
+-- > sink2 = intermediate >-> printD where
+-- >     intermediate () = runIdentityP $ do
+-- >         takeB_ 3 ()          -- Intermediate stage 1
+-- >         takeWhileD (< 4) ()  -- Intermediate stage 2
+-- > 
+-- > pairs :: (ListT p) => () -> ProduceT p IO (Int, Int)
+-- > pairs () = do
+-- >     x <- rangeS 1 3     -- Select a number betwen 1 and 3
+-- >     lift $ putStrLn $ "Currently using: " ++ show x
+-- >     y <- eachS [4,6,8]  -- Select one of 4, 6, or 8
+-- >     return (x, y)
+-- > 
+-- > pairs2 :: (ListT p) => () -> ProduceT p IO (Int, Int)
+-- > pairs2 () = do
+-- >     x <- RespondT $ runIdentityP $ do
+-- >         respond 1
+-- >         lift $ putStrLn "Here"
+-- >         respond 2
+-- >     y <- RespondT $ runIdentityP $ do
+-- >         respond 3
+-- >         lift $ putStrLn "There"
+-- >         respond 4
+-- >     return (x, y)
+-- >
+-- > pairs3 :: (ListT p) => () -> RespondT p () Int () IO (Int, Int)
+-- > pairs3 () = do
+-- >     x <- RespondT $ runIdentityP $ replicateM_ 2 $ do
+-- >         a <- request ()
+-- >         lift $ putStrLn $ "Received " ++ show a
+-- >         respond a
+-- >     y <- RespondT $ runIdentityP $ replicateM_ 3 $ do
+-- >         a <- request ()
+-- >         lift $ putStrLn $ "Received " ++ show a
+-- >         respond a
+-- >     return (x, y)
+-- >
+-- > readFileS :: (Proxy p) => FilePath -> () -> Producer p String IO ()
+-- > readFileS file () = runIdentityP $ do
+-- >     h <- lift $ openFile file ReadMode
+-- >     lift $ putStrLn "Opening file"
+-- >     hGetLineS h ()
+-- >     lift $ putStrLn "Closing file"
+-- >     lift $ hClose h
+-- > 
+-- > cp :: FilePath -> FilePath -> IO ()
+-- > cp inFile outFile =
+-- >     withFile inFile  ReadMode  $ \hIn  ->
+-- >     withFile outFile WriteMode $ \hOut ->
+-- >     runProxy $ hGetLineS hIn >-> hPutStrLnD hOut
+-- > 
+-- > promptInt3 :: (Proxy p) => () -> Producer (E.EitherP String p) Int IO r
+-- > promptInt3 () = forever $ do
+-- >     str <- lift $ do
+-- >         putStrLn "Enter an Integer:"
+-- >         getLine
+-- >     case readMay str of
+-- >         Nothing -> E.throw "Could not read an Integer"
+-- >         Just n  -> respond n
+-- > 
+-- > heartbeat
+-- >     :: (Proxy p)
+-- >     => E.EitherP String p a' a b' b IO r
+-- >     -> E.EitherP String p a' a b' b IO r
+-- > heartbeat p = p `E.catch` \err -> do
+-- >     lift $ putStrLn err  -- Print the error
+-- >     heartbeat p          -- Restart 'p'
+-- > 
+-- > increment :: (Monad m, Proxy p) => () -> Producer (S.StateP Int p) Int m r
+-- > increment () = forever $ do
+-- >     n <- S.get
+-- >     respond n
+-- >     S.put (n + 1)
+-- > 
+-- > numbers :: (Monad m, Proxy p) => () -> Producer p Int m ()
+-- > numbers () = runIdentityP $ do
+-- >     (takeB_ 5 <-< S.evalStateK 10 increment) ()
+-- >     S.evalStateK 1  (takeB_ 3 <-< increment) () -- This works, too!
+-- > 
+-- > increment2 :: (Proxy p) => () -> Consumer (S.StateP Int p) Int IO r
+-- > increment2 () = forever $ do
+-- >     nOurs   <- S.get
+-- >     nTheirs <- request ()
+-- >     lift $ print (nTheirs, nOurs)
+-- >     S.put (nOurs + 2)
+-- > 
+-- > zipD
+-- >     :: (Monad m, Proxy p1, Proxy p2, Proxy p3)
+-- >     => () -> Consumer p1 a (Consumer p2 b (Producer p3 (a, b) m)) r
+-- > zipD () =
+-- >     runIdentityP . hoist (runIdentityP . hoist runIdentityP) $ forever $ do
+-- >     -- Yes, this 'runIdentityP' mess is necessary.  Sorry!
+-- > 
+-- >         a <- request ()               -- Request from the outer 'Consumer'
+-- >         b <- lift $ request ()        -- Request from the inner 'Consumer'
+-- >         lift $ lift $ respond (a, b)  -- Respond to the 'Producer'
+-- > 
+-- > p1 = runProxyK $ zipD <-< fromListS [1..3]
+-- > p2 = runProxyK $ p1 <-< fromListS [4..]
+-- > p3 = runProxy $ printD <-< p2
+-- > 
+-- > fork
+-- >     :: (Monad m, Proxy p1, Proxy p2, Proxy p3)
+-- >     => () -> Consumer p1 a (Producer p2 a (Producer p3 a m)) r
+-- > fork () =
+-- >     runIdentityP . hoist (runIdentityP . hoist runIdentityP) $ forever $ do
+-- >         a <- request ()          -- Request output from the 'Consumer'
+-- >         lift $ respond a         -- Send output to the outer 'Producer'
+-- >         lift $ lift $ respond a  -- Send output to the inner 'Producer'
+-- > 
+-- > {-
+-- > p1 = runProxyK $ fork <-< fromListS [1..3]
+-- > p2 = runProxyK $ raiseK printD <-< mapD (> 2) <-< p1
+-- > p3 = runProxy  $ printD <-< mapD show <-< p2
+-- > -}
+-- > 
+-- > {-
+-- > p1 = runProxyK $ S.evalStateK 0 $ fork <-< increment
+-- > p2 = runProxyK $ raiseK printD <-< mapD (+ 10) <-< p1
+-- > p3 = runProxy  $ E.runEitherK $ printD <-< (takeB_ 3 >=> E.throw) <-< p2
+-- > -}
+-- > 
+-- > twoLayers
+-- >     :: (Proxy p)
+-- >     => () -> Consumer (E.EitherP String (S.StateP Int p)) Int IO r
+-- > twoLayers () = forever $ do
+-- >     a <- request ()
+-- >     if (a >= 0)
+-- >         then liftP $ S.modify (+ a)
+-- >         else E.throw "Negative number"
diff --git a/pipes.cabal b/pipes.cabal
--- a/pipes.cabal
+++ b/pipes.cabal
@@ -1,6 +1,6 @@
 Name: pipes
-Version: 3.1.0
-Cabal-Version: >=1.14.0
+Version: 3.2.0
+Cabal-Version: >=1.8.0.2
 Build-Type: Simple
 License: BSD3
 License-File: LICENSE
@@ -10,8 +10,8 @@
 Bug-Reports: https://github.com/Gabriel439/Haskell-Pipes-Library/issues
 Synopsis: Compositional pipelines
 Description:
-  \"Coroutines done right\".  This library generalizes
-  iteratees\/enumerators\/enumeratees simply and elegantly.
+  \"Coroutines done right\".  This library generalizes iteratees and coroutines
+  simply and elegantly.
   .
   Advantages over traditional iteratee\/coroutine implementations:
   .
@@ -25,6 +25,8 @@
   .
   * /Extension Framework/: Mix and match extensions and create your own
   .
+  * /ListT/: Correct implementation of ListT that interconverts with pipes
+  .
   * /Lightweight Dependency/: @pipes@ depends only on @transformers@ and
     compiles rapidly
   .
@@ -34,27 +36,28 @@
   .
   Read "Control.Proxy.Tutorial" for a really extensive tutorial.
 Category: Control, Pipes, Proxies
-Tested-With: GHC ==7.4.1
 Source-Repository head
     Type: git
     Location: https://github.com/Gabriel439/Haskell-Pipes-Library
 
 Library
     Build-Depends:
-        base >= 4 && < 5,
-        transformers >= 0.2.0.0
+        base         >= 4       && < 5  ,
+        mmorph       >= 1.0.0   && < 1.1,
+        transformers >= 0.2.0.0 && < 0.4
     Exposed-Modules:
-        Control.MFunctor,
-        Control.PFunctor,
         Control.Pipe,
         Control.Proxy,
         Control.Proxy.Class,
         Control.Proxy.Core,
         Control.Proxy.Core.Fast,
         Control.Proxy.Core.Correct,
+        Control.Proxy.ListT,
+        Control.Proxy.Morph,
         Control.Proxy.Pipe,
         Control.Proxy.Synonym,
         Control.Proxy.Trans,
+        Control.Proxy.Trans.Codensity,
         Control.Proxy.Trans.Either,
         Control.Proxy.Trans.Identity,
         Control.Proxy.Trans.Maybe,
@@ -66,4 +69,4 @@
         Control.Proxy.Prelude.Base,
         Control.Proxy.Prelude.IO,
         Control.Proxy.Prelude.Kleisli
-    Default-Language: Haskell98
+    GHC-Options: -O2
