diff --git a/Control/Comonad/Trans/Class.hs b/Control/Comonad/Trans/Class.hs
new file mode 100644
--- /dev/null
+++ b/Control/Comonad/Trans/Class.hs
@@ -0,0 +1,21 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Control.Comonad.Trans.Class
+-- Copyright   :  (C) 2008-2011 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  provisional
+-- Portability :  portable
+----------------------------------------------------------------------------
+module Control.Comonad.Trans.Class (ComonadTrans(..)) where
+
+import Control.Comonad
+import Control.Monad.Trans.Identity
+
+class ComonadTrans t where
+  lower :: Comonad w => t w a -> w a 
+
+-- avoiding orphans
+instance ComonadTrans IdentityT where
+  lower = runIdentityT
diff --git a/Control/Comonad/Trans/Discont.hs b/Control/Comonad/Trans/Discont.hs
new file mode 100644
--- /dev/null
+++ b/Control/Comonad/Trans/Discont.hs
@@ -0,0 +1,56 @@
+{-# LANGUAGE RankNTypes #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Control.Comonad.Trans.Discont
+-- Copyright   :  (C) 2008-2011 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  provisional
+-- Portability :  portable
+-- 
+-- Discont is the Density comonad of a constant functor, just as Cont is a 
+-- Codensity monad of a constant functor.
+--
+-- Note that Discont and Context are isomorphic, but DiscontT and ContextT are
+-- not.
+--
+----------------------------------------------------------------------------
+module Control.Comonad.Trans.Discont
+  ( Discont
+  , discont
+  , runDiscont
+  , DiscontT(..)
+  , runDiscontT
+  , callCV
+  ) where
+
+import Data.Functor.Identity
+import Control.Comonad
+import Control.Comonad.Trans.Class
+
+type Discont s = DiscontT s Identity
+
+data DiscontT s w a = DiscontT (w s -> a) (w s)
+
+discont :: (s -> a) -> s -> Discont s a 
+discont f s = DiscontT (f . runIdentity) (Identity s)
+
+runDiscont :: Discont s a -> (s -> a, s) 
+runDiscont (DiscontT f (Identity s)) = (f . Identity,  s)
+
+runDiscontT :: DiscontT s w a -> (w s -> a, w s)
+runDiscontT (DiscontT f s) = (f, s)
+
+instance Functor w => Functor (DiscontT s w) where
+  fmap g (DiscontT f ws) = DiscontT (g . f) ws
+
+instance Comonad w => Comonad (DiscontT s w) where
+  extract (DiscontT f ws) = f ws
+  duplicate (DiscontT f ws) = DiscontT (DiscontT f) ws
+
+instance ComonadTrans (DiscontT s) where
+  lower (DiscontT f s) = extend f s
+
+callCV :: DiscontT s w (DiscontT s w (DiscontT s w a -> a) -> b) -> b
+callCV (DiscontT k s) = k s (DiscontT (\s' (DiscontT k' _) -> k' s') s)
diff --git a/Control/Comonad/Trans/Env.hs b/Control/Comonad/Trans/Env.hs
new file mode 100644
--- /dev/null
+++ b/Control/Comonad/Trans/Env.hs
@@ -0,0 +1,52 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Control.Comonad.Trans.Context
+-- Copyright   :  (C) 2008-2011 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  provisional
+-- Portability :  portable
+--
+-- The environment comonad transformer (aka coreader).
+-- This adds an extra value that can be accessed in the environment.
+--
+-- Left adjoint to the reader comonad.
+----------------------------------------------------------------------------
+module Control.Comonad.Trans.Env
+  ( Env
+  , env
+  , runEnv
+  , EnvT(..)
+  , runEnvT
+  , ask
+  ) where
+
+import Control.Comonad
+import Control.Comonad.Trans.Class
+import Data.Functor.Identity
+
+type Env e = EnvT e Identity
+data EnvT e w a = EnvT e (w a)
+
+env :: e -> a -> Env e a
+env e a = EnvT e (Identity a)
+
+runEnv :: Env e a -> (e, a)
+runEnv (EnvT e (Identity a)) = (e, a)
+
+runEnvT :: EnvT e w a -> (e, w a)
+runEnvT (EnvT e wa) = (e, wa)
+
+instance Functor w => Functor (EnvT e w) where
+  fmap g (EnvT e wa) = EnvT e (fmap g wa)
+
+instance Comonad w => Comonad (EnvT e w) where
+  extract (EnvT _ wa) = extract wa
+  duplicate p@(EnvT e wa) = EnvT e (p <$ wa)
+
+instance ComonadTrans (EnvT e) where
+  lower (EnvT _ wa) = wa
+
+ask :: EnvT e w a -> e
+ask (EnvT e _) = e
diff --git a/Control/Comonad/Trans/Identity.hs b/Control/Comonad/Trans/Identity.hs
new file mode 100644
--- /dev/null
+++ b/Control/Comonad/Trans/Identity.hs
@@ -0,0 +1,29 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Control.Comonad.Trans.Identity
+-- Copyright   :  (C) 2008-2011 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  provisional
+-- Portability :  portable
+-- 
+----------------------------------------------------------------------------
+module Control.Comonad.Trans.Identity
+  ( IdentityT(..)
+  ) where
+
+import Control.Monad.Trans.Identity
+
+-- Provided by Control.Comonad to avoid an orphan
+{-
+instance Comonad w => Comonad (IdentityT w) where
+  extract = extract . runIdentityT
+  extend f (IdentityT m) = IdentityT (extend (f . IdentityT) m)
+-}
+
+-- Provided by Control.Comonad.Trans.Class to avoid an orphan
+{-
+instance ComonadTrans IdentityT where
+  colift = IdentityT
+-}
diff --git a/Control/Comonad/Trans/Store.hs b/Control/Comonad/Trans/Store.hs
new file mode 100644
--- /dev/null
+++ b/Control/Comonad/Trans/Store.hs
@@ -0,0 +1,71 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Control.Comonad.Trans.Store
+-- Copyright   :  (C) 2008-2011 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  provisional
+-- Portability :  portable
+--
+-- The store (state-in-context/costate) comonad transformer is subject to the laws:
+-- 
+-- > x = put (get x) x
+-- > y = get (put y x)
+-- > put y x = put y (put z x)
+--
+-- Thanks go to Russell O'Connor and Daniel Peebles for their help formulating 
+-- and proving the laws for this comonad transformer.
+----------------------------------------------------------------------------
+module Control.Comonad.Trans.Store 
+  ( 
+  -- * The Store comonad
+    Store, store, runStore
+  -- * The Store comonad transformer
+  , StoreT(..), runStoreT
+  -- * Operations
+  , get
+  , put
+  , modify
+  , experiment
+  ) where
+
+import Control.Comonad
+import Control.Comonad.Trans.Class
+import Data.Functor.Identity
+
+type Store s = StoreT s Identity
+
+store :: (s -> a) -> s -> Store s a 
+store f s = StoreT (Identity f) s
+
+runStore :: Store s a -> (s -> a, s)
+runStore (StoreT (Identity f) s) = (f, s)
+
+data StoreT s w a = StoreT (w (s -> a)) s
+
+runStoreT :: StoreT s w a -> (w (s -> a), s)
+runStoreT (StoreT wf s) = (wf, s)
+
+instance Functor w => Functor (StoreT s w) where
+  fmap f (StoreT wf s) = StoreT (fmap (f .) wf) s
+
+instance Comonad w => Comonad (StoreT s w) where
+  extract (StoreT wf s) = extract wf s
+  duplicate (StoreT wf s) = StoreT (extend StoreT wf) s
+  extend f (StoreT wf s) = StoreT (extend (\wf' s' -> f (StoreT wf' s')) wf) s
+
+instance ComonadTrans (StoreT s) where
+  lower (StoreT f s) = fmap ($s) f
+
+get :: StoreT s w a -> s
+get (StoreT _ s) = s
+
+put :: Comonad w => s -> StoreT s w a -> a 
+put s (StoreT f _) = extract f s
+
+modify :: Comonad w => (s -> s) -> StoreT s w a -> a
+modify f (StoreT g s) = extract g (f s)
+
+experiment :: (Comonad w, Functor f) => f (s -> s) -> StoreT s w a -> f a
+experiment fs (StoreT g s) = fmap (\f -> extract g (f s)) fs
diff --git a/Control/Comonad/Trans/Stream.hs b/Control/Comonad/Trans/Stream.hs
new file mode 100644
--- /dev/null
+++ b/Control/Comonad/Trans/Stream.hs
@@ -0,0 +1,70 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Control.Comonad.Trans.Stream
+-- Copyright   :  (C) 2008-2011 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  provisional
+-- Portability :  portable
+--
+-- The f-branching stream comonad, aka the cofree comonad for a Functor f.
+-- 
+-- Provided here as a comonad-transformer version of the 'ListT done right' 
+-- monad transformer.
+----------------------------------------------------------------------------
+module Control.Comonad.Trans.Stream 
+  ( 
+  -- * The Stream comonad
+    Stream, stream, runStream
+  -- * The Stream comonad transformer
+  , StreamT(..)
+  -- * Operations
+  , tails
+  , unfolds
+  , unfoldsW
+  ) where
+
+import Control.Applicative
+import Control.Comonad
+import Control.Comonad.Trans.Class
+import Data.Functor.Identity
+import Data.Foldable
+import Data.Monoid
+import Data.Traversable
+
+type Stream f = StreamT f Identity
+
+stream :: a -> f (Stream f a) -> Stream f a 
+stream a as = StreamT (Identity (a, as))
+
+runStream :: Stream f a -> (a, f (Stream f a))
+runStream = runIdentity . runStreamT
+
+data StreamT f w a = StreamT { runStreamT :: w (a, f (StreamT f w a)) }
+
+instance (Functor w, Functor f) => Functor (StreamT f w) where
+  fmap f = StreamT . fmap (\(a, as) -> (f a, fmap f <$> as)) . runStreamT
+
+instance (Comonad w, Functor f) => Comonad (StreamT f w) where
+  extract = fst . extract . runStreamT
+  duplicate = StreamT . extend (\w -> (StreamT w, duplicate <$> snd (extract w))) . runStreamT
+  extend f = StreamT . extend (\w -> (f (StreamT w), extend f <$> snd (extract w))) . runStreamT
+
+instance Functor f => ComonadTrans (StreamT f) where
+  lower = fmap fst . runStreamT
+
+instance (Foldable w, Foldable f) => Foldable (StreamT f w) where
+  foldMap f = foldMap (\(a, as) -> f a `mappend` foldMap (foldMap f) as) . runStreamT
+
+instance (Traversable w, Traversable f) => Traversable (StreamT f w) where
+  traverse f (StreamT w) = StreamT <$> traverse (\(a, as) -> (,) <$> f a <*> traverse (traverse f) as) w
+
+tails :: Comonad w => StreamT f w a -> f (StreamT f w a)
+tails = snd . extract . runStreamT
+
+unfolds :: Functor f => (a -> (b, f a)) -> a -> Stream f b
+unfolds f a = let (h, t) = f a in stream h (unfolds f <$> t)
+
+unfoldsW :: (Comonad w, Functor f) => (w a -> (b, f a)) -> w a -> StreamT f w b
+unfoldsW f = StreamT . extend (\s -> let (h, t) = f s in (h, fmap (\a -> unfoldsW f (a <$ s)) t))
diff --git a/Control/Comonad/Trans/Traced.hs b/Control/Comonad/Trans/Traced.hs
new file mode 100644
--- /dev/null
+++ b/Control/Comonad/Trans/Traced.hs
@@ -0,0 +1,52 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Control.Comonad.Trans.Traced
+-- Copyright   :  (C) 2008-2011 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  provisional
+-- Portability :  portable
+--
+-- The trace comonad transformer (aka the cowriter or exponential comonad transformer).
+--
+----------------------------------------------------------------------------
+module Control.Comonad.Trans.Traced
+  ( 
+  -- * Traced comonad
+    Traced
+  , traced
+  , runTraced
+  -- * Traced comonad transformer
+  , TracedT(..)
+  -- * Operations
+  , trace
+  ) where
+
+import Control.Comonad
+import Control.Comonad.Trans.Class
+import Data.Functor.Identity
+import Data.Monoid
+
+type Traced m = TracedT m Identity
+
+traced :: (m -> a) -> Traced m a
+traced f = TracedT (Identity f)
+
+runTraced :: Monoid m => Traced m a -> m -> a
+runTraced (TracedT (Identity f)) = f
+
+newtype TracedT m w a = TracedT { runTracedT :: w (m -> a) }
+
+instance Functor w => Functor (TracedT m w) where
+  fmap g = TracedT . fmap (g .) . runTracedT
+
+instance (Comonad w, Monoid m) => Comonad (TracedT m w) where
+  extract (TracedT wf) = extract wf mempty
+  extend f = TracedT . extend (\wf m -> f (TracedT (fmap (. mappend m) wf))) . runTracedT
+
+instance Monoid m => ComonadTrans (TracedT m) where
+  lower = fmap ($mempty) . runTracedT
+
+trace :: (Comonad w, Monoid m) => m -> TracedT m w a -> a
+trace m (TracedT wf) = extract wf m
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright 2008-2011 Edward Kmett
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright
+   notice, this list of conditions and the following disclaimer in the
+   documentation and/or other materials provided with the distribution.
+
+3. Neither the name of the author nor the names of his contributors
+   may be used to endorse or promote products derived from this software
+   without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS OR
+IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED.  IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE FOR
+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,
+STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
+ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.lhs b/Setup.lhs
new file mode 100644
--- /dev/null
+++ b/Setup.lhs
@@ -0,0 +1,7 @@
+#!/usr/bin/runhaskell
+> module Main (main) where
+
+> import Distribution.Simple
+
+> main :: IO ()
+> main = defaultMain
diff --git a/comonad-transformers.cabal b/comonad-transformers.cabal
new file mode 100644
--- /dev/null
+++ b/comonad-transformers.cabal
@@ -0,0 +1,33 @@
+name:          comonad-transformers
+category:      Control, Comonads
+version:       0.1.0
+license:       BSD3
+cabal-version: >= 1.2
+license-file:  LICENSE
+author:        Edward A. Kmett
+maintainer:    Edward A. Kmett <ekmett@gmail.com>
+stability:     provisional
+homepage:      http://comonad.com/reader/
+copyright:     Copyright (C) 2008-2011 Edward A. Kmett
+synopsis:      Comonad transformers
+description:   Comonad transformers
+build-type:    Simple
+extra-source-files: coq/Store.v
+
+library
+  build-depends: 
+    base > 4 && < 5,
+    array >= 0.3.0.1 && < 0.4,
+    comonad >= 0.1.0 && < 0.2,
+    transformers >= 0.2.0 && <= 0.3
+
+  exposed-modules:
+    Control.Comonad.Trans.Class
+    Control.Comonad.Trans.Discont
+    Control.Comonad.Trans.Env
+    Control.Comonad.Trans.Identity
+    Control.Comonad.Trans.Store
+    Control.Comonad.Trans.Traced
+    Control.Comonad.Trans.Stream
+
+  ghc-options:      -Wall 
diff --git a/coq/Store.v b/coq/Store.v
new file mode 100644
--- /dev/null
+++ b/coq/Store.v
@@ -0,0 +1,96 @@
+(* Proof StoreT forms a comonad -- Russell O'Connor *)
+
+Set Implict Arguments.
+Unset Strict Implicit.
+
+Require Import FunctionalExtensionality.
+
+Record Comonad (w : Type -> Type) : Type :=
+ { extract : forall a, w a -> a
+ ; extend : forall a b, (w a -> b) -> w a -> w b
+ ; law1 : forall a x, extend _ _ (extract a) x = x
+ ; law2 : forall a b f x, extract b (extend a _ f x) = f x
+ ; law3 : forall a b c f g x, extend b c f (extend a b g x) = extend a c (fun y => f (extend a b g y)) x
+ }.
+
+Section StoreT.
+
+Variables (s : Type) (w:Type -> Type).
+Hypothesis wH : Comonad w.
+
+Definition map a b f x := extend _ wH a b (fun y => f (extract _ wH _ y)) x.
+
+Lemma map_extend : forall a b c f g x, map b c f (extend _ wH a b g x) = extend _ wH _ _ (fun y => f (g y)) x.
+Proof.
+intros a b c f g x.
+unfold map.
+rewrite law3.
+apply equal_f.
+apply f_equal.
+extensionality y.
+rewrite law2.
+reflexivity.
+Qed.
+
+Record StoreT (a:Type): Type := mkStoreT
+  {store : w (s -> a)
+  ;loc   : s}.
+
+Definition extractST a (x:StoreT a) : a := 
+ extract _ wH _ (store _ x) (loc _ x).
+
+Definition mapST a b (f:a -> b) (x:StoreT a) : StoreT b :=
+ mkStoreT _ (map _ _ (fun g x => f (g x)) (store _ x)) (loc _ x).
+
+Definition duplicateST a (x:StoreT a) : StoreT (StoreT a) :=
+ mkStoreT _ (extend _ wH _ _ (mkStoreT _) (store _ x)) (loc _ x).
+
+Let extendST := fun a b f x => mapST _ b f (duplicateST a x).
+
+Lemma law1ST : forall a x, extendST _ _ (extractST a) x = x.
+Proof.
+intros a [v b].
+unfold extractST, extendST, duplicateST, mapST.
+simpl.
+rewrite map_extend.
+simpl.
+replace (fun (y : w (s -> a)) (x : s) => extract w wH (s -> a) y x)
+ with (extract w wH (s -> a)).
+ rewrite law1.
+ reflexivity.
+extensionality y.
+extensionality x.
+reflexivity.
+Qed.
+
+Lemma law2ST : forall a b f x, extractST b (extendST a _ f x) = f x.
+Proof.
+intros a b f [v c].
+unfold extendST, mapST, extractST.
+simpl.
+rewrite map_extend.
+rewrite law2.
+reflexivity.
+Qed.
+
+Lemma law3ST : forall a b c f g x, extendST b c f (extendST a b g x) = extendST a c (fun y => f (extendST a b g y)) x.
+Proof.
+intros a b c f g [v d].
+unfold extendST, mapST, extractST.
+simpl.
+repeat rewrite map_extend.
+rewrite law3.
+repeat (apply equal_f||apply f_equal).
+extensionality y.
+extensionality x.
+rewrite map_extend.
+reflexivity.
+Qed.
+
+Definition StoreTComonad : Comonad StoreT :=
+ Build_Comonad _ _ _ law1ST law2ST law3ST.
+
+End StoreT.
+
+Check StoreTComonad.
+