diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,11 @@
 # Changelog for free-algebras
 
+## Version 0.0.3.0
+
+- Breaking change: changed proofs in FreeAlgebra and FreeAlgebra1 class; now
+  using `FreeAlgebra` and `FreeAlgebra1` classes let us deduce an adjunction.
+- Monadicity example
+
 ## Version 0.0.2.0
 - Simplified `Proof` type.
 
diff --git a/free-algebras.cabal b/free-algebras.cabal
--- a/free-algebras.cabal
+++ b/free-algebras.cabal
@@ -2,13 +2,13 @@
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 01ca145922d0171eb90e9232004a0c588b6403c06f81dcae21bd5416c907bd75
+-- hash: 9cf25d016d878667110e6394084d060d946ebb54650a1bb2b8786fd56371dc93
 
 name:           free-algebras
-version:        0.0.2.0
+version:        0.0.3.0
 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
+category:       Algebra, Control, Monads
 homepage:       https://github.com/coot/free-algebras#readme
 bug-reports:    https://github.com/coot/free-algebras/issues
 author:         Marcin Szamotulski
@@ -67,7 +67,7 @@
 
 test-suite free-algebras-test
   type: exitcode-stdio-1.0
-  main-is: Spec.hs
+  main-is: Main.hs
   other-modules:
       Test.Control.Algebra.Free
       Test.Data.Algebra.Free
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
@@ -67,14 +67,14 @@
 -- free applicative functors, free monads, state monads etc.
 --
 -- A lawful instance should guarantee that @'foldNatFree'@ is an isomorphism
--- with inversese @'unFoldNatFree'@.
+-- with inverses @'unFoldNatFree'@.
 --
 -- This guaranties that @m@ is a left adjoint functor from the category of
 -- types of kind @Type -> Type@ which satisfy @'AlgebraType0' m@ constraint, to the
 -- category of types of kind @Type -> Type@ which satisfy the @'AlgebraType' m@
