diff --git a/free-functors.cabal b/free-functors.cabal
--- a/free-functors.cabal
+++ b/free-functors.cabal
@@ -1,5 +1,5 @@
 name:                free-functors
-version:             0.1.2
+version:             0.2
 synopsis:            Provides free functors that are adjoint to functors that forget class constraints. 
 description:         A free functor is a left adjoint to a forgetful functor. It used to be the case
                      that the only category that was easy to work with in Haskell was Hask itself, so
@@ -33,6 +33,7 @@
   exposed-modules:   
     Data.Functor.Cofree,
     Data.Functor.Free,
+    Data.Functor.HCofree,
     Data.Functor.HFree
 
   default-language:  
diff --git a/src/Data/Functor/Cofree.hs b/src/Data/Functor/Cofree.hs
--- a/src/Data/Functor/Cofree.hs
+++ b/src/Data/Functor/Cofree.hs
@@ -37,14 +37,14 @@
 data Cofree c b where
   Cofree :: c a => (a -> b) -> a -> Cofree c b
 
+counit :: Cofree c b -> b
+counit (Cofree k a) = k a
+
 leftAdjunct :: c a => (a -> b) -> a -> Cofree c b
 leftAdjunct f a = Cofree f a
 
-rightAdjunct :: (a -> Cofree c b) -> a -> b
-rightAdjunct f a = case f a of Cofree k a' -> k a'
-
-leftAdjunct' :: ForallF c f => (f a -> b) -> f a -> Cofree c b
-leftAdjunct' = h instF leftAdjunct
+leftAdjunctF :: ForallF c f => (f a -> b) -> f a -> Cofree c b
+leftAdjunctF = h instF leftAdjunct
   where
     h :: ForallF c f
       => (ForallF c f :- c (f a))
@@ -52,22 +52,30 @@
       -> (f a -> b) -> f a -> Cofree c b
     h (Sub Dict) f = f
 
+-- | @unit = leftAdjunct id@
+unit :: c b => b -> Cofree c b
+unit = leftAdjunct id
+
+-- | @rightAdjunct f = counit . f@
+rightAdjunct :: (a -> Cofree c b) -> a -> b
+rightAdjunct f = counit . f
+
 instance Functor (Cofree c) where
   fmap f (Cofree k a) = Cofree (f . k) a
 
 instance ForallF c (Cofree c) => Comonad (Cofree c) where
-  extract = rightAdjunct id
-  extend = leftAdjunct'
+  extract = counit
+  extend = leftAdjunctF
 
 instance (ForallF c Identity, ForallF c (Cofree c), ForallF c (Compose (Cofree c) (Cofree c)))
   => Applicative (Cofree c) where
-  pure = leftAdjunct' runIdentity . Identity
+  pure = leftAdjunctF runIdentity . Identity
   (<*>) = ap
 
 instance (ForallF c Identity, ForallF c (Cofree c), ForallF c (Compose (Cofree c) (Cofree c)))
   => Monad (Cofree c) where
   return = pure
-  m >>= g = leftAdjunct' (extract . extract . getCompose) (Compose $ fmap g m)
+  m >>= g = leftAdjunctF (extract . extract . getCompose) (Compose $ fmap g m)
 
 convert :: (c (w a), Comonad w) => w a -> Cofree c a
-convert wa = Cofree extract wa
+convert = leftAdjunct extract
diff --git a/src/Data/Functor/Free.hs b/src/Data/Functor/Free.hs
--- a/src/Data/Functor/Free.hs
+++ b/src/Data/Functor/Free.hs
@@ -37,14 +37,14 @@
 -- | The free functor for constraint @c@.
 newtype Free c a = Free { runFree :: forall b. c b => (a -> b) -> b }
 
-leftAdjunct :: (Free c a -> b) -> a -> b
-leftAdjunct f a = f (Free ($ a))
+unit :: a -> Free c a
+unit a = Free $ \k -> k a
 
 rightAdjunct :: c b => (a -> b) -> Free c a -> b
 rightAdjunct f g = runFree g f
 
-rightAdjunct' :: ForallF c f => (a -> f b) -> Free c a -> f b
-rightAdjunct' = h instF rightAdjunct
+rightAdjunctF :: ForallF c f => (a -> f b) -> Free c a -> f b
+rightAdjunctF = h instF rightAdjunct
   where
     h :: ForallF c f
       => (ForallF c f :- c (f b))
