diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,8 @@
 # Changelog for free-algebras
 
+## Version 0.0.5.1
+- Improved documentation
+
 ## Version 0.0.5.0
 - `FreeAlgebra` renamed `proof` to `codom`, added `Proof` smart constructor `proof`.
 - `FreeAlgebra` instance for `Identity` functor
@@ -25,3 +28,4 @@
 - Simplified `Proof` type.
 
 ## Unreleased changes
+
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -2,9 +2,10 @@
 [![Maintainer: coot](https://img.shields.io/badge/maintainer-coot-lightgrey.svg)](http://github.com/coot)
 [![Travis Build Status](https://travis-ci.org/coot/free-algebras.svg?branch=master)](https://travis-ci.org/coot/free-algebras)
 
-Universal algebra approach to free algebras (including higher order structures
-like functors, applicative functors or monads).  Mathematical introduction
-alongside with some  Haskell ideas can be found
+Universal algebra approach (which is compatible with categorical approach) to
+free algebras (including higher order structures like functors, applicative
+functors or monads).  Mathematical introduction alongside with some Haskell
+ideas can be found
 [here](https://marcinszamotulski.me/posts/free-monads.html).
 
 For an example check out [this](https://github.com/coot/free-algebras/blob/master/examples/src/Network/TCP.hs).
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.5.0
+version:        0.0.5.1
 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
@@ -1,14 +1,15 @@
 {-# LANGUAGE GADTs                      #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 module Control.Algebra.Free
-    (
-    -- * Classes
-      AlgebraType0
-    , AlgebraType
+    ( -- Higher free algebra class
+      FreeAlgebra1 (..)
+      -- ** Type level witnesses
     , Proof (..)
     , proof
-    , FreeAlgebra1 (..)
-    -- * Combinators
+      -- ** Higher algebra type
+    , AlgebraType0
+    , AlgebraType
+      -- * Combinators
     , wrapFree
     , foldFree1
     , unFoldNatFree
@@ -19,11 +20,11 @@
     , assocFree1
     , iterFree1
     , cataFree1
-    -- * Day convolution
+      -- * Day convolution
     , DayF (..)
     , dayToAp
     , apToDay
-    -- * Various classes (higher algebra types)
+      -- * Various classes (higher algebra types)
     , MonadList (..)
     , MonadMaybe (..)
     ) where
@@ -98,9 +99,9 @@
            , AlgebraType0 m f
            )
         => (forall x. f x -> d x)
-        -- ^ natural transformation which embeds generators of @m@ into @d@
+        -- ^ a natural transformation which embeds generators of @m@ into @d@
         -> (m f a -> d a)
-        -- ^ a homomorphism from @m f@ to @d@
+        -- ^ a morphism from @m f@ to @d@
 
     -- |
     -- A proof that @'AlgebraType' m (m f)@ holds for all @AlgebraType0 f => f@.
@@ -119,7 +120,7 @@
 -- |
 -- Anything that carries @'FreeAlgebra1'@ constraint is also an instance of
 -- @'Control.Monad.Free.Class.MonadFree'@, but not vice versa. You can use
--- @'wrap'@ to define a @'Contorl.Monad.Free.Class.MonadFree'@ instance.
+-- @'wrap'@ to define a @'Control.Monad.Free.Class.MonadFree'@ instance.
 -- @'ContT'@ is an example of a monad which does have an  @'FreeAlgebra1'@
 -- instance, but has an @'MonadFree'@ instance.
 --
@@ -239,7 +240,7 @@
 --
 -- For @'Control.Monad.State.Lazy.StateT'@,
 -- @'Control.Monad.Writer.Lazy.WriterT'@ or
--- @'Contorl.Monad.Reader.Lazy.ReaderT'@ (or any @'FreeAlgebra1' m => m@ such
+-- @'Control.Monad.Reader.Lazy.ReaderT'@ (or any @'FreeAlgebra1' m => m@ such
 -- that @'AlgebraType0' m@ subsumes @'Monad' m@), this is the @>>=@ version of
 -- @Control.Monad.Morph.embed@.
 bindFree1 :: forall m f g a .
@@ -280,7 +281,7 @@
 
 -- |
 -- @'Fix' (m f)@ is the initial /algebra/ of type @'AlgebraType' m@ and
--- @'AlgebraType0' f@ (whenever it /exists/).
+-- @'AlgebraType0' f@.
 cataFree1 :: forall m f a .
              ( FreeAlgebra1 m
              , AlgebraType  m f
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
@@ -1,13 +1,14 @@
 {-# LANGUAGE CPP   #-}
 {-# LANGUAGE GADTs #-}
 module Data.Algebra.Free
-    ( -- * Algebra type
-      AlgebraType
-    , AlgebraType0
-      -- * FreeAlgebra class
-    , FreeAlgebra (..)
+    ( -- * Free algebra class
+      FreeAlgebra (..)
+      -- ** Type level witnesses
     , Proof (..)
     , proof
+    , -- ** Algebra type
+      AlgebraType
+    , AlgebraType0
       -- * Combinators
     , unFoldMapFree
     , foldFree
@@ -20,6 +21,7 @@
     , foldrFree'
     , foldlFree
     , foldlFree'
+      -- * General free type
     , Free (..)
     )
     where
@@ -39,6 +41,10 @@
 
 import           Data.Algebra.Pointed (Pointed (..))
 
+--
+-- Prerequisites for @'FreeAlgebra'@
+--
+
 -- |
 -- Type family which for each free algebra @m@ returns a type level lambda from
 -- types to constraints.  It is describe the class of algebras for which this
@@ -85,8 +91,8 @@
          . ( AlgebraType m d
            , AlgebraType0 m a
            )
-        => (a -> d)   -- ^ map generators of @m@ into @d@
-        -> (m a -> d) -- ^ returns a homomorphism from @m a@ to @d@
+        => (a -> d)   -- ^ a mappping of generators of @m@ into @d@
+        -> (m a -> d) -- ^ a homomorphism from @m a@ to @d@
 
     -- |
     -- Proof that @AlgebraType0 m a => m a@ is an algebra of type @AlgebraType m@.
@@ -101,6 +107,10 @@
     forget :: forall a. AlgebraType  m a => Proof (AlgebraType0 m a) (m a)
 
 
+--
+-- Free combinators
+--
+
 -- |
 -- Inverse of @'foldMapFree'@
 --
@@ -144,7 +154,7 @@
 --
 -- the constraints:
 -- * the algebra @n a@ is of the same type as algebra @m@ (this is
---    always true, just ghc cannot prove it here)
+--    always true, just GHC cannot prove it here)
 -- * @m@ is a free algebra generated by @a@
 -- * @n@ is a free algebra generated by @a@
 natFree :: forall m n a .
@@ -206,8 +216,7 @@
 --   fixToFree :: (FreeAlgebra m, AlgebraType m (m Void), Functor m) => Fix m -> m Void
 --   fixToFree = cataFree
 -- @
--- For monoids the inverse is given by @'Data.Fix.ana' (\_ -> [])@.  The
--- category of semigroups, however,  does not have the initial object.
+-- For monoids the inverse is given by @'Data.Fix.ana' (\_ -> [])@.
 cataFree :: ( FreeAlgebra  m
             , AlgebraType  m a
             , Functor m
@@ -250,7 +259,7 @@
     f' k x z = k $! f x z
 
 -- |
--- Generalizes @'Data.Foldabale.foldl'@, e.g. it can specialize to
+-- Generalizes @'Data.Foldable.foldl'@, e.g. it can specialize to
 --
 -- * @foldlFree \@[] :: (b -> a -> b) -> b -> [a] -> b@
 -- * @foldlFree \@'Data.List.NonEmpty.NonEmpty' :: (b -> a -> b) -> b -> 'Data.List.NonEmpty.NonEmpty' a -> b@
@@ -281,6 +290,12 @@
 foldlFree' f z0 xs = foldrFree f' id xs z0
     where
     f' x k z = k $! f z x
+
+
+--
+-- Instances
+--
+
 
 type instance AlgebraType0 Identity a = ()
 type instance AlgebraType  Identity a = ()