diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,3 +1,6 @@
 # Changelog for free-algebras
 
+## Version 0.0.2.0
+- Simplified `Proof` type.
+
 ## Unreleased changes
diff --git a/free-algebras.cabal b/free-algebras.cabal
--- a/free-algebras.cabal
+++ b/free-algebras.cabal
@@ -2,13 +2,15 @@
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 8252360922bbd229818e963e538ab0a45e583719ce19477848aa674083eb9377
+-- hash: 01ca145922d0171eb90e9232004a0c588b6403c06f81dcae21bd5416c907bd75
 
 name:           free-algebras
-version:        0.0.1.0
-description:    Please see the README on GitHub at <https://github.com/coot/free-algebras#readme>
+version:        0.0.2.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
 homepage:       https://github.com/coot/free-algebras#readme
-bug-reports:    https://github.com/git@github.com:coot/free-algebras/issues
+bug-reports:    https://github.com/coot/free-algebras/issues
 author:         Marcin Szamotulski
 maintainer:     profunctor@pm.me
 copyright:      (c) 2018 Marcin Szamotulski
@@ -22,7 +24,7 @@
 
 source-repository head
   type: git
-  location: https://github.com/git@github.com:coot/free-algebras
+  location: https://github.com/coot/free-algebras
 
 flag develop
   description: Set -Werror flag
@@ -48,6 +50,7 @@
   default-extensions: ConstraintKinds DataKinds DeriveFunctor EmptyDataDecls FlexibleInstances FlexibleContexts KindSignatures InstanceSigs MultiParamTypeClasses OverloadedStrings PolyKinds RankNTypes ScopedTypeVariables TupleSections TypeApplications TypeFamilies
   build-depends:
       base >=4.11 && <5
+    , constraints
     , containers
     , data-fix
     , free
@@ -72,9 +75,10 @@
   hs-source-dirs:
       test
   default-extensions: ConstraintKinds DataKinds DeriveFunctor EmptyDataDecls FlexibleInstances FlexibleContexts KindSignatures InstanceSigs MultiParamTypeClasses OverloadedStrings PolyKinds RankNTypes ScopedTypeVariables TupleSections TypeApplications TypeFamilies
-  ghc-options: -threaded -rtsopts -with-rtsopts=-N -main-is Spec
+  ghc-options: -threaded -rtsopts -with-rtsopts=-N
   build-depends:
       base >=4.11 && <5
+    , constraints
     , containers
     , data-fix
     , 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
@@ -52,6 +52,7 @@
 import           Control.Monad.Writer.Class (MonadWriter (..))
 import qualified Control.Monad.Writer.Lazy as L (WriterT (..))
 import qualified Control.Monad.Writer.Strict as S (WriterT (..))
+import           Data.Constraint (Dict (..))
 import           Data.Kind (Type)
 import           Data.Fix (Fix, cataM)
 import           Data.Functor.Coyoneda (Coyoneda (..), liftCoyoneda)
@@ -93,11 +94,11 @@
         -- ^ a homomorphism from @m f@ to @d@
 
     -- |
-    -- A proof that @'AlgebraType0' m (m f)@ holds.
-    proof0 :: forall f. AlgebraType0 m f => Proof (AlgebraType0 m (m f)) m f
+    -- 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.
-    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)
 
 -- |
 -- Anything that carries @'FreeAlgebra1'@ constraint is also an instance of
@@ -163,9 +164,9 @@
            => (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 nat = foldNatFree (liftFree . nat)
+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 #-}
 
 -- |
@@ -191,7 +192,7 @@
 
 -- |
 -- @'joinFree1'@ makes @m@ a monad in some subcatgory of types of kind @Type -> Type@
--- (usually the end-functor category of @Hask@).  It is just a specialization
+-- (usually the endo-functor category of @Hask@).  It is just a specialization
 -- of @'foldFree1'@.
 joinFree1 :: forall m f a .
              ( FreeAlgebra1 m
@@ -199,10 +200,10 @@
              )
           => 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)
+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 Proof = foldFree1
+    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 #-}
 
 -- |
@@ -215,10 +216,10 @@
           => 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)