@@ -52,8 +52,8 @@
       -> (a -> f b) -> Free c a -> f b
     h (Sub Dict) f = f
 
-rightAdjunct'' :: ForallT c t => (a -> t f b) -> Free c a -> t f b
-rightAdjunct'' = h instT rightAdjunct
+rightAdjunctT :: ForallT c t => (a -> t f b) -> Free c a -> t f b
+rightAdjunctT = h instT rightAdjunct
   where
     h :: ForallT c t
       => (ForallT c t :- c (t f b))
@@ -61,21 +61,29 @@
       -> (a -> t f b) -> Free c a -> t f b
     h (Sub Dict) f = f
 
+-- | @counit = rightAdjunct id@
+counit :: c a => Free c a -> a
+counit = rightAdjunct id
+
+-- | @leftAdjunct f = f . unit@
+leftAdjunct :: (Free c a -> b) -> a -> b
+leftAdjunct f = f . unit
+
 instance Functor (Free c) where
   fmap f (Free g) = Free (g . (. f))
 
 instance Applicative (Free c) where
-  pure = leftAdjunct id
+  pure = unit
   fs <*> as = Free $ \k -> runFree fs (\f -> runFree as (k . f))
 
 instance ForallF c (Free c) => Monad (Free c) where
-  return = pure
-  (>>=) = flip rightAdjunct'
+  return = unit
+  (>>=) = flip rightAdjunctF
 
 instance (ForallF c Identity, ForallF c (Free c), ForallF c (Compose (Free c) (Free c)))
   => Comonad (Free c) where
-  extract = runIdentity . rightAdjunct' Identity
-  extend g = fmap g . getCompose . rightAdjunct' (Compose . return . return)
+  extract = runIdentity . rightAdjunctF Identity
+  extend g = fmap g . getCompose . rightAdjunctF (Compose . return . return)
 
 newtype LiftAFree c f a = LiftAFree { getLiftAFree :: f (Free c a) }
 
@@ -83,7 +91,7 @@
   foldMap = foldMapDefault
 
 instance ForallT c (LiftAFree c) => Traversable (Free c) where
-  traverse f = getLiftAFree . rightAdjunct'' (LiftAFree . fmap pure . f)
+  traverse f = getLiftAFree . rightAdjunctT (LiftAFree . fmap pure . f)
 
 convert :: (c (f a), Applicative f) => Free c a -> f a
 convert = rightAdjunct pure
