diff --git a/Control/MFunctor.hs b/Control/MFunctor.hs
--- a/Control/MFunctor.hs
+++ b/Control/MFunctor.hs
@@ -5,7 +5,9 @@
 module Control.MFunctor (
     -- * Functors over Monads
     MFunctor(..),
-    raise
+    hoistK,
+    raise,
+    raiseK
     ) where
 
 import Control.Monad.Trans.Class (MonadTrans(lift))
@@ -18,11 +20,26 @@
 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
+{- | 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) -> t m b -> t n b
+    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
@@ -48,9 +65,26 @@
 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
--- a/Control/PFunctor.hs
+++ b/Control/PFunctor.hs
@@ -5,28 +5,85 @@
 module Control.PFunctor (
     -- * Functors over Proxies
     PFunctor(..),
-    raiseP
+    hoistPK,
+    raiseP,
+    raisePK,
     ) where
 
 import Control.Proxy.Class (Proxy)
 import Control.Proxy.Trans (ProxyTrans(liftP))
 
--- | A functor in the category of monads
-class PFunctor (
-    t :: (* -> * -> * -> * -> (* -> *) -> * -> *)
-      ->  * -> * -> * -> * -> (* -> *) -> * -> * ) where
-    {-| Lift a proxy morphism from @p@ to @q@ into a proxy morphism from
-        @(t p)@ to @(t q)@ -}
+{-| 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 p)
-     => (forall a' a b' b r1 . p a' a b' b m r1 -> q a' a b' b m r1)
-     -> (t p a' a b' b m r2 -> t q a' a b' b m r2)
+     :: (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 -> t1 (t2 p) a' a b' b m r
+ => 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/Proxy/Class.hs b/Control/Proxy/Class.hs
--- a/Control/Proxy/Class.hs
+++ b/Control/Proxy/Class.hs
@@ -1,5 +1,3 @@
-{-# LANGUAGE Rank2Types #-}
-
 {-| 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.
@@ -9,6 +7,8 @@
     duplicate methods.  Instead, read the \"Polymorphic proxies\" section below
     which explains their purpose and how they help clean up type signatures. -}
 
+{-# LANGUAGE Rank2Types #-}
+
 module Control.Proxy.Class (
     -- * Core proxy class
     Proxy(..),
@@ -258,18 +258,6 @@
 > p >~> coidT = p
 >
 > (p1 >~> p2) >~> p3 = p1 >~> (p2 >~> p3)
-
-    * @(hoistK f)@ defines a functor between proxy categories:
-
-> Define: hoistK f = (hoist f .)
->
-> hoistK f (p1 >-> p2) = hoistK f p1 >-> hoistK p2
->
-> hoistK f idT = idT
->
-> hoistK f (p1 >~> p2) = hoistK f p1 >~> hoistK p2
->
-> hoistK f coidT = coidT
 
     Also, all proxies must satisfy the following 'Proxy' laws:
 
diff --git a/Control/Proxy/Core.hs b/Control/Proxy/Core.hs
--- a/Control/Proxy/Core.hs
+++ b/Control/Proxy/Core.hs
@@ -10,10 +10,11 @@
     module Control.Proxy.Trans.Identity,
     module Control.Monad,
     module Control.Monad.Trans.Class,
-    module Control.MFunctor
+    module Control.MFunctor,
+    module Control.PFunctor
     ) where
 
-import Control.MFunctor (MFunctor(hoist))
+import Control.MFunctor
 import Control.Monad (forever, (>=>), (<=<))
 import Control.Monad.Trans.Class (MonadTrans(lift))
 import Control.Proxy.Class
@@ -21,6 +22,7 @@
 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
@@ -42,4 +44,6 @@
     "Control.Monad.Trans.Class" exports 'lift'.
 
     "Control.MFunctor" exports 'hoist'.
+
+    "Control.PFunctor" exports 'hoistP'.
 -}
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
@@ -21,6 +21,10 @@
     laws, but also guarantees that it works with the other proxy implementations
     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. -}
+
 module Control.Proxy.Core.Fast (
     -- * Types
     ProxyFast(..),
@@ -36,7 +40,6 @@
     ) where
 
 import Control.Applicative (Applicative(pure, (<*>)))
--- import Control.Monad (ap, forever, liftM, (>=>))
 import Control.Monad.IO.Class (MonadIO(liftIO))
 import Control.Monad.Trans.Class (MonadTrans(lift))
 import Control.MFunctor (MFunctor(hoist))
@@ -98,6 +101,37 @@
         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
+  #-}
+{- 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'
 instance MonadTrans (ProxyFast a' a b' b) where
     lift = _lift
@@ -112,7 +146,22 @@
     "_lift m ?>= f" forall m f .
         _bind (_lift m) f = M (m >>= \r -> return (f r))
   #-}
+{- Proof that the rewrite rule is Trustworthy:
 
+  _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 (MonadIO m) => MonadIO (ProxyFast a' a b' b m) where
     liftIO m = M (liftIO (m >>= \r -> return (Pure r)))
  -- liftIO = M . liftIO . liftM Pure
@@ -154,13 +203,6 @@
     lift_P = _lift
 
     hoist_P = hoist
-
-{-# 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
-  #-}
 
 instance Interact ProxyFast where
     k2 \>\ k1 = \a' -> go (k1 a') where
diff --git a/Control/Proxy/Pipe.hs b/Control/Proxy/Pipe.hs
--- a/Control/Proxy/Pipe.hs
+++ b/Control/Proxy/Pipe.hs
@@ -1,11 +1,12 @@
-{-# LANGUAGE KindSignatures #-}
-
 {-| This module provides an API similar to "Control.Pipe" for those who prefer
     the classic 'Pipe' API.
 
     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. -}
+
+{-# LANGUAGE KindSignatures #-}
+
 module Control.Proxy.Pipe (
     -- * Create Pipes
     await,
@@ -41,7 +42,7 @@
 {-| Deliver output downstream
 
     'yield' restores control back downstream and binds its value to 'await'. -}
-yield :: (Monad m, Proxy p) => b -> p a' a b' b m ()
+yield :: (Monad m, Proxy p) => b -> p a' a () b m ()
 yield b = runIdentityP $ do
     respond b
     return ()
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
@@ -79,16 +79,17 @@
     -- * Modules
     -- $modules
     module Control.Monad.Trans.State.Strict,
-    module Control.Monad.Trans.Writer.Strict,
+    module W,
     module Data.Monoid
     ) where
 
 import Control.MFunctor (hoist)
 import Control.Monad.Trans.Class (lift)
-import Control.Monad.Trans.Writer.Strict (
-    WriterT(runWriterT), execWriterT, runWriter, tell )
+import Control.Monad.Trans.Writer.Lazy as W (
+    WriterT(runWriterT), execWriterT, runWriter )
+import Control.Monad.Trans.Writer.Lazy (tell)
 import Control.Monad.Trans.State.Strict (
-    StateT(runStateT), execStateT, runState, execState, get, put )
+    StateT(StateT, runStateT), execStateT, runState, execState )
 import Control.Proxy.Class
 import Control.Proxy.Synonym
 import Control.Proxy.Trans.Identity (runIdentityP, runIdentityK)
@@ -723,9 +724,7 @@
 foldlD' f = runIdentityK go where
     go x = do
         a  <- request x
-        lift $ do
-            b <- get
-            put $! f b a
+        lift $ StateT $ \b -> let b' = f b a in b' `seq` return ((), b')
         x2 <- respond a
         go x2
 
@@ -734,9 +733,7 @@
  :: (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 $ do
-            b <- get
-            put $! f b a'
+        lift $ StateT $ \b -> let b' = f b a' in b' `seq` return ((), b')
         x   <- request a'
         a'2 <- respond x
         go a'2
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
@@ -1,14 +1,12 @@
-{-# LANGUAGE Rank2Types #-}
-
 -- | Utility functions for Kleisli arrows
 
+{-# LANGUAGE Rank2Types #-}
+
 module Control.Proxy.Prelude.Kleisli (
     -- * Core utility functions
     foreverK,
     replicateK,
     liftK,
-    hoistK,
-    raiseK,
     ) where
 
 import Control.MFunctor (MFunctor(hoist))
@@ -51,37 +49,3 @@
 liftK :: (Monad m, MonadTrans t) => (a -> m b) -> (a -> t m b)
 liftK k a = lift (k a)
 -- liftK = (lift .)
-
-{-| Convenience function equivalent to @(hoist f .)@
-
-> hoistK f p1 >-> hoistK f p2 = hoistK f (p1 >-> p2)
->
-> hoistK f idT = idT
-
-> hoistK f p1 >=> hoistK f p2 = hoistK f (p1 >=> p2)
->
-> hoistK f return = return
-
-> hoistK f . hoistK g = hoistK (f . g)
->
-> hoistK id = id
--}
-hoistK
- :: (Monad m, MFunctor t)
- => (forall a . m a -> n a) -> ((b' -> t m b) -> (b' -> t n b))
-hoistK k p a' = hoist k (p a')
--- hoistK k = (hoist k .)
-
-{-| Convenience function equivalent to @(hoist lift .)@
-
-> raiseK p1 >-> raiseK p2 = raiseK (p1 >-> p2)
->
-> raiseK idT = idT
-
-> raiseK p1 >=> raiseK p2 = raiseK (p1 >=> p2)
->
-> raiseK return = return
--}
-raiseK
- :: (Monad m, MFunctor t1, MonadTrans t2) => (q -> t1 m r) -> (q -> t1 (t2 m) r)
-raiseK = (hoist lift .)
diff --git a/Control/Proxy/Synonym.hs b/Control/Proxy/Synonym.hs
--- a/Control/Proxy/Synonym.hs
+++ b/Control/Proxy/Synonym.hs
@@ -1,7 +1,7 @@
-{-# LANGUAGE KindSignatures #-}
-
 {-| These type synonyms simplify type signatures when proxies do not use all
     their type variables. -}
+
+{-# LANGUAGE KindSignatures #-}
 
 module Control.Proxy.Synonym (
     -- * Synonyms
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
@@ -1,6 +1,6 @@
 -- | This module provides the proxy transformer equivalent of 'EitherT'.
 
-{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE KindSignatures, CPP #-}
 
 module Control.Proxy.Trans.Either (
     -- * EitherP
@@ -24,7 +24,10 @@
 import Control.PFunctor (PFunctor(hoistP))
 import Control.Proxy.Class
 import Control.Proxy.Trans (ProxyTrans(liftP))
+#if MIN_VERSION_base(4,6,0)
+#else
 import Prelude hiding (catch)
+#endif
 
 -- | The 'Either' proxy transformer
 newtype EitherP e p a' a b' b (m :: * -> *) r
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,11 +7,11 @@
     ReaderP(..),
     runReaderP,
     runReaderK,
-    withReaderP,
     -- * Reader operations
     ask,
-    local,
     asks,
+    local,
+    withReaderP,
     ) where
 
 import Control.Applicative (Applicative(pure, (<*>)), Alternative(empty, (<|>)))
@@ -133,12 +133,6 @@
 runReaderK i p q = runReaderP i (p q)
 -- runReaderK i = (runReaderP i .)
 
--- | 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
-withReaderP f p = ReaderP (\i -> unReaderP p (f i))
--- withReaderP f p = ReaderP $ unReaderP p . f
-
 -- | Get the environment
 ask :: (Proxy p, Monad m) => ReaderP i p a' a b' b m i
 ask = ReaderP return_P
@@ -151,3 +145,9 @@
 local
  :: (i -> i) -> ReaderP i p a' a b' b m r -> ReaderP i p a' a b' b m r
 local = withReaderP
+
+-- | 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
+withReaderP f p = ReaderP (\i -> unReaderP p (f i))
+-- withReaderP f p = ReaderP $ unReaderP p . f
diff --git a/Control/Proxy/Tutorial.hs b/Control/Proxy/Tutorial.hs
--- a/Control/Proxy/Tutorial.hs
+++ b/Control/Proxy/Tutorial.hs
@@ -66,7 +66,6 @@
 import Control.Proxy
 import Control.Proxy.Core.Correct (ProxyCorrect)
 import Control.Proxy.Trans.Either
-import Prelude hiding (catch)
 
 {- $intro
     The @pipes@ library replaces lazy 'IO' with a safe, elegant, and
@@ -91,10 +90,10 @@
 > import Control.Proxy
 > import System.IO
 > 
-> --                Produces Strings ---+----------+
-> --                                    |          |
-> --                                    v          v
-> lines' :: (Proxy p) => Handle -> () -> Producer p String IO r
+> --                 Produces Strings ---+----------+
+> --                                     |          |
+> --                                     v          v
+> lines' :: (Proxy p) => Handle -> () -> Producer p String IO ()
 > lines' h () = runIdentityP loop where
 >     loop = do
 >         eof <- lift $ hIsEOF h
@@ -138,9 +137,9 @@
 > --                Self-contained session ---+         +--+-- These must match
 > --                                          |         |  |   each component
 > --                                          v         v  v
-> promptInt >-> printer :: (Proxy p) => () -> Session p IO r
->
 > lines' h  >-> printer :: (Proxy p) => () -> Session p IO ()
+>
+> promptInt >-> printer :: (Proxy p) => () -> Session p IO r
 
     ('>->') connects each 'request' in @printer@ with a 'respond' in
     @lines'@ or @promptInt@.
@@ -157,7 +156,7 @@
     The following program never brings more than a single line into memory (not
     that it matters for such a small file):
 
->>> withFile "test.txt" $ \h -> runProxy $ lines' h >-> printer
+>>> withFile "test.txt" ReadMode $ \h -> runProxy $ lines' h >-> printer
 Received a value:
 "Line 1"
 Received a value:
@@ -220,7 +219,8 @@
 
     * You can define your own lazy components that have nothing to do with files
 
-    * @pipes@ never uses 'unsafePerformIO' or violates referential transparency.
+    * @pipes@ never uses 'unsafePerformIO' and never violates referential
+      transparency.
 
     * You don't need strictness hacks to ensure the proper ordering of effects
 
@@ -811,14 +811,14 @@
     When you compose two proxies, you interleave their effects in the base
     monad.  The following two proxies demonstrate this interleaving of effects:
 
-> downstream :: (Proxy p) => Consumer p () IO ()
+> 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 :: (Proxy p) => () -> Producer p () IO ()
 > upstream () = runIdentityP $ do
 >     lift $ print 2
 >     respond () -- Switch to downstraem
@@ -999,7 +999,7 @@
 
     The @S@ suffix indicates that it belongs in the \'@S@\'erver position.
 
-    @(takeB_ n)@ allows at most @n@ value to pass through it in \'@B@\'oth
+    @(takeB_ n)@ allows at most @n@ values to pass through it in \'@B@\'oth
     directions:
 
 > takeB_ :: (Monad m, Proxy p) => Int -> a' -> p a' a a' a m ()
@@ -1071,7 +1071,7 @@
 Received a value:
 37
 
-    What about our original @lines@ function?  That's just 'hGetLineS':
+    What about our original @lines'@ function?  That's just 'hGetLineS':
 
 > hGetLineS :: (Proxy p) => Handle -> () -> Producer p String IO ()
 
@@ -1094,7 +1094,7 @@
     Composition isn't the only way to assemble proxies.  You can also sequence
     predefined proxies using @do@ notation to generate more elaborate behaviors.
 
-    Most commonly, you will sequence two sources to combine their outputs, very
+    Most commonly, you will sequence sources to combine their outputs, very
     similar to how the Unix @cat@ utility behaves:
 
 > threeSources () = do
@@ -1262,7 +1262,7 @@
     You can also run multiple folds at the same time just by adding more
     'WriterT' layers to your base monad:
 
->>> runWriterT $ runWriterT $ fromListS [9, 10] >-> anyD even >-> raiseK sumD
+>>> runWriterT $ runWriterT $ runProxy $ fromListS [9, 10] >-> anyD even >-> raiseK sumD
 (((), Any {getAny = True},Sum {getSum = 19})
 
     I designed certain special folds to terminate the 'Session' early if they
@@ -1297,8 +1297,8 @@
     and write a streaming utility that lazily opens a file only in response to
     a 'request', such as the following 'Producer':
 
-> readFile' :: FilePath -> () -> Producer p String IO
-> readFile' file () = runIdentityP $ do
+> readFileS :: FilePath -> () -> Producer p String IO
+> readFileS file () = runIdentityP $ do
 >     h <- lift $ openFile file ReadMode
 >     lift $ putStrLn "Opening file"
 >     hGetLineS h ()
@@ -1307,7 +1307,7 @@
 
     This works well if we fully demand the file:
 
->>> runProxy $ readFile' "test.txt" >-> printD
+>>> runProxy $ readFileS "test.txt" >-> printD
 Opening file
 "Line 1"
 "Line 2"
@@ -1317,27 +1317,32 @@
     This also works well if we never demand the file at all, in which case we
     never open it:
 
->>> runProxy $ readFile' "test.txt" >-> return
+>>> runProxy $ readFileS "test.txt" >-> return
 -- Outputs nothing
 
     But it gives exactly the wrong behavior if we partially demand the file:
 
->>> runProxy $ readFile' "test.txt" >-> takeB_ 1 >-> printD
+>>> runProxy $ readFileS "test.txt" >-> takeB_ 1 >-> printD
 Opening file
 "Line 1"
 
     Notice that this does not close the file, because once @takeB_ 1@ terminates
-    it terminates the entire 'Session' and @readFile'@ does not get a chance to
+    it terminates the entire 'Session' and @readFileS@ does not get a chance to
     finalize the file.
 
-    I will release a separate library in the near future that offers lazy
-    resource management, too, but in the meantime I advise that you use one of
-    the following two strategies to guarantee deterministic resource
-    deallocation.
+    The @pipes-safe@ library solves this problem by providing resource
+    management abstractions built on top of @pipes@ and offers several other
+    nice features:
 
-    The first approach opens all resources before running the session and close
+    * It is completely exception safe, even against asynchronous exceptions
+
+    * 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@
-    command, streaming one line at a time, I would write:
+    command, streaming one line at a time, I might write:
 
 > import System.IO
 >
@@ -1345,46 +1350,36 @@
 > cp inFile outFile =
 >     withFile file1 ReadMode  $ \hIn  ->
 >     withFile file2 WriteMode $ \hOut ->
->     runProxy $ hGetLineS hIn >-> hPutLineS hOut2
-
-    The advantage of this approach is that it:
+>     runProxy $ hGetLineS hIn >-> hPutLineS hOut
 
-    * is straightforward,
+    Some people prefer that approach because it:
 
-    * requires no special integration with existing libraries, and
+    * is straightforward, and
 
-    * is exception safe.
+    * can reuse functions from @Control.Exception@
 
     The disadvantage is that this does not lazily allocate resources, nor does
-    this promptly deallocate them.
-
-    The second approach is to use something like 'ResourceT' (from the
-    @resourceT@ package) to register finalizers and ensure they get released
-    deterministically.  You may prefer this approach if you have previously used
-    the @conduit@ library, which uses 'ResourceT' in its base monad to offer
-    resource determinism.  You can use 'ResourceT' with @pipes@, too, just by
-    including it in the base monad.
-
-    I plan to release a lazy resource management library very soon built on top
-    of @pipes@ that behaves similarly to 'ResourceT'.  The main advantages of
-    this upcoming implementation will be that it:
+    this promptly deallocate them.  Also, there is no way to recover from
+    exceptions and resume the 'Session'.  On the other hand, @pipes-safe@ lets
+    you do all of these.
 
-    * uses a simpler and pure implementation
+    Fortunately, you can choose whichever approach you prefer and rest assured
+    that the two approaches safely interoperate.  @Control.Proxy.Safe.Tutorial@
+    from the @pipes-safe@ package provides a separate tutorial on how to:
 
-    * obeys several useful theoretical laws
+    * extend @pipes@ with resource management,
 
-    * requires no dependencies other than @pipes@
+    * handle exceptions natively within proxies, and
 
-    However, if you don't need this extra power, then just stick to the former
-    simpler approach.  I plan to release all standard libraries to be agnostic
-    of the finalization approach to let you use which one you prefer.
+    * interoperate with unmanaged code.
 -}
 
 {- $extend
     This library provides several extensions that add features on top of the
     base 'Proxy' API.  These extensions behave like monad transformers, except
     that they also lift the 'Proxy' class through the extension so that the
-    extended proxy can still 'request', 'respond', compose with other proxies:
+    extended proxy can still 'request', 'respond', and compose with other
+    proxies:
 
 > instance (Proxy p) => Proxy (IdentityP p)  -- Equivalent to IdentityT
 > instance (Proxy p) => Proxy (EitherP e p)  -- Equivalent to EitherT
@@ -1411,8 +1406,8 @@
 >         Just n  -> respond n
 
     There is no way to recover from the error and resume streaming data.  You
-    can only handle 'Left' value after using 'runProxy', but by then it is too 
-    late.
+    can only handle the 'Left' value after using 'runProxy', but by then it is
+    too late.
 
     We can solve this by switching the order of the two monad transformers, but
     using 'EitherP' this time instead of 'EitherT':
@@ -1474,7 +1469,7 @@
 >     lift $ putStrLn err  -- Print the error
 >     heartbeat p          -- Restart 'p'
 
-    This uses the 'catch' function from "Control.Proxy.Trans.Either", which
+    This uses the 'E.catch' function from "Control.Proxy.Trans.Either", which
     lets you catch and handle errors locally without disturbing other proxies.
 
 >>> runProxy $ E.runEitherK $ (heartbeat . promptInt3) >-> takeB_ 2 >-> printer
@@ -1560,13 +1555,14 @@
 
 > zipD
 >  :: (Monad m, Proxy p1, Proxy p2, Proxy p3)
->  => () -> Consumer p1 a (Consumer p2 b (Consumer p3 (a, b) m)) r
-> zipD = runIdentityP . hoist (runIdentityP . hoist runIdentityP) $ forever $ do
+>  => () -> 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'
+>         a <- request ()               -- Request from the outer 'Consumer'
+>         b <- lift $ request ()        -- Request from the inner 'Consumer'
+>         lift $ lift $ respond (a, b)  -- Respond to the 'Producer'
 
     'zipD' behaves analogously to a curried function.  We partially apply it to
     each layer using composition and 'runProxyK' or 'runProxy':
@@ -1699,15 +1695,15 @@
 >       :: (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)
->      => (q -> p a' a b' b m r) -> (q -> t p a' a b' b m r)
->     mapP = (liftP . )
+> -- 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 . )
 
-    It's very easy to use.  Just use 'mapP' (equivalent to @(liftP .)@ to lift
-    one proxy transformer to match another one.  For example, we can 'mapP'
-    @increment2@ to match @promptInt3@:
+    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 >-> mapP increment2
 >  :: (Proxy p) => () -> Session (EitherP String (StateP Int p)) IO r
@@ -1773,10 +1769,9 @@
 >
 > (liftP .) return = return
 
-    The only difference is that I also include 'mapP' in the 'ProxyTrans' type
-    class for convenience, which sweetens these laws a little bit:
+    The only difference is 'mapP' sweetens these laws a little bit:
 
-> mapP = (lift .)
+> mapP = (liftP .)
 >
 > mapP (f >=> g) = mapP f >=> mapP g  -- These are functor laws!
 >
@@ -1788,7 +1783,7 @@
 
     This means that we need a set of laws that guarantee that the proxy
     transformer lifts the 'Proxy' instance correctly.  I call these laws the
-    \"proxy transformer laws\":
+    \"proxy morphism laws\":
 
 > mapP (f >-> g) = mapP f >-> mapP g  -- These are functor laws, too!
 >
@@ -1828,16 +1823,16 @@
 >
 > mapP respond = respond
 
-    We can translate those to 'liftP' to get:
+    We can translate those back to 'liftP' to get:
 
-> liftP $ request a' = request a'
+> liftP (request a') = request a'
 >
-> liftP $ respond b  = respond b
+> liftP (respond b)  = respond b
 
     In other words, 'request' and 'respond' in the extended proxy must behave
     exactly the same as lifting 'request' and 'respond' from the base proxy.
 
-    All the proxy transformers in this library obey the proxy transformer laws,
+    All the proxy transformers in this library obey the proxy morphism laws,
     which ensure that 'liftP' / 'mapP' always do \"the right thing\".
 
     Proxy transformers also implement 'hoistP' from the 'PFunctor' class in
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c) 2012, Gabriel Gonzalez
+Copyright (c) 2012, 2013 Gabriel Gonzalez
 All rights reserved.
 
 Redistribution and use in source and binary forms, with or without modification,
diff --git a/pipes.cabal b/pipes.cabal
--- a/pipes.cabal
+++ b/pipes.cabal
@@ -1,10 +1,10 @@
 Name: pipes
-Version: 3.0.0
+Version: 3.1.0
 Cabal-Version: >=1.14.0
 Build-Type: Simple
 License: BSD3
 License-File: LICENSE
-Copyright: 2012 Gabriel Gonzalez
+Copyright: 2012, 2013 Gabriel Gonzalez
 Author: Gabriel Gonzalez
 Maintainer: Gabriel439@gmail.com
 Bug-Reports: https://github.com/Gabriel439/Haskell-Pipes-Library/issues