diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,9 +1,12 @@
 # Changelog for free-algebras
 
+## Version 0.0.7.2
+- Enhanced documentation, and properly attributed fix in ChangeLog.
+
 ## Version 0.0.7.1
 - `Data.Group.Free.normalize` and `Data.Group.Free.normalizeL` are not both
   `O(n)`, but the former is implemented using the latter (e.g. transforms
-  `DList` to a list).
+  `DList` to a list), by Justin Le (https://github.com/mstsg)
 
 ## Version 0.0.7.0
 - Poly kinded `Control.Algebra.Free.FreeAlgebra` and
diff --git a/free-algebras.cabal b/free-algebras.cabal
--- a/free-algebras.cabal
+++ b/free-algebras.cabal
@@ -1,5 +1,5 @@
 name:           free-algebras
-version:        0.0.7.1
+version:        0.0.7.2
 synopsis:       Free algebras in Haskell.
 description:    Universal algebra approach to free algebras including higher kinded algebraic structures like functors, applicative functors or monads.
 category:       Algebra, Control, Monads
diff --git a/src/Control/Algebra/Free.hs b/src/Control/Algebra/Free.hs
--- a/src/Control/Algebra/Free.hs
+++ b/src/Control/Algebra/Free.hs
@@ -15,7 +15,7 @@
       -- ** Type level witnesses
     , Proof (..)
     , proof
-      -- ** Higher algebra type
+      -- ** Higher algebra type \/ constraints
     , AlgebraType0
     , AlgebraType
       -- * Combinators
@@ -163,7 +163,7 @@
 --
 -- * @'Data.Functor.Coyoneda.lowerCoyoneda' :: 'Functor' f => 'Coyoneda' f a -> f a@
 -- * @'Control.Applicative.Free.retractAp' :: 'Applicative' f => 'Ap' f a -> f a@
--- * @'Control.Monad.Free.foldFree' :: 'Monad' m => (forall x. f x -> m x) -> 'Free' f a -> m a@
+-- * @'Control.Monad.Free.retract' :: 'Monad' f => 'Free' f a -> f a@
 foldFree1 :: forall m f a .
              ( FreeAlgebra1 m
              , AlgebraType  m f
@@ -177,6 +177,8 @@
 -- |
 -- @'unFoldNatFree'@ is an inverse of @'foldNatFree'@
 --
+-- It is uniquelly determined by its universal property (by Yonneda lemma):
+--
 -- prop> unFoldNatFree id = ruturnFree1
 --
 -- Note that @'unFoldNatFree' id@ is the
@@ -192,8 +194,12 @@
 
 -- |
 -- This is a functor instance for @m@ when considered as an endofuctor of some
--- subcategory of @Type -> Type@ (e.g. endofunctors of _Hask_).
+-- subcategory of @Type -> Type@ (e.g. endofunctors of /Hask/) and it satisfies
+-- the functor laws:
 --
+-- prop> hoistFree1 id = id
+-- prop> hoistFree1 f . hoistFree1 g = hoistFree1 (f . g)
+--
 -- It can be specialized to:
 --
 -- * @'Control.Applicative.Free.hoistAp' :: (forall a. f a -> g a) -> 'Ap' f b -> 'Ap' g b @
@@ -289,6 +295,7 @@
 -- |
 -- @'Fix' (m f)@ is the initial /algebra/ of type @'AlgebraType' m@ and
 -- @'AlgebraType0' f@.
+--
 cataFree1 :: forall m f a .
              ( FreeAlgebra1 m
              , AlgebraType  m f
diff --git a/src/Control/Algebra/Free2.hs b/src/Control/Algebra/Free2.hs
--- a/src/Control/Algebra/Free2.hs
+++ b/src/Control/Algebra/Free2.hs
@@ -2,12 +2,24 @@
 {-# LANGUAGE PolyKinds           #-}
 {-# LANGUAGE RankNTypes          #-}
 
+-- |
+-- A type class for free objects of kind @k -> k -> Type@, i.e. /graphs/ (we
+-- will use this name for types of this kind in this documentation).  Examples
+-- include various flavors of /free categories/ and /arrows/ which
+-- are not included in this package, see
+-- __[free-category](https://hackage.haskell.org/package/free-category)__ on
+-- /Hackage/).
+--
 module Control.Algebra.Free2
-    ( FreeAlgebra2 (..)
+    ( -- * Free algebra class
+      FreeAlgebra2 (..)
+      -- ** Type level witnesses
     , Proof (..)
     , proof
+      -- ** Algebra types \/ constraints
     , AlgebraType0
     , AlgebraType
+      -- * Combinators
     , wrapFree2
     , foldFree2
     , unFoldNatFree2
@@ -25,22 +37,69 @@
 import           Data.Algebra.Free (AlgebraType, AlgebraType0, Proof (..), proof)
 
 -- |
--- Free algebra similar to @'FreeAlgebra1'@ and @'FreeAlgebra'@, but for types
--- of kind @Type -> Type -> Type@.  Examples include free categories, free
--- arrows, etc (see 'free-category' package).
+-- Free algebra class similar to @'FreeAlgebra1'@ and @'FreeAlgebra'@, but for
+-- types of kind @k -> k -> Type@.
+--
 class FreeAlgebra2 (m :: (k -> k -> Type) -> k -> k -> Type) where
-    liftFree2    :: AlgebraType0 m f => f a b -> m f a b
-    foldNatFree2 :: forall (d :: k -> k -> Type) (f :: k -> k -> Type) a b .
+
+    -- |
+    -- Lift a graph @f@ satsifying the constraint @'AlgebraType0'@ to
+    -- a free its object @m f@.
+    --
+    liftFree2    :: AlgebraType0 m f
+                 => f a b
+                 -> m f a b
+
+    -- |
+    -- This represents the theorem that @m f@ is indeed free object (as
+    -- in propositions as types).  The types of kind @k -> k -> Type@ form
+    -- a category, where an arrow from @f :: k -> k -> Type@ to @d :: k ->
+    -- k -> Type@ is represented by type @forall x y. f x y -> d x y@.
+    -- @foldNatFree2@ states that whenever we have such a morphism and @d@
+    -- satisfies the constraint @AlgebraType m d@ then we can construct
+    -- a morphism from @m f@ to @d@.
+    --
+    foldNatFree2 :: forall (d :: k -> k -> Type)
+                           (f :: k -> k -> Type) a b .
                     ( AlgebraType  m d
                     , AlgebraType0 m f
                     )
                  => (forall x y. f x y -> d x y)
                  -> (m f a b -> d a b)
 
-    codom2  :: forall (f :: k -> k -> Type). AlgebraType0 m f => Proof (AlgebraType m (m f)) (m f)
-    forget2 :: forall (f :: k -> k -> Type). AlgebraType  m f => Proof (AlgebraType0 m f) (m f)
+    -- |
+    -- A proof that for each @f@ satisfying @AlgebraType0 m f@, @m f@
+    -- satisfies @AlgebraType m (m f)@ constrant.  This means that @m@ is
+    -- a well defined /functor/ from the full sub-category of types of
+    -- kind @k -> k -> Type@ which satisfy the @AlgebraType0 m@ constraint
+    -- to the full subcategory of types of the same kind which satifsfy
+    -- the constraint @AlgebraType m@.
+    --
+    codom2  :: forall (f :: k -> k -> Type).
+               AlgebraType0 m f
+            => Proof (AlgebraType m (m f)) (m f)
 
-wrapFree2 :: forall (m :: (Type -> Type -> Type) -> Type -> Type -> Type) (f :: Type -> Type -> Type) a b .
+    -- | 
+    -- A proof that each type @f :: k -> k -> Type@ satisfying the
+    -- @Algebra m f@ constraint also satisfies @AlgebraType0 m f@.  This
+    -- states that there is a well defined /forgetful functor/ from the
+    -- category of types of kind @k -> k -> Type@ which satisfy the
+    -- @AlgebraType m@ to the category of types of the same kind which
+    -- satisfy the @AlgebraType0 m@ constraint.
+    --
+    forget2 :: forall (f :: k -> k -> Type).
+               AlgebraType  m f
+            => Proof (AlgebraType0 m f) (m f)
+
+--
+-- Combinaators
+--
+
+-- | A version of @wrap@ from __free__ package but for graphs.
+--
+wrapFree2 :: forall (m :: (Type -> Type -> Type) -> Type -> Type -> Type)
+                    (f :: Type -> Type -> Type)
+                    a b .
              ( AlgebraType0 m f
              , FreeAlgebra2 m
              , Monad (m f a)
@@ -50,6 +109,17 @@
 wrapFree2 = join . liftFree2
 {-# INLINE wrapFree2 #-}
 
+-- | Like @'foldFree'@ or @'foldFree1'@ but for graphs.
+-- 
+-- A lawful instance will satisfy:
+--
+-- @
+--  'foldFree2' . 'liftFree2' == 'id' :: f a b -> f a b
+-- @
+--
+-- It is the [unit](https://ncatlab.org/nlab/show/unit+of+an+adjunction) of
+-- adjuction defined by @'FreeAlgebra1'@ class.
+--
 foldFree2 :: forall (m :: (k -> k -> Type) -> k -> k -> Type)
                     (f :: k -> k -> Type)
                     a b .
@@ -62,6 +132,13 @@
     Proof Dict -> foldNatFree2 id
 {-# INLINE foldFree2 #-}
 
+-- | 
+-- Inverse of @'foldNatFree2'@.
+--
+-- It is uniquelly determined by its universal property (by Yonneda lemma):
+--
+-- prop> unFoldNatFree id = liftFree2
+--
 unFoldNatFree2
     :: forall (m :: (k -> k -> Type) -> k -> k -> Type)
               (f :: k -> k -> Type)
@@ -74,6 +151,15 @@
 unFoldNatFree2 nat = nat . liftFree2
 {-# INLINE unFoldNatFree2 #-}
 
+-- |
+-- Hoist the underlying graph in the free structure.
+-- This is a higher version of a functor (analogous to @'fmapFree'@, which
+-- defined functor instance for @'FreeAlgebra'@ instances) and it satisfies the
+-- functor laws:
+--
+-- prop> hoistFree2 id = id
+-- prop> hoistFree2 f . hoistFree2 g = hoistFree2 (f . g)
+--
 hoistFree2 :: forall (m :: (k -> k -> Type) -> k -> k -> Type)
                      (f :: k -> k -> Type)
                      g a b .
@@ -88,6 +174,9 @@
     Proof Dict -> foldNatFree2 (liftFree2 . nat)
 {-# INLINE hoistFree2 #-}
 
+-- |
+-- Hoist the top level free structure.
+--
 hoistFreeH2 :: forall m n f a b .
            ( FreeAlgebra2 m
            , FreeAlgebra2 n
@@ -100,6 +189,10 @@
 hoistFreeH2 = foldNatFree2 liftFree2
 {-# INLINE hoistFreeH2 #-}
 
+-- |
+-- @'FreeAlgebra2' m@ is a monad on some subcategory of graphs (types of kind
+-- @k -> k -> Type@), @'joinFree'@ it is the @join@ of this monad.
+--
 joinFree2 :: forall (m :: (k -> k -> Type) -> k -> k -> Type)
                     (f :: k -> k -> Type)
                     a b .
@@ -113,6 +206,10 @@
         Proof Dict -> foldFree2
 {-# INLINE joinFree2 #-}
 
+-- |
+-- @bind@ of the monad defined by @m@ on the subcategory of graphs (typed of
+-- kind @k -> k -> Type@).
+--
 bindFree2 :: forall m f g a b .
              ( FreeAlgebra2 m
              , AlgebraType0 m g
diff --git a/src/Data/Algebra/Free.hs b/src/Data/Algebra/Free.hs
--- a/src/Data/Algebra/Free.hs
+++ b/src/Data/Algebra/Free.hs
@@ -15,7 +15,7 @@
       -- ** Type level witnesses
     , Proof (..)
     , proof
-    , -- ** Algebra type
+    , -- ** Algebra types \/ constraints
       AlgebraType
     , AlgebraType0
       -- * Combinators
@@ -139,11 +139,23 @@
 -- |
 -- All types which satisfy @'FreeAlgebra'@ constraint are foldable.
 --
+-- It is uniquelly determined by its universal property (by Yonneda lemma):
+--
 -- prop> foldFree . returnFree == id
 --
 -- @foldFree@ is the
 -- [unit](https://ncatlab.org/nlab/show/unit+of+an+adjunction) of the
 -- adjunction imposed by @FreeAlgebra@ constraint.
+--
+-- Examples:
+--
+-- > foldFree @[] = foldMap id
+-- >              = foldr (<>) mempty
+-- > foldFree @NonEmpty
+-- >              = foldr1 (<>)
+--
+-- Note that @foldFree@ replaces the abstract \/ free algebraic operation in
+-- @m a@ to concrete one in @a@.
 foldFree
     :: forall m a .
        ( FreeAlgebra  m