diff --git a/src/Data/Functor/HCofree.hs b/src/Data/Functor/HCofree.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Functor/HCofree.hs
@@ -0,0 +1,81 @@
+{-# LANGUAGE
+    ConstraintKinds
+  , RankNTypes
+  , TypeOperators  
+  , FlexibleInstances
+  , GADTs
+  #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Functor.HCofree
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  sjoerd@w3future.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- A cofree functor is right adjoint to a forgetful functor.
+-- In this package the forgetful functor forgets class constraints.
+--
+-- Compared to @Data.Functor.Cofree@ we're going up a level.
+-- These free functors go between categories of functors and the natural
+-- transformations between them.
+-----------------------------------------------------------------------------
+module Data.Functor.HCofree where
+
+import Control.Comonad
+import Data.Foldable
+import Data.Traversable
+import Data.Functor.Identity
+
+-- | Natural transformations.
+type f :~> g = forall b. f b -> g b
+
+-- | The higher order cofree functor for constraint @c@.
+data HCofree c g a where
+  HCofree :: (c f, Functor f) => (f :~> g) -> f a -> HCofree c g a
+
+instance Functor (HCofree c g) where
+  fmap f (HCofree k a) = HCofree k (fmap f a)
+
+counit :: HCofree c g :~> g
+counit (HCofree k fa) = k fa
+
+leftAdjunct :: (c f, Functor f) => (f :~> g) -> f :~> HCofree c g
+leftAdjunct k fa = HCofree k fa
+
+-- | @unit = leftAdjunct id@
+unit :: (c g, Functor g) => g :~> HCofree c g
+unit = leftAdjunct id
+
+-- | @rightAdjunct f = counit . f@
+rightAdjunct :: (f :~> HCofree c g) -> f :~> g
+rightAdjunct f = counit . f
+
+hfmap :: (f :~> g) -> HCofree c f :~> HCofree c g
+hfmap f (HCofree k a) = HCofree (f . k) a
+
+liftCofree :: (c f, Functor f) => f a -> HCofree c f a
+liftCofree = leftAdjunct id
+
+lowerCofree :: HCofree c f a -> f a
+lowerCofree = counit
+
+coiter :: c Identity => (forall b. b -> f b) -> a -> HCofree c f a
+coiter f = leftAdjunct (f . runIdentity) . Identity
+
+instance Foldable (HCofree Foldable g) where
+  foldMap f (HCofree _ a) = foldMap f a
+instance Foldable (HCofree Traversable g) where
+  foldMap f (HCofree _ a) = foldMap f a
+instance Traversable (HCofree Traversable g) where
+  traverse f (HCofree k a) = HCofree k <$> traverse f a
+
+-- | The cofree comonad of a functor.
+instance Comonad (HCofree Comonad g) where
+  extract (HCofree _ a) = extract a
+  extend f (HCofree k a) = HCofree k $ extend (f . HCofree k) a
+  duplicate (HCofree k a) = HCofree k $ extend (HCofree k) a
+
+unwrap :: HCofree Comonad g a -> g (HCofree Comonad g a)
+unwrap = counit . duplicate
diff --git a/src/Data/Functor/HFree.hs b/src/Data/Functor/HFree.hs
--- a/src/Data/Functor/HFree.hs
+++ b/src/Data/Functor/HFree.hs
@@ -23,6 +23,7 @@
 module Data.Functor.HFree where
   
 import Control.Applicative
+import Control.Monad
 import Control.Monad.Trans.Class
 import Data.Functor.Identity
 
@@ -33,12 +34,20 @@
 -- | The higher order free functor for constraint @c@.
 newtype HFree c f a = HFree { runHFree :: forall g. (c g, Functor g) => (f :~> g) -> g a }
 
-leftAdjunct :: (HFree c f :~> g) -> f :~> g
-leftAdjunct f fa = f (HFree $ \k -> k fa)
+unit :: f :~> HFree c f
+unit fa = HFree $ \k -> k fa
 
 rightAdjunct :: (c g, Functor g) => (f :~> g) -> HFree c f :~> g
 rightAdjunct f h = runHFree h f
 
+-- | @counit = rightAdjunct id@
+counit :: (c f, Functor f) => HFree c f :~> f
+counit = rightAdjunct id
+
+-- | @leftAdjunct f = f . unit@
+leftAdjunct :: (HFree c f :~> g) -> f :~> g
+leftAdjunct f = f . unit
+
 instance Functor (HFree c f) where
   fmap f (HFree g) = HFree (fmap f . g)
 
@@ -46,10 +55,10 @@
 hfmap f (HFree g) = HFree $ \k -> g (k . f)
 
 liftFree :: f a -> HFree c f a
-liftFree = leftAdjunct id
+liftFree = unit
 
 lowerFree :: (c f, Functor f) => HFree c f a -> f a
-lowerFree = rightAdjunct id
+lowerFree = counit
 
 convert :: (c (t f), Functor (t f), Monad f, MonadTrans t) => HFree c f a -> t f a
 convert = rightAdjunct lift
@@ -60,8 +69,12 @@
 -- | The free monad of a functor.
 instance Monad (HFree Monad f) where
   return a = HFree $ const (return a)
-  HFree f >>= g = HFree $ \k -> f k >>= (\a -> runHFree (g a) k)
-
+  HFree f >>= g = HFree $ \k -> f k >>= (rightAdjunct k . g)
+-- HFree Monad is only a monad transformer if rightAdjunct is called with monad morphisms.
+-- F.e. lift . return == return fails if the results are inspected with rightAdjunct (const Nothing).
+-- instance MonadTrans (HFree Monad) where
+--   lift = liftFree
+  
 instance Applicative (HFree Applicative f) where
   pure a = HFree $ const (pure a)
   HFree f <*> HFree g = HFree $ \k -> f k <*> g k
@@ -74,4 +87,4 @@
   HFree f <|> HFree g = HFree $ \k -> f k <|> g k
   
 wrap :: f (HFree Monad f a) -> HFree Monad f a
-wrap ff = HFree $ \k -> k ff >>= rightAdjunct k
+wrap = join . unit