+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 Proof mfa nat = joinFree1 $ hoistFree1 nat mfa
+    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 #-}
 
 assocFree1 :: forall m f a .
@@ -229,16 +230,16 @@
               )
            => m f (m f a)
            -> m (m f) (f a)
-assocFree1 = outer (proof0 :: Proof (AlgebraType0 m (m f)) m f)
+assocFree1 = outer (proof0 :: Proof (AlgebraType0 m (m f)) (m 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 = inner (proof1 :: Proof (AlgebraType m (m (m f))) m (m f))
+        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 = fmap g <$> foldNatFree f
+            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
@@ -286,8 +287,8 @@
     liftFree = liftCoyoneda
     foldNatFree nat (Coyoneda ba fx) = ba <$> nat fx
 
-    proof0 = Proof
-    proof1 = Proof
+    proof0 = Proof Dict
+    proof1 = Proof Dict
 
 -- |
 -- Algebras of the same type as @'Ap'@ are the applicative functors.
@@ -300,8 +301,8 @@
     liftFree  = Ap.liftAp
     foldNatFree = Ap.runAp
 
-    proof0 = Proof
-    proof1 = Proof
+    proof0 = Proof Dict
+    proof1 = Proof Dict
 
 type instance AlgebraType0 Fast.Ap g = Functor g
 type instance AlgebraType  Fast.Ap g = Applicative g
@@ -309,8 +310,8 @@
     liftFree  = Fast.liftAp
     foldNatFree = Fast.runAp
 
-    proof0 = Proof
-    proof1 = Proof
+    proof0 = Proof Dict
+    proof1 = Proof Dict
 
 type instance AlgebraType0 Final.Ap g = Functor g
 type instance AlgebraType  Final.Ap g = Applicative g
@@ -318,8 +319,8 @@
     liftFree  = Final.liftAp
     foldNatFree = Final.runAp
 
-    proof0 = Proof
-    proof1 = Proof
+    proof0 = Proof Dict
+    proof1 = Proof Dict
 
 -- |
 -- @'Day' f f@ newtype wrapper.  It is isomorphic with @'Ap' f@ for applicative
@@ -345,8 +346,8 @@
     foldNatFree nat (DayF day)
         = Day.dap . Day.trans2 nat . Day.trans1 nat $ day
 
-    proof0 = Proof
-    proof1 = Proof
+    proof0 = Proof Dict
+    proof1 = Proof Dict
 
 -- |
 -- Algebras of the same type as @'Free'@ monad is the class of all monads.
@@ -358,8 +359,8 @@
     liftFree    = Free.liftF
     foldNatFree = Free.foldFree
 
-    proof0 = Proof
-    proof1 = Proof
+    proof0 = Proof Dict
+    proof1 = Proof Dict
 
 type instance AlgebraType0 Church.F f = Functor f
 type instance AlgebraType  Church.F m = Monad m
@@ -367,8 +368,8 @@
     liftFree    = Church.liftF
     foldNatFree = Church.foldF
 
-    proof0 = Proof
-    proof1 = Proof
+    proof0 = Proof Dict
+    proof1 = Proof Dict
 
 type instance AlgebraType0 Alt f = Functor f
 type instance AlgebraType  Alt m = Alternative m
@@ -376,8 +377,8 @@
     liftFree    = Alt.liftAlt
     foldNatFree = Alt.runAlt
 
-    proof0 = Proof
-    proof1 = Proof
+    proof0 = Proof Dict
+    proof1 = Proof Dict
 
 -- |
 -- Algebras of the same type as @'L.StateT'@ monad is the class of all state
@@ -401,8 +402,8 @@
         put s
         return a
 
-    proof0 = Proof
-    proof1 = Proof
+    proof0 = Proof Dict
+    proof1 = Proof Dict
 
 -- |
 -- Algebras of the same type as @'S.StateT'@ monad is the class of all state
@@ -420,8 +421,8 @@
         put s
         return a
 
-    proof0 = Proof
-    proof1 = Proof
+    proof0 = Proof Dict
+    proof1 = Proof Dict
 
 -- |
 -- Algebras of the same type as @'L.WriterT'@ monad is the class of all writer
@@ -434,8 +435,8 @@
     liftFree = lift
     foldNatFree nat (L.WriterT m) = fst <$> nat m
 
-    proof0 = Proof
-    proof1 = Proof
+    proof0 = Proof Dict
+    proof1 = Proof Dict
 
 -- |
 -- Algebras of the same type as @'S.WriterT'@ monad is the class of all writer
@@ -449,8 +450,8 @@
     liftFree = lift
     foldNatFree nat (S.WriterT m) = fst <$> nat m
 
-    proof0 = Proof
-    proof1 = Proof
+    proof0 = Proof Dict
+    proof1 = Proof Dict
 
 -- |
 -- Algebras of the same type as @'L.ReaderT'@ monad is the class of all reader
@@ -464,8 +465,8 @@
     foldNatFree nat (ReaderT g) =
         ask >>= nat . g
 
-    proof0 = Proof
-    proof1 = Proof
+    proof0 = Proof Dict
+    proof1 = Proof Dict
 
 -- |
 -- Algebras of the same type as @'S.ReaderT'@ monad is the class of all reader
@@ -482,8 +483,8 @@
             Left e  -> throwError e
             Right a -> return a
 
-    proof0 = Proof
-    proof1 = Proof
+    proof0 = Proof Dict
+    proof1 = 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
@@ -497,8 +498,8 @@
         tell w
         return a
 
-    proof0 = Proof
-    proof1 = Proof
+    proof0 = Proof Dict
+    proof1 = 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
@@ -512,8 +513,8 @@
         tell w
         return a
 
-    proof0 = Proof
-    proof1 = Proof
+    proof0 = Proof Dict
+    proof1 = Proof Dict
 
 -- |
 -- Algebra type for @'ListT'@ monad transformer.
@@ -538,8 +539,8 @@
         a <- foldM (\x y -> x `mappend1_` y) empty as
         return a
 
-    proof0 = Proof
-    proof1 = Proof
+    proof0 = Proof Dict
+    proof1 = Proof Dict
 
 -- $monadContT
 --
@@ -565,5 +566,5 @@
             Nothing -> point
             Just a  -> return a
 
-    proof0 = Proof
-    proof1 = Proof
+    proof0 = Proof Dict
+    proof1 = 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
@@ -3,6 +3,7 @@
 module Control.Monad.Action where
 
 import           Control.Monad (join)
+import           Data.Constraint (Dict (..))
 import           Data.Functor.Const (Const (..))
 
 import           Control.Algebra.Free
@@ -62,5 +63,5 @@
 instance Monad m => FreeAlgebra1 (FreeMAction m) where
     liftFree = FreeMAction . return
     foldNatFree nat (FreeMAction mfa) = mact $ nat <$> mfa
-    proof0 = Proof
-    proof1 = Proof
+    proof0 = Proof Dict
+    proof1 = 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
@@ -19,6 +19,7 @@
 
 import           Prelude
 
+import           Data.Constraint (Dict (..))
 import           Data.Fix (Fix, cata)
 import           Data.Kind (Constraint, Type)
 import           Data.List.NonEmpty (NonEmpty (..))
@@ -47,9 +48,8 @@
 type family AlgebraType0 (f :: k) (a :: l) :: Constraint
 
 -- |
--- Proof that @a@ is an algebra of type @'AlgebraType' m a@.
-data Proof (c :: Constraint) (f :: k) (a :: l) where
-    Proof :: c => Proof c f a
+-- A proof that constraint @c@ holds for type @a@.
+newtype Proof (c :: Constraint) (a :: l) = Proof (Dict c)
 
 -- |
 -- A lawful instance has to guarantee that @'unFoldFree'@ is an inverse of
@@ -71,9 +71,9 @@
         => (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, e.g. if @m ~ []@
+    -- | 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 :: forall a. AlgebraType0 m a => Proof (AlgebraType m (m a)) (m a)
 
 -- |
 -- Inverse of @'foldMapFree'@
@@ -132,10 +132,10 @@
          => (a -> b)
          -> m a
          -> m b
-fmapFree = go (proof :: Proof (AlgebraType m (m b)) 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 -> foldMapFree (returnFree . f) ma
+    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 #-}
 
 -- |
@@ -147,10 +147,10 @@
           )
          => m (m a)
          -> m a
-joinFree = go (proof :: Proof (AlgebraType 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 -> foldFree mma
+    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 #-}
 
 -- |
@@ -196,14 +196,14 @@
     foldMapFree f (a :| []) = f a
     foldMapFree f (a :| (b : bs)) = f a <> foldMapFree f (b :| bs)
 
-    proof = Proof
+    proof = Proof Dict
 
 type instance AlgebraType0 [] a = ()
 type instance AlgebraType  [] m = Monoid m
 instance FreeAlgebra [] where
     returnFree a = [a]
     foldMapFree = foldMap
-    proof = Proof
+    proof = Proof Dict
 
 type instance AlgebraType0 Maybe a = ()
 type instance AlgebraType  Maybe m = Pointed m
@@ -212,4 +212,4 @@
     foldMapFree _ Nothing  = point
     foldMapFree f (Just a) = f a
 
-    proof = Proof
+    proof = 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
@@ -11,6 +11,7 @@
     ) where
 
 import           Control.Monad (ap)
+import           Data.Constraint (Dict (..))
 import           Data.Group (Group (..))
 import           Data.Semigroup (Semigroup (..))
 
@@ -107,4 +108,4 @@
     foldMapFree _ (FreeGroup [])       = mempty
     foldMapFree f (FreeGroup (a : as)) = either (invert . f) f a <> foldMapFree f (FreeGroup as)
 
-    proof = Proof
+    proof = 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
@@ -2,6 +2,7 @@
     ( FreeAbelianMonoid (..)
     ) where
 
+import           Data.Constraint (Dict (..))
 import           Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
 import           Data.Semigroup (stimes)
@@ -29,5 +30,4 @@
 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
+    proof = 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
@@ -13,12 +13,13 @@
     ) where
 
 import           Control.Monad (ap)
-import           Data.Monoid (Monoid, Endo (..), Sum (..))
-import           Data.List.NonEmpty (NonEmpty)
+import           Data.Constraint (Dict (..))
 import           Data.Functor.Const (Const (..))
 import           Data.Functor.Identity (Identity (..))
 import qualified Data.Functor.Product as Functor (Product)
 import qualified Data.Functor.Sum as Functor (Sum)
+import           Data.List.NonEmpty (NonEmpty)
+import           Data.Monoid (Monoid, Endo (..), Sum (..))
 import           Data.Natural (Natural)
 import           Data.Ord (Down)
 import           Data.Set (Set)
@@ -118,4 +119,4 @@
 instance Monoid m => FreeAlgebra (FreeMSet m) where
     returnFree a = FreeMSet (mempty, a)
     foldMapFree f (FreeMSet (m, a)) = act m (f a)
-    proof = Proof
+    proof = 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
@@ -5,6 +5,7 @@
     , fromNonEmpty
     ) where
 
+import           Data.Constraint (Dict (..))
 import           Data.IntSet (IntSet)
 import           Data.List.NonEmpty (NonEmpty)
 import qualified Data.List.NonEmpty as NE
@@ -100,4 +101,4 @@
         toNonEmpty_ :: Map a Integer -> NonEmpty a
         toNonEmpty_ = NE.fromList . concat . map (uncurry replicate_) . Map.toList
 
-    proof = Proof
+    proof = 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
@@ -5,6 +5,7 @@
     , toNonEmpty
     ) where
 
+import           Data.Constraint (Dict (..))
 import           Data.List.NonEmpty (NonEmpty (..))
 import qualified Data.List.NonEmpty as NE
 import           Data.IntSet (IntSet)
@@ -54,4 +55,4 @@
     returnFree a = FreeSemiLattice $ Set.singleton a
     foldMapFree f (FreeSemiLattice as) = sconcat $ fmap f $ NE.fromList $ Set.toList as
 
-    proof = Proof
+    proof = Proof Dict