--- constraint.  This functor is left afjoin to the forgetful functor (which is
+-- constraint.  This functor is left adjoin to the forgetful functor (which is
 -- well defined if the laws on @'AlgebraType0'@ family are satisfied.  This in
--- turn guarantess that @m@ componsed with this forgetful functor is a monad.
+-- turn guarantees that @m@ composed with this forgetful functor is a monad.
 -- In result we get the monadic combinators: @'liftFree'@ (@'return'@ of
 -- this monad) and @'bindFree1'@ (its @'bind'@) and @'joinFree1'@ - its
 -- @'join'@ operator.
@@ -85,7 +85,7 @@
     -- | The freeness property.
     foldNatFree
         :: forall (d :: Type -> Type) f a .
-           ( AlgebraType m d
+           ( AlgebraType  m d
            , AlgebraType0 m f
            )
         => (forall x. f x -> d x)
@@ -94,16 +94,23 @@
         -- ^ a homomorphism from @m f@ to @d@
 
     -- |
-    -- A proof that @'AlgebraType0' m (m f)@ holds for all @f@.
-    proof0 :: forall f. AlgebraType0 m f => Proof (AlgebraType0 m (m f)) (m f)
+    -- A proof that @'AlgebraType' m (m f)@ holds for all @AlgebraType0 f => f@.
+    -- Together with @hoistFree1@ this proves that @FreeAlgebra m => m@ is
+    -- a functor from the full subcategory of types of kind @Type -> Type@
+    -- which satisfy @'AlgebraType0' m f@ to ones that satisfy @'AlgebraType'
+    -- m f@.
+    proof1  :: forall f. AlgebraType0 m f => Proof (AlgebraType m (m f)) (m f)
+
     -- |
-    -- A proof that @'AlgebraType' m (m f)@ holds for all @f@.
-    proof1 :: forall f. AlgebraType0 m f => Proof (AlgebraType m (m f)) (m f)
+    -- A proof that the forgetful functor from the full subcategory of types of
+    -- kind @Type -> Type@ satisfying @'AlgebraType' m f@ constraint to types
+    -- satisfying @'AlgebraType0' m f@ is well defined.
+    forget1 :: forall f. AlgebraType  m f => Proof (AlgebraType0 m f) (m f)
 
 -- |
 -- 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 the a @'Contorl.Monad.Free.Class.MonadFree'@ instance.
+-- @'wrap'@ to define a @'Contorl.Monad.Free.Class.MonadFree'@ instance.
 -- @'ContT'@ is an example of a monad which does have an  @'FreeAlgebra1'@
 -- instance, but has an @'MonadFree'@ instance.
 --
@@ -119,36 +126,47 @@
 wrapFree = join . liftFree
 
 -- |
--- @'unFoldNatFree'@ is an inverse of @'foldNatFree'@
-unFoldNatFree
-    :: ( FreeAlgebra1 m
-       , AlgebraType0 m f
-       )
-    => (forall x . m f x -> d x)
-    -> f a -> d a
-unFoldNatFree nat = nat . liftFree
-
--- |
 -- @'FreeAlgebra1' m@ implies that @m f@ is a foldable.
 --
 -- @
 --  'foldFree1' . 'liftFree' == 'id' :: f a -> f a
 -- @
 --
+-- @foldFree1@ is the
+-- [unit](https://ncatlab.org/nlab/show/unit+of+an+adjunction) of the
+-- adjunction imposed by @FreeAlgebra1@ constraint.
+--
 -- It can be specialized to:
 --
 -- * @'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@
-foldFree1 :: ( FreeAlgebra1 m
-             , AlgebraType0 m f
+foldFree1 :: forall m f a .
+             ( FreeAlgebra1 m
              , AlgebraType  m f
              )
           => m f a
           -> f a
-foldFree1 = foldNatFree id
+foldFree1 = case forget1 @m @f of
+    Proof Dict -> foldNatFree id
 
 -- |
+-- @'unFoldNatFree'@ is an inverse of @'foldNatFree'@
+--
+-- prop> unFoldNatFree id = ruturnFree1
+--
+-- Note that @'unFoldNatFree' id@ is the
+-- [unit](https://ncatlab.org/nlab/show/unit+of+an+adjunction) of the
+-- adjunction imposed by the @'FreeAlgebra1'@ constraint.
+unFoldNatFree
+    :: ( FreeAlgebra1 m
+       , AlgebraType0 m f
+       )
+    => (forall x . m f x -> d x)
+    -> f a -> d a
+unFoldNatFree nat = nat . liftFree
+
+-- |
 -- This is a functor instance for @m@ when considered as an endofuctor of some
 -- subcategory of @Type -> Type@ (e.g. endofunctors of _Hask_).
 --
@@ -164,10 +182,8 @@
            => (forall x. f x -> g x) -- ^ a natural transformation @f ~> g@
            -> m f a
            -> m g a
-hoistFree1 = go (proof1 :: Proof (AlgebraType m (m g)) (m g)) where
-    go :: Proof (AlgebraType m (m g)) (m g) -> (forall x. f x -> g x) -> m f a -> m g a
-    go (Proof Dict) nat = foldNatFree (liftFree . nat)
-    {-# INLINE go #-}
+hoistFree1 nat = case proof1 @m @g of
+    Proof Dict -> foldNatFree (liftFree . nat)
 
 -- |
 -- @
@@ -200,14 +216,13 @@
              )
           => m (m f) a
           -> m f a
-joinFree1 = go (proof0 :: Proof (AlgebraType0 m (m f)) (m f)) (proof1 :: Proof (AlgebraType m (m f)) (m f))
-    where
-    go :: Proof (AlgebraType0 m (m f)) (m f) -> Proof (AlgebraType m (m f)) (m f) -> m (m f) a -> m f a
-    go (Proof Dict) (Proof Dict) = foldFree1
-    {-# INLINE go #-}
+joinFree1 = case proof1 @m @f of
+    Proof Dict -> case forget1 @m @(m f) of
+        Proof Dict -> foldFree1
 
 -- |
--- Bind operator for the @'joinFree1'@ monad
+-- Bind operator for the @'joinFree1'@ monad, this is just @'foldNatFree'@ in
+-- disguise.
 bindFree1 :: forall m f g a .
              ( FreeAlgebra1 m
              , AlgebraType0 m g
@@ -216,36 +231,33 @@
           => m f a
           -> (forall x . f x -> m g x) -- ^ natural transformation @f ~> m g@
           -> m g a
-bindFree1 = go (proof0 :: Proof (AlgebraType0 m (m g)) (m g)) (proof1 :: Proof (AlgebraType m (m g)) (m g))
-    where
-    go :: Proof (AlgebraType0 m (m g)) (m g) -> Proof (AlgebraType m (m g)) (m g) -> m f a -> (forall x . f x -> m g x) -> m g a
-    go (Proof Dict) (Proof Dict) mfa nat = joinFree1 $ hoistFree1 nat mfa
-    {-# INLINE go #-}
+bindFree1 mfa nat = case proof1 @m @g of
+    Proof Dict -> foldNatFree nat mfa
 
 assocFree1 :: forall m f a .
               ( FreeAlgebra1 m
               , AlgebraType  m f
-              , AlgebraType0 m f
               , Functor (m (m f))
               )
            => m f (m f a)
            -> m (m f) (f a)
-assocFree1 = outer (proof0 :: Proof (AlgebraType0 m (m f)) (m f))
+assocFree1 = case forget1 @m @f of
+    Proof Dict -> case proof1 @m @f of
+        Proof Dict -> case forget1 @m @(m f) of
+            Proof Dict -> case proof1 @m @(m f) of
+                Proof Dict -> case forget1 @m @(m (m f)) of
+                    Proof Dict -> fmap g <$> foldNatFree f
     where
-        -- `Proof0` is needed to prove `Proof1`
-        {-# INLINE outer #-}
-        outer :: Proof (AlgebraType0 m (m f)) (m f) -> m f (m f a) -> m (m f) (f a)
-        outer (Proof Dict) = inner (proof1 :: Proof (AlgebraType m (m (m f))) (m (m f)))
-            where
-            {-# INLINE inner #-}
-            inner :: Proof (AlgebraType m (m (m f))) (m (m f)) -> m f (m f a) -> m (m f) (f a)
-            inner (Proof Dict) = fmap g <$> foldNatFree f
-
-            f :: forall x. f x -> m (m f) x
-            f = hoistFree1 liftFree . liftFree
+        f :: forall x .
+             ( AlgebraType0 m f
+             , AlgebraType0 m (m f)
+             )
+          => f x
+          -> m (m f) x
+        f = hoistFree1 liftFree . liftFree
 
-            g :: m f a -> f a
-            g = foldFree1
+        g :: m f a -> f a
+        g = foldFree1
 
 -- |
 -- @'Fix' (m f)@ is the initial /algebra/ of type @'AlgebraType' m@ and
@@ -253,7 +265,6 @@
 cataFree1 :: forall m f a .
              ( FreeAlgebra1 m
              , AlgebraType  m f
-             , AlgebraType0 m f
              , Monad f
              , Traversable (m f)
              )
@@ -287,8 +298,8 @@
     liftFree = liftCoyoneda
     foldNatFree nat (Coyoneda ba fx) = ba <$> nat fx
 
-    proof0 = Proof Dict
-    proof1 = Proof Dict
+    proof1  = Proof Dict
+    forget1 = Proof Dict
 
 -- |
 -- Algebras of the same type as @'Ap'@ are the applicative functors.
@@ -301,8 +312,8 @@
     liftFree  = Ap.liftAp
     foldNatFree = Ap.runAp
 
-    proof0 = Proof Dict
-    proof1 = Proof Dict
+    proof1  = Proof Dict
+    forget1 = Proof Dict
 
 type instance AlgebraType0 Fast.Ap g = Functor g
 type instance AlgebraType  Fast.Ap g = Applicative g
@@ -310,8 +321,8 @@
     liftFree  = Fast.liftAp
     foldNatFree = Fast.runAp
 
-    proof0 = Proof Dict
-    proof1 = Proof Dict
+    proof1  = Proof Dict
+    forget1 = Proof Dict
 
 type instance AlgebraType0 Final.Ap g = Functor g
 type instance AlgebraType  Final.Ap g = Applicative g
@@ -319,8 +330,8 @@
     liftFree  = Final.liftAp
     foldNatFree = Final.runAp
 
-    proof0 = Proof Dict
-    proof1 = Proof Dict
+    proof1  = Proof Dict
+    forget1 = Proof Dict
 
 -- |
 -- @'Day' f f@ newtype wrapper.  It is isomorphic with @'Ap' f@ for applicative
@@ -346,8 +357,8 @@
     foldNatFree nat (DayF day)
         = Day.dap . Day.trans2 nat . Day.trans1 nat $ day
 
-    proof0 = Proof Dict
-    proof1 = Proof Dict
+    proof1  = Proof Dict
+    forget1 = Proof Dict
 
 -- |
 -- Algebras of the same type as @'Free'@ monad is the class of all monads.
@@ -359,8 +370,8 @@
     liftFree    = Free.liftF
     foldNatFree = Free.foldFree
 
-    proof0 = Proof Dict
-    proof1 = Proof Dict
+    proof1  = Proof Dict
+    forget1 = Proof Dict
 
 type instance AlgebraType0 Church.F f = Functor f
 type instance AlgebraType  Church.F m = Monad m
@@ -368,8 +379,8 @@
     liftFree    = Church.liftF
     foldNatFree = Church.foldF
 
-    proof0 = Proof Dict
-    proof1 = Proof Dict
+    proof1  = Proof Dict
+    forget1 = Proof Dict
 
 type instance AlgebraType0 Alt f = Functor f
 type instance AlgebraType  Alt m = Alternative m
@@ -377,8 +388,8 @@
     liftFree    = Alt.liftAlt
     foldNatFree = Alt.runAlt
 
-    proof0 = Proof Dict
-    proof1 = Proof Dict
+    proof1  = Proof Dict
+    forget1 = Proof Dict
 
 -- |
 -- Algebras of the same type as @'L.StateT'@ monad is the class of all state
@@ -402,8 +413,8 @@
         put s
         return a
 
-    proof0 = Proof Dict
-    proof1 = Proof Dict
+    proof1  = Proof Dict
+    forget1 = Proof Dict
 
 -- |
 -- Algebras of the same type as @'S.StateT'@ monad is the class of all state
@@ -421,8 +432,8 @@
         put s
         return a
 
-    proof0 = Proof Dict
-    proof1 = Proof Dict
+    proof1  = Proof Dict
+    forget1 = Proof Dict
 
 -- |
 -- Algebras of the same type as @'L.WriterT'@ monad is the class of all writer
@@ -435,8 +446,8 @@
     liftFree = lift
     foldNatFree nat (L.WriterT m) = fst <$> nat m
 
-    proof0 = Proof Dict
-    proof1 = Proof Dict
+    proof1  = Proof Dict
+    forget1 = Proof Dict
 
 -- |
 -- Algebras of the same type as @'S.WriterT'@ monad is the class of all writer
@@ -450,8 +461,8 @@
     liftFree = lift
     foldNatFree nat (S.WriterT m) = fst <$> nat m
 
-    proof0 = Proof Dict
-    proof1 = Proof Dict
+    proof1  = Proof Dict
+    forget1 = Proof Dict
 
 -- |
 -- Algebras of the same type as @'L.ReaderT'@ monad is the class of all reader
@@ -465,8 +476,8 @@
     foldNatFree nat (ReaderT g) =
         ask >>= nat . g
 
-    proof0 = Proof Dict
-    proof1 = Proof Dict
+    proof1  = Proof Dict
+    forget1 = Proof Dict
 
 -- |
 -- Algebras of the same type as @'S.ReaderT'@ monad is the class of all reader
@@ -483,8 +494,8 @@
             Left e  -> throwError e
             Right a -> return a
 
-    proof0 = Proof Dict
-    proof1 = Proof Dict
+    proof1  = Proof Dict
+    forget1 = Proof Dict
 
 type instance AlgebraType0 (L.RWST r w s) m = ( Monad m, Monoid w )
 type instance AlgebraType  (L.RWST r w s) m = MonadRWS r w s m
@@ -498,8 +509,8 @@
         tell w
         return a
 
-    proof0 = Proof Dict
-    proof1 = Proof Dict
+    proof1  = Proof Dict
+    forget1 = Proof Dict
 
 type instance AlgebraType0 (S.RWST r w s) m = ( Monad m, Monoid w )
 type instance AlgebraType  (S.RWST r w s) m = MonadRWS r w s m
@@ -513,8 +524,8 @@
         tell w
         return a
 
-    proof0 = Proof Dict
-    proof1 = Proof Dict
+    proof1  = Proof Dict
+    forget1 = Proof Dict
 
 -- |
 -- Algebra type for @'ListT'@ monad transformer.
@@ -539,8 +550,8 @@
         a <- foldM (\x y -> x `mappend1_` y) empty as
         return a
 
-    proof0 = Proof Dict
-    proof1 = Proof Dict
+    proof1  = Proof Dict
+    forget1 = Proof Dict
 
 -- $monadContT
 --
@@ -566,5 +577,5 @@
             Nothing -> point
             Just a  -> return a
 
-    proof0 = Proof Dict
-    proof1 = Proof Dict
+    proof1  = Proof Dict
+    forget1 = Proof Dict
diff --git a/src/Control/Monad/Action.hs b/src/Control/Monad/Action.hs
--- a/src/Control/Monad/Action.hs
+++ b/src/Control/Monad/Action.hs
@@ -45,7 +45,6 @@
 instance ( Monad m
          , FreeAlgebra  m
          , AlgebraType  m d
-         , AlgebraType0 m d
          )
          => MAction m (Const d) where
     mact mca = Const $ foldFree $ getConst <$> mca
@@ -63,5 +62,6 @@
 instance Monad m => FreeAlgebra1 (FreeMAction m) where
     liftFree = FreeMAction . return
     foldNatFree nat (FreeMAction mfa) = mact $ nat <$> mfa
-    proof0 = Proof Dict
-    proof1 = Proof Dict
+
+    proof1  = Proof Dict
+    forget1 = Proof Dict
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
@@ -35,7 +35,7 @@
 --
 -- A lawful instance for this type family must guarantee
 -- that the constraint @'AlgebraType0' m f@ is implied by the @'AlgebraType'
--- m f@ constraint.  This guaranees that there exists a forgetful functor from
+-- m f@ constraint.  This guarantees that there exists a forgetful functor from
 -- the category of types of kind @* -> *@ which satisfy @'AlgebraType' m@
 -- constrain to the category of types of kind @* -> *@ which satisfy the
 -- @'AlgebraType0 m@ constraint.
@@ -71,12 +71,26 @@
         => (a -> d)   -- ^ map generators of @m@ into @d@
         -> (m a -> d) -- ^ returns a homomorphism from @m a@ to @d@
 
-    -- | Proof that @'AlgebraType' m (m a)@ holds for all @a@, e.g. if @m ~ []@
-    -- then @[a]@ is a monoid for all @a@.
-    proof :: forall a. AlgebraType0 m a => Proof (AlgebraType m (m a)) (m a)
+    -- |
+    -- Proof that @AlgebraType0 m a => m a@ is an algebra of type @AlgebraType m@.
+    -- This proves that @m@ is a mapping from the full subcategory of @Hask@ of
+    -- types satisfying @AlgebraType0 m a@ constraint to the full subcategory
+    -- satisfying @AlgebraType m a@, @fmapFree@ below proves that it's a functor.
+    proof  :: forall a. AlgebraType0 m a => Proof (AlgebraType m (m a)) (m a)
+    -- |
+    -- Proof that the forgetful functor from types @a@ satisfying @AgelbraType
+    -- m a@ to @AlgebraType0 m a@ is well defined.
+    forget :: forall a. AlgebraType  m a => Proof (AlgebraType0 m a) (m a)
 
+
 -- |
 -- Inverse of @'foldMapFree'@
+--
+-- prop> unFoldMapFree id = returnFree
+--
+-- Note that @'unFoldMapFree' id@ is the unit of the
+-- [unit](https://ncatlab.org/nlab/show/unit+of+an+adjunction) of the
+-- adjunction imposed by the @'FreeAlgebra'@ constraint.
 unFoldMapFree
     :: FreeAlgebra m
     => (m a -> d)
@@ -84,18 +98,22 @@
 unFoldMapFree f = f . returnFree
 
 -- |
--- All types which satisfy @'FreeAlgebra'@ constraint are foldable.  You can
--- use this map to build a @'Foldable'@ instance.
+-- All types which satisfy @'FreeAlgebra'@ constraint are foldable.
 --
 -- prop> foldFree . returnFree == id
+--
+-- @foldFree@ is the
+-- [unit](https://ncatlab.org/nlab/show/unit+of+an+adjunction) of the
+-- adjunction imposed by @FreeAlgebra@ constraint.
 foldFree
-    :: ( FreeAlgebra  m
-       , AlgebraType0 m a
+    :: forall m a .
+       ( FreeAlgebra  m
        , AlgebraType  m a
        )
     => m a
     -> a
-foldFree = foldMapFree id
+foldFree ma = case forget @m @a of
+    Proof Dict -> foldMapFree id ma
 
 -- |
 -- The canonical quotient map from a free algebra of a wider class to a free
@@ -112,10 +130,10 @@
 -- * @m@ is a free algebra generated by @a@
 -- * @n@ is a free algebra generated by @a@
 natFree :: forall m n a .
-           ( AlgebraType  m (n a)
-           , AlgebraType0 m a
-           , FreeAlgebra  m
+           ( FreeAlgebra  m
            , FreeAlgebra  n
+           , AlgebraType0 m a
+           , AlgebraType  m (n a)
            )
         => m a
         -> n a
@@ -132,45 +150,39 @@
          => (a -> b)
          -> m a
          -> m b
-fmapFree = go (proof :: Proof (AlgebraType m (m b)) (m b))
-    where
-    go :: Proof (AlgebraType m (m b)) (m b) -> (a -> b) -> m a -> m b
-    go p f ma = case p of Proof Dict -> foldMapFree (returnFree . f) ma
-    {-# INLINE go #-}
+fmapFree f ma = case proof @m @b of
+    Proof Dict -> foldMapFree (returnFree . f) ma
 
 -- |
 -- @'FreeAlgebra'@ constraint implies @Monad@ constrain.
 joinFree :: forall m a .
           ( FreeAlgebra  m
           , AlgebraType0 m a
-          , AlgebraType0 m (m a)
           )
          => m (m a)
          -> m a
-joinFree = go (proof :: Proof (AlgebraType m (m a)) (m a))
-    where
-    go :: Proof (AlgebraType m (m a)) (m a) -> m (m a) -> m a
-    go p mma = case p of Proof Dict  -> foldFree mma
-    {-# INLINE go #-}
+joinFree mma = case proof @m @a of
+    Proof Dict -> foldFree mma
 
 -- |
 -- The monadic @'bind'@ operator.  @'returnFree'@ is the corresponding
--- @'return'@ for this monad.
-bindFree :: ( FreeAlgebra  m
+-- @'return'@ for this monad.  This just @'foldMapFree'@ in disguise.
+bindFree :: forall m a b .
+            ( FreeAlgebra  m
             , AlgebraType0 m a
             , AlgebraType0 m b
-            , AlgebraType0 m (m b)
             )
          => m a
          -> (a -> m b)
          -> m b
-bindFree ma f = joinFree $ fmapFree f ma
+bindFree ma f = case proof @m @b of
+    Proof Dict -> foldMapFree f ma
 
 -- |
 -- @'Fix' m@ is the initial algebra in the category of algebras of type
 -- @'AlgebraType' m@, whenever it /exists/.
 --
--- Another way of puting this is observing that @'Fix' m@ is isomorphic to @m
+-- Another way of putting this is observing that @'Fix' m@ is isomorphic to @m
 -- Void@ where @m@ is the /free algebra/.  This isomorphisms is given by
 -- @
 --   fixToFree :: (FreeAlgebra m, AlgebraType m (m Void), Functor m) => Fix m -> m Void
@@ -179,7 +191,6 @@
 -- For monoids the inverse is given by @'Data.Fix.ana' (\_ -> [])@.  The
 -- category of semigroups, however,  does not have the initial object.
 cataFree :: ( FreeAlgebra  m
-            , AlgebraType0 m a
             , AlgebraType  m a
             , Functor m
             )
@@ -196,14 +207,16 @@
     foldMapFree f (a :| []) = f a
     foldMapFree f (a :| (b : bs)) = f a <> foldMapFree f (b :| bs)
 
-    proof = Proof Dict
+    proof  = Proof Dict
+    forget = Proof Dict
 
 type instance AlgebraType0 [] a = ()
 type instance AlgebraType  [] m = Monoid m
 instance FreeAlgebra [] where
     returnFree a = [a]
     foldMapFree = foldMap
-    proof = Proof Dict
+    proof  = Proof Dict
+    forget = Proof Dict
 
 type instance AlgebraType0 Maybe a = ()
 type instance AlgebraType  Maybe m = Pointed m
@@ -212,4 +225,5 @@
     foldMapFree _ Nothing  = point
     foldMapFree f (Just a) = f a
 
-    proof = Proof Dict
+    proof  = Proof Dict
+    forget = Proof Dict
diff --git a/src/Data/Group/Free.hs b/src/Data/Group/Free.hs
--- a/src/Data/Group/Free.hs
+++ b/src/Data/Group/Free.hs
@@ -1,7 +1,9 @@
 {- |
    Free groups
+
      * https://en.wikipedia.org/wiki/Free_group
      * https://ncatlab.org/nlab/show/Nielsen-Schreier+theorem
+
  -}
 module Data.Group.Free
     ( FreeGroup
@@ -102,10 +104,11 @@
     invert (FreeGroup as) = FreeGroup $ foldl (\acu a -> either Right Left a : acu) [] as
 
 type instance AlgebraType0 FreeGroup a = Eq a
-type instance AlgebraType  FreeGroup g = Group g
+type instance AlgebraType  FreeGroup g = (Eq g, Group g)
 instance FreeAlgebra FreeGroup where
     returnFree a = FreeGroup [Right a]
     foldMapFree _ (FreeGroup [])       = mempty
     foldMapFree f (FreeGroup (a : as)) = either (invert . f) f a <> foldMapFree f (FreeGroup as)
 
-    proof = Proof Dict
+    proof  = Proof Dict
+    forget = Proof Dict
diff --git a/src/Data/Monoid/Abelian.hs b/src/Data/Monoid/Abelian.hs
--- a/src/Data/Monoid/Abelian.hs
+++ b/src/Data/Monoid/Abelian.hs
@@ -26,8 +26,9 @@
     mempty = FreeAbelianMonoid (Map.empty)
 
 type instance AlgebraType0 FreeAbelianMonoid a = Ord a
-type instance AlgebraType  FreeAbelianMonoid m = (Monoid m, AbelianSemigroup m)
+type instance AlgebraType  FreeAbelianMonoid m = (Ord m, Monoid m, AbelianSemigroup m)
 instance FreeAlgebra FreeAbelianMonoid where
     returnFree a = FreeAbelianMonoid (Map.singleton a 1)
     foldMapFree g (FreeAbelianMonoid as) = Map.foldMapWithKey (\a n -> stimes n $ g a) as 
-    proof = Proof Dict
+    proof  = Proof Dict
+    forget = Proof Dict
diff --git a/src/Data/Monoid/MSet.hs b/src/Data/Monoid/MSet.hs
--- a/src/Data/Monoid/MSet.hs
+++ b/src/Data/Monoid/MSet.hs
@@ -119,4 +119,5 @@
 instance Monoid m => FreeAlgebra (FreeMSet m) where
     returnFree a = FreeMSet (mempty, a)
     foldMapFree f (FreeMSet (m, a)) = act m (f a)
-    proof = Proof Dict
+    proof  = Proof Dict
+    forget = Proof Dict
diff --git a/src/Data/Semigroup/Abelian.hs b/src/Data/Semigroup/Abelian.hs
--- a/src/Data/Semigroup/Abelian.hs
+++ b/src/Data/Semigroup/Abelian.hs
@@ -88,7 +88,7 @@
 instance Ord a => AbelianSemigroup (FreeAbelianSemigroup a)
 
 type instance AlgebraType0 FreeAbelianSemigroup a = Ord a
-type instance AlgebraType  FreeAbelianSemigroup a = AbelianSemigroup a
+type instance AlgebraType  FreeAbelianSemigroup a = (Ord a, AbelianSemigroup a)
 instance FreeAlgebra FreeAbelianSemigroup where
     returnFree a = FreeAbelianSemigroup $ Map.singleton a 1
     foldMapFree f (FreeAbelianSemigroup as) = foldMapFree f (toNonEmpty_ as)
@@ -101,4 +101,5 @@
         toNonEmpty_ :: Map a Integer -> NonEmpty a
         toNonEmpty_ = NE.fromList . concat . map (uncurry replicate_) . Map.toList
 
-    proof = Proof Dict
+    proof  = Proof Dict
+    forget = Proof Dict
diff --git a/src/Data/Semigroup/SemiLattice.hs b/src/Data/Semigroup/SemiLattice.hs
--- a/src/Data/Semigroup/SemiLattice.hs
+++ b/src/Data/Semigroup/SemiLattice.hs
@@ -50,9 +50,10 @@
 toNonEmpty (FreeSemiLattice as) = NE.fromList $ Set.toList as
 
 type instance AlgebraType0 FreeSemiLattice a = Ord a
-type instance AlgebraType  FreeSemiLattice a = SemiLattice a
+type instance AlgebraType  FreeSemiLattice a = (Ord a, SemiLattice a)
 instance FreeAlgebra FreeSemiLattice where
     returnFree a = FreeSemiLattice $ Set.singleton a
     foldMapFree f (FreeSemiLattice as) = sconcat $ fmap f $ NE.fromList $ Set.toList as
 
-    proof = Proof Dict
+    proof  = Proof Dict
+    forget = Proof Dict
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,22 @@
+module Main
+   ( main
+   ) where
+
+import           Control.Monad (unless)
+import           System.Exit (exitFailure)
+
+import qualified Test.Data.Algebra.Free (tests)
+import qualified Test.Control.Algebra.Free (tests)
+
+runTests :: [IO Bool] -> IO ()
+runTests tests = do
+    res <- and <$> sequence tests
+    unless res
+        exitFailure
+
+main :: IO ()
+main = do
+    runTests
+        [ Test.Data.Algebra.Free.tests
+        , Test.Control.Algebra.Free.tests
+        ]
diff --git a/test/Spec.hs b/test/Spec.hs
deleted file mode 100644
--- a/test/Spec.hs
+++ /dev/null
@@ -1,22 +0,0 @@
-module Spec
-   ( main
-   ) where
-
-import           Control.Monad (unless)
-import           System.Exit (exitFailure)
-
-import qualified Test.Data.Algebra.Free (tests)
-import qualified Test.Control.Algebra.Free (tests)
-
-runTests :: [IO Bool] -> IO ()
-runTests tests = do
-    res <- and <$> sequence tests
-    unless res
-        exitFailure
-
-main :: IO ()
-main = do
-    runTests
-        [ Test.Data.Algebra.Free.tests
-        , Test.Control.Algebra.Free.tests
-        ]