diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,12 @@
+# Changelog
+
+`hedgehog-classes` uses [PVP Versioning][1].
+The changelog is available [on GitHub][2].
+
+0.0.0
+=====
+
+* Initially created.
+
+[1]: https://pvp.haskell.org
+[2]: https://github.com/chessai/hedgehog-classes/releases
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,29 @@
+BSD 3-Clause License
+
+Copyright (c) 2019, chessai
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+* Redistributions of source code must retain the above copyright notice, this
+  list of conditions and the following disclaimer.
+
+* Redistributions in binary form must reproduce the above copyright notice,
+  this list of conditions and the following disclaimer in the documentation
+  and/or other materials provided with the distribution.
+
+* Neither the name of the copyright holder nor the names of its
+  contributors may be used to endorse or promote products derived from
+  this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,8 @@
+# hedgehog-classes
+
+[![Hackage](https://img.shields.io/hackage/v/hedgehog-classes.svg)](https://hackage.haskell.org/package/hedgehog-classes)
+[![BSD3 license](https://img.shields.io/badge/license-BSD3-blue.svg)](LICENSE)
+<!--- [![Stackage Lts](http://stackage.org/package/hedgehog-classes/badge/lts)](http://stackage.org/lts/package/hedgehog-classes)--->
+<!--- [![Stackage Nightly](http://stackage.org/package/hedgehog-classes/badge/nightly)](http://stackage.org/nightly/package/hedgehog-classes) --->
+
+Hedgehog will eat your typeclass bugs
diff --git a/hedgehog-classes.cabal b/hedgehog-classes.cabal
new file mode 100644
--- /dev/null
+++ b/hedgehog-classes.cabal
@@ -0,0 +1,186 @@
+cabal-version: 2.0
+name: 
+  hedgehog-classes
+version:
+  0.1.0.0
+synopsis:
+  Hedgehog will eat your typeclass bugs
+description:
+  This library provides Hedgehog properties to ensure
+  that typeclass instances adhere to the set of laws
+  that they are supposed to. There are other libraries
+  that do similar things, such as `genvalidity-hspec` and `checkers`.
+  This library differs from other solutions by not introducing any
+  new typeclasses that the user needs to learn, and otherwise minimal
+  API overhead.
+  .
+  This library is directly inspired by `quickcheck-classes`.
+homepage:
+  https://github.com/chessai/hedgehog-classes
+bug-reports:
+  https://github.com/chessai/hedgehog-classes/issues
+license:
+  BSD3
+license-file:
+  LICENSE
+author:
+  chessai
+maintainer:
+  chessai1996@gmail.com
+copyright:
+  2019 chessai
+category:
+  Testing
+build-type:
+  Simple
+extra-doc-files:
+    README.md
+  , CHANGELOG.md
+tested-with: GHC == 8.6.1, GHC == 8.6.2, GHC == 8.6.3
+
+source-repository head
+  type:                git
+  location:            https://github.com/chessai/hedgehog-classes.git
+
+flag aeson
+  description:
+    You can disable the use of the `aeson` package using `-f-aeson`.
+    .
+    This may be useful for accelerating builds in sandboxes for expert users.
+  default: True
+  manual: True
+
+-- flag semigroupoids
+--   description:
+--     You can disable the use of the `semirings` package using `-f-semirings`.
+--     .
+--     This may be useful for accelerating builds in sandboxes for expert users.
+--   default: True
+--   manual: True
+
+-- flag semirings
+--   description:
+--     You can disable the use of the `semirings` package using `-f-semirings`.
+--     .
+--     This may be useful for accelerating builds in sandboxes for expert users.
+--   default: True
+--   manual: True
+
+library
+  hs-source-dirs:
+    src
+  exposed-modules:
+    Hedgehog.Classes
+  other-modules:
+    Hedgehog.Classes.Alternative
+    Hedgehog.Classes.Applicative
+    Hedgehog.Classes.Arrow
+    Hedgehog.Classes.Bifoldable
+    Hedgehog.Classes.Bifunctor
+    Hedgehog.Classes.Bitraversable
+    Hedgehog.Classes.Bits
+    Hedgehog.Classes.Category
+    Hedgehog.Classes.Common
+      Hedgehog.Classes.Common.ApTrans
+      Hedgehog.Classes.Common.Bottom
+      Hedgehog.Classes.Common.Compat
+      Hedgehog.Classes.Common.Equation
+      Hedgehog.Classes.Common.Func
+      Hedgehog.Classes.Common.Gen
+      Hedgehog.Classes.Common.IO
+      Hedgehog.Classes.Common.Laws
+      Hedgehog.Classes.Common.Property
+      Hedgehog.Classes.Common.PP
+    Hedgehog.Classes.Contravariant
+    Hedgehog.Classes.Enum
+    Hedgehog.Classes.Eq
+    Hedgehog.Classes.Foldable
+    Hedgehog.Classes.Functor
+    Hedgehog.Classes.Generic
+    Hedgehog.Classes.Integral
+--    Hedgehog.Classes.Ix
+    Hedgehog.Classes.Json
+    Hedgehog.Classes.Monad
+--    Hedgehog.Classes.MonadFix
+    Hedgehog.Classes.MonadIO
+    Hedgehog.Classes.MonadPlus
+    Hedgehog.Classes.MonadZip
+    Hedgehog.Classes.Monoid
+    Hedgehog.Classes.Ord
+    Hedgehog.Classes.Semigroup
+--    Hedgehog.Classes.Semiring
+    Hedgehog.Classes.Show
+    Hedgehog.Classes.ShowRead
+    Hedgehog.Classes.Storable
+    Hedgehog.Classes.Traversable
+  build-depends:
+      base                >= 4.12.0.0 && < 4.14.0.0
+    , hedgehog            >= 0.5.0.0  && < 0.7.0.0
+    , containers          >= 0.5.9.2  && < 0.7.0.0
+    , pretty-show         >= 1.6.0.0  && < 2.0.0.0
+    , transformers        >= 0.5.0.0  && < 0.6.0.0
+    , wl-pprint-annotated >= 0.0.0.0  && < 0.2.0.0
+  ghc-options:
+    -Wall
+  default-language:
+    Haskell2010
+  if impl(ghc < 8.5)
+    buildable: False
+  if impl(ghc >= 8.5)
+    cpp-options: -DHAVE_QUANTIFIED_CONSTRAINTS
+  if flag(aeson)
+    build-depends: aeson >= 0.9.0.0 && < 1.5.0.0
+    cpp-options: -DHAVE_AESON
+--  if flag(semigroupoids)
+--    build-depends: semigroupoids >= 0.5.3.0 && < 0.6.0.0
+--    cpp-options: -DHAVE_SEMIGROUPOIDS
+--  if flag(semirings)
+--    build-depends: semirings >= 0.3.1.1 && < 0.4.0.0
+--    cpp-options: -DHAVE_SEMIRINGS
+--  if flag(vector)
+--    build-depends: vector >= 0.12.0.0 && < 0.13.0.0 
+--    cpp-options: -DHAVE_VECTOR
+ 
+--test-suite spec
+--  type:                exitcode-stdio-1.0
+--  hs-source-dirs:      test
+--  main-is:             Spec.hs
+--
+--  other-modules:       Spec.Alternative
+--                       Spec.Applicative
+--                       Spec.Arrow
+--                       Spec.Bifoldable
+--                       Spec.Bifunctor
+--                       Spec.Bitraversable
+--                       Spec.Bits
+--                       Spec.Category
+--                       Spec.Contravariant
+--                       Spec.Enum
+--                       Spec.Eq
+--                       Spec.Foldable
+--                       Spec.Functor
+--                      Spec.Generic
+--                       Spec.Integral
+--                       Spec.Ix
+--                       Spec.Json
+--                       Spec.Monad
+--                       Spec.MonadIO
+--                       Spec.MonadPlus
+--                       Spec.MonadZip
+--                       Spec.Monoid
+--                       Spec.Ord
+--                       Spec.Semigroup
+--                       Spec.Show
+--                       Spec.ShowRead
+--                       Spec.Storable
+--                       Spec.Traversable
+--
+--  build-depends:       base >= 4.12.0.0 && < 4.13
+--                     , aeson 
+--                     , containers 
+--                     , hedgehog 
+--                     , hedgehog-classes
+--
+--  ghc-options:         -Wall
+-- 
+--  default-language:    Haskell2010
diff --git a/src/Hedgehog/Classes.hs b/src/Hedgehog/Classes.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes.hs
@@ -0,0 +1,102 @@
+{-| This library provides sets of properties that should hold for common
+    typeclasses.
+
+    /Note:/ on GHC < 8.5, this library uses the higher-kinded typeclasses
+    ('Data.Functor.Classes.Show1', 'Data.Functor.Classes.Eq1', 'Data.Functor.Classes.Ord1', etc.),
+    but on GHC >= 8.5, it uses `-XQuantifiedConstraints` to express these
+    constraints more cleanly.
+-}
+module Hedgehog.Classes
+  ( -- * Running
+    lawsCheck
+  , lawsCheckOne
+  , lawsCheckMany
+
+    -- * Properties
+    -- ** Ground types
+  , bitsLaws
+  , eqLaws
+  , integralLaws
+  , monoidLaws
+  , commutativeMonoidLaws
+  , ordLaws
+--  , ixLaws
+  , enumLaws
+  , boundedEnumLaws
+  , semigroupLaws
+  , commutativeSemigroupLaws
+  , exponentialSemigroupLaws
+  , idempotentSemigroupLaws
+  , rectangularBandSemigroupLaws
+  , showLaws
+  , showReadLaws
+  , storableLaws
+  , genericLaws
+  , jsonLaws
+
+    -- ** Unary type constructors
+  , alternativeLaws
+  , applicativeLaws
+  , contravariantLaws 
+  , foldableLaws
+  , functorLaws
+  , monadLaws
+--  , monadFixLaws
+  , monadIOLaws
+  , monadPlusLaws
+  , monadZipLaws
+  , traversableLaws
+
+    -- ** Binary type constructors
+  , arrowLaws
+  , bifoldableLaws
+  , bifoldableFunctorLaws
+  , bifunctorLaws
+  , bitraversableLaws
+  , categoryLaws
+  , commutativeCategoryLaws
+
+    -- * Defining your own laws
+  , Laws(..)
+  , LawContext(..)
+  , Context(..)
+  , contextualise
+
+    -- * Hedgehog equality tests sans source information
+  , hLessThan, hGreaterThan
+  , heq, heq1, heq2
+  , heqCtx, heqCtx1, heqCtx2
+  , hneq, hneq1, hneq2
+  , hneqCtx, hneqCtx1, hneqCtx2
+  ) where
+
+import Hedgehog.Classes.Alternative (alternativeLaws)
+import Hedgehog.Classes.Applicative (applicativeLaws)
+import Hedgehog.Classes.Arrow (arrowLaws)
+import Hedgehog.Classes.Bifoldable (bifoldableLaws, bifoldableFunctorLaws)
+import Hedgehog.Classes.Bifunctor (bifunctorLaws)
+import Hedgehog.Classes.Bitraversable (bitraversableLaws)
+import Hedgehog.Classes.Bits (bitsLaws)
+import Hedgehog.Classes.Category (categoryLaws, commutativeCategoryLaws)
+import Hedgehog.Classes.Common
+import Hedgehog.Classes.Contravariant (contravariantLaws)
+import Hedgehog.Classes.Enum (enumLaws, boundedEnumLaws)
+import Hedgehog.Classes.Eq (eqLaws)
+import Hedgehog.Classes.Foldable (foldableLaws)
+import Hedgehog.Classes.Functor (functorLaws)
+import Hedgehog.Classes.Generic (genericLaws)
+import Hedgehog.Classes.Integral (integralLaws)
+--import Hedgehog.Classes.Ix (ixLaws)
+import Hedgehog.Classes.Json (jsonLaws)
+import Hedgehog.Classes.Monad (monadLaws)
+import Hedgehog.Classes.MonadIO (monadIOLaws)
+import Hedgehog.Classes.MonadPlus (monadPlusLaws)
+import Hedgehog.Classes.MonadZip (monadZipLaws)
+import Hedgehog.Classes.Monoid (monoidLaws, commutativeMonoidLaws)
+import Hedgehog.Classes.Ord (ordLaws)
+import Hedgehog.Classes.Semigroup (semigroupLaws, commutativeSemigroupLaws, exponentialSemigroupLaws, idempotentSemigroupLaws, rectangularBandSemigroupLaws)
+import Hedgehog.Classes.Show (showLaws)
+import Hedgehog.Classes.ShowRead (showReadLaws)
+import Hedgehog.Classes.Storable (storableLaws)
+import Hedgehog.Classes.Traversable (traversableLaws)
+ 
diff --git a/src/Hedgehog/Classes/Alternative.hs b/src/Hedgehog/Classes/Alternative.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Alternative.hs
@@ -0,0 +1,85 @@
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RankNTypes            #-}
+
+module Hedgehog.Classes.Alternative (alternativeLaws) where
+
+import Control.Applicative (Alternative(..))
+
+import Hedgehog
+import Hedgehog.Classes.Common
+
+-- | Tests the following 'Alternative' laws:
+-- 
+-- [__Left Identity__]: @'empty' '<|>' a@ ≡ @a@
+-- [__Right Identity__]: @a '<|>' 'empty'@ ≡ @a@
+-- [__Associativity__]: @a '<|>' (b '<|>' c)@ ≡ @(a '<|>' b) '<|>' c@
+alternativeLaws ::
+  ( Alternative f
+  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
+  ) => (forall x. Gen x -> Gen (f x)) -> Laws
+alternativeLaws gen = Laws "Alternative"
+  [ ("Left Identity", alternativeLeftIdentity gen)
+  , ("Right Identity", alternativeRightIdentity gen)
+  , ("Associativity", alternativeAssociativity gen)
+  ]
+
+type AlternativeProp f =
+  ( Alternative f
+  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
+  ) => (forall x. Gen x -> Gen (f x)) -> Property
+
+alternativeLeftIdentity :: forall f. AlternativeProp f
+alternativeLeftIdentity fgen = property $ do
+  a <- forAll $ fgen genSmallInteger
+  let lhs = empty <|> a
+  let rhs = a
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Left Identity", lawContextLawBody = "empty <|> a" `congruency` "a"
+        , lawContextTcName = "Alternative", lawContextTcProp =
+            let showA = show a;
+            in lawWhere
+              [ "empty <|> a" `congruency` "a, where"
+              , "a = " ++ showA
+              ]
+        , lawContextReduced = reduced lhs rhs
+        }
+  heqCtx1 lhs rhs ctx
+
+alternativeRightIdentity :: forall f. AlternativeProp f
+alternativeRightIdentity fgen = property $ do
+  a <- forAll $ fgen genSmallInteger
+  let lhs = a <|> empty
+  let rhs = a
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Right Identity", lawContextLawBody = "a <|> empty" `congruency` "a"
+        , lawContextTcName = "Alternative", lawContextTcProp =
+            let showA = show a;
+            in lawWhere
+              [ "a <|> empty" `congruency` "a, where"
+              , "a = " ++ showA
+              ]
+        , lawContextReduced = reduced lhs rhs
+        }
+  heqCtx1 lhs rhs ctx  
+
+alternativeAssociativity :: forall f. AlternativeProp f
+alternativeAssociativity fgen = property $ do
+  a <- forAll $ fgen genSmallInteger
+  b <- forAll $ fgen genSmallInteger
+  c <- forAll $ fgen genSmallInteger
+  let lhs = (a <|> (b <|> c))
+  let rhs = ((a <|> b) <|> c)
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Associativity", lawContextLawBody = "a <|> (b <|> c)" `congruency` "(a <|> b) <|> c"
+        , lawContextTcName = "Alternative", lawContextTcProp =
+            let showA = show a; showB = show b; showC = show c;
+            in lawWhere
+                 [ "a <|> (b <|> c)" `congruency` "(a <|> b) <|> c), where"
+                 , "a = " ++ showA
+                 , "b = " ++ showB
+                 , "c = " ++ showC
+                 ]
+        , lawContextReduced = reduced lhs rhs
+        }
+  heqCtx1 lhs rhs ctx
diff --git a/src/Hedgehog/Classes/Applicative.hs b/src/Hedgehog/Classes/Applicative.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Applicative.hs
@@ -0,0 +1,161 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RankNTypes #-}
+
+module Hedgehog.Classes.Applicative (applicativeLaws) where
+
+import Control.Applicative (Applicative(..))
+
+import Hedgehog
+import Hedgehog.Classes.Common
+
+-- | Tests the following 'Applicative' laws:
+--
+-- [__Identity__]: @'pure' 'id' '<*>' v@ ≡ @v@
+-- [__Composition__]: @'pure' ('.') '<*>' u '<*>' v '<*>' w@ ≡ @u '<*>' (v '<*>' w)@
+-- [__Homomorphism__]: @'pure' f '<*>' 'pure'@ x ≡ @'pure' (f x)@
+-- [__Interchange__]: @u '<*>' 'pure' y@ ≡ @'pure' ('$' y) '<*>' u@
+-- [__LiftA2 1__]: @'liftA2' 'id' f x@ ≡ @f '<*>' x@
+-- [__LiftA2 2__]: @'liftA2' f x y@ ≡ @f '<$>' x '<*>' y@
+applicativeLaws ::
+  ( Applicative f
+  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
+  ) => (forall x. Gen x -> Gen (f x)) -> Laws
+applicativeLaws gen = Laws "Applicative"
+  [ ("Identity", applicativeIdentity gen)
+  , ("Composition", applicativeComposition gen)
+  , ("Homomorphism", applicativeHomomorphism gen)
+  , ("Interchange", applicativeInterchange gen)
+  , ("LiftA2 Part 1", applicativeLiftA2_1 gen)
+  , ("LiftA2 Part 2", applicativeLiftA2_2 gen) 
+  ]
+
+type ApplicativeProp f =
+  ( Applicative f
+  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
+  ) => (forall x. Gen x -> Gen (f x)) -> Property
+
+applicativeIdentity :: forall f. ApplicativeProp f
+applicativeIdentity fgen = property $ do
+  a <- forAll $ fgen genSmallInteger
+  let lhs = pure id <*> a
+  let rhs = a
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Identity", lawContextLawBody = "pure id <*> v" `congruency` "v"
+        , lawContextTcName = "Applicative", lawContextTcProp =
+             let showA = show a
+             in lawWhere
+                 [ "pure id <*> v" `congruency` "v, where"
+                 , "v = " ++ showA
+                 ]
+        , lawContextReduced = reduced lhs rhs
+        }
+  heqCtx1 lhs rhs ctx
+
+applicativeComposition :: forall f. ApplicativeProp f
+applicativeComposition fgen = property $ do
+  u' <- forAll $ fgen genQuadraticEquation
+  v' <- forAll $ fgen genQuadraticEquation
+  w' <- forAll genSmallInteger
+  let u = runQuadraticEquation <$> u'
+      v = runQuadraticEquation <$> v'
+      w = pure w'
+  let lhs = pure (.) <*> u <*> v <*> w
+  let rhs = u <*> (v <*> w)
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Composition", lawContextLawBody = "pure (.) <*> u <*> v <*> w == u <*> (v <*> w)"
+        , lawContextTcName = "Applicative", lawContextTcProp =
+            let showU = show u'; showV = show v'; showW = show w';
+            in lawWhere
+                 [ "pure (.) <*> u <*> v <*> w", congruent, "u <*> (v <*> w), where"
+                 , "u = " ++ showU
+                 , "v = " ++ showV
+                 , "w = " ++ showW
+                 ]
+        , lawContextReduced = reduced lhs rhs
+        }
+
+  heqCtx1 lhs rhs ctx
+
+applicativeHomomorphism :: forall f. ApplicativeProp f
+applicativeHomomorphism _ = property $ do
+  e <- forAll genQuadraticEquation
+  a <- forAll genSmallInteger
+  let f = runQuadraticEquation e
+  let lhs = pure f <*> pure a
+  let rhs = pure (f a) :: f Integer
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Homomorphism", lawContextLawBody = "pure f <*> pure x" `congruency` "pure (f x)"
+        , lawContextTcName = "Applicative", lawContextTcProp =
+            let showF = show e; showX = show a;
+            in lawWhere
+              [ "pure f <*> pure x", congruent, "pure (f x), where"
+              , "f = " ++ showF
+              , "x = " ++ showX
+              ]
+        , lawContextReduced = reduced lhs rhs
+        }
+  heqCtx1 lhs rhs ctx
+
+applicativeInterchange :: forall f. ApplicativeProp f
+applicativeInterchange fgen = property $ do
+  u' <- forAll $ fgen genQuadraticEquation
+  y <- forAll genSmallInteger
+  let u = fmap runQuadraticEquation u'
+  let lhs = (u <*> pure y)
+  let rhs = pure ($ y) <*> u
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Interchange", lawContextLawBody = "u <*> pure y" `congruency` "pure ($ y) <*> u"
+        , lawContextTcName = "Applicative", lawContextTcProp =
+            let showU = show u'; showY = show y;
+            in lawWhere
+              [ "u <*> pure y", congruent, "pure ($ y) <*> u, where"
+              , "u = " ++ showU
+              , "y = " ++ showY
+              ]
+        , lawContextReduced = reduced lhs rhs
+        }
+  heqCtx1 lhs rhs ctx
+
+applicativeLiftA2_1 :: forall f. ApplicativeProp f
+applicativeLiftA2_1 fgen = property $ do
+  f' <- forAll $ fgen genQuadraticEquation
+  x <- forAll $ fgen genSmallInteger
+  let f = fmap runQuadraticEquation f'
+  let lhs = liftA2 id f x
+  let rhs = f <*> x
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "LiftA2 1", lawContextLawBody = "liftA2 id f x" `congruency` "f <*> x"
+        , lawContextTcName = "Applicative", lawContextTcProp =
+            let showF = show f'; showX = show x;
+            in lawWhere
+              [ "liftA2 id f x", congruent, "f <*> x, where"
+              , "f = " ++ showF
+              , "x = " ++ showX
+              ]
+        , lawContextReduced = reduced lhs rhs
+        }
+  heqCtx1 lhs rhs ctx
+
+applicativeLiftA2_2 :: forall f. ApplicativeProp f
+applicativeLiftA2_2 fgen = property $ do
+  x <- forAll $ fgen genSmallInteger
+  y <- forAll $ fgen genSmallInteger
+  f' <- forAll $ genLinearEquationTwo
+  let f = runLinearEquationTwo f'
+  let lhs = liftA2 f x y
+  let rhs = f <$> x <*> y
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "LiftA2 2", lawContextLawBody = "liftA2 f x y == f <$> x <*> y"
+        , lawContextTcName = "Applicative", lawContextTcProp =
+            let showF = show f'; showX = show x; showY = show y;
+            in lawWhere
+              [ "liftA2 f x y" `congruency` "f <$> x <*> y, where"
+              , "f = " ++ showF
+              , "x = " ++ showX
+              , "y = " ++ showY
+              ]
+        , lawContextReduced = reduced lhs rhs
+        }
+  heqCtx1 lhs rhs ctx
+
diff --git a/src/Hedgehog/Classes/Arrow.hs b/src/Hedgehog/Classes/Arrow.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Arrow.hs
@@ -0,0 +1,96 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+
+module Hedgehog.Classes.Arrow (arrowLaws) where
+
+import Hedgehog
+import Hedgehog.Classes.Common
+
+import Control.Arrow(Arrow(..), (>>>))
+import Control.Category(Category(..))
+import Prelude hiding (id, (.))
+import qualified Prelude
+
+-- | Tests the following 'Arrow' laws:
+--
+-- [__Arr Identity__]: @'arr' 'id'@ ≡ @'id'@
+-- [__Arr Composition__]: @'arr' (f '>>>' g)@ ≡ @'arr' f '>>>' 'arr' g@
+-- [__Arr-First inverse__]: @'first' ('arr' f)@ ≡ @'arr' ('first' f)@
+-- [__First Composition__]: @'first' (f '>>>' g)@ ≡ @'first' f '>>>' 'first' g@
+-- [__Arrow Law 5__]: @'first' f '>>>' 'arr' 'fst'@ ≡ @'arr' 'fst' '>>>' f@
+-- [__Arrow Law 6__]: @'first' f '>>>' 'arr' ('id' '***' g)@ ≡ @'arr' ('id' '***' g) '>>>' 'first' f@
+-- [__Arrow Law 7__]: @'first' ('first' f) '>>>' 'arr' assoc@ ≡ @'arr' assoc '>>>' 'first' f, where assoc ((a,b),c) = (a,(b,c))@
+arrowLaws :: forall f.
+  ( Arrow f
+  , forall x y. (Eq x, Eq y) => Eq (f x y)
+  , forall x y. (Show x, Show y) => Show (f x y)
+  ) => (forall x y. Gen x -> Gen y -> Gen (f x y)) -> Laws
+arrowLaws gen = Laws "Arrow"
+  [ ("Arr Identity", arrowLaw1 gen)
+  , ("Arr Composition", arrowLaw2 gen)
+  , ("Arr . First == First . Arr", arrowLaw3 gen)
+  , ("First Composition", arrowLaw4 gen)
+  , ("Arrow Law 5", arrowLaw5 gen)
+  , ("Arrow Law 6", arrowLaw6 gen)
+  , ("Arrow Law 7", arrowLaw7 gen)
+  ]
+
+type ArrowProp f =
+  ( Arrow f
+  , forall x y. (Eq x, Eq y) => Eq (f x y)
+  , forall x y. (Show x, Show y) => Show (f x y)
+  ) => (forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
+
+arrowLaw1 :: forall f. ArrowProp f
+arrowLaw1 _ = property $ do
+  arr Prelude.id `heq2` (id :: f Integer Integer)
+
+arrowLaw2 :: forall f. ArrowProp f
+arrowLaw2 _ = property $ do
+  f' <- forAll genQuadraticEquation
+  g' <- forAll genQuadraticEquation
+  let f = runQuadraticEquation f'
+      g = runQuadraticEquation g'
+  (arr (f >>> g) :: f Integer Integer) `heq2` (arr f >>> arr g) 
+
+arrowLaw3 :: forall f. ArrowProp f
+arrowLaw3 _ = property $ do
+  f' <- forAll genQuadraticEquation
+  let f = runQuadraticEquation f'
+  let x = first (arr f) :: f (Integer, Integer) (Integer, Integer)
+  let y = arr (first f) :: f (Integer, Integer) (Integer, Integer) 
+  x `heq2` y
+
+arrowLaw4 :: forall f. ArrowProp f
+arrowLaw4 fgen = property $ do
+  f <- forAll $ fgen genSmallInteger genSmallInteger
+  g <- forAll $ fgen genSmallInteger genSmallInteger
+  let x = first (f >>> g) :: f (Integer, Integer) (Integer, Integer)
+  let y = first f >>> first g :: f (Integer, Integer) (Integer, Integer)
+  x `heq2` y 
+
+arrowLaw5 :: forall f. ArrowProp f
+arrowLaw5 fgen = property $ do
+  f <- forAll $ fgen genSmallInteger genSmallInteger
+  let x = first f >>> arr fst :: f (Integer, Integer) Integer
+  let y = arr fst >>> f :: f (Integer, Integer) Integer
+  x `heq2` y 
+
+arrowLaw6 :: forall f. ArrowProp f
+arrowLaw6 fgen = property $ do
+  f <- forAll $ fgen genSmallInteger genSmallInteger
+  g' <- forAll genQuadraticEquation
+  let g = runQuadraticEquation g'
+  let x = ((first f) >>> (arr (Prelude.id *** g))) :: f (Integer, Integer) (Integer, Integer) 
+  let y = arr (id *** g) >>> first f :: f (Integer, Integer) (Integer, Integer) 
+  x `heq2` y
+
+arrowLaw7 :: forall f. ArrowProp f
+arrowLaw7 fgen = property $ do
+  let assoc ((a,b),c) = (a,(b,c))
+  f <- forAll $ fgen genSmallInteger genSmallInteger
+  let x = first (first f) >>> arr assoc :: f ((Integer, Integer), Integer) (Integer, (Integer, Integer))
+  let y = arr assoc >>> first f :: f ((Integer, Integer), Integer) (Integer, (Integer, Integer))
+  x `heq2` y
+
diff --git a/src/Hedgehog/Classes/Bifoldable.hs b/src/Hedgehog/Classes/Bifoldable.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Bifoldable.hs
@@ -0,0 +1,161 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+
+module Hedgehog.Classes.Bifoldable (bifoldableLaws, bifoldableFunctorLaws) where
+
+import Hedgehog
+import Hedgehog.Classes.Common
+
+import Data.Bifoldable (Bifoldable(..))
+import Data.Bifunctor (Bifunctor(..))
+import Data.Monoid (Endo(..), Sum(..), Product(..))
+
+-- | Tests the following 'Bifoldable' laws:
+--
+-- [__Identity__]: @'bifold'@ ≡ @'bifoldMap' 'id' 'id'@ 
+-- [__FoldMap__]: @'bifoldMap' f g@ ≡ @'bifoldr' ('mappend' '.' f) ('mappend' '.' g) 'mempty'@
+-- [__Foldr__]: @'bifoldr' f g z t@ ≡ @'appEndo' ('bifoldMap' ('Endo' '.' f) ('Endo' '.' g) t) z@
+bifoldableLaws :: forall f.
+  ( Bifoldable f
+  , forall x y. (Eq x, Eq y) => Eq (f x y)
+  , forall x y. (Show x, Show y) => Show (f x y)
+  ) => (forall x y. Gen x -> Gen y -> Gen (f x y)) -> Laws
+bifoldableLaws gen = Laws "Bifoldable"
+  [ ("Identity", bifoldableIdentity gen)
+  , ("FoldMap", bifoldableFoldMap gen)
+  , ("Foldr", bifoldableFoldr gen)
+  ]
+
+-- | Tests the following 'Bifoldable' / 'Bifunctor' laws:
+--
+-- [__Composition__]: @'bifoldMap' f g@ ≡ @'bifold' '.' 'bimap' f g@
+-- [__FoldMap__]: @'bifoldMap' f g '.' 'bimap' h i@ ≡ @'bifoldMap' (f '.' h) (g '.' i)@
+bifoldableFunctorLaws :: forall f.
+  ( Bifoldable f, Bifunctor f
+  , forall x y. (Eq x, Eq y) => Eq (f x y)
+  , forall x y. (Show x, Show y) => Show (f x y)
+  ) => (forall x y. Gen x -> Gen y -> Gen (f x y)) -> Laws
+bifoldableFunctorLaws gen = Laws "Bifoldable/Bifunctor"
+  [ ("Composition", bifoldableFunctorComposition gen)
+  , ("FoldMap", bifoldableFunctorFoldMap gen)
+  ]
+
+type BifoldableProp f =
+  ( Bifoldable f
+  , forall x y. (Eq x, Eq y) => Eq (f x y)
+  , forall x y. (Show x, Show y) => Show (f x y)
+  ) => (forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
+
+bifoldableIdentity :: forall f. BifoldableProp f
+bifoldableIdentity fgen = property $ do
+  x <- forAll $ fgen genSmallSum genSmallSum
+  let lhs = bifold x
+  let rhs = bifoldMap id id x
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Identity", lawContextLawBody = "bifold" `congruency` "bifoldMap id id"
+        , lawContextTcName = "Bifoldable", lawContextTcProp =
+             let showX = show x;
+             in lawWhere
+                 [ "bimap id id x" `congruency` "x, where"
+                 , "x = " ++ showX
+                 ]
+        , lawContextReduced = reduced lhs rhs 
+        } 
+  heqCtx lhs rhs ctx
+        
+bifoldableFoldMap :: forall f. BifoldableProp f
+bifoldableFoldMap fgen = property $ do
+  x <- forAll $ fgen genSmallInteger genSmallInteger
+  let f = Sum; g = Sum . (+1)
+  let lhs = (bifoldMap f g x)
+  let rhs = (bifoldr (mappend . f) (mappend . g) mempty x)
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "FoldMap", lawContextLawBody = "bifoldMap f g" `congruency` "bifoldr (mappend . f) (mappend . g) mempty"
+        , lawContextTcName = "Bifoldable", lawContextTcProp =
+             let showX = show x;
+             in lawWhere
+                 [ "bifoldMap f g x" `congruency` "bifoldr (mappend . f) (mappend . g) mempty x, where"
+                 , "f = \\x -> Sum x"
+                 , "g = \\x -> Sum (x + 1)"
+                 , "x = " ++ showX
+                 ]
+        , lawContextReduced = reduced lhs rhs 
+        } 
+  heqCtx lhs rhs ctx
+
+bifoldableFoldr :: forall f. BifoldableProp f
+bifoldableFoldr fgen = property $ do
+  x <- forAll $ fgen genSmallInteger genSmallInteger
+  f' <- forAll genLinearEquationTwo
+  g' <- forAll genLinearEquationTwo
+  let f = runLinearEquationTwo f'
+  let g = runLinearEquationTwo g'
+  let z0 = 0
+  let lhs = (bifoldr f g z0 x)
+  let rhs = (appEndo (bifoldMap (Endo . f) (Endo . g) x) z0)
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Foldr", lawContextLawBody = "bifoldr f g z t" `congruency` "appEndo (bifoldMap (Endo . f) (Endo . g) t) z"
+        , lawContextTcName = "Bifoldable", lawContextTcProp =
+            let showX = show x; showF = show f'; showG = show g'; showZ = show z0;
+            in lawWhere
+              [ "bifoldr f g z t" `congruency` "appEndo (bifoldMap (Endo . f) (Endo . g) t z, where"
+              , "f = " ++ showF
+              , "g = " ++ showG
+              , "t = " ++ showX
+              , "z = " ++ showZ
+              ]
+        , lawContextReduced = reduced lhs rhs 
+        }
+  heqCtx lhs rhs ctx 
+
+type BifoldableFunctorProp f =
+  ( Bifoldable f, Bifunctor f
+  , forall x y. (Eq x, Eq y) => Eq (f x y)
+  , forall x y. (Show x, Show y) => Show (f x y)
+  ) => (forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
+
+bifoldableFunctorComposition :: forall f. BifoldableFunctorProp f
+bifoldableFunctorComposition fgen = property $ do
+  x <- forAll $ fgen genSmallSum genSmallSum
+  let f = Product; g = Product . (+1)
+  let lhs = bifoldMap f g x
+  let rhs = bifold (bimap f g x)
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Composition", lawContextLawBody = "bifoldMap f g" `congruency` "bifold . bimap f g"
+        , lawContextTcName = "Bifoldable/Bifunctor", lawContextTcProp =
+            let showX = show x;
+            in lawWhere
+              [ "bifoldMap f g x" `congruency` "bifold . bimap f g $ x"
+              , "f = \\x -> Product x"
+              , "g = \\x -> Product (x + 1)"
+              , "x = " ++ showX
+              ]
+        , lawContextReduced = reduced lhs rhs 
+        }
+  heqCtx lhs rhs ctx 
+
+bifoldableFunctorFoldMap :: forall f. BifoldableFunctorProp f
+bifoldableFunctorFoldMap fgen = property $ do
+  x <- forAll $ fgen genSmallSum genSmallSum
+  let h (Sum s) = s * s + 3; showH = "\\(Sum s) -> s * s + 3"
+  let i (Sum s) = s + s - 7; showI = "\\(Sum s) -> s + s - 7"
+  let f = Sum; showF = "\\x -> Sum x"; g = Sum . (+1); showG = "\\x -> Sum (x + 1)"
+  let lhs = bifoldMap f g (bimap h i x)
+  let rhs = bifoldMap (f . h) (g . i) x
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "FoldMap", lawContextLawBody = "bifoldMap f g . bimap h i" `congruency` "bifoldMap (f . h) (g . i)"
+        , lawContextTcName = "Bifoldable/Bifunctor", lawContextTcProp =
+            let showX = show x;
+            in lawWhere
+              [ "bifoldMap f g . bimap h i $ x" `congruency` "bifoldMap (f . h) (g . i) $ x, where"
+              , "f = " ++ showF
+              , "g = " ++ showG
+              , "h = " ++ showH
+              , "i = " ++ showI
+              , "x = " ++ showX
+              ]
+        , lawContextReduced = reduced lhs rhs 
+        }
+  heqCtx lhs rhs ctx
+
diff --git a/src/Hedgehog/Classes/Bifunctor.hs b/src/Hedgehog/Classes/Bifunctor.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Bifunctor.hs
@@ -0,0 +1,102 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+
+module Hedgehog.Classes.Bifunctor (bifunctorLaws) where
+
+import Hedgehog
+import Hedgehog.Classes.Common
+
+import Data.Bifunctor (Bifunctor(..))
+
+-- | Tests the following 'Bifunctor' laws:
+--
+-- [__Identity__]: @'bimap' 'id' 'id'@ ≡ @'id'@
+-- [__First Identity__]: @'first' 'id'@ ≡ @'id'@
+-- [__Second Identity__]: @'second' 'id'@ ≡ @'id'@
+-- [__Composition__]: @'bimap' 'id' 'id'@ ≡ @'first' 'id' '.' 'second' 'id'@
+bifunctorLaws :: forall f.
+  ( Bifunctor f
+  , forall x y. (Eq x, Eq y) => Eq (f x y)
+  , forall x y. (Show x, Show y) => Show (f x y)
+  ) => (forall x y. Gen x -> Gen y -> Gen (f x y)) -> Laws
+bifunctorLaws gen = Laws "Bifunctor"
+  [ ("Identity", bifunctorIdentity gen)
+  , ("First Identity", bifunctorFirstIdentity gen)
+  , ("Second Identity", bifunctorSecondIdentity gen)
+  , ("Composition", bifunctorComposition gen) 
+  ]
+
+type BifunctorProp f =
+  ( Bifunctor f
+  , forall x y. (Eq x, Eq y) => Eq (f x y)
+  , forall x y. (Show x, Show y) => Show (f x y)
+  ) => (forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
+
+bifunctorIdentity :: forall f. BifunctorProp f
+bifunctorIdentity fgen = property $ do
+  x <- forAll $ fgen genSmallInteger genSmallInteger
+  let lhs = bimap id id x
+  let rhs = x
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Identity", lawContextLawBody = "bimap id id" `congruency` "id"
+        , lawContextTcName = "Bifunctor", lawContextTcProp =
+             let showX = show x;
+             in lawWhere
+                 [ "bimap id id x" `congruency` "x, where"
+                 , "x = " ++ showX
+                 ]
+        , lawContextReduced = reduced lhs rhs 
+        } 
+  heqCtx2 lhs rhs ctx 
+
+bifunctorFirstIdentity :: forall f. BifunctorProp f
+bifunctorFirstIdentity fgen = property $ do
+  x <- forAll $ fgen genSmallInteger genSmallInteger
+  let lhs = first id x
+  let rhs = x
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "First Identity", lawContextLawBody = "first id" `congruency` "id"
+        , lawContextTcName = "Bifunctor", lawContextTcProp =
+            let showX = show x;
+            in lawWhere
+              [ "first id x" `congruency` "x, where"
+              , "x = " ++ showX
+              ]
+        , lawContextReduced = reduced lhs rhs 
+        }
+  heqCtx2 lhs rhs ctx
+
+bifunctorSecondIdentity :: forall f. BifunctorProp f
+bifunctorSecondIdentity fgen = property $ do
+  x <- forAll $ fgen genSmallInteger genSmallInteger
+  let lhs = second id x
+  let rhs = x
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Second Identity", lawContextLawBody = "second id" `congruency` "id"
+        , lawContextTcName = "Bifunctor", lawContextTcProp =
+            let showX = show x;
+            in lawWhere
+              [ "second id x" `congruency` "x, where"
+              , "x = " ++ showX
+              ]
+        , lawContextReduced = reduced lhs rhs 
+        }
+  heqCtx2 lhs rhs ctx
+
+bifunctorComposition :: forall f. BifunctorProp f
+bifunctorComposition fgen = property $ do
+  z <- forAll $ fgen genSmallInteger genSmallInteger
+  let lhs = bimap id id z
+  let rhs = (first id . second id) z
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Composition", lawContextLawBody = "bimap id id" `congruency` "first id . second id"
+        , lawContextTcName = "Bifunctor", lawContextTcProp =
+            let showX = show z;
+            in lawWhere
+              [ "bimap id id x" `congruency` "first id . second id $ x, where"
+              , "x = " ++ showX
+              ]
+        , lawContextReduced = reduced lhs rhs 
+        }       
+  heqCtx2 lhs rhs ctx
diff --git a/src/Hedgehog/Classes/Bitraversable.hs b/src/Hedgehog/Classes/Bitraversable.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Bitraversable.hs
@@ -0,0 +1,93 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+
+module Hedgehog.Classes.Bitraversable (bitraversableLaws) where
+
+import Hedgehog
+import Hedgehog.Classes.Common
+
+import Data.Bitraversable (Bitraversable(..))
+import Data.Functor.Compose (Compose(..))
+import Data.Functor.Identity (Identity(..))
+
+import qualified Data.Set as S
+import qualified Control.Monad.Trans.Writer.Lazy as WL
+
+-- | Tests the following 'Bitraversable' laws:
+--
+-- [__Naturality__]: @'bitraverse' (t '.' f) (t '.' g)@ ≡ @t '.' 'bitraverse' f g, for every applicative transformation t@
+-- [__Identity__]: @'bitraverse' 'Identity' 'Identity'@ ≡ @'Identity'@
+-- [__Composition__]: @'Compose' '.' 'fmap' ('bitraverse' g1 g2) '.' 'bitraverse' f1 f2@ ≡ @'bitraverse' ('Compose' '.' 'fmap' g1 '.' f1) ('Compose' '.' 'fmap' g2 '.' f2)@
+bitraversableLaws :: forall f.
+  ( Bitraversable f
+  , forall x y. (Eq x, Eq y) => Eq (f x y)
+  , forall x y. (Show x, Show y) => Show (f x y)
+  ) => (forall x y. Gen x -> Gen y -> Gen (f x y)) -> Laws
+bitraversableLaws gen = Laws "Bitraversable"
+  [ ("Naturality", bitraversableNaturality gen)
+  , ("Identity", bitraversableIdentity gen)
+  , ("Composition", bitraversableComposition gen) 
+  ]
+
+type BitraversableProp f =
+  ( Bitraversable f
+  , forall x y. (Eq x, Eq y) => Eq (f x y)
+  , forall x y. (Show x, Show y) => Show (f x y)
+  ) => (forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
+
+bitraversableNaturality :: forall f. BitraversableProp f
+bitraversableNaturality fgen = property $ do
+  x <- forAll $ fgen genSmallInteger genSmallInteger
+  let t = apTrans; f = func4; g = func4
+  let lhs = bitraverse (t . f) (t . g) x
+  let rhs = t (bitraverse f g x)
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Naturality", lawContextLawBody = "bitraverse (t . f) (t . g)" `congruency` "t . bitraverse f g, for every applicative transformation t"
+        , lawContextTcName = "Bitraversable", lawContextTcProp =
+            let showX = show x;
+            in lawWhere
+                 [ "bitraverse (t . f) (t . g) $ x" `congruency` "t . bitraverse f g $ x, for every applicative transformation t, where"
+                 , "x = " ++ showX
+                 ]
+        , lawContextReduced = reduced lhs rhs 
+        }
+  heqCtx1 lhs rhs ctx  
+
+bitraversableIdentity :: forall f. BitraversableProp f
+bitraversableIdentity fgen = property $ do
+  x <- forAll $ fgen genSmallInteger genSmallInteger
+  let lhs = bitraverse Identity Identity x
+  let rhs = Identity x
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Identity", lawContextLawBody = "bitraverse Identity Identity" `congruency` "Identity"
+        , lawContextTcName = "Bitraversable", lawContextTcProp =
+            let showX = show x;
+            in lawWhere
+                 [ "bitraverse Identity Identity x" `congruency` "Identity x, where"
+                 , "x = " ++ showX
+                 ]
+        , lawContextReduced = reduced lhs rhs 
+        }
+  heqCtx1 lhs rhs ctx  
+  
+bitraversableComposition :: forall f. BitraversableProp f
+bitraversableComposition fgen = property $ do
+  x <- forAll $ fgen genSmallInteger genSmallInteger
+  let f1 = func6; f2 = func5; g1 = func4; g2 = func4
+  let lhs :: Compose Triple (Compose Triple (WL.Writer (S.Set Integer))) (f Integer Integer)
+      lhs = Compose . fmap (bitraverse g1 g2) . bitraverse f1 f2 $ x
+      
+  let rhs :: Compose Triple (Compose Triple (WL.Writer (S.Set Integer))) (f Integer Integer)
+      rhs = bitraverse (Compose . fmap g1 . f1) (Compose . fmap g2 . f2) x
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Composition", lawContextLawBody = "Compose . fmap (bitraverse g1 g2) . bitraverse f1 f2" `congruency` "bitraverse (Compose . fmap g1 . f1) (Compose . fmap g2 . f2)"
+        , lawContextTcName = "Bitraversable", lawContextTcProp =
+            let showX = show x;  
+            in lawWhere
+                 [ "Compose . fmap (bitraverse g1 g2) . bitraverse f1 f2 $ x" `congruency` "bitraverse (Compose . fmap g1 . f1) (Compose . fmap g2 . f2) $ x, where"
+                 , "x = " ++ showX
+                 ]
+        , lawContextReduced = reduced lhs rhs 
+        }
+  heqCtx1 lhs rhs ctx
diff --git a/src/Hedgehog/Classes/Bits.hs b/src/Hedgehog/Classes/Bits.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Bits.hs
@@ -0,0 +1,281 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Hedgehog.Classes.Bits (bitsLaws) where
+
+import Data.Bits
+import Hedgehog
+import Hedgehog.Classes.Common
+
+import qualified Hedgehog.Gen as Gen
+import qualified Hedgehog.Range as Range
+
+-- | Tests the following 'Bits' laws:
+--
+-- [__Conjunction Idempotence__]: @n '.&.' n@ ≡ @n@
+-- [__Disjunction Idempotence__]: @n '.|.' n@ ≡ @n@
+-- [__Double Complement__]: @'complement' '.' 'complement'@ ≡ @id@
+-- [__Set Bit__]: @'setBit' n i ≡ n '.|.' 'bit' i@
+-- [__Clear Bit__]: @'clearBit' n i@ ≡ @n '.&.' 'complement' ('bit' i)@
+-- [__Complement Bit__]: @'complement' n i@ ≡ @'xor' n ('bit' i)@
+-- [__Clear Zero__]: @'clearBit' 'zeroBits' i@ ≡ @'zeroBits'@
+-- [__Set Zero__]: @'setBit' 'zeroBits' i@ ≡ @'zeroBits'@
+-- [__Test Zero__]: @'testBit' 'zeroBits' i@ ≡ @'False'@
+-- [__Pop Zero__]: @'popCount' 'zeroBits'@ ≡ @0@
+-- [__Count Leading Zeros of Zero__]: @'countLeadingZeros' 'zeroBits'@ ≡ @'finiteBitSize' ('undefined' :: a)@
+-- [__Count Trailing Zeros of Zero__]: @'countTrailingZeros' 'zeroBits'@ ≡ @'finiteBitSize' ('undefined' :: a)@
+bitsLaws :: (FiniteBits a, Show a) => Gen a -> Laws
+bitsLaws gen = Laws "Bits"
+  [ ("Conjunction Idempotence", bitsConjunctionIdempotence gen)
+  , ("Disjunction Idempotence", bitsDisjunctionIdempotence gen)
+  , ("Double Complement", bitsDoubleComplement gen) 
+  , ("Set Bit", bitsSetBit gen) 
+  , ("Clear Bit", bitsClearBit gen)
+  , ("Complement Bit", bitsComplementBit gen)
+  , ("Clear Zero", bitsClearZero gen)
+  , ("Set Zero", bitsSetZero gen)
+  , ("Test Zero", bitsTestZero gen)
+  , ("Pop Zero", bitsPopZero gen)
+  , ("Count Leading Zeros of Zero", bitsCountLeadingZeros gen)
+  , ("Count Trailing Zeros of Zero", bitsCountTrailingZeros gen)
+  ]
+
+newtype BitIndex a = BitIndex Int
+  deriving (Show)
+
+genBitIndex :: forall a. FiniteBits a => Gen (BitIndex a)
+genBitIndex = let n = finiteBitSize (undefined :: a) in if n > 0
+  then fmap BitIndex (Gen.integral $ Range.linear 0 (n - 1))
+  else pure (BitIndex 0)
+
+bitsConjunctionIdempotence :: forall a. (Bits a, Show a) => Gen a -> Property
+bitsConjunctionIdempotence gen = property $ do
+  n <- forAll gen
+  let lhs = n .&. n; rhs = n; 
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Conjunction Idempotence"
+        , lawContextLawBody = "n .&. n" `congruency` "n"
+        , lawContextTcName = "Bits"
+        , lawContextTcProp =
+            let showN = show n;
+            in lawWhere [ "n .&. n" `congruency` "n, where", "n = " ++ showN ]
+        , lawContextReduced = reduced lhs rhs 
+        }
+  heqCtx lhs rhs ctx
+
+bitsDisjunctionIdempotence :: forall a. (Bits a, Show a) => Gen a -> Property
+bitsDisjunctionIdempotence gen = property $ do
+  n <- forAll gen
+  let lhs = n .|. n; rhs = n; 
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Disjunction Idempotence"
+        , lawContextLawBody = "n .|. n" `congruency` "n"
+        , lawContextTcName = "Bits"
+        , lawContextTcProp =
+            let showN = show n
+            in lawWhere [ "n .|. n" `congruency` "n, where", "n = " ++ showN ]
+        , lawContextReduced = reduced lhs rhs 
+        }
+  heqCtx lhs rhs ctx
+
+bitsDoubleComplement :: forall a. (Bits a, Show a) => Gen a -> Property
+bitsDoubleComplement gen = property $ do
+  n <- forAll gen
+  let lhs = complement (complement n); rhs = n;
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Double Complement"
+        , lawContextLawBody = "complement . complement" `congruency` "id"
+        , lawContextTcName = "Bits"
+        , lawContextTcProp =
+            let showN = show n
+            in lawWhere [ "complement . complement $ n" `congruency` "id n, where", "n = " ++ showN ]
+        , lawContextReduced = reduced lhs rhs 
+        }
+  
+  heqCtx lhs rhs ctx
+
+bitsSetBit :: forall a. (FiniteBits a, Show a) => Gen a -> Property
+bitsSetBit gen = property $ do
+  n <- forAll gen
+  (BitIndex i) :: BitIndex a <- forAll genBitIndex
+  let lhs = setBit n i; rhs = n .|. bit i;
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Set Bit"
+        , lawContextLawBody = "setBit n i" `congruency` "n .|. bit i"
+        , lawContextTcName = "Bits"
+        , lawContextTcProp =
+            let showN = show n
+                showI = show i
+            in lawWhere
+                 [ "setBit n i" `congruency` "n .|. bit i, where"
+                 , "n = " ++ showN
+                 , "i = " ++ showI
+                 ]
+        , lawContextReduced = reduced lhs rhs 
+        } 
+  heqCtx lhs rhs ctx
+
+bitsClearBit :: forall a. (FiniteBits a, Show a) => Gen a -> Property
+bitsClearBit gen = property $ do
+  n <- forAll gen
+  (BitIndex i) :: BitIndex a <- forAll genBitIndex
+  let lhs = clearBit n i; rhs = n .&. complement (bit i)
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Clear Bit"
+        , lawContextLawBody = "clearBit n i" `congruency` "n .&. complement (bit i)"
+        , lawContextTcName = "Bits"
+        , lawContextTcProp =
+            let showN = show n
+                showI = show i
+            in lawWhere
+                 [ "clearBit n i" `congruency` "n .&. complement (bit i), where"
+                 , "n = " ++ showN
+                 , "i = " ++ showI
+                 ]
+        , lawContextReduced = reduced lhs rhs 
+        }
+  heqCtx lhs rhs ctx
+
+bitsComplementBit :: forall a. (FiniteBits a, Show a) => Gen a -> Property
+bitsComplementBit gen = property $ do
+  n <- forAll gen
+  (BitIndex i) :: BitIndex a <- forAll genBitIndex
+  let lhs = complementBit n i; rhs = xor n (bit i);
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Complement Bit"
+        , lawContextLawBody = "complement n i" `congruency` "xor n (bit i)"
+        , lawContextTcName = "Bits"
+        , lawContextTcProp =
+            let showN = show n
+                showI = show i
+            in lawWhere
+                 [ "complement n i" `congruency` "xor n (bit i), where"
+                 , "n = " ++ showN
+                 , "i = " ++ showI
+                 ]
+        , lawContextReduced = reduced lhs rhs 
+        } 
+  heqCtx lhs rhs ctx
+
+bitsClearZero :: forall a. (FiniteBits a, Show a) => Gen a -> Property
+bitsClearZero _ = property $ do
+  (BitIndex i) :: BitIndex a <- forAll genBitIndex
+  let z = zeroBits :: a
+  let lhs = clearBit z i; rhs = z
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Clear Zero"
+        , lawContextLawBody = "clearBit zeroBits i" `congruency` "zeroBits"
+        , lawContextTcName = "Bits"
+        , lawContextTcProp =
+            let showZ = show z
+                showI = show i
+            in lawWhere
+                 [ "clearBit zeroBits i" `congruency` "zeroBits, where"
+                 , "zerBits = " ++ showZ
+                 , "i = " ++ showI
+                 ]
+        , lawContextReduced = reduced lhs rhs 
+        }
+  heqCtx lhs rhs ctx
+
+bitsSetZero :: forall a. (FiniteBits a, Show a) => Gen a -> Property
+bitsSetZero _ = property $ do
+  (BitIndex i) :: BitIndex a <- forAll genBitIndex
+  let z = zeroBits :: a
+  let lhs = setBit z i; rhs = bit i;
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Set Zero"
+        , lawContextLawBody = "setBit zeroBits i" `congruency` "zeroBits"
+        , lawContextTcName = "Bits"
+        , lawContextTcProp =
+            let showZ = show z
+                showI = show i
+            in lawWhere
+              [ "setBit zeroBits i" `congruency` "zeroBits, where"
+              , "zeroBits = " ++ showZ
+              , "i = " ++ showI
+              ]
+        , lawContextReduced = reduced lhs rhs 
+        }
+  heqCtx lhs rhs ctx
+
+bitsTestZero :: forall a. (FiniteBits a, Show a) => Gen a -> Property
+bitsTestZero _ = property $ do
+  (BitIndex i) :: BitIndex a <- forAll genBitIndex
+  let z = zeroBits :: a
+  let lhs = testBit z i; rhs = False;
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Test Zero"
+        , lawContextLawBody = "testBit zeroBits i" `congruency` "False"
+        , lawContextTcName = "Bits"
+        , lawContextTcProp =
+            let showZ = show z
+                showI = show i
+            in lawWhere
+              [ "testBit zeroBits i" `congruency` "False, where"
+              , "zeroBits = " ++ showZ
+              , "i = " ++ showI
+              ]
+        , lawContextReduced = reduced lhs rhs 
+        }
+  heqCtx lhs rhs ctx  
+
+bitsPopZero :: forall a. (FiniteBits a, Show a) => Gen a -> Property
+bitsPopZero _ = property $ do
+  let z = zeroBits :: a
+  let lhs = popCount z; rhs = 0;
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Pop Zero"
+        , lawContextLawBody = "popCount zeroBits" `congruency` "0"
+        , lawContextTcName = "Bits"
+        , lawContextTcProp =
+            let showZ = show z
+            in lawWhere
+              [ "popCount zeroBits" `congruency` "0, where"
+              , "zeroBits = " ++ showZ
+              ]
+        , lawContextReduced = reduced lhs rhs 
+        } 
+  heqCtx lhs rhs ctx
+
+bitsCountLeadingZeros :: forall a. (FiniteBits a, Show a) => Gen a -> Property
+bitsCountLeadingZeros _ = property $ do
+  let z = zeroBits :: a
+  let f = finiteBitSize (undefined :: a)
+  let lhs = countLeadingZeros z; rhs = f;
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Count Leading Zeros of Zero"
+        , lawContextLawBody = "countLeadingZeros zeroBits" `congruency` "finiteBitSize (undefined :: a)"
+        , lawContextTcName = "Bits"
+        , lawContextTcProp =
+            let showZ = show z
+                showF = show f
+            in lawWhere
+              [ "countLeadingZeros zeroBits" `congruency` "finiteBitSize (undefined :: a), where"
+              , "zeroBits = " ++ showZ
+              , "finiteBitSize = " ++ showF
+              ]
+        , lawContextReduced = reduced lhs rhs 
+        } 
+  heqCtx lhs rhs ctx
+
+bitsCountTrailingZeros :: forall a. (FiniteBits a, Show a) => Gen a -> Property
+bitsCountTrailingZeros _ = property $ do
+  let z = zeroBits :: a
+  let f = finiteBitSize (undefined :: a)
+  let lhs = countTrailingZeros z; rhs = f;
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Count Trailing Zeros of Zero"
+        , lawContextLawBody = "countTrailingZeros zeroBits" `congruency` "finiteBitSize (undefined :: a)"
+        , lawContextTcName = "Bits"
+        , lawContextTcProp =
+            let showZ = show z
+                showF = show f
+            in lawWhere
+              [ "countTrailingZeros zeroBits" `congruency` "finiteBitSize (undefined :: a), where"
+              , "zeroBits = " ++ showZ
+              , "finiteBitSize = " ++ showF
+              ]           
+        , lawContextReduced = reduced lhs rhs 
+        }
+  heqCtx lhs rhs ctx
+
diff --git a/src/Hedgehog/Classes/Category.hs b/src/Hedgehog/Classes/Category.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Category.hs
@@ -0,0 +1,78 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+
+module Hedgehog.Classes.Category (categoryLaws, commutativeCategoryLaws) where
+
+import Hedgehog
+import Hedgehog.Classes.Common
+
+import Control.Category(Category(..))
+import Prelude hiding (id, (.))
+
+-- | Tests the following 'Category' laws:
+--
+-- [__Left Identity__]: @'id' '.' f@ ≡ @f@
+-- [__Right Identity__]: @f '.' 'id'@ ≡ @f@
+-- [__Associativity__]: @f '.' (g '.' h)@ ≡ @(f '.' g) '.' h@
+categoryLaws :: forall f.
+  ( Category f
+  , forall x y. (Eq x, Eq y) => Eq (f x y)
+  , forall x y. (Show x, Show y) => Show (f x y)
+  ) => (forall x y. Gen x -> Gen y -> Gen (f x y)) -> Laws
+categoryLaws gen = Laws "Category"
+  [ ("Left Identity", categoryLeftIdentity gen)
+  , ("Right Identity", categoryRightIdentity gen)
+  , ("Associativity", categoryAssociativity gen)
+  ]
+
+-- | Tests the following 'Category' laws:
+--
+-- [__Commutativity__]: @f '.' g@ ≡ @g '.' f@
+commutativeCategoryLaws :: forall f.
+  ( Category f
+  , forall x y. (Eq x, Eq y) => Eq (f x y)
+  , forall x y. (Show x, Show y) => Show (f x y)
+  ) => (forall x y. Gen x -> Gen y -> Gen (f x y)) -> Laws
+commutativeCategoryLaws gen = Laws "Commutative Category"
+  [ ("Commutativity", categoryCommutativity gen)
+  ]
+
+categoryRightIdentity :: forall f.
+  ( Category f
+  , forall x y. (Eq x, Eq y) => Eq (f x y)
+  , forall x y. (Show x, Show y) => Show (f x y)
+  ) => (forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
+categoryRightIdentity fgen = property $ do
+  x <- forAll $ fgen genSmallInteger genSmallInteger
+  (x . id) `heq2` x
+
+categoryLeftIdentity :: forall f.
+  ( Category f
+  , forall x y. (Eq x, Eq y) => Eq (f x y)
+  , forall x y. (Show x, Show y) => Show (f x y)
+  ) => (forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
+categoryLeftIdentity fgen = property $ do
+  x <- forAll $ fgen genSmallInteger genSmallInteger
+  (id . x) `heq2` x
+
+categoryAssociativity :: forall f.
+  ( Category f
+  , forall x y. (Eq x, Eq y) => Eq (f x y)
+  , forall x y. (Show x, Show y) => Show (f x y)
+  ) => (forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
+categoryAssociativity fgen = property $ do
+  f <- forAll $ fgen genSmallInteger genSmallInteger
+  g <- forAll $ fgen genSmallInteger genSmallInteger 
+  h <- forAll $ fgen genSmallInteger genSmallInteger 
+  (f . (g . h)) `heq2` ((f . g) . h)
+
+categoryCommutativity :: forall f.
+  ( Category f
+  , forall x y. (Eq x, Eq y) => Eq (f x y)
+  , forall x y. (Show x, Show y) => Show (f x y)
+  ) => (forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
+categoryCommutativity fgen = property $ do
+  f <- forAll $ fgen genSmallInteger genSmallInteger
+  g <- forAll $ fgen genSmallInteger genSmallInteger
+  (f . g) `heq2` (g . f)
diff --git a/src/Hedgehog/Classes/Common.hs b/src/Hedgehog/Classes/Common.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Common.hs
@@ -0,0 +1,13 @@
+module Hedgehog.Classes.Common
+  ( module Common 
+  ) where
+
+import Hedgehog.Classes.Common.ApTrans  as Common
+import Hedgehog.Classes.Common.Bottom   as Common
+import Hedgehog.Classes.Common.Compat   as Common
+import Hedgehog.Classes.Common.Equation as Common
+import Hedgehog.Classes.Common.Func     as Common
+import Hedgehog.Classes.Common.Gen      as Common
+import Hedgehog.Classes.Common.IO       as Common
+import Hedgehog.Classes.Common.Laws     as Common
+import Hedgehog.Classes.Common.Property as Common
diff --git a/src/Hedgehog/Classes/Common/ApTrans.hs b/src/Hedgehog/Classes/Common/ApTrans.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Common/ApTrans.hs
@@ -0,0 +1,25 @@
+module Hedgehog.Classes.Common.ApTrans
+  ( apTrans
+  , toSpecialApplicative
+  ) where
+
+import Data.Tuple (swap)
+import Data.Functor.Compose
+import qualified Data.Set as S
+import qualified Control.Monad.Trans.Writer.Lazy as WL
+
+import Hedgehog.Classes.Common.Func
+
+-- Reverse the list and accumulate the writers. We
+-- cannot use Sum or Product or else it won't actually
+-- be a valid applicative transformation.
+apTrans ::
+     Compose Triple (WL.Writer (S.Set Integer)) a
+  -> Compose (WL.Writer (S.Set Integer)) Triple a
+apTrans (Compose xs) = Compose (sequenceA (reverseTriple xs))
+
+toSpecialApplicative ::
+     Compose Triple ((,) (S.Set Integer)) Integer
+  -> Compose Triple (WL.Writer (S.Set Integer)) Integer
+toSpecialApplicative (Compose (Triple a b c)) =
+  Compose (Triple (WL.writer (swap a)) (WL.writer (swap b)) (WL.writer (swap c)))
diff --git a/src/Hedgehog/Classes/Common/Bottom.hs b/src/Hedgehog/Classes/Common/Bottom.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Common/Bottom.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE LambdaCase #-}
+
+module Hedgehog.Classes.Common.Bottom
+  ( Bottom(..), genBottom
+  ) where
+
+import Hedgehog
+import qualified Hedgehog.Gen as Gen
+ 
+data Bottom a = BottomUndefined | BottomValue a
+  deriving (Eq)
+
+instance Show a => Show (Bottom a) where
+  show = \case
+    BottomUndefined -> "undefined"
+    BottomValue a   -> show a
+
+genBottom :: Gen a -> Gen (Bottom a)
+genBottom = fmap maybeToBottom . Gen.maybe
+
+maybeToBottom :: Maybe a -> Bottom a
+maybeToBottom = \case { Nothing -> BottomUndefined; Just a -> BottomValue a }
diff --git a/src/Hedgehog/Classes/Common/Compat.hs b/src/Hedgehog/Classes/Common/Compat.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Common/Compat.hs
@@ -0,0 +1,79 @@
+{-# LANGUAGE CPP #-}
+
+#if HAVE_QUANTIFIED_CONSTRAINTS
+{-# LANGUAGE QuantifiedConstraints #-}
+#endif
+
+module Hedgehog.Classes.Common.Compat
+  ( readMaybe
+  , eq 
+  , eq1
+  , eq2
+
+  , show1
+  , show2
+
+  , neq
+  , neq1
+  , neq2
+  ) where
+
+#if HAVE_QUANTIFIED_CONSTRAINTS == 0
+import qualified Data.Functor.Classes as C
+#endif
+
+import Text.Read (readMaybe)
+
+eq :: Eq a => a -> a -> Bool
+eq = (==)
+
+neq :: Eq a => a -> a -> Bool
+neq = (/=)
+
+#if HAVE_QUANTIFIED_CONSTRAINTS
+eq1 :: (Eq a, forall x. Eq x => Eq (f x)) => f a -> f a -> Bool
+eq1 = (==)
+#else
+eq1 :: (C.Eq1 f, Eq a) => f a -> f a -> Bool
+eq1 = C.eq1
+#endif
+
+#if HAVE_QUANTIFIED_CONSTRAINTS
+neq1 :: (Eq a, forall x. Eq x => Eq (f x)) => f a -> f a -> Bool
+neq1 = (/=)
+#else
+neq1 :: (C.Eq1 f, Eq a) => f a -> f a -> Bool
+neq1 x y = not $ C.eq1 x y 
+#endif
+
+#if HAVE_QUANTIFIED_CONSTRAINTS
+eq2 :: (Eq a, Eq b, forall x y. (Eq x, Eq y) => Eq (f x y)) => f a b -> f a b -> Bool
+eq2 = (==)
+#else
+eq2 :: (C.Eq2 f, Eq a, Eq b) => f a b -> f a b -> Bool
+eq2 = C.eq2
+#endif
+
+#if HAVE_QUANTIFIED_CONSTRAINTS
+neq2 :: (Eq a, Eq b, forall x y. (Eq x, Eq y) => Eq (f x y)) => f a b -> f a b -> Bool
+neq2 = (/=)
+#else
+neq2 :: (C.Eq2 f, Eq a, Eq b) => f a b -> f a b -> Bool
+neq2 x y = not $ C.eq2 x y
+#endif
+
+#if HAVE_QUANTIFIED_CONSTRAINTS
+show1 :: (Show a, forall x. (Show x) => Show (f x)) => f a -> String
+show1 = Prelude.show
+#else
+show1 :: (C.Show1 f, Show a) => f a -> String
+show1 x = C.showsPrec1 0 x ""
+#endif
+
+#if HAVE_QUANTIFIED_CONSTRAINTS
+show2 :: (Show a, Show b, forall x y. (Show x, Show y) => Show (f x y)) => f a b -> String
+show2 = Prelude.show
+#else
+show2 :: (C.Show2 f, Show a, Show b) => f a b -> String
+show2 x = C.showsPrec2 0 x ""
+#endif
diff --git a/src/Hedgehog/Classes/Common/Equation.hs b/src/Hedgehog/Classes/Common/Equation.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Common/Equation.hs
@@ -0,0 +1,115 @@
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Hedgehog.Classes.Common.Equation
+  ( LinearEquation(..), runLinearEquation, genLinearEquation
+  , LinearEquationTwo(..), runLinearEquationTwo, genLinearEquationTwo
+  , LinearEquationM(..), runLinearEquationM, genLinearEquationM
+  , QuadraticEquation(..), runQuadraticEquation, genQuadraticEquation
+  , CubicEquation(..), runCubicEquation, genCubicEquation
+
+  ) where
+
+import Hedgehog
+import Hedgehog.Classes.Common.Gen
+import qualified Hedgehog.Gen as Gen
+import qualified Hedgehog.Range as Range
+import qualified Data.List as List
+
+import Data.Monoid (Endo(..))
+
+data QuadraticEquation = QuadraticEquation
+  { _quadraticEquationQuadratic :: Integer
+  , _quadraticEquationLinear :: Integer
+  , _quadraticEquationConstant :: Integer
+  }
+  deriving (Eq)
+
+-- This show instance does not actually provide a way
+-- to create an equation. Instead, it makes it look
+-- like a lambda.
+instance Show QuadraticEquation where
+  show (QuadraticEquation a b c) = "\\x -> " ++ show a ++ " * x ^ 2 + " ++ show b ++ " * x + " ++ show c
+
+genQuadraticEquation :: Gen QuadraticEquation
+genQuadraticEquation = do
+  a <- Gen.integral (Range.linear 0 15)
+  b <- Gen.integral (Range.linear 0 15)
+  c <- Gen.integral (Range.linear 0 15)
+  pure (QuadraticEquation a b c)
+
+runQuadraticEquation :: QuadraticEquation -> Integer -> Integer
+runQuadraticEquation (QuadraticEquation a b c) x = a * x ^ (2 :: Integer) + b * x + c
+
+data LinearEquation = LinearEquation
+  { _linearEquationLinear :: Integer
+  , _linearEquationConstant :: Integer
+  }
+  deriving (Eq)
+
+instance Show LinearEquation where
+  showsPrec _ (LinearEquation a b) = shows a . showString " * x + " . shows b
+  showList xs = appEndo
+    $ mconcat
+    $  [Endo (showChar '[')]
+    ++ List.intersperse (Endo (showChar ',')) (map (Endo . showsPrec 0) xs)
+    ++ [Endo (showChar ']')]
+
+runLinearEquation :: LinearEquation -> Integer -> Integer
+runLinearEquation (LinearEquation a b) x = a * x + b
+
+genLinearEquation :: Gen LinearEquation
+genLinearEquation = LinearEquation <$> genSmallInteger <*> genSmallInteger
+
+data LinearEquationM m = LinearEquationM (m LinearEquation) (m LinearEquation)
+
+deriving instance (forall x. Eq x => Eq (m x)) => Eq (LinearEquationM m)
+
+instance (forall x. Show x => Show (m x)) => Show (LinearEquationM m) where
+  show (LinearEquationM a b) = (\f -> f "")
+    $ showString "\\x -> if odd x then "
+    . showsPrec 0 a
+    . showString " else "
+    . showsPrec 0 b
+
+runLinearEquationM :: Functor m => LinearEquationM m -> Integer -> m Integer
+runLinearEquationM (LinearEquationM e1 e2) i = if odd i
+  then fmap (flip runLinearEquation i) e1
+  else fmap (flip runLinearEquation i) e2
+
+genLinearEquationM :: Applicative m => Gen (LinearEquationM m)
+genLinearEquationM = LinearEquationM <$> (pure <$> genLinearEquation) <*> (pure <$> genLinearEquation)
+
+data LinearEquationTwo = LinearEquationTwo
+  { _linearEquationTwoX :: Integer
+  , _linearEquationTwoY :: Integer
+  , _linearEquationTwoConstant :: Integer
+  }
+
+instance Show LinearEquationTwo where
+  show (LinearEquationTwo x y c) = "\\x y -> " ++ show x ++ " * x + " ++ show y ++ " * y + " ++ show c
+
+genLinearEquationTwo :: Gen LinearEquationTwo
+genLinearEquationTwo = LinearEquationTwo <$> absGenInteger <*> absGenInteger <*> absGenInteger
+  where
+    absGenInteger = abs <$> genSmallInteger
+
+runLinearEquationTwo :: LinearEquationTwo -> Integer -> Integer -> Integer
+runLinearEquationTwo (LinearEquationTwo a b c) x y = a * x + b * y + c
+
+data CubicEquation = CubicEquation
+  { _cubicEquationCubic :: Integer
+  , _cubicEquationQuadratic :: Integer
+  , _cubicEquationLinear :: Integer
+  , _cubicEquationConstant :: Integer
+  }
+
+instance Show CubicEquation where
+  show (CubicEquation x y z c) = "\\x -> " ++ show x ++ " * x ^ 3 + " ++ show y ++ " * x ^ 2 + " ++ show z ++ " * x + " ++ show c
+
+genCubicEquation :: Gen CubicEquation
+genCubicEquation = CubicEquation <$> genSmallInteger <*> genSmallInteger <*> genSmallInteger <*> genSmallInteger
+
+runCubicEquation :: CubicEquation -> Integer -> Integer -> Integer -> Integer
+runCubicEquation (CubicEquation a b c d) x y z = a * x + b * y + c * z + d
diff --git a/src/Hedgehog/Classes/Common/Func.hs b/src/Hedgehog/Classes/Common/Func.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Common/Func.hs
@@ -0,0 +1,80 @@
+module Hedgehog.Classes.Common.Func
+  ( func1
+  , func2
+  , func3
+  , func4
+  , func5
+  , func6
+
+  , Triple(..), reverseTriple, genTriple
+  ) where
+
+import Hedgehog
+import Data.Functor.Classes (Eq1(..), Show1(..))
+import Data.Functor.Compose
+import qualified Data.Set as S
+import qualified Control.Monad.Trans.Writer.Lazy as WL
+import Data.Semigroup
+
+func1 :: Integer -> (Integer, Integer)
+func1 i = (div (i + 5) 3, i * i - 2 * i + 1)
+
+func2 :: (Integer, Integer) -> (Bool, Either Ordering Integer)
+func2 (a,b) = (odd a, if even a then Left (compare a b) else Right (b + 2))
+
+func3 :: Integer -> Sum Integer
+func3 i = Sum (3 * i * i - 7 * i + 4)
+
+func4 :: Integer -> Compose Triple (WL.Writer (S.Set Integer)) Integer
+func4 i = Compose $ Triple
+  (WL.writer (i * i, S.singleton (i * 7 + 5)))
+  (WL.writer (i + 2, S.singleton (i * i + 3)))
+  (WL.writer (i * 7, S.singleton 4))
+
+func5 :: Integer -> Triple Integer
+func5 i = Triple (i + 2) (i * 3) (i * i)
+
+func6 :: Integer -> Triple Integer
+func6 i = Triple (i * i * i) (4 * i - 7) (i * i * i)
+
+reverseTriple :: Triple a -> Triple a
+reverseTriple (Triple a b c) = Triple c b a
+
+data Triple a = Triple a a a
+  deriving (Show, Eq)
+
+instance Functor Triple where
+  fmap f (Triple a b c) = Triple (f a) (f b) (f c)
+
+instance Applicative Triple where
+  pure a = Triple a a a
+  Triple f g h <*> Triple a b c = Triple (f a) (g b) (h c)
+
+instance Foldable Triple where
+  foldMap f (Triple a b c) = f a <> f b <> f c
+
+instance Traversable Triple where
+  traverse f (Triple a b c) = Triple <$> f a <*> f b <*> f c
+
+tripleLiftEq :: (a -> b -> Bool) -> Triple a -> Triple b -> Bool
+tripleLiftEq p (Triple a1 b1 c1) (Triple a2 b2 c2) =
+  p a1 a2 && p b1 b2 && p c1 c2
+
+tripleLiftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Triple a -> ShowS
+tripleLiftShowsPrec elemShowsPrec _ p (Triple a b c) = showParen (p > 10)
+  $ showString "Triple "
+  . elemShowsPrec 11 a
+  . showString " "
+  . elemShowsPrec 11 b
+  . showString " "
+  . elemShowsPrec 11 c
+
+instance Eq1 Triple where
+  liftEq = tripleLiftEq
+
+instance Show1 Triple where
+  liftShowsPrec = tripleLiftShowsPrec
+
+genTriple :: Gen a -> Gen (Triple a)
+genTriple gen = Triple <$> gen <*> gen <*> gen
+  
diff --git a/src/Hedgehog/Classes/Common/Gen.hs b/src/Hedgehog/Classes/Common/Gen.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Common/Gen.hs
@@ -0,0 +1,76 @@
+{-# LANGUAGE RankNTypes #-}
+
+module Hedgehog.Classes.Common.Gen
+  ( genSmallList
+  , genSmallNonEmptyList
+  , genShowReadPrecedence
+  , genSmallString
+  , genSmallInteger
+  , genSmallSum
+  , genCompose
+  , genSetInteger
+
+  -- * Used for 'Hedgehog.Classes.ixLaws' 
+  , genTuple
+  , genTuple3
+  , genInRange
+  , genValidRange
+  ) where
+
+import Data.Ix (Ix(..))
+import Hedgehog
+import Data.Functor.Compose
+import qualified Data.Set as S
+import Data.Semigroup
+import qualified Hedgehog.Gen as Gen
+import qualified Hedgehog.Range as Range
+
+genSmallSum :: Gen (Sum Integer)
+genSmallSum = fmap Sum genSmallInteger
+
+genSmallInteger :: Gen Integer
+genSmallInteger = Gen.integral (Range.linear 0 20)
+
+genSmallNonEmptyList :: Gen a -> Gen [a]
+genSmallNonEmptyList gen = Gen.list (Range.linear 1 7) gen
+
+genSmallList :: Gen a -> Gen [a]
+genSmallList gen = Gen.list (Range.linear 0 6) gen
+
+genSmallString :: Gen String
+genSmallString = Gen.string (Range.linear 0 6) Gen.ascii
+
+-- Haskell uses the operator precedences 0..9, the special function application
+-- precedence 10 and the precedence 11 for function arguments. Both show and
+-- read instances have to accept this range. According to the Haskell Language
+-- Report, the output of derived show instances in precedence context 11 has to
+-- be an atomic expression.
+genShowReadPrecedence :: Gen Int
+genShowReadPrecedence = Gen.element [0..11]
+
+genCompose :: forall f g a. Gen a -> (forall x. Gen x -> Gen (f x)) -> (forall x. Gen x -> Gen (g x)) -> Gen (Compose f g a)
+genCompose gen fgen ggen = Compose <$> fgen (ggen gen) 
+
+genTuple :: Gen a -> Gen b -> Gen (a,b)
+genTuple a b = (,) <$> a <*> b
+
+genTuple3 :: Gen a -> Gen b -> Gen c -> Gen (a, b, c)
+genTuple3 gena genb genc = do
+  a <- gena
+  b <- genb
+  c <- genc
+  pure (a, b, c)
+
+genValidRange :: Ix a => Gen a -> Gen (a, a)
+genValidRange gen = do
+  Gen.filter (\(l,u) -> l <= u) (genTuple gen gen)
+
+genInRange :: (Ix a) => Gen a -> Gen (a, a, a)
+genInRange gen = do
+  Gen.filter (\(l,u,i) -> inRange (l,u) i) (genTuple3 gen gen gen)
+ 
+genSetInteger :: Gen (S.Set Integer)
+genSetInteger = do
+  xs <- sequence $ fmap (const genSmallInteger) [1..10 :: Integer]
+  pure $ foldMap S.singleton xs
+
diff --git a/src/Hedgehog/Classes/Common/IO.hs b/src/Hedgehog/Classes/Common/IO.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Common/IO.hs
@@ -0,0 +1,16 @@
+module Hedgehog.Classes.Common.IO
+  ( genIO
+  , showIO
+  ) where
+
+import Hedgehog
+import System.IO.Unsafe (unsafePerformIO)
+
+genIO :: Gen a -> Gen (IO a)
+genIO gen = fmap pure gen
+
+showIO :: Show a => IO a -> String
+showIO io = unsafePerformIO $ do
+  x <- fmap show io
+  let y = "IO " ++ x
+  pure y
diff --git a/src/Hedgehog/Classes/Common/Laws.hs b/src/Hedgehog/Classes/Common/Laws.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Common/Laws.hs
@@ -0,0 +1,270 @@
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE RecordWildCards #-}
+
+module Hedgehog.Classes.Common.Laws
+  ( Laws(..)
+  , LawContext(..)
+
+  , lawsCheck
+  , lawsCheckOne
+  , lawsCheckMany
+
+  , contextualise
+  , reduced
+  , lawWhere
+  , congruency
+
+  , congruent
+  , newline
+  , tab
+  , tab2
+  ) where
+
+import Control.Monad.IO.Class (MonadIO(liftIO))
+import Data.Monoid (All(..), Ap(..))
+import Hedgehog (Gen)
+import Hedgehog.Classes.Common.Property (Context(..))
+import Hedgehog.Internal.Property (Property(..))
+import Hedgehog.Internal.Region (Region)
+import Hedgehog.Internal.Report (Report, Result(..), Progress(..), renderProgress, reportStatus)
+import Hedgehog.Internal.Runner (checkReport)
+import System.Exit (exitFailure)
+import qualified Hedgehog.Classes.Common.PP as PP
+import qualified Hedgehog.Internal.Region as Region
+import qualified Hedgehog.Internal.Seed as Seed
+
+congruent :: String
+congruent = " ≡ "
+
+congruency :: String -> String -> String
+congruency x y = x ++ congruent ++ y
+
+newline, tab, tab2 :: String
+newline = "\n"
+tab = "    "
+tab2 = "  "
+
+-- | For footnotes
+dagger :: String
+dagger = "†"
+
+lawWhere :: [String] -> String
+lawWhere [] = []
+lawWhere (l:ls) = l ++ newline ++ tab2 ++ lawWhere ls
+
+-- | A 'Laws' is the name of the typeclass and the set of named properties associated with that typeclass.
+data Laws = Laws
+  { lawsTypeClass :: String
+  , lawsProperties :: [(String, Property)]
+  }
+
+-- | The context surrounding the property test of a law. Use 'contextualise' to turn this into a 'Context'.
+data LawContext = LawContext
+  { lawContextLawName :: String -- ^ law name
+  , lawContextLawBody :: String -- ^ law body
+  , lawContextTcName  :: String -- ^ typeclass name
+  , lawContextTcProp  :: String -- ^ how to show the specific property test
+  , lawContextReduced :: String -- ^ reduced equation, eg "LHS = RHS" where neither LHS nor RHS are reducible
+  }
+
+reduced :: Show a => a -> a -> String
+reduced lhs rhs = show lhs ++ congruent ++ show rhs
+
+-- | Turn a 'LawContext' into a 'Context'.
+contextualise :: LawContext -> Context
+contextualise LawContext{..} = Context $ unlines 
+  [ "When testing the " ++ lawContextLawName ++ " law(" ++ dagger ++"), for the " ++ lawContextTcName ++ " typeclass, the following test failed: "
+  , newline ++ lawContextTcProp
+  , newline ++ "The reduced test is: "
+  , tab2 ++ lawContextReduced
+  , newline ++ "The law in question: "
+  , tab2 ++ "(" ++ dagger ++ ") " ++ lawContextLawName ++ " Law: " ++ lawContextLawBody
+  ]
+
+-- | A convenience function for testing the properties of a typeclass.
+--   For example, in GHCi:
+--
+-- >>> genOrdering :: Gen Ordering; genOrdering = frequency [(1,pure EQ),(1,pure LT),(1,pure GT)]
+-- >>> lawsCheck (monoidLaws genOrdering)
+--   ✓ <interactive> passed 100 tests.
+--   ✓ <interactive> passed 100 tests.
+--   ✓ <interactive> passed 100 tests.
+--   ✓ <interactive> passed 100 tests.
+-- True
+lawsCheck ::
+     Laws -- ^ The 'Laws' you would like to check.
+  -> IO Bool -- ^ 'True' if your tests pass, 'False' otherwise.
+lawsCheck = fmap getAll . lawsCheckInternal
+
+-- | A convenience function for testing many typeclass instances of
+--   a single type.
+--
+-- >>> lawsCheckOne (word8 constantBounded) [jsonLaws, showReadLaws]
+--   ✓ <interactive> passed 100 tests.
+--   ✓ <interactive> passed 100 tests.
+--   ✓ <interactive> passed 100 tests.
+--   ✓ <interactive> passed 100 tests.
+--   ✓ <interactive> passed 100 tests.
+--   ✓ <interactive> passed 100 tests.
+--   ✓ <interactive> passed 100 tests.
+-- True
+lawsCheckOne ::
+     Gen a -- ^ The generator for your type.
+  -> [Gen a -> Laws] -- ^ Functions that take a generator and output 'Laws'.
+  -> IO Bool -- ^ 'True' if your tests pass. 'False' otherwise.
+lawsCheckOne g = fmap getAll . lawsCheckOneInternal g
+
+-- | A convenience function for checking many typeclass instances of
+--   multiple types.
+--
+-- @
+-- import Control.Applicative (liftA2)
+--
+-- import Data.Map (Map)
+-- import Data.Set (Set)
+--
+-- import qualified Data.List as List
+-- import qualified Data.Set as Set
+-- import qualified Data.Map as Map
+--
+-- import qualified Hedgehog.Gen as Gen
+-- import qualified Hedgehog.Range as Range
+--
+-- import Hedgehog (Gen)
+-- import Hedgehog.Classes
+--
+-- -- Generate a small @Set Int@
+-- genSet :: Gen (Set Int)
+-- genSet = Set.fromList <$> (Gen.list (Range.linear 2 10) (Gen.int Range.constantBounded))
+--
+-- -- Generate a small @Map String Int@
+-- genMap :: Gen (Map String Int)
+-- genMap = Map.fromList <$> (liftA2 List.zip genStrings genInts)
+--   where
+--     rng = Range.linear 2 6
+--     genStrings = Gen.list rng (Gen.string rng Gen.lower)
+--     genInts = Gen.list rng (Gen.int Range.constantBounded)
+--
+-- commonLaws :: (Eq a, Monoid a, Show a) => Gen a -> [Laws]
+-- commonLaws p = [eqLaws p, monoidLaws p]
+--
+-- tests :: [(String, [Laws])]
+-- tests =
+--   [ ("Set Int", commonLaws genSet)
+--   , ("Map String Int", commonLaws genMap)
+--   ]
+-- @
+--
+-- Now, in GHCi:
+--
+-- >>> lawsCheckMany tests
+--
+-- Testing properties for common typeclasses...
+--
+-- -------------
+-- -- Set Int --
+-- -------------
+-- 
+--   ✓ <interactive> passed 100 tests.
+--   ✓ <interactive> passed 100 tests.
+--   ✓ <interactive> passed 100 tests.
+--   ✓ <interactive> passed 100 tests.
+--   ✓ <interactive> passed 100 tests.
+--   ✓ <interactive> passed 100 tests.
+--   ✓ <interactive> passed 100 tests.
+-- 
+-- --------------------
+-- -- Map String Int --
+-- --------------------
+-- 
+--   ✓ <interactive> passed 100 tests.
+--   ✓ <interactive> passed 100 tests.
+--   ✓ <interactive> passed 100 tests.
+--   ✓ <interactive> passed 100 tests.
+--   ✓ <interactive> passed 100 tests.
+--   ✓ <interactive> passed 100 tests.
+--   ✓ <interactive> passed 100 tests.
+-- 
+-- 
+-- All tests succeeded
+-- True
+lawsCheckMany ::
+     [(String, [Laws])] -- ^ Pairs of type names and their associated laws to test.
+  -> IO Bool -- ^ 'True' if your tests pass. 'False' otherwise.
+lawsCheckMany = fmap getAll . lawsCheckManyInternal
+
+lawsCheckInternal :: Laws -> IO All
+lawsCheckInternal (Laws className properties) =
+  flip foldMapA properties $ \(name,p) -> do
+    putStr (className ++ ": " ++ name ++ " ")
+    All <$> check p
+
+lawsCheckOneInternal :: Gen a -> [Gen a -> Laws] -> IO All
+lawsCheckOneInternal p ls = foldMap (lawsCheckInternal . ($ p)) ls
+
+lawsCheckManyInternal :: [(String, [Laws])] -> IO All
+lawsCheckManyInternal xs = do
+  putStrLn ""
+  putStrLn "Testing properties for common typeclasses..."
+  putStrLn ""
+  r <- flip foldMapA xs $ \(typeName, laws) -> do
+    putStrLn $ prettyHeader typeName
+    r <- flip foldMapA laws $ \(Laws typeclassName properties) -> do
+      flip foldMapA properties $ \(name,p) -> do
+        putStr (typeclassName ++ ": " ++ name ++ " ")
+        check p >>= \case { True -> pure Good; _ -> pure Bad }
+    putStrLn ""
+    pure r
+  putStrLn ""
+  case r of
+    Good -> putStrLn "All tests succeeded" *> pure mempty
+    Bad  -> do
+      putStrLn "One or more tests failed"
+      exitFailure
+
+foldMapA :: (Foldable t, Monoid m, Applicative f) => (a -> f m) -> t a -> f m
+foldMapA f = getAp . foldMap (Ap . f)
+
+prettyHeader :: String -> String
+prettyHeader s = unlines [topLine, middleLine, bottomLine]
+  where
+    line = replicate (length s + 6) '-'
+    topLine = line
+    bottomLine = line
+    middleLine = "-- " ++ s ++ " --"
+
+data Status = Bad | Good
+
+instance Semigroup Status where
+  Good <> x = x
+  Bad <> _ = Bad
+
+instance Monoid Status where
+  mempty = Good
+
+checkRegion :: MonadIO m
+  => Region
+  -> Property
+  -> m (Report Result)
+checkRegion region prop = liftIO $ do
+  seed <- liftIO Seed.random 
+  result <- checkReport (propertyConfig prop) 0 seed (propertyTest prop) $ \progress -> do
+    ppprogress <- renderProgress Nothing Nothing progress
+    case reportStatus progress of
+      Running -> Region.setRegion region ppprogress
+      Shrinking _ -> Region.openRegion region ppprogress
+  ppresult <- PP.renderResult result
+  case reportStatus result of
+    Failed _ -> Region.openRegion region ppresult
+    GaveUp -> Region.openRegion region ppresult
+    OK -> Region.setRegion region ppresult
+
+  pure result 
+
+check :: MonadIO m
+  => Property
+  -> m Bool
+check prop = liftIO . Region.displayRegion $ \region ->
+  (== OK) . reportStatus <$> checkRegion region prop
+
diff --git a/src/Hedgehog/Classes/Common/PP.hs b/src/Hedgehog/Classes/Common/PP.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Common/PP.hs
@@ -0,0 +1,134 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+#if HAVE_QUANTIFIED_CONSTRAINTS
+{-# LANGUAGE QuantifiedConstraints #-}
+#endif
+
+-- | Reverse-engineered hedgehog internals that don't print out source locations.
+module Hedgehog.Classes.Common.PP
+  ( ppDiscardCount
+  , ppDoc
+  , ppName
+  , ppResult
+  , ppShrinkCount
+  , ppShrinkDiscard
+  , ppTestCount
+  , renderResult
+  ) where
+
+import Hedgehog.Range (Size)
+import Control.Monad.IO.Class (MonadIO(..))
+import qualified Data.List as List
+import Hedgehog.Internal.Report
+  ( DiscardCount(..), TestCount(..), ShrinkCount(..), Markup(..), Report(..)
+  , Result(..), FailureReport(..), renderDoc
+  )
+import qualified Text.PrettyPrint.Annotated.WL as WL
+import Text.PrettyPrint.Annotated.WL ( (<+>) )
+import qualified Hedgehog.Internal.Seed as Seed
+import Text.PrettyPrint.Annotated.WL (Doc)
+
+ppDoc :: Show x => x -> Doc a
+ppDoc = WL.text . show
+
+ppName :: Doc a
+ppName = "<interactive>"
+
+ppDiscardCount :: DiscardCount -> Doc a
+ppDiscardCount = \case
+  DiscardCount 1 -> "1 discard"
+  DiscardCount n -> ppDoc n <+> "discards"
+
+ppTestCount :: TestCount -> Doc a
+ppTestCount = \case
+  TestCount 1 -> "1 test"
+  TestCount n -> ppDoc n <+> "tests"
+
+ppShrinkCount :: ShrinkCount -> Doc a
+ppShrinkCount = \case
+  ShrinkCount 1 -> "1 shrink"
+  ShrinkCount n -> ppDoc n <+> "shrinks"
+
+ppShrinkDiscard :: ShrinkCount -> DiscardCount -> Doc Markup
+ppShrinkDiscard s d = case (s, d) of
+  (0, 0) -> ""
+  (0, _) -> " and" <+> ppDiscardCount d
+  (_, 0) -> " and" <+> ppShrinkCount s
+  (_, _) -> "," <+> ppShrinkCount s <+> "and" <+> ppDiscardCount d
+
+ppResult :: MonadIO m => Report Result -> m (Doc Markup)
+ppResult (Report tests discards result) = case result of
+  Failed failure -> do
+    pfailure <- ppFailure failure
+    pure . WL.vsep $
+      [ icon FailedIcon '✗' . markup FailedHeader $
+          ppName <+>
+          "failed after" <+>
+          ppTestCount tests <>
+          ppShrinkDiscard (failureShrinks failure) discards <>
+          "."
+      , mempty
+      , pfailure
+      , mempty
+      ] 
+  
+  GaveUp -> pure . icon GaveUpIcon '⚐' . WL.annotate GaveUpHeader $
+    ppName <+>
+    "gave up after" <+>
+    ppDiscardCount discards <>
+    ", passed" <+>
+    ppTestCount tests <>
+    "." 
+  OK -> pure . icon SuccessIcon '✓' . WL.annotate SuccessHeader $
+    ppName <+>
+    "passed" <+>
+    ppTestCount tests <>
+    "."
+
+icon :: Markup -> Char -> Doc Markup -> Doc Markup
+icon m i x = WL.annotate m (WL.char i) <+> x
+
+ppTextLines :: String -> [Doc Markup]
+ppTextLines = fmap WL.text . List.lines
+
+markup :: Markup -> Doc Markup -> Doc Markup
+markup = WL.annotate
+
+gutter :: Markup -> Doc Markup -> Doc Markup
+gutter m x = markup m ">" <+> x
+
+ppFailure :: MonadIO m => FailureReport -> m (Doc Markup)
+ppFailure (FailureReport size seed _ _inputs0 mlocation0 msg _mdiff msgs0) = do
+  msgs <- case mlocation0 of
+    Nothing ->
+      let msgs1 = msgs0 ++ (if null msg then [] else [msg])
+          docs = concatMap ppTextLines msgs1
+      in pure docs
+    Just _location0 -> 
+      let l = concatMap ppTextLines msgs0
+      in pure l
+
+  let with xs f = if null xs then [] else [f xs]
+
+  pure . WL.indent 2 . WL.vsep . WL.punctuate WL.line $ concat
+    [ with msgs WL.vsep
+    , [ppReproduce size seed]
+    ]
+
+ppReproduce :: Size -> Seed.Seed -> Doc Markup
+ppReproduce size seed = WL.vsep
+  [ markup ReproduceHeader "This failure can be reproduced by running:"
+  , gutter ReproduceGutter . markup ReproduceSource $
+      "recheck" <+>
+      WL.text (showsPrec 11 size "") <+>
+      WL.text (showsPrec 11 seed "") <+>
+      "<property>"
+  ]
+
+renderResult :: MonadIO m => Report Result -> m String
+renderResult x = renderDoc Nothing =<< ppResult x
diff --git a/src/Hedgehog/Classes/Common/Property.hs b/src/Hedgehog/Classes/Common/Property.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Common/Property.hs
@@ -0,0 +1,307 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+#if HAVE_QUANTIFIED_CONSTRAINTS
+{-# LANGUAGE QuantifiedConstraints #-}
+#endif
+
+-- | This module exports hedgehog comparison tests
+--   that don't contain CallStack information, since this would
+--   expose library internals in error messages.
+module Hedgehog.Classes.Common.Property
+  ( hLessThan, hGreaterThan
+  , heq, heq1, heq2
+  , heqCtx, heqCtx1, heqCtx2
+  , hneq, hneq1, hneq2
+  , hneqCtx, hneqCtx1, hneqCtx2 
+  , bar
+  , Context(..)
+  ) where
+
+import Control.Exception (SomeException(..), displayException)
+import Data.Typeable (typeOf)
+import GHC.Stack
+import Hedgehog.Classes.Common.Compat
+import Hedgehog.Internal.Exception (tryEvaluate)
+import Hedgehog.Internal.Property (MonadTest, liftTest, mkTest, success, Failure(..), Log(..))
+import Text.Show.Pretty (ppShow)
+import qualified Data.Char as Char
+import qualified Data.List as List
+
+#if HAVE_QUANTIFIED_CONSTRAINTS == 0
+import qualified Data.Functor.Classes as C
+#endif
+
+bar :: String
+bar = "━━━"
+
+bar5 :: String
+bar5 = "━━━━━━━━━━━━━━━"
+
+evalNoSrc :: (MonadTest m, HasCallStack) => a -> m a
+evalNoSrc x = either (withFrozenCallStack failExceptionNoSrc) pure (tryEvaluate x)
+
+failWithNoSrc :: (MonadTest m, HasCallStack) => String -> m a
+failWithNoSrc msg = do
+  liftTest $ mkTest (Left $ Failure Nothing "" Nothing, [Footnote msg])
+ 
+failExceptionNoSrc :: (MonadTest m, HasCallStack) => SomeException -> m a
+failExceptionNoSrc (SomeException x) = withFrozenCallStack $
+  failWithNoSrc $ unlines
+    [ bar ++ " Exception: " ++ show (typeOf x) ++ " " ++ bar
+      , List.dropWhileEnd Char.isSpace (displayException x)
+    ]
+
+-- | You can provide a 'Context' to 'heqCtx','heqCtx1','heqCtx2','hneqCtx','hneqCtx1',or 'hneqCtx2'. The 'Context' is used to provide useful error messages in the event of a failure.
+data Context = NoContext | Context String
+
+contextToString :: Context -> String
+contextToString = \case
+  NoContext -> "No Context provided."
+  Context ctx -> bar ++ " Context " ++ bar ++ "\n" ++ ctx ++ bar5
+
+failContext::
+  ( MonadTest m, HasCallStack
+  , Show a, Show b
+  ) => a -> b -> Context -> m ()
+failContext _x _y ctx = withFrozenCallStack $
+  failWithNoSrc $ contextToString ctx
+
+-- | Fails the test if the right argument is less than or equal to the left.
+-- see https://github.com/hedgehogqa/haskell-hedgehog/pull/196 
+hLessThan :: (MonadTest m, Ord a, Show a, HasCallStack) => a -> a -> m ()
+hLessThan x y = do
+  ok <- withFrozenCallStack $ evalNoSrc (x < y)
+  if ok
+    then success
+    else withFrozenCallStack $ failWithNoSrc $ unlines
+      [ bar ++ "Not Less Than " ++ bar
+      , ppShow x ++ " is not less than " ++ ppShow y
+      ]
+
+-- | Fails the test if the right argument is greater than or equal to the left.
+-- see https://github.com/hedgehogqa/haskell-hedgehog/pull/196
+hGreaterThan :: (MonadTest m, Ord a, Show a, HasCallStack) => a -> a -> m ()
+hGreaterThan x y = do
+  ok <- withFrozenCallStack $ evalNoSrc (x > y)
+  if ok
+    then success
+    else withFrozenCallStack $ failWithNoSrc $ unlines
+      [ bar ++ "Not Greater Than " ++ bar
+      , ppShow x ++ " is not greater than " ++ ppShow y
+      ]
+
+infix 4 `hneq`
+
+-- | Passes the test if the given arguments are not equal. Otherwise fails
+--   with the given 'Context'.
+hneqCtx ::
+  ( MonadTest m
+  , HasCallStack
+  , Eq a
+  , Show a
+  ) => a -> a -> Context -> m ()
+hneqCtx x y ctx = do
+  ok <- withFrozenCallStack $ evalNoSrc (x `neq` y)
+  if ok
+    then success
+    else withFrozenCallStack $ failContext x y ctx
+
+-- | Passes the test if the given arguments are not equal. Otherwise fails
+--   with 'NoContext'.
+hneq ::
+  ( MonadTest m
+  , HasCallStack
+  , Eq a
+  , Show a
+  ) => a -> a -> m ()
+hneq x y = hneqCtx x y NoContext
+
+infix 4 `heq`
+
+-- | Passes the test if the given arguments are equal. Otherwise fails
+--   with the given 'Context'.
+heqCtx ::
+    ( MonadTest m
+    , HasCallStack
+    , Eq a
+    , Show a
+    ) => a -> a -> Context -> m ()
+heqCtx x y ctx = do
+  ok <- withFrozenCallStack $ evalNoSrc (x `eq` y)
+  if ok
+    then success
+    else withFrozenCallStack $ failContext x y ctx
+
+-- | Passes the test if the given arguments are equal. Otherwise fails
+--   with 'NoContext'.
+heq ::
+    ( MonadTest m
+    , HasCallStack
+    , Eq a
+    , Show a
+    ) => a -> a -> m ()
+heq x y = heqCtx x y NoContext
+
+infix 4 `heq1`
+
+-- | Passes the test if the given arguments are not equal. Otherwise fails
+--   with the given 'Context'.
+hneqCtx1 ::
+     ( MonadTest m
+     , HasCallStack
+     , Eq a
+     , Show a
+#if HAVE_QUANTIFIED_CONSTRAINTS
+     , forall x. Eq x => Eq (f x)
+     , forall x. Show x => Show (f x)
+#else
+     , C.Eq1 f, C.Show1 f
+#endif 
+     ) => f a -> f a -> Context -> m ()
+hneqCtx1 x y ctx = do
+  ok <- withFrozenCallStack $ evalNoSrc (x `neq1` y)
+  if ok
+    then success
+    else withFrozenCallStack $ failContext x y ctx
+
+-- | Passes the test if the given arguments are not equal. Otherwise fails
+--   with 'NoContext'.
+hneq1 ::
+     ( MonadTest m
+     , HasCallStack
+     , Eq a
+     , Show a
+#if HAVE_QUANTIFIED_CONSTRAINTS
+     , forall x. Eq x => Eq (f x)
+     , forall x. Show x => Show (f x)
+#else
+     , C.Eq1 f, C.Show1 f
+#endif 
+     ) => f a -> f a -> m ()
+hneq1 x y = hneqCtx1 x y NoContext
+
+-- | Passes the test if the given arguments are equal. Otherwise fails
+--   with the given 'Context'.
+heqCtx1 ::
+     ( MonadTest m
+     , HasCallStack
+     , Eq a
+     , Show a
+#if HAVE_QUANTIFIED_CONSTRAINTS
+     , forall x. Eq x => Eq (f x)
+     , forall x. Show x => Show (f x)
+#else
+     , C.Eq1 f, C.Show1 f
+#endif 
+     ) => f a -> f a -> Context -> m ()
+heqCtx1 x y ctx = do
+  ok <- withFrozenCallStack $ evalNoSrc (x `eq1` y)
+  if ok
+    then success
+    else withFrozenCallStack $ failContext x y ctx
+
+-- | Passes the test if the given arguments are equal. Otherwise fails
+--   with 'NoContext'.
+heq1 ::
+     ( MonadTest m
+     , HasCallStack
+     , Eq a
+     , Show a
+#if HAVE_QUANTIFIED_CONSTRAINTS
+     , forall x. Eq x => Eq (f x)
+     , forall x. Show x => Show (f x)
+#else
+     , C.Eq1 f, C.Show1 f
+#endif 
+     ) => f a -> f a -> m ()
+heq1 x y = heqCtx1 x y NoContext
+
+infix 4 `heq2`
+
+-- | Passes the test if the given arguments are equal. Otherwise fails
+--   with the given 'Context'.
+heqCtx2 ::
+     ( MonadTest m
+     , HasCallStack
+     , Eq a
+     , Eq b
+     , Show a
+     , Show b
+#if HAVE_QUANTIFIED_CONSTRAINTS
+     , forall x y. (Eq x, Eq y) => Eq (f x y)
+     , forall x y. (Show x, Show y) => Show (f x y)
+#else
+     , C.Eq2 f, C.Show2 f
+#endif 
+     ) => f a b -> f a b -> Context -> m ()
+heqCtx2 x y ctx = do
+  ok <- withFrozenCallStack $ evalNoSrc (x `eq2` y)
+  if ok
+    then success
+    else withFrozenCallStack $ failContext x y ctx
+
+-- | Passes the test if the given arguments are equal. Otherwise fails
+--   with 'NoContext'.
+heq2 ::
+     ( MonadTest m
+     , HasCallStack
+     , Eq a
+     , Eq b
+     , Show a
+     , Show b
+#if HAVE_QUANTIFIED_CONSTRAINTS
+     , forall x y. (Eq x, Eq y) => Eq (f x y)
+     , forall x y. (Show x, Show y) => Show (f x y)
+#else
+     , C.Eq2 f, C.Show2 f
+#endif 
+     ) => f a b -> f a b -> m ()
+heq2 x y = heqCtx2 x y NoContext
+
+infix 4 `hneq2`
+
+-- | Passes the test if the given arguments are not equal. Otherwise fails
+--   with the given 'Context'.
+hneqCtx2 ::
+     ( MonadTest m
+     , HasCallStack
+     , Eq a
+     , Eq b
+     , Show a
+     , Show b
+#if HAVE_QUANTIFIED_CONSTRAINTS
+     , forall x y. (Eq x, Eq y) => Eq (f x y)
+     , forall x y. (Show x, Show y) => Show (f x y)
+#else
+     , C.Eq2 f, C.Show2 f
+#endif 
+     ) => f a b -> f a b -> Context -> m ()
+hneqCtx2 x y ctx = do
+  ok <- withFrozenCallStack $ evalNoSrc (x `neq2` y)
+  if ok
+    then success
+    else withFrozenCallStack $ failContext x y ctx
+
+-- | Passes the test if the given arguments are not equal. Otherwise fails
+--   with 'NoContext'.
+hneq2 ::
+     ( MonadTest m
+     , HasCallStack
+     , Eq a
+     , Eq b
+     , Show a
+     , Show b
+#if HAVE_QUANTIFIED_CONSTRAINTS
+     , forall x y. (Eq x, Eq y) => Eq (f x y)
+     , forall x y. (Show x, Show y) => Show (f x y)
+#else
+     , C.Eq2 f, C.Show2 f
+#endif 
+     ) => f a b -> f a b -> m ()
+hneq2 x y = hneqCtx2 x y NoContext
+
diff --git a/src/Hedgehog/Classes/Contravariant.hs b/src/Hedgehog/Classes/Contravariant.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Contravariant.hs
@@ -0,0 +1,70 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RankNTypes #-}
+
+module Hedgehog.Classes.Contravariant (contravariantLaws) where
+
+import Data.Functor.Contravariant (Contravariant(..))
+
+import Hedgehog
+import Hedgehog.Classes.Common
+
+-- | Tests the following 'Contravariant' laws:
+--
+-- [__Identity__]: @'contramap' 'id'@ ≡ @'id'@
+-- [__Composition__]: @'contramap' f '.' 'contramap' g@ ≡ @'contramap' (g '.' f)@
+contravariantLaws ::
+  ( Contravariant f
+  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
+  ) => (forall x. Gen x -> Gen (f x)) -> Laws
+contravariantLaws gen = Laws "Contravariant"
+  [ ("Identity", contravariantIdentity gen)
+  , ("Composition", contravariantComposition gen)
+  ]
+
+contravariantIdentity ::
+  ( Contravariant f
+  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
+  ) => (forall x. Gen x -> Gen (f x)) -> Property
+contravariantIdentity fgen = property $ do
+  a <- forAll $ fgen genSmallInteger
+  let lhs = contramap id a
+  let rhs = id a
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Identity", lawContextLawBody = "contramap id" `congruency` "id"
+        , lawContextTcName = "Contravariant", lawContextTcProp =
+            let showA = show a
+            in lawWhere
+              [ "contramap id x" `congruency` "id x, where"
+              , "x = " ++ showA
+              ]
+        , lawContextReduced = reduced lhs rhs
+        }
+  heqCtx1 lhs rhs ctx
+
+contravariantComposition ::
+  ( Contravariant f
+  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
+  ) => (forall x. Gen x -> Gen (f x)) -> Property
+contravariantComposition fgen = property $ do
+  a <- forAll $ fgen genSmallInteger
+  f' <- forAll genQuadraticEquation
+  g' <- forAll genQuadraticEquation
+  let f = runQuadraticEquation f'
+  let g = runQuadraticEquation g'
+  let lhs = contramap f (contramap g a)
+  let rhs = contramap (g . f) a
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Composition", lawContextLawBody = "contramap f . contramap g" `congruency` "contramap (g . f)"
+        , lawContextTcName = "Contravariant", lawContextTcProp =
+            let showF = show f'; showG = show g'; showA = show a;
+            in lawWhere
+                 [ "contramap f . contramap g $ a" `congruency` "contramap (g . f) a, where"
+                 , "f = " ++ showF
+                 , "g = " ++ showG
+                 , "a = " ++ showA
+                 ]
+        , lawContextReduced = reduced lhs rhs
+        }
+  heqCtx1 lhs rhs ctx
+
diff --git a/src/Hedgehog/Classes/Enum.hs b/src/Hedgehog/Classes/Enum.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Enum.hs
@@ -0,0 +1,101 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Hedgehog.Classes.Enum (enumLaws, boundedEnumLaws) where
+
+import Hedgehog
+import Hedgehog.Classes.Common
+
+import qualified Hedgehog.Gen as Gen
+
+-- | Tests the following 'Enum' laws:
+--
+-- [__Succ-Pred Identity__]: @'succ' '.' 'pred'@ ≡ @'id'@
+-- [__Pred-Succ Identity__]: @'pred' '.' 'succ'@ ≡ @'id'@
+enumLaws :: (Enum a, Eq a, Show a) => Gen a -> Laws
+enumLaws gen = Laws "Enum"
+  [ ("Succ Pred Identity", succPredIdentity gen)
+  , ("Pred Succ Identity", predSuccIdentity gen)
+  ]
+
+-- | Tests the same laws as 'enumLaws', but uses the 'Bounded'
+--   constraint to ensure that 'succ' and 'pred' behave as though
+--   they are total. This should always be preferred if your type
+--   has a 'Bounded' instance.
+boundedEnumLaws :: (Bounded a, Enum a, Eq a, Show a) => Gen a -> Laws
+boundedEnumLaws gen = Laws "Bounded Enum"
+  [ ("Succ Pred Identity", succPredBoundedIdentity gen)
+  , ("Pred Succ Identity", predSuccBoundedIdentity gen)
+  ]
+
+succPredIdentity :: forall a. (Enum a, Eq a, Show a) => Gen a -> Property
+succPredIdentity gen = property $ do
+  x <- forAll gen
+  let lhs = succ (pred x); rhs = x;
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Succ-Pred Identity"
+        , lawContextLawBody = "succ . pred" `congruency` "id"
+        , lawContextTcName = "Enum"
+        , lawContextTcProp =
+            let showX = show x
+            in lawWhere
+              [ "succ . pred $ x" `congruency` "id x, where"
+              , "x = " ++ showX
+              ]
+        , lawContextReduced = reduced lhs rhs
+        }
+  heqCtx lhs rhs ctx
+
+predSuccIdentity :: forall a. (Enum a, Eq a, Show a) => Gen a -> Property
+predSuccIdentity gen = property $ do
+  x <- forAll gen
+  let lhs = pred (succ x); rhs = x;
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Pred-Succ Identity"
+        , lawContextLawBody = "pred . succ" `congruency` "id"
+        , lawContextTcName = "Enum"
+        , lawContextTcProp =
+            let showX = show x
+            in lawWhere
+              [ "pred . succ $ x" `congruency` "id x, where"
+              , "x = " ++ showX
+              ]
+        , lawContextReduced = reduced lhs rhs
+        }
+  heqCtx lhs rhs ctx
+
+succPredBoundedIdentity :: forall a. (Bounded a, Enum a, Eq a, Show a) => Gen a -> Property
+succPredBoundedIdentity gen = property $ do
+  x <- forAll $ Gen.filter (/= minBound) gen
+  let lhs = succ (pred x); rhs = x;
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Succ-Pred Identity"
+        , lawContextLawBody = "succ . pred" `congruency` "id"
+        , lawContextTcName = "Enum"
+        , lawContextTcProp =
+            let showX = show x
+            in lawWhere
+              [ "succ . pred $ x" `congruency` "id x, where"
+              , "x = " ++ showX
+              ]
+        , lawContextReduced = reduced lhs rhs
+        }
+  heqCtx lhs rhs ctx
+
+predSuccBoundedIdentity :: forall a. (Bounded a, Enum a, Eq a, Show a) => Gen a -> Property
+predSuccBoundedIdentity gen = property $ do
+  x <- forAll $ Gen.filter (/= maxBound) gen
+  let lhs = pred (succ x); rhs = x;
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Pred-Succ Identity"
+        , lawContextLawBody = "pred . succ" `congruency` "id"
+        , lawContextTcName = "Enum"
+        , lawContextTcProp =
+            let showX = show x
+            in lawWhere
+              [ "pred . succ $ x" `congruency` "id x, where"
+              , "x = " ++ showX
+              ]
+        , lawContextReduced = reduced lhs rhs
+        }
+  heqCtx lhs rhs ctx
+  
diff --git a/src/Hedgehog/Classes/Eq.hs b/src/Hedgehog/Classes/Eq.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Eq.hs
@@ -0,0 +1,94 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Hedgehog.Classes.Eq (eqLaws) where
+
+import Hedgehog
+import Hedgehog.Classes.Common
+
+-- | Tests the following 'Eq' laws:
+--
+-- [__Reflexivity__]: @x '==' x@ ≡ @'True'@
+-- [__Symmetry__]: @x '==' y@ ≡ @y '==' x@
+-- [__Transitivity__]: @x '==' y '&&' y '==' z@ ≡ @x '==' z@
+-- [__Substitutivity__]: @x '==' y@ ≡ @f x '==' f y@
+-- [__Negation__]: @x '/=' y@ ≡ @'not' (x '==' y)@
+eqLaws :: (Eq a, Show a) => Gen a -> Laws
+eqLaws gen = Laws "Eq"
+  [ ("Transitive", eqTransitive gen)
+  , ("Symmetric", eqSymmetric gen)  
+  , ("Reflexive", eqReflexive gen) 
+  , ("Negation", eqNegation gen) 
+  ]
+
+eqTransitive :: forall a. (Eq a, Show a) => Gen a -> Property
+eqTransitive gen = property $ do
+  a <- forAll gen
+  b <- forAll gen
+  c <- forAll gen
+  let lhs = a == b && b == c; rhs = a == c
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Transitivity", lawContextLawBody = "a == b ∧ b == c" `congruency` "a == c"
+        , lawContextTcName = "Eq", lawContextTcProp =
+            let showA = show a; showB = show b; showC = show c;
+            in lawWhere
+              [ "a == b ∧ b == c" `congruency` "a == c, where"
+              , "a = " ++ showA
+              , "b = " ++ showB
+              , "c = " ++ showC
+              ]
+        , lawContextReduced = reduced lhs rhs
+        }
+  case a == b of
+    True -> case b == c of { True -> heqCtx a c ctx; False -> hneqCtx a c ctx }
+    False -> case b == c of { True -> hneqCtx a c ctx; False -> success }
+
+eqSymmetric :: forall a. (Eq a, Show a) => Gen a -> Property
+eqSymmetric gen = property $ do
+  a <- forAll gen
+  b <- forAll gen
+  let lhs = a == b; rhs = b == a
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Symmetry", lawContextLawBody = "a == b" `congruency` "b == a"
+        , lawContextTcName = "Eq", lawContextTcProp =
+            let showA = show a; showB = show b;
+            in lawWhere
+              [ "a == b" `congruency` "b == a, where"
+              , "a = " ++ showA
+              , "b = " ++ showB
+              ]
+        , lawContextReduced = reduced lhs rhs
+        }
+  heqCtx lhs rhs ctx
+
+eqReflexive :: forall a. (Eq a, Show a) => Gen a -> Property
+eqReflexive gen = property $ do
+  a <- forAll gen
+  let lhs = a
+  let rhs = a
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Reflexivity", lawContextLawBody = "a" `congruency` "a"
+        , lawContextTcName = "Eq"
+        , lawContextTcProp = let showA = show a in lawWhere [ "a" `congruency` "a, where", "a = " ++ showA ]
+        , lawContextReduced = reduced a a
+        }
+  heqCtx lhs rhs ctx
+
+eqNegation :: forall a. (Eq a, Show a) => Gen a -> Property
+eqNegation gen = property $ do
+  x <- forAll gen
+  y <- forAll gen
+  let lhs = x /= y
+  let rhs = not (x == y)
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Negation", lawContextLawBody = "x /= y" `congruency` "not (x == y)"
+        , lawContextTcName = "Eq"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showX = show x; showY = show y;
+            in lawWhere
+              [ "x /= y" `congruency` "not (x == y), where"
+              , "x = " ++ showX
+              , "y = " ++ showY
+              ]
+        }
+  heqCtx lhs rhs ctx
diff --git a/src/Hedgehog/Classes/Foldable.hs b/src/Hedgehog/Classes/Foldable.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Foldable.hs
@@ -0,0 +1,384 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE LambdaCase #-}
+
+module Hedgehog.Classes.Foldable (foldableLaws) where
+
+import Hedgehog
+import Hedgehog.Classes.Common
+
+import Control.Monad.IO.Class (MonadIO(..))
+import Control.Exception (ErrorCall(..), try, evaluate)
+import Data.Monoid (Sum(..), Endo(..), Dual(..))
+import qualified Data.Foldable as Foldable
+
+-- | Tests the following 'Foldable' laws:
+--
+-- [__Fold__]: @'Foldable.fold' ≡ 'Foldable.foldMap' 'id'@
+-- [__FoldMap__]: @'Foldable.foldMap' f ≡ 'Foldable.foldr' ('mappend' '.' f) 'mempty'@
+-- [__Foldr__]: @'Foldable.foldr' f z t ≡ 'appEndo' ('Foldable.foldMap' ('Endo' '.' f) t) z@
+-- [__Foldr'__]: @'Foldable.foldr'' f z0 t ≡ 'Foldable.foldl' f' 'id' t z0, where f' k x z = k '$!' f x z@
+-- [__Foldl__]: @'Foldable.foldl' f z t ≡ 'appEndo' ('getDual' ('Foldable.foldMap' ('Dual' '.' 'Endo' '.' 'flip' f) t)) z@
+-- [__Foldl'__]: @'Foldable.foldl'' f z0 xs ≡ 'Foldable.foldr' f' 'id' xs z0, where f' x k z = k '$!' f z x@
+-- [__Foldl1__]: @'Foldable.foldl1' f t ≡ let (x:xs) = 'Foldable.toList' t in 'foldl' f x xs@
+-- [__Foldr1__]: @'Foldable.foldr1' f t ≡ let (xs,x)@ = @unsnoc ('Foldable.toList' t) in 'foldr' f x xs@
+-- [__ToList__]: @'Foldable.toList' ≡ 'Foldable.foldr' (:) []@
+-- [__Null__]: @'Foldable.null' ≡ 'Foldable.foldr' ('const' ('const' 'False')) 'True'@
+-- [__Length__]: @'Foldable.length' ≡ 'getSum' '.' 'Foldable.foldMap' ('const' ('Sum' 1))@
+foldableLaws ::
+  ( Foldable f
+  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
+  ) => (forall x. Gen x -> Gen (f x)) -> Laws
+foldableLaws gen = Laws "Foldable"
+  [ ("fold", foldableFold gen)
+  , ("foldMap", foldableFoldMap gen)
+  , ("foldr", foldableFoldr gen)
+  , ("foldr'", foldableFoldr' gen)
+  , ("foldl", foldableFoldl gen)
+  , ("foldl'", foldableFoldl' gen)
+  , ("foldl1", foldableFoldl1 gen)
+  , ("foldr1", foldableFoldr1 gen)
+  , ("toList", foldableToList gen)
+  , ("null", foldableNull gen)
+  , ("length", foldableLength gen)
+  ]
+
+foldableFold ::
+  ( Foldable f
+  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
+  ) => (forall x. Gen x -> Gen (f x)) -> Property
+foldableFold fgen = property $ do
+  a <- forAll $ fgen genSmallSum
+  let lhs = Foldable.fold a
+  let rhs = Foldable.foldMap id a
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Fold"
+        , lawContextLawBody = "fold" `congruency` "foldMap id"
+        , lawContextTcName = "Foldable"
+        , lawContextTcProp =
+            let showA = show a
+            in lawWhere
+              [ "fold a" `congruency` "foldMap id a, where"
+              , "a = " ++ showA
+              ]
+        , lawContextReduced = reduced lhs rhs 
+        } 
+
+  heqCtx lhs rhs ctx
+
+foldableFoldMap ::
+  ( Foldable f
+  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
+  ) => (forall x. Gen x -> Gen (f x)) -> Property
+foldableFoldMap fgen = property $ do
+  a <- forAll $ fgen genSmallInteger
+  e <- forAll genQuadraticEquation
+  let f = Sum . runQuadraticEquation e
+  let lhs = Foldable.foldMap f a
+  let rhs = Foldable.foldr (mappend . f) mempty a
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "FoldMap"
+        , lawContextLawBody = "foldMap f" `congruency` "foldr (mappend . f) mempty"
+        , lawContextTcName = "Foldable"
+        , lawContextTcProp =
+            let showA = show a
+                showF = "Sum $ " ++ show e
+            in lawWhere
+              [ "foldMap f a" `congruency` "foldr (mappend . f) mempty  a, where"
+              , "f = " ++ showF
+              , "a = " ++ showA
+              ]
+        , lawContextReduced = reduced lhs rhs 
+        } 
+  heqCtx lhs rhs ctx
+
+foldableFoldr ::
+  ( Foldable f
+  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
+  ) => (forall x. Gen x -> Gen (f x)) -> Property
+foldableFoldr fgen = property $ do
+  e <- forAll genLinearEquationTwo
+  z <- forAll genSmallInteger
+  t <- forAll $ fgen genSmallInteger
+  let f = runLinearEquationTwo e
+  let lhs = Foldable.foldr f z t
+  let rhs = appEndo (Foldable.foldMap (Endo . f) t) z
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Foldr"
+        , lawContextLawBody = "foldr f z t" `congruency` "appEndo (foldMap (Endo . f) t) z"
+        , lawContextTcName = "Foldable"
+        , lawContextTcProp =
+            let showT = show t
+                showF = show e
+                showZ = show z
+            in lawWhere
+              [ "foldr f z t" `congruency` "appEndo (foldMap (Endo . f) t) z"
+              , "f = " ++ showF
+              , "z = " ++ showZ
+              , "t = " ++ showT
+              ]
+        , lawContextReduced = reduced lhs rhs 
+        } 
+  heqCtx lhs rhs ctx
+ 
+foldableFoldl ::
+  ( Foldable f
+  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
+  ) => (forall x. Gen x -> Gen (f x)) -> Property
+foldableFoldl fgen = property $ do
+  e <- forAll genLinearEquationTwo
+  z <- forAll genSmallInteger
+  t <- forAll $ fgen genSmallInteger
+  let f = runLinearEquationTwo e
+  let lhs = Foldable.foldl f z t
+  let rhs = appEndo (getDual (Foldable.foldMap (Dual . Endo . flip f) t)) z
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Foldl"
+        , lawContextLawBody = "foldl f z t" `congruency` "appEndo (getDual (foldMap (Dual . Endo . flip f) t)) z"
+        , lawContextTcName = "Foldable"
+        , lawContextTcProp =
+            let showT = show t
+                showF = show e
+                showZ = show z
+            in lawWhere
+              [ "foldl f z t" `congruency` "appEndo (getDual (foldMap (Dual . Endo . flip f) t)) z"
+              , "f = " ++ showF
+              , "z = " ++ showZ
+              , "t = " ++ showT
+              ]
+        , lawContextReduced = reduced lhs rhs 
+        } 
+  heqCtx lhs rhs ctx
+
+ctxNotStrict :: String -> Context
+ctxNotStrict str = Context $ "Your implementation of " ++ str ++ " is not strict."
+
+foldableFoldr' ::
+  ( Foldable f
+  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
+  ) => (forall x. Gen x -> Gen (f x)) -> Property
+foldableFoldr' fgen = property $ do
+  xs <- forAll $ fgen (genBottom genSmallInteger)
+  let f :: Bottom Integer -> Integer -> Integer
+      f a b = case a of
+        BottomUndefined -> error "foldableFoldr': your foldr' is not strict!"
+        BottomValue v -> if even v then v else b
+  z0 <- forAll genSmallInteger
+  (rhs, ctx1) <- liftIO $ do
+    let f' k x z = k $! f x z
+    e <- try (evaluate (Foldable.foldl f' id xs z0))
+    case e of
+      Left (_ :: ErrorCall) -> pure (Nothing, ctxNotStrict "foldr'")
+      Right i -> pure (Just i, NoContext)
+  (lhs, ctx2) <- liftIO $ do
+    e <- try (evaluate (Foldable.foldr' f z0 xs))
+    case e of
+      Left (_ :: ErrorCall) -> pure (Nothing, ctxNotStrict "foldr'")
+      Right i -> pure (Just i, NoContext)
+  let ctx = case ctx1 of
+        NoContext -> case ctx2 of
+          NoContext -> contextualise $ LawContext
+            { lawContextLawName = "Foldr'"
+            , lawContextLawBody = "foldr' f z0 t" `congruency` "foldl f' id t z0, where f' k x z = k $! f x z"
+            , lawContextTcName = "Foldable"
+            , lawContextTcProp =
+                let showT = show xs
+                    showF = "\\a b -> case a of\n  BottomUndefined -> error \"foldableFoldr': not strict\"\n  BottomValue v -> if even v then v else b"
+                    showZ = show z0
+                in lawWhere
+                  [ "foldr' f z0 t" `congruency` "foldl f' id t z0, where f' k x z = k $! f x z"
+                  , "f = " ++ showF
+                  , "z0 = " ++ showZ
+                  , "t = " ++ showT
+                  ]
+            , lawContextReduced = reduced lhs rhs 
+            } 
+          c2 -> c2
+        c1 -> c1
+  heqCtx lhs rhs ctx
+
+foldableFoldl' ::
+  ( Foldable f
+  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
+  ) => (forall x. Gen x -> Gen (f x)) -> Property
+foldableFoldl' fgen = property $ do
+  xs <- forAll $ fgen (genBottom genSmallInteger)
+  let f :: Integer -> Bottom Integer -> Integer
+      f a b = case b of
+        BottomUndefined -> error "foldableFoldl': your foldl' is not strict!"
+        BottomValue v -> if even v then a else v
+  let z0 = 0
+  (rhs,ctx1) <- liftIO $ do
+    let f' x k z = k $! f z x
+    e <- try (evaluate (Foldable.foldr f' id xs z0))
+    case e of
+      Left (_ :: ErrorCall) -> pure (Nothing, ctxNotStrict "foldl'")
+      Right i -> pure (Just i, NoContext)
+  (lhs,ctx2) <- liftIO $ do
+    e <- try (evaluate (Foldable.foldl' f z0 xs))
+    case e of
+      Left (_ :: ErrorCall) -> pure (Nothing, ctxNotStrict "foldl'")
+      Right i -> pure (Just i, NoContext) 
+  let ctx = case ctx1 of
+        NoContext -> case ctx2 of
+          NoContext -> contextualise $ LawContext
+            { lawContextLawName = "Foldl'"
+            , lawContextLawBody = "foldl' f z0 xs" `congruency` "foldr f' id xs z0, where f' x k z = k $! f z x"
+            , lawContextTcName = "Foldable"
+            , lawContextTcProp =
+                let showT = show xs
+                    showF = "\\a b -> case a of\n  BottomUndefined -> error \"foldableFoldr': not strict\"\n  BottomValue v -> if even v then v else b"
+                    showZ = show z0
+                in lawWhere
+                  [ "foldl' f z0 xs" `congruency` "foldr f' id xs z0, where f' x k z = k $! f z x"
+                  , "f = " ++ showF
+                  , "z0 = " ++ showZ
+                  , "t = " ++ showT
+                  ]
+            , lawContextReduced = reduced lhs rhs 
+            } 
+          c2 -> c2
+        c1 -> c1
+  heqCtx lhs rhs ctx
+ 
+foldableFoldl1 ::
+  ( Foldable f
+  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
+  ) => (forall x. Gen x -> Gen (f x)) -> Property
+foldableFoldl1 fgen = property $ do
+  e <- forAll genLinearEquationTwo
+  t <- forAll $ fgen genSmallInteger
+  case compatToList t of
+    [] -> success
+    (x:xs) ->
+      let f = runLinearEquationTwo e
+          lhs = Foldable.foldl1 f t
+          rhs = Foldable.foldl f x xs
+          ctx = contextualise $ LawContext
+            { lawContextLawName = "Foldl1"
+            , lawContextLawBody = "foldl1 f t" `congruency` "let (x:xs) = toList t in foldl f x xs"
+            , lawContextTcName = "Foldable"
+            , lawContextTcProp =
+                let showF = show e
+                    showT = show t
+                    showX = show x
+                    showXS = show xs
+                in lawWhere
+                  [ "foldl1 f t" `congruency` "let (x:xs) = toList t in foldl f x xs, where"
+                  , "f = " ++ showF
+                  , "t = " ++ showT
+                  , "x = " ++ showX
+                  , "xs = " ++ showXS
+                  ] 
+            , lawContextReduced = reduced lhs rhs
+            }
+      in heqCtx lhs rhs ctx
+
+foldableFoldr1 ::
+  ( Foldable f
+  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
+  ) => (forall x. Gen x -> Gen (f x)) -> Property
+foldableFoldr1 fgen = property $ do
+  e <- forAll genLinearEquationTwo
+  t <- forAll $ fgen genSmallInteger
+  case unsnoc (compatToList t) of
+    Nothing -> success
+    Just (xs, x) ->
+      let f = runLinearEquationTwo e
+          lhs = Foldable.foldr1 f t
+          rhs = Foldable.foldr f x xs
+          ctx = contextualise $ LawContext
+            { lawContextLawName = "Foldr1"
+            , lawContextLawBody = "foldr1 f t" `congruency` "let (xs, x) = unsnoc (toList t) in foldr f x xs"
+            , lawContextTcName = "Foldable"
+            , lawContextTcProp =
+                let showF = show e
+                    showT = show t
+                    showX = show x
+                    showXS = show xs
+                in lawWhere
+                  [ "foldr1 f t" `congruency` "let (xs, x) = unsnoc (toList t) in foldr f x xs, where"
+                  , "f = " ++ showF
+                  , "t = " ++ showT
+                  , "x = " ++ showX
+                  , "xs = " ++ showXS
+                  ]
+            , lawContextReduced = reduced lhs rhs
+            }
+      in heqCtx lhs rhs ctx
+
+foldableToList ::
+  ( Foldable f
+  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
+  ) => (forall x. Gen x -> Gen (f x)) -> Property
+foldableToList fgen = property $ do
+  t <- forAll $ fgen genSmallInteger
+  let lhs = Foldable.toList t
+  let rhs = Foldable.foldr (:) [] t
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "ToList"
+        , lawContextLawBody = "toList" `congruency` "foldr (:) []"
+        , lawContextTcName = "Foldable"
+        , lawContextTcProp =
+            let showT = show t
+            in lawWhere
+              [ "toList t" `congruency` "foldr (:) [] t, where"
+              , "t = " ++ showT
+              ]
+        , lawContextReduced = reduced lhs rhs
+        } 
+  heqCtx lhs rhs ctx
+
+foldableNull ::
+  ( Foldable f
+  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
+  ) => (forall x. Gen x -> Gen (f x)) -> Property
+foldableNull fgen = property $ do
+  t <- forAll $ fgen genSmallInteger
+  let lhs = Foldable.null t
+  let rhs = Foldable.foldr (const (const False)) True t
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Null"
+        , lawContextLawBody = "null" `congruency` "foldr (const (const False)) True"
+        , lawContextTcName = "Foldable"
+        , lawContextTcProp =
+            let showT = show t
+            in lawWhere
+              [ "null t" `congruency` "foldr (const (const False)) True t, where"
+              , "t = " ++ showT
+              ]
+        , lawContextReduced = reduced lhs rhs
+        } 
+  heqCtx lhs rhs ctx  
+
+foldableLength ::
+  ( Foldable f
+  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
+  ) => (forall x. Gen x -> Gen (f x)) -> Property
+foldableLength fgen = property $ do
+  t <- forAll $ fgen genSmallInteger
+  let lhs = Foldable.length t
+  let rhs = getSum (Foldable.foldMap (const (Sum 1)) t)
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Length"
+        , lawContextLawBody = "length" `congruency` "getSum . foldMap (const (Sum 1))"
+        , lawContextTcName = "Foldable"
+        , lawContextTcProp =
+            let showT = show t
+            in lawWhere
+              [ "length t" `congruency` "getSum . foldMap (const (Sum 1)) $ t, where"
+              , "t = " ++ showT
+              ]
+        , lawContextReduced = reduced lhs rhs
+        }
+  heqCtx lhs rhs ctx
+
+unsnoc :: [a] -> Maybe ([a], a)
+unsnoc = \case
+  [] -> Nothing
+  [x] -> Just ([], x)
+  (x:y:xs) -> fmap (\(bs,b) -> (x:bs,b)) (unsnoc (y : xs))
+
+compatToList :: Foldable f => f a -> [a]
+compatToList = Foldable.foldMap (\x -> [x])
diff --git a/src/Hedgehog/Classes/Functor.hs b/src/Hedgehog/Classes/Functor.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Functor.hs
@@ -0,0 +1,94 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RankNTypes #-}
+
+module Hedgehog.Classes.Functor (functorLaws) where
+
+import Hedgehog
+import Hedgehog.Classes.Common
+
+-- | Tests the following 'Functor' laws:
+--
+-- [__Identity__]: @'fmap' 'id'@ ≡ @'id'@
+-- [__Composition__]: @'fmap' f '.' 'fmap' g@ ≡ @'fmap' (f '.' g)@
+-- [__Const__]: @'fmap' ('const' x)@ ≡ @x '<$'@
+functorLaws ::
+  ( Functor f
+  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
+  ) => (forall x. Gen x -> Gen (f x)) -> Laws
+functorLaws gen = Laws "Functor"
+  [ ("Identity", functorIdentity gen)
+  , ("Composition", functorComposition gen)
+  , ("Const", functorConst gen)
+  ]
+
+functorIdentity ::
+  ( Functor f
+  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
+  ) => (forall x. Gen x -> Gen (f x)) -> Property
+functorIdentity fgen = property $ do
+  a <- forAll $ fgen genSmallInteger
+  let lhs = fmap id a
+  let rhs = id a
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Identity", lawContextTcName = "Functor"
+        , lawContextLawBody = "fmap id" `congruency` "id"
+        , lawContextTcProp =
+            let showA = show a
+            in lawWhere
+              [ "fmap id a" `congruency` "id a, where"
+              , "a = " ++ showA
+              ]
+        , lawContextReduced = reduced lhs rhs
+        } 
+  heqCtx lhs rhs ctx
+
+functorComposition ::
+  ( Functor f
+  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
+  ) => (forall x. Gen x -> Gen (f x)) -> Property
+functorComposition fgen = property $ do
+  a <- forAll $ fgen genSmallInteger
+  let f = func2; g = func1 
+  let lhs = fmap f (fmap g a)
+  let rhs = fmap (f . g) a
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Composition", lawContextTcName = "Functor"
+        , lawContextLawBody = "fmap f . fmap g" `congruency` "fmap (f . g)"
+        , lawContextTcProp =
+            let showA = show a
+                showF = "\\(a,b) -> (odd a, if even a then Left (compare a b) else Right (b + 2)"
+                showG = "\\i -> (div (i + 5) 3, i * i - 2 * i + 1)"
+            in lawWhere
+              [ "fmap f . fmap g $ a" `congruency` "fmap (f . g) a, where"
+              , "f = " ++ showF
+              , "g = " ++ showG
+              , "a = " ++ showA
+              ]
+        , lawContextReduced = reduced lhs rhs
+        }
+  heqCtx lhs rhs ctx
+
+functorConst ::
+  ( Functor f
+  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
+  ) => (forall x. Gen x -> Gen (f x)) -> Property
+functorConst fgen = property $ do
+  a <- forAll $ fgen genSmallInteger
+  let x = 'X'
+  let lhs = fmap (const x) a
+  let rhs = x <$ a
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Const", lawContextTcName = "Functor"
+        , lawContextLawBody = "fmap (const x)" `congruency` "x <$"
+        , lawContextTcProp =
+            let showA = show a
+                showX = show x
+            in lawWhere
+              [ "fmap (const x) a" `congruency` "x <$ a, where"
+              , "x = " ++ showX
+              , "a = " ++ showA
+              ]
+        , lawContextReduced = reduced lhs rhs
+        }
+  heqCtx lhs rhs ctx
diff --git a/src/Hedgehog/Classes/Generic.hs b/src/Hedgehog/Classes/Generic.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Generic.hs
@@ -0,0 +1,110 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+
+module Hedgehog.Classes.Generic (genericLaws) where
+
+import Hedgehog
+import Hedgehog.Classes.Common
+
+import GHC.Generics (Generic(..))
+
+-- | Tests the following 'Generic' laws:
+--
+-- [__From-To Inverse__]: @'from' '.' 'to'@ ≡ @'id'@
+-- [__To-From Inverse__]: @'to' '.' 'from'@ ≡ @'id'@
+genericLaws ::
+  ( Generic a, Eq a, Show a
+  , Eq (Rep a x), Show (Rep a x)
+  )
+  => Gen a
+  -> Gen (Rep a x) 
+  -> Laws
+genericLaws gena genr = Laws "Generic"
+  [ ("From-To inverse", fromToInverse gena genr)
+  , ("To-From inverse", toFromInverse gena genr) 
+  ]
+
+fromToInverse :: forall a x.
+  ( Generic a
+  , Eq (Rep a x)
+  , Show (Rep a x)
+  ) => Gen a -> Gen (Rep a x) -> Property
+fromToInverse _gena genr = property $ do
+  r <- forAll genr
+  let lhs = r
+  let rhs = from (to r :: a)
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "From-To inverse", lawContextTcName = "Generic"
+        , lawContextLawBody = "from . to" `congruency` "id"
+        , lawContextTcProp =
+            let showR = show r
+            in lawWhere
+              [ "from . to $ r" `congruency` "id r, where"
+              , "r = " ++ showR
+              ]
+        , lawContextReduced = reduced lhs rhs
+        } 
+  heqCtx lhs rhs ctx
+
+toFromInverse :: forall a x.
+  ( Generic a
+  , Eq a
+  , Show a
+  ) => Gen a -> Gen (Rep a x) -> Property
+toFromInverse gena _genr = property $ do
+  v <- forAll gena
+  let lhs = to (from v)
+  let rhs = v
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "To-From inverse", lawContextTcName = "Generic"
+        , lawContextLawBody = "to . from" `congruency` "id"
+        , lawContextTcProp =
+            let showV = show v
+            in lawWhere
+              [ "to . from $ v" `congruency` "id v, where"
+              , "v = " ++ showV
+              ]
+        , lawContextReduced = reduced lhs rhs
+        } 
+  heqCtx lhs rhs ctx
+       
+{-
+type Generic1Prop f =
+  ( Generic1 f
+  , forall x. Eq x => Eq (f x)
+  , forall x. Show x => Show (f x)
+  , forall x. Eq x => Eq (Rep1 f x)
+  , forall x. Show x => Show (Rep1 f x)
+  ) => (forall x. Gen x -> Gen (f x))
+    -> (forall x. Gen x -> Gen (Rep1 f x))
+    -> Property
+
+fromToInverse1 :: forall f. Generic1Prop f
+fromToInverse1 _genf genr = property $ do
+  r <- forAll $ genr genSmallInteger
+  r === (from1 (to1 r :: f Integer))
+
+toFromInverse1 :: forall f. Generic1Prop f
+toFromInverse1 genf _genr = property $ do
+  v <- forAll $ genf genSmallInteger
+  v === (to1 . from1 $ v)
+-}
+
+{-
+generic1Laws ::
+  ( Generic1 f
+  , forall x. Eq x => Eq (f x)
+  , forall x. Show x => Show (f x)
+  , forall x. Eq x => Eq (Rep1 f x)
+  , forall x. Show x => Show (Rep1 f x)
+  ) => (forall x. Gen x -> Gen (f x))
+    -> (forall x. Gen x -> Gen (Rep1 f x))
+    -> Laws
+generic1Laws genf genr = Laws "Generic1"
+  [ ("From1-To1 inverse", fromToInverse1 genf genr)
+  , ("To1-From1 inverse", toFromInverse1 genf genr)
+  ]
+-}
diff --git a/src/Hedgehog/Classes/Integral.hs b/src/Hedgehog/Classes/Integral.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Integral.hs
@@ -0,0 +1,76 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Hedgehog.Classes.Integral (integralLaws) where
+
+import Hedgehog
+import Hedgehog.Classes.Common
+
+-- | Tests the following 'Integral' laws:
+--
+-- [__Quotient Remainder__]: @'quot' x y '*' y '+' ('rem' x y)@ ≡ @x@
+-- [__Division Modulus__]: @('div' x y) '*' y '+' ('mod' x y)@ ≡ @x@
+-- [__Integer Roundtrip__]: @'fromInteger' '.' 'toInteger'@ ≡ @'id'@
+integralLaws :: (Integral a, Show a) => Gen a -> Laws
+integralLaws gen = Laws "Integral"
+  [ ("Quotient Remainder", integralQuotientRemainder gen)
+  , ("Division Modulus", integralDivisionModulus gen)
+  , ("Integer Roundtrip", integralIntegerRoundtrip gen)
+  ]
+
+integralQuotientRemainder :: forall a. (Integral a, Show a) => Gen a -> Property
+integralQuotientRemainder gen = property $ do
+  x <- forAll gen
+  y <- forAll gen
+  let lhs = (quot x y) * y + (rem x y)
+  let rhs = x
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Quotient Remainder", lawContextTcName = "Integral"
+        , lawContextLawBody = "quot x y * y + (rem x y)" `congruency` "x"
+        , lawContextTcProp =
+            let showX = show x; showY = show y;
+            in lawWhere
+              [ "quot x y * y + (rem x y)" `congruency` "x, where"
+              , "x = " ++ showX
+              , "y = " ++ showY
+              ]
+        , lawContextReduced = reduced lhs rhs
+        }  
+  heqCtx lhs rhs ctx
+
+integralDivisionModulus :: forall a. (Integral a, Show a) => Gen a -> Property
+integralDivisionModulus gen = property $ do
+  x <- forAll gen
+  y <- forAll gen
+  let lhs = (div x y) * y + (mod x y)
+  let rhs = x
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Division Modulus", lawContextTcName = "Integral"
+        , lawContextLawBody = "(div x y) * y + (mod x y)" `congruency` "x"
+        , lawContextTcProp =
+            let showX = show x; showY = show y;
+            in lawWhere
+              [ "(div x y) * y + (mod x y)" `congruency` "x, where"
+              , "x = " ++ showX
+              , "y = " ++ showY
+              ]
+        , lawContextReduced = reduced lhs rhs
+        } 
+  heqCtx lhs rhs ctx  
+
+integralIntegerRoundtrip :: forall a. (Integral a, Show a) => Gen a -> Property
+integralIntegerRoundtrip gen = property $ do
+  x <- forAll gen
+  let lhs = fromInteger (toInteger x)
+  let rhs = x
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Integer Roundtrip", lawContextTcName = "Integral"
+        , lawContextLawBody = "fromInteger . toInteger" `congruency` "id"
+        , lawContextTcProp =
+            let showX = show x;
+            in lawWhere
+              [ "fromInteger . toInteger $ x" `congruency` "id x, where"
+              , "x = " ++ showX
+              ]
+        , lawContextReduced = reduced lhs rhs
+        }
+  heqCtx lhs rhs ctx
diff --git a/src/Hedgehog/Classes/Json.hs b/src/Hedgehog/Classes/Json.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Json.hs
@@ -0,0 +1,64 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Hedgehog.Classes.Json (jsonLaws) where
+
+import Hedgehog
+import Hedgehog.Classes.Common
+import Data.Aeson (FromJSON, ToJSON(toJSON))
+import qualified Data.Aeson as Aeson
+
+-- | Tests the following 'ToJSON' / 'FromJSON' laws:
+--
+-- [__Encoding Partial Isomorphism__]: @'Aeson.decode' '.' 'Aeson.encode'@ ≡ @'Just'@
+-- [__Encoding Equals Value__]: @'Aeson.decode' '.' 'Aeson.encode'@ ≡ @'Just' '.' 'Aeson.toJSON'@
+jsonLaws :: (FromJSON a, ToJSON a, Eq a, Show a) => Gen a -> Laws
+jsonLaws gen = Laws "ToJSON/FromJSON"
+  [ ("Partial Isomorphism", jsonEncodingPartialIsomorphism gen)
+  , ("Encoding equals value", jsonEncodingEqualsValue gen)
+  ]
+
+jsonEncodingPartialIsomorphism :: forall a. (ToJSON a, FromJSON a, Show a, Eq a) => Gen a -> Property
+jsonEncodingPartialIsomorphism gen = property $ do
+  x <- forAll gen
+  let encoded = Aeson.encode x
+  let lhs = Aeson.decode encoded
+  let rhs = Just x
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Partial Isomorphism", lawContextTcName = "ToJSON/FromJSON"
+        , lawContextLawBody = "decode . encode" `congruency` "Just"
+        , lawContextTcProp =
+            let showX = show x
+                showEncoded = show encoded
+            in lawWhere
+              [ "decode . encode $ x" `congruency` "Just x, where"
+              , "x = " ++ showX
+              , "encode x = " ++ showEncoded
+              ]
+        , lawContextReduced = reduced lhs rhs
+        }  
+  heqCtx lhs rhs ctx
+
+jsonEncodingEqualsValue :: forall a. (ToJSON a, Show a) => Gen a -> Property
+jsonEncodingEqualsValue gen = property $ do
+  x <- forAll gen
+  let encoded = Aeson.encode x
+  let decoded = Aeson.decode encoded :: Maybe Aeson.Value
+  let lhs = decoded
+  let rhs = Just (toJSON x)
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Encoding equals value", lawContextTcName = "ToJSON"
+        , lawContextLawBody = "decode . encode" `congruency` "Just . toJSON"
+        , lawContextTcProp =
+            let showX = show x
+                showEncoded = show encoded
+                showDecoded = show decoded
+            in lawWhere
+              [ "decode . encode $ x" `congruency` "Just . toJSON, where"
+              , "x = " ++ showX
+              , "encoded = " ++ showEncoded
+              , "decoded = " ++ showDecoded
+              ]
+        , lawContextReduced = reduced lhs rhs 
+        }
+  heqCtx lhs rhs ctx 
+
diff --git a/src/Hedgehog/Classes/Monad.hs b/src/Hedgehog/Classes/Monad.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Monad.hs
@@ -0,0 +1,143 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RankNTypes #-}
+
+module Hedgehog.Classes.Monad (monadLaws) where
+
+import Control.Monad (ap)
+
+import Hedgehog
+import Hedgehog.Classes.Common
+
+-- | Tests the following 'Monad' laws:
+--
+-- [__Left Identity__]: @'return' a '>>=' k@ ≡ @k a@
+-- [__Right Identity__]: @m '>>=' 'return'@ ≡ @m@
+-- [__Associativity__]: @m '>>=' (\\x -> k x '>>=' h)@ ≡ @(m '>>=' k) '>>=' h@
+-- [__Return__]: @'return'@ ≡ @'pure'@
+-- [__Ap__]: @'ap' f x@ ≡ @f '<*>' x@
+monadLaws ::
+  ( Monad f
+  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
+  ) => (forall x. Gen x -> Gen (f x)) -> Laws
+monadLaws gen = Laws "Monad"
+  [ ("Left Identity", monadLeftIdentity gen)
+  , ("Right Identity", monadRightIdentity gen)
+  , ("Associativity", monadAssociativity gen)
+  , ("Return", monadReturn gen)
+  , ("Ap", monadAp gen)
+  ]
+
+type MonadProp f =
+  ( Monad f
+  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
+  ) => (forall x. Gen x -> Gen (f x)) -> Property
+
+monadLeftIdentity :: forall f. MonadProp f
+monadLeftIdentity _ = property $ do
+  k' :: LinearEquationM f <- forAll genLinearEquationM
+  a <- forAll $ genSmallInteger
+  let k = runLinearEquationM k'
+
+  let lhs = return a >>= k
+  let rhs = k a
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Left Identity", lawContextTcName = "Monad"
+        , lawContextLawBody = "return a >>= k" `congruency` "k a"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showK = show k'
+                showA = show a
+            in lawWhere
+              [ "return a >>= k" `congruency` "k a, where"
+              , "k = " ++ showK
+              , "a = " ++ showA
+              ]
+        }
+  heqCtx1 lhs rhs ctx
+
+monadRightIdentity :: forall f. MonadProp f
+monadRightIdentity fgen = property $ do
+  m <- forAll $ fgen genSmallInteger
+  let lhs = m >>= return
+  let rhs = m
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Right Identity", lawContextTcName = "Monad"
+        , lawContextLawBody = "m >>= return" `congruency` "m"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showM = show m
+            in lawWhere
+              [ "m >>= return" `congruency` "m, where"
+              , "m = " ++ showM
+              ]
+        }  
+  heqCtx1 lhs rhs ctx
+
+monadAssociativity :: forall f. MonadProp f
+monadAssociativity fgen = property $ do
+  m <- forAll $ fgen genSmallInteger
+  k' :: LinearEquationM f <- forAll genLinearEquationM
+  h' :: LinearEquationM f <- forAll genLinearEquationM
+  let k = runLinearEquationM k'
+      h = runLinearEquationM h'
+  let lhs = m >>= (\x -> k x >>= h)
+  let rhs = (m >>= k) >>= h
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Associativity", lawContextTcName = "Monad"
+        , lawContextLawBody = "m >>= (\\x -> k x >>= h)" `congruency` "(m >>= k) >>= h"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showM = show m
+                showK = show k'
+                showH = show h'
+            in lawWhere
+              [ "m >>= (\\x -> k x >>= h)" `congruency` "(m >>= k) >>= h, where"
+              , "m = " ++ showM
+              , "k = " ++ showK
+              , "h = " ++ showH
+              ]
+        }
+  heqCtx1 lhs rhs ctx
+
+monadReturn :: forall f. MonadProp f
+monadReturn _ = property $ do
+  x <- forAll genSmallInteger
+  let lhs = return x
+  let rhs = pure x :: f Integer
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Return", lawContextTcName = "Monad"
+        , lawContextLawBody = "return" `congruency` "pure"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showX = show x
+            in lawWhere
+              [ "return x" `congruency` "pure x, where"
+              , "x = " ++ showX
+              ]
+        }  
+  heqCtx1 lhs rhs ctx
+
+monadAp :: forall f. MonadProp f
+monadAp _ = property $ do
+  f' :: f QuadraticEquation <- forAll $ pure <$> genQuadraticEquation
+  x :: f Integer <- forAll $ pure <$> genSmallInteger
+  let f = fmap runQuadraticEquation f'
+
+  let lhs = ap f x
+  let rhs = f <*> x
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Ap", lawContextTcName = "Monad"
+        , lawContextLawBody = "ap f" `congruency` "f <*>"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showX = show x
+                showF = show f'
+            in lawWhere
+              [ "ap f x" `congruency` "f <*> x, where"
+              , "f = " ++ showF 
+              , "x = " ++ showX
+              ]
+        }
+  heqCtx1 lhs rhs ctx
+
diff --git a/src/Hedgehog/Classes/MonadIO.hs b/src/Hedgehog/Classes/MonadIO.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/MonadIO.hs
@@ -0,0 +1,68 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RankNTypes #-}
+
+module Hedgehog.Classes.MonadIO (monadIOLaws) where
+
+import Control.Monad.IO.Class (MonadIO(..))
+
+import Hedgehog
+import Hedgehog.Classes.Common
+
+-- | Tests the following 'MonadIO' laws:
+--
+-- [__Return__]: @'liftIO' '.' 'return'@ ≡ @'return'@
+-- [__Lift__]: @'liftIO' (m '>>=' f)@ ≡ @'liftIO' m '>>=' ('liftIO' '.' f)@
+monadIOLaws ::
+  ( MonadIO f
+  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
+  ) => (forall x. Gen x -> Gen (f x)) -> Laws
+monadIOLaws gen = Laws "MonadIO"
+  [ ("Return", monadIOReturn gen)
+  , ("Lift", monadIOLift gen)
+  ]
+
+type MonadIOProp f =
+  ( MonadIO f
+  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
+  ) => (forall x. Gen x -> Gen (f x)) -> Property
+
+monadIOReturn :: forall f. MonadIOProp f
+monadIOReturn _fgen = property $ do
+  x <- forAll genSmallInteger
+  let lhs = liftIO (return x)
+  let rhs = return x :: f Integer
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Return", lawContextTcName = "MonadIO"
+        , lawContextLawBody = "liftIO . return" `congruency` "return"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showX = show x
+            in lawWhere
+              [ "liftIO . return $ x" `congruency` "return x, where"
+              , "x = " ++ showX
+              ]
+        }
+  heqCtx1 lhs rhs ctx
+
+monadIOLift :: forall f. MonadIOProp f
+monadIOLift _fgen = property $ do
+  m <- forAllWith showIO $ genIO genSmallInteger
+  f' <- forAll genLinearEquation
+  let f = pure . runLinearEquation f'
+  let lhs = liftIO (m >>= f) :: f Integer
+  let rhs = liftIO m >>= (liftIO . f) :: f Integer
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Lift", lawContextTcName = "MonadIO"
+        , lawContextLawBody = "liftIO (m >>= f)" `congruency` "liftIO m >>= (liftIO . f)"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showM = showIO m
+                showF = show f'
+            in lawWhere
+              [ "liftIO (m >>= f)" `congruency` "liftIO m >>= (liftIO . f), where"
+              , "f = " ++ showF
+              , "m = " ++ showM
+              ]
+        }
+  heqCtx1 lhs rhs ctx
diff --git a/src/Hedgehog/Classes/MonadPlus.hs b/src/Hedgehog/Classes/MonadPlus.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/MonadPlus.hs
@@ -0,0 +1,134 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RankNTypes #-}
+
+module Hedgehog.Classes.MonadPlus (monadPlusLaws) where
+
+import Control.Monad (MonadPlus(..))
+
+import Hedgehog
+import Hedgehog.Classes.Common
+
+-- | Tests the following 'MonadPlus' laws:
+--
+-- [__Left Identity__]: @'mplus' 'mzero'@ ≡ @'id'@
+-- [__Right Identity__]: @'flip' 'mplus' 'mzero'@ ≡ @'id'@
+-- [__Associativity__]: @'mplus' a ('mplus' b c)@ ≡ @'mplus' ('mplus' a b) c@
+-- [__Left Zero__]: @'mzero' '>>=' f@ ≡ @'mzero'@
+-- [__Right Zero__]: @v '>>' 'mzero'@ ≡ @'mzero'@
+monadPlusLaws ::
+  ( MonadPlus f
+  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
+  ) => (forall x. Gen x -> Gen (f x)) -> Laws
+monadPlusLaws gen = Laws "Monad"
+  [ ("Left Identity", monadPlusLeftIdentity gen)
+  , ("Right Identity", monadPlusRightIdentity gen)
+  , ("Associativity", monadPlusAssociativity gen)
+  , ("Left Zero", monadPlusLeftZero gen)
+  , ("Right Zero", monadPlusRightZero gen)
+  ]
+
+type MonadPlusProp f =
+  ( MonadPlus f
+  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
+  ) => (forall x. Gen x -> Gen (f x)) -> Property
+
+monadPlusLeftIdentity :: forall f. MonadPlusProp f
+monadPlusLeftIdentity fgen = property $ do
+  x <- forAll $ fgen genSmallInteger
+  let lhs = mplus mzero x
+  let rhs = x
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Left Identity", lawContextTcName = "MonadPlus"
+        , lawContextLawBody = "mplus mzero" `congruency` "id"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp  =
+            let showX = show x; showMZero = show (mzero :: f Integer);
+            in lawWhere
+              [ "mplus mzero x" `congruency` "id x, where"
+              , "x = " ++ showX
+              , "mzero = " ++ showMZero
+              ]
+        }
+  heqCtx1 lhs rhs ctx  
+
+monadPlusRightIdentity :: forall f. MonadPlusProp f
+monadPlusRightIdentity fgen = property $ do
+  x <- forAll $ fgen genSmallInteger
+  let lhs = mplus x mzero
+  let rhs = x
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Right Identity", lawContextTcName = "MonadPlus"
+        , lawContextLawBody = "flip mplus mzero" `congruency` "id"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp  =
+            let showX = show x; showMZero = show (mzero :: f Integer);
+            in lawWhere
+              [ "mplus x mzero" `congruency` "id x, where"
+              , "x = " ++ showX
+              , "mzero = " ++ showMZero
+              ]
+        } 
+  heqCtx1 lhs rhs ctx  
+
+monadPlusAssociativity :: forall f. MonadPlusProp f
+monadPlusAssociativity fgen = property $ do
+  a <- forAll $ fgen genSmallInteger
+  b <- forAll $ fgen genSmallInteger
+  c <- forAll $ fgen genSmallInteger
+  let lhs = mplus a (mplus b c)
+  let rhs = mplus (mplus a b) c
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Associativity", lawContextTcName = "MonadPlus"
+        , lawContextLawBody = "mplus a (mplus b c)" `congruency` "mplus (mplus a b) c"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showA = show a; showB = show b; showC = show c;
+            in lawWhere
+              [ "mplus a (mplus b c)" `congruency` "mplus (mplus a b) c, where"
+              , "a = " ++ showA
+              , "b = " ++ showB
+              , "c = " ++ showC
+              ]
+        }
+  heqCtx1 lhs rhs ctx 
+
+monadPlusLeftZero :: forall f. MonadPlusProp f
+monadPlusLeftZero _ = property $ do
+  k' :: LinearEquationM f <- forAll genLinearEquationM
+  let lhs = mzero >>= runLinearEquationM k'
+  let rhs = mzero
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Left Zero", lawContextTcName = "MonadPlus"
+        , lawContextLawBody = "mzero >>= f" `congruency` "mzero"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp  =
+            let showF = show k'; showMZero = show (mzero :: f Integer);
+            in lawWhere
+              [ "mzero >>= f" `congruency` "mzero, where"
+              , "f = " ++ showF
+              , "mzero = " ++ showMZero
+              ]
+        }
+  heqCtx1 lhs rhs ctx
+
+monadPlusRightZero :: forall f. MonadPlusProp f
+monadPlusRightZero fgen = property $ do
+  v <- forAll $ fgen genSmallInteger
+  let lhs = v >> (mzero :: f Integer)
+  let rhs = mzero
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Right Zero", lawContextTcName = "MonadPlus"
+        , lawContextLawBody = "v >> mzero" `congruency` "mzero"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp  =
+            let showV = show v; showMZero = show (mzero :: f Integer);
+            in lawWhere
+              [ "v >> mzero" `congruency` "mzero, where"
+              , "v = " ++ showV
+              , "mzero = " ++ showMZero
+              ]
+        } 
+  heqCtx1 lhs rhs ctx   
+
+
diff --git a/src/Hedgehog/Classes/MonadZip.hs b/src/Hedgehog/Classes/MonadZip.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/MonadZip.hs
@@ -0,0 +1,53 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RankNTypes #-}
+
+module Hedgehog.Classes.MonadZip (monadZipLaws) where
+
+import Control.Arrow (Arrow(..))
+import Control.Monad.Zip (MonadZip(mzip))
+
+import Hedgehog
+import Hedgehog.Classes.Common
+
+-- | Tests the following 'MonadZip' laws:
+--
+-- [__Naturality__]: @'fmap' (f '***' g) ('mzip' ma mb)@ ≡ @'mzip' ('fmap' f ma) ('fmap' g mb)@
+monadZipLaws ::
+  ( MonadZip f
+  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
+  ) => (forall x. Gen x -> Gen (f x)) -> Laws
+monadZipLaws gen = Laws "Monad"
+  [ ("Naturality", monadZipNaturality gen)
+  ]
+
+type MonadZipProp f =
+  ( MonadZip f
+  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
+  ) => (forall x. Gen x -> Gen (f x)) -> Property
+
+monadZipNaturality :: forall f. MonadZipProp f
+monadZipNaturality fgen = property $ do
+  f' <- forAll genLinearEquation
+  g' <- forAll genLinearEquation
+  let f = runLinearEquation f'
+      g = runLinearEquation g'
+  ma <- forAll $ fgen genSmallInteger
+  mb <- forAll $ fgen genSmallInteger
+  let lhs = fmap (f *** g) (mzip ma mb)
+  let rhs = mzip (fmap f ma) (fmap g mb)
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Naturality", lawContextTcName = "MonadZip"
+        , lawContextLawBody = "(fmap (f *** g) (mzip ma mb)" `congruency` "mzip (fmap f ma) (fmap g mb)"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showF = show f'; showG = show g'; showMA = show ma; showMB = show mb;
+            in lawWhere
+              [ "fmap (f *** g) (mzip ma mb)" `congruency` "mzip (fmap f ma) (fmap g mb), where"
+              , "f = " ++ showF
+              , "g = " ++ showG
+              , "ma = " ++ showMA  
+              , "mb = " ++ showMB
+              ]
+        }
+  heqCtx1 lhs rhs ctx
diff --git a/src/Hedgehog/Classes/Monoid.hs b/src/Hedgehog/Classes/Monoid.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Monoid.hs
@@ -0,0 +1,127 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Hedgehog.Classes.Monoid (monoidLaws, commutativeMonoidLaws) where
+
+import Hedgehog
+import Hedgehog.Classes.Common
+
+-- | Tests the following 'Monoid' laws:
+--
+-- [__Left Identity__]: @'mappend' 'mempty'@ ≡ @'id'@
+-- [__Right Identity__]: @'flip' 'mappend' 'mempty'@ ≡ @'id'@
+-- [__Associativity__]: @'mappend' a ('mappend' b c)@ ≡ @'mappend' ('mappend' a b) c@
+-- [__Concatenation__]: @'mconcat'@ ≡ @'foldr' 'mappend' 'mempty'@
+monoidLaws :: (Eq a, Monoid a, Show a) => Gen a -> Laws
+monoidLaws gen = Laws "Monoid"
+  [ ("Left Identity", monoidLeftIdentity gen)
+  , ("Right Identity", monoidRightIdentity gen)
+  , ("Associativity", monoidAssociative gen)
+  , ("Concatenation", monoidConcatenation gen)
+  ]
+
+-- | Tests the following 'Monoid' laws:
+--
+-- [__Commutativity__]: @'mappend' a b@ ≡ @'mappend' b a@
+commutativeMonoidLaws :: (Eq a, Monoid a, Show a) => Gen a -> Laws
+commutativeMonoidLaws gen = Laws "Commutative Monoid"
+  [ ("Commutativity", monoidCommutative gen)
+  ]
+
+monoidConcatenation :: forall a. (Eq a, Monoid a, Show a) => Gen a -> Property
+monoidConcatenation gen = property $ do
+  as <- forAll $ genSmallList gen
+  let lhs = mconcat as
+  let rhs = foldr mappend mempty as
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Concatenation", lawContextTcName = "Monoid"
+        , lawContextLawBody = "mconcat" `congruency` "foldr mappend mempty"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showAS = show as; showMempty = show (mempty :: a);
+            in lawWhere
+              [ "mconcat as" `congruency` "foldr mappend mempty as, where"
+              , "as = " ++ showAS
+              , "mempty = " ++ showMempty
+              ]
+        }  
+  heqCtx lhs rhs ctx
+
+monoidAssociative :: forall a. (Eq a, Monoid a, Show a) => Gen a -> Property
+monoidAssociative gen = property $ do
+  a <- forAll gen
+  b <- forAll gen
+  c <- forAll gen
+  let lhs = mappend a (mappend b c)
+  let rhs = mappend (mappend a b) c
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Associativity", lawContextTcName = "Monoid"
+        , lawContextLawBody = "mappend a (mappend b c)" `congruency` "mappend (mappend a b) c"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showA = show a; showB = show b; showC = show c;
+            in lawWhere
+              [ "mappend a (mappend b c)" `congruency` "mappend (mappend a b) c, where"
+              , "a = " ++ showA
+              , "b = " ++ showB
+              , "c = " ++ showC
+              ]
+        }
+  heqCtx lhs rhs ctx
+
+monoidLeftIdentity :: forall a. (Eq a, Monoid a, Show a) => Gen a -> Property
+monoidLeftIdentity gen = property $ do
+  a <- forAll gen
+  let lhs = mappend mempty a
+  let rhs = a
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Left Identity", lawContextTcName = "Monoid"
+        , lawContextLawBody = "mappend mempty" `congruency` "id"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showA = show a; showMempty = show (mempty :: a);
+            in lawWhere
+              [ "mappend mempty a" `congruency` "a, where"
+              , "a = " ++ showA
+              , "mempty = " ++ showMempty
+              ]
+        }
+  heqCtx lhs rhs ctx
+
+monoidRightIdentity :: forall a. (Eq a, Monoid a, Show a) => Gen a -> Property
+monoidRightIdentity gen = property $ do
+  a <- forAll gen
+  let lhs = mappend a mempty
+  let rhs = a 
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Right Identity", lawContextTcName = "Monoid"
+        , lawContextLawBody = "flip mappend mempty" `congruency` "id"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showA = show a; showMempty = show (mempty :: a);
+            in lawWhere
+              [ "mappend a mempty" `congruency` "a, where"
+              , "a = " ++ showA
+              , "mempty = " ++ showMempty
+              ]
+        }
+  heqCtx lhs rhs ctx 
+
+monoidCommutative :: forall a. (Eq a, Monoid a, Show a) => Gen a -> Property
+monoidCommutative gen = property $ do
+  a <- forAll gen
+  b <- forAll gen
+  let lhs = mappend a b
+  let rhs = mappend b a
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Commutativity", lawContextTcName = "Monoid (Commutative)"
+        , lawContextLawBody = "mappend" `congruency` "flip mappend"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showA = show a; showB = show b;
+            in lawWhere
+              [ "mappend a b" `congruency` "mappend b a, where"
+              , "a = " ++ showA
+              , "b = " ++ showB
+              ]
+        }
+  heqCtx lhs rhs ctx
diff --git a/src/Hedgehog/Classes/Ord.hs b/src/Hedgehog/Classes/Ord.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Ord.hs
@@ -0,0 +1,113 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Hedgehog.Classes.Ord (ordLaws) where
+
+import Hedgehog
+import Hedgehog.Classes.Common
+
+-- | Tests the following 'Ord' laws:
+--
+-- [__Antisymmetry__]: @@ ≡ @@
+-- [__Transitivity__]: @@ ≡ @@
+-- [__Reflexivity__]: @@ ≡ @@
+-- [__Totality__]: @@ ≡ @@
+ordLaws :: forall a. (Ord a, Show a) => Gen a -> Laws
+ordLaws gen = Laws "Ord"
+  [ ("Antisymmetry", ordAntisymmetric gen)
+  , ("Transitivity", ordTransitive gen)
+  , ("Reflexivity", ordReflexive gen)
+  , ("Totality", ordTotal gen) 
+  ]
+
+ordAntisymmetric :: forall a. (Ord a, Show a) => Gen a -> Property
+ordAntisymmetric gen = property $ do
+  a <- forAll gen
+  b <- forAll gen
+  let lhs = (a <= b) && (b <= a)
+  let rhs = a == b
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Antisymmetry", lawContextTcName = "Ord"
+        , lawContextLawBody = "x <= y && y <= x" `congruency` "x == y"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showA = show a; showB = show b;
+            in lawWhere
+              [ "x <= y && y <= x" `congruency` "x == y, where"
+              , "x = " ++ showA 
+              , "y = " ++ showB
+              ]
+        } 
+  heqCtx lhs rhs ctx
+
+ordTransitive :: forall a. (Ord a, Show a) => Gen a -> Property
+ordTransitive gen = property $ do
+  x <- forAll gen
+  y <- forAll gen
+  z <- forAll gen
+  let lhs = x <= y && y <= z
+  let rhs = x <= z
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Transitivity", lawContextTcName = "Ord"
+        , lawContextLawBody = "x <= y && y <= z" `congruency` "x <= z"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showX = show x; showY = show y; showZ = show z;
+            in lawWhere
+              [ "x <= y && y <= z" `congruency` "x <= z, where"
+              , "x = " ++ showX
+              , "y = " ++ showY
+              , "z = " ++ showZ
+              ]
+        }
+  heqCtx lhs rhs ctx
+
+{-
+  case (compare a b, compare b c) of
+    (LT,LT) -> a `hLessThan` c
+    (LT,EQ) -> a `hLessThan` c
+    (LT,GT) -> success
+    (EQ,LT) -> a `hLessThan` c
+    (EQ,EQ) -> a === c
+    (EQ,GT) -> a `hGreaterThan` c
+    (GT,LT) -> success
+    (GT,EQ) -> a `hGreaterThan` c
+    (GT,GT) -> a `hGreaterThan` c
+-}
+
+ordTotal :: forall a. (Ord a, Show a) => Gen a -> Property
+ordTotal gen = property $ do
+  a <- forAll gen
+  b <- forAll gen
+  let lhs = (a <= b) || (b <= a)
+  let rhs = True
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Totality", lawContextTcName = "Ord"
+        , lawContextLawBody = "x <= y || y <= x" `congruency` "True"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showA = show a; showB = show b;
+            in lawWhere
+              [ "(x <= y) || (y <= x)" `congruency` "True, where"
+              , "x = " ++ showA
+              , "y = " ++ showB
+              ]
+        }
+  heqCtx lhs rhs ctx
+
+ordReflexive :: forall a. (Ord a, Show a) => Gen a -> Property
+ordReflexive gen = property $ do
+  x <- forAll gen
+  let lhs = x <= x
+  let rhs = True
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Reflexivity", lawContextTcName = "Ord"
+        , lawContextLawBody = "x <= x" `congruency` "True"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showX = show x;
+            in lawWhere
+              [ "x <= x" `congruency` "True, where"
+              , "x = " ++ showX
+              ]
+        }
+  heqCtx lhs rhs ctx
diff --git a/src/Hedgehog/Classes/Semigroup.hs b/src/Hedgehog/Classes/Semigroup.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Semigroup.hs
@@ -0,0 +1,203 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Hedgehog.Classes.Semigroup
+  ( semigroupLaws
+  , commutativeSemigroupLaws
+  , exponentialSemigroupLaws
+  , idempotentSemigroupLaws
+  , rectangularBandSemigroupLaws
+  ) where
+
+import Data.Semigroup (Semigroup(..))
+import Hedgehog
+import Hedgehog.Classes.Common
+import Data.List.NonEmpty
+import qualified Hedgehog.Gen as Gen
+import qualified Hedgehog.Range as Range
+import qualified Data.Foldable as Foldable
+
+-- | Tests the following 'Semigroup' laws:
+--
+-- [__Associativity__]: @@ ≡ @@
+-- [__Concatenation__]: @@ ≡ @@
+-- [__Times__]: @@ ≡ @@
+semigroupLaws :: (Eq a, Semigroup a, Show a) => Gen a -> Laws
+semigroupLaws gen = Laws "Semigroup"
+  [ ("Associativity", semigroupAssociative gen)
+  , ("Concatenation", semigroupConcatenation gen)
+  , ("Times", semigroupTimes gen)
+  ]
+
+-- | Tests the following 'Semigroup' laws:
+--
+-- [__Commutativity__]: @@ ≡ @@
+commutativeSemigroupLaws :: (Eq a, Semigroup a, Show a) => Gen a -> Laws
+commutativeSemigroupLaws gen = Laws "Commutative Semigroup"
+  [ ("Commutative", semigroupCommutative gen)
+  ]
+
+-- | Tests the following 'Semigroup' laws:
+--
+-- [__Exponential__]: @@ ≡ @@
+exponentialSemigroupLaws :: (Eq a, Semigroup a, Show a) => Gen a -> Laws
+exponentialSemigroupLaws gen = Laws "Exponential Semigroup"
+  [ ("Exponential", semigroupExponential gen)
+  ]
+
+-- | Tests the following 'Semigroup' laws:
+--
+-- [__Idempotent__]: @@ ≡ @@
+idempotentSemigroupLaws :: (Eq a, Semigroup a, Show a) => Gen a -> Laws
+idempotentSemigroupLaws gen = Laws "Idempotent Semigroup"
+  [ ("Idempotent", semigroupIdempotent gen)
+  ]
+
+-- | Tests the following 'Semigroup' laws:
+--
+-- [__Rectangular Band__]: @@ ≡ @@
+rectangularBandSemigroupLaws :: (Eq a, Semigroup a, Show a) => Gen a -> Laws
+rectangularBandSemigroupLaws gen = Laws "Rectangular Band Semigroup"
+  [ ("Rectangular Band", semigroupRectangularBand gen)
+  ]
+
+semigroupAssociative :: forall a. (Eq a, Semigroup a, Show a) => Gen a -> Property
+semigroupAssociative gen = property $ do
+  a <- forAll gen
+  b <- forAll gen
+  c <- forAll gen
+  let lhs = a <> (b <> c)
+  let rhs = (a <> b) <> c
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Associativity", lawContextTcName = "Semigroup"
+        , lawContextLawBody = "a <> (b <> c)" `congruency` "(a <> b) <> c"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showA = show a; showB = show b; showC = show c;
+            in lawWhere
+              [ "a <> (b <> c)" `congruency` "(a <> b) <> c, where"
+              , "a = " ++ showA
+              , "b = " ++ showB
+              , "c = " ++ showC
+              ]
+        }
+  heqCtx lhs rhs ctx
+
+semigroupCommutative :: forall a. (Eq a, Semigroup a, Show a) => Gen a -> Property
+semigroupCommutative gen = property $ do
+  a <- forAll gen
+  b <- forAll gen
+  let lhs = a <> b
+  let rhs = b <> a
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Commutativity", lawContextTcName = "Semigroup"
+        , lawContextLawBody = "a <> b" `congruency` "b <> a"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showA = show a; showB = show b;
+            in lawWhere
+              [ "a <> b" `congruency` "b <> a, where"
+              , "a = " ++ showA
+              , "b = " ++ showB
+              ]
+        }  
+  heqCtx lhs rhs ctx
+
+semigroupConcatenation :: forall a. (Eq a, Semigroup a, Show a) => Gen a -> Property
+semigroupConcatenation gen = property $ do
+  a <- forAll gen 
+  as <- forAll $ genSmallList gen
+  let ne = a :| as
+  let lhs = sconcat ne
+  let rhs = Foldable.foldr1 (<>) ne
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Concatenation", lawContextTcName = "Semigroup"
+        , lawContextLawBody = "sconcat" `congruency` "foldr1 (<>)"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showNE = show ne;
+            in lawWhere
+              [ "sconcat ne" `congruency` "foldr1 (<>) ne, where"
+              , "ne = " ++ showNE
+              ]
+        }
+  heqCtx lhs rhs ctx  
+
+semigroupTimes :: forall a. (Eq a, Semigroup a, Show a) => Gen a -> Property
+semigroupTimes gen = property $ do
+  a <- forAll gen
+  n <- forAll (Gen.int Range.constantBounded)
+  let lhs = stimes n a
+  let rhs = Foldable.foldr1 (<>) (replicate n a)
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Times", lawContextTcName = "Semigroup"
+        , lawContextLawBody = "stimes" `congruency` "(foldr1 (<>) .) . replicate"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showN = show n; showA = show a;
+            in lawWhere
+              [ "stimes n a" `congruency` "foldr1 (<>) (replicate n a), where"
+              , "a = " ++ showA
+              , "n = " ++ showN
+              ]
+        }  
+  heqCtx lhs rhs ctx
+
+semigroupExponential :: forall a. (Eq a, Semigroup a, Show a) => Gen a -> Property
+semigroupExponential gen = property $ do
+  a <- forAll gen
+  b <- forAll gen
+  n <- forAll (Gen.int Range.constantBounded)
+  let lhs = stimes n (a <> b)
+  let rhs = stimes n a <> stimes n b
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Exponential", lawContextTcName = "Semigroup"
+        , lawContextLawBody = "stimes n (a <> b)" `congruency` "stimes n a <> stimes n b"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showN = show n; showA = show a; showB = show b;
+            in lawWhere
+              [ "stimes n (a <> b)" `congruency` "stimes n a <> stimes n b, where"
+              , "a = " ++ showA
+              , "b = " ++ showB
+              , "n = " ++ showN
+              ]
+        }  
+  heqCtx lhs rhs ctx
+
+semigroupIdempotent :: forall a. (Eq a, Semigroup a, Show a) => Gen a -> Property
+semigroupIdempotent gen = property $ do
+  a <- forAll gen
+  let lhs = a <> a
+  let rhs = a
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Idempotency", lawContextTcName = "Semigroup"
+        , lawContextLawBody = "a <> a" `congruency` "a"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showA = show a;
+            in lawWhere
+              [ "a <> a" `congruency` "a, where"
+              , "a = " ++ showA
+              ]
+        }
+  heqCtx lhs rhs ctx
+
+semigroupRectangularBand :: forall a. (Eq a, Semigroup a, Show a) => Gen a -> Property
+semigroupRectangularBand gen = property $ do
+  a <- forAll gen
+  b <- forAll gen
+  let lhs = a <> b <> a
+  let rhs = a
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Rectangular Band", lawContextTcName = "Semigroup"
+        , lawContextLawBody = "a <> b <> a" `congruency` "a"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showA = show a; showB = show b;
+            in lawWhere
+              [ "a <> b <> a" `congruency` "a, where"
+              , "a = " ++ showA
+              , "b = " ++ showB
+              ]
+        }  
+  heqCtx lhs rhs ctx
diff --git a/src/Hedgehog/Classes/Show.hs b/src/Hedgehog/Classes/Show.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Show.hs
@@ -0,0 +1,82 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Hedgehog.Classes.Show (showLaws) where
+
+import Hedgehog
+import Hedgehog.Classes.Common
+
+-- | Tests the following 'Show' laws:
+--
+-- [__ __]: @@ ≡ @@
+-- [__ __]: @@ ≡ @@
+-- [__ __]: @@ ≡ @@
+showLaws :: (Show a) => Gen a -> Laws
+showLaws gen = Laws "Show"
+  [ ("Show", showShowsPrecZero gen)
+  , ("Equivariance: showsPrec", equivarianceShowsPrec gen)
+  , ("Equivariance: showList", equivarianceShowList gen)
+  ]
+
+showShowsPrecZero :: forall a. (Show a) => Gen a -> Property
+showShowsPrecZero gen = property $ do
+  a <- forAll gen
+  let lhs = show a
+  let rhs = showsPrec 0 a ""
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "ShowsPrec Zero", lawContextTcName = "Show"
+        , lawContextLawBody = "show a" `congruency` "showsPrec 0 a \"\""
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showA = show a;
+            in lawWhere
+              [ "show a" `congruency` "showsPrec 0 a \"\", where"
+              , "a = " ++ showA
+              ]
+        }  
+  heqCtx lhs rhs ctx
+
+equivarianceShowsPrec :: forall a. (Show a) => Gen a -> Property
+equivarianceShowsPrec gen = property $ do
+  p <- forAll genShowReadPrecedence
+  a <- forAll gen
+  r <- forAll genSmallString
+  s <- forAll genSmallString
+  let lhs = showsPrec p a r ++ s
+  let rhs = showsPrec p a (r ++ s)
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "ShowsPrec Equivariance", lawContextTcName = "Show"
+        , lawContextLawBody = "showsPrec p a r ++ s" `congruency` "showsPrec p a (r ++ s)"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showP = show p; showA = show a; showR = show r; showS = show s;
+            in lawWhere
+              [ "showsPrec p a r ++ s" `congruency` "showsPrec p a (r ++ s), where"
+              , "p = " ++ showP
+              , "a = " ++ showA
+              , "r = " ++ showR
+              , "s = " ++ showS
+              ]
+        }  
+  heqCtx lhs rhs ctx
+
+equivarianceShowList :: forall a. (Show a) => Gen a -> Property
+equivarianceShowList gen = property $ do
+  as <- forAll $ genSmallList gen
+  r <- forAll genSmallString
+  s <- forAll genSmallString
+  let lhs = showList as r ++ s
+  let rhs = showList as (r ++ s)
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "ShowList Equivariance", lawContextTcName = "Show"
+        , lawContextLawBody = "showList as r ++ s" `congruency` "showList as (r ++ s)"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showAS = show as; showR = show r; showS = show s;
+            in lawWhere
+              [ "showList as r ++ s" `congruency` "showList as (r ++ s), where"
+              , "as = " ++ showAS
+              , "r = " ++ showR
+              , "s = " ++ showS
+              ]
+        }  
+  heqCtx lhs rhs ctx
diff --git a/src/Hedgehog/Classes/ShowRead.hs b/src/Hedgehog/Classes/ShowRead.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/ShowRead.hs
@@ -0,0 +1,116 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Hedgehog.Classes.ShowRead (showReadLaws) where
+
+import Hedgehog
+import Hedgehog.Classes.Common
+
+import Text.Read (readListDefault, readMaybe)
+import Text.Show (showListWith)
+
+-- | Tests the following 'Show' / 'Read' laws:
+--
+-- [__ __]: @@ ≡ @@
+-- [__ __]: @@ ≡ @@
+-- [__ __]: @@ ≡ @@
+showReadLaws :: (Eq a, Read a, Show a) => Gen a -> Laws
+showReadLaws gen = Laws "Show/Read"
+  [ ("Partial Isomorphism: show/read", showReadPartialIsomorphism gen)
+  , ("Partial Isomorphism: show/read with initial space", showReadSpacePartialIsomorphism gen)
+  , ("Partial Isomorphism: showsPrec/readsPrec", showsPrecReadsPrecPartialIsomorphism gen)
+  , ("Partial Isomorphism: showList/readList", showListReadListPartialIsomorphism gen)
+  , ("Partial Isomorphism: showListWith shows / readListDefault", showListWithShowsReadListDefaultPartialIsomorphism gen)
+  ]
+
+showReadPartialIsomorphism :: forall a. (Eq a, Read a, Show a) => Gen a -> Property
+showReadPartialIsomorphism gen = property $ do
+  a <- forAll gen
+  let lhs = readMaybe (show a)
+  let rhs = Just a
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Show/Read Partial Isomorphism", lawContextTcName = "Show/Read"
+        , lawContextLawBody = "readMaybe . show" `congruency` "Just"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showA = show a;
+            in lawWhere
+              [ "readMaybe . show $ a" `congruency` "Just a, where"
+              , "a = " ++ showA
+              ]
+        } 
+  heqCtx lhs rhs ctx
+
+showReadSpacePartialIsomorphism :: forall a. (Eq a, Read a, Show a) => Gen a -> Property
+showReadSpacePartialIsomorphism gen = property $ do
+  a <- forAll gen
+  let lhs = readMaybe (" " ++ show a)
+  let rhs = Just a
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "Show/Read Partial Isomorphism With Initial Space", lawContextTcName = "Show/Read"
+        , lawContextLawBody = "readMaybe . (\" \" ++ show)" `congruency` "Just"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showA = show a;
+            in lawWhere
+              [ "readMaybe . (\" \" ++ show) $ a" `congruency` "Just a, where"
+              , "a = " ++ showA
+              ]
+        }
+  heqCtx lhs rhs ctx
+
+showsPrecReadsPrecPartialIsomorphism :: forall a. (Eq a, Read a, Show a) => Gen a -> Property
+showsPrecReadsPrecPartialIsomorphism gen = property $ do
+  a <- forAll gen
+  p <- forAll genShowReadPrecedence
+  let lhs = (a,"") `elem` readsPrec p (showsPrec p a "")
+  let rhs = True
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "ShowsPrec/ReadsPrec partial isomorphism", lawContextTcName = "Show/Read"
+        , lawContextLawBody = "(a,\"\") `elem` readsPrec p (showsPrec p a \"\")" `congruency` "True"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showA = show a; showP = show p
+            in lawWhere
+              [ "(a,\"\") `elem` readsPrec p (showsPrec p a \"\")" `congruency` "True, where"
+              , "a = " ++ showA
+              , "p = " ++ showP
+              ]
+        }  
+  heqCtx lhs rhs ctx
+
+showListReadListPartialIsomorphism :: forall a. (Eq a, Read a, Show a) => Gen a -> Property
+showListReadListPartialIsomorphism gen = property $ do
+  as <- forAll $ genSmallList gen
+  let lhs = (as,"") `elem` readList (showList as "")
+  let rhs = True
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "ShowsList/ReadsList partial isomorphism", lawContextTcName = "Show/Read"
+        , lawContextLawBody = "(as,\"\") `elem` readList (showList as \"\")" `congruency` "True"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showAS = show as
+            in lawWhere
+              [ "(as,\"\") `elem` readList (showList as \"\")" `congruency` "True, where"
+              , "as = " ++ showAS
+              ]
+        }  
+  heqCtx lhs rhs ctx
+ 
+showListWithShowsReadListDefaultPartialIsomorphism :: forall a. (Eq a, Read a, Show a) => Gen a -> Property
+showListWithShowsReadListDefaultPartialIsomorphism gen = property $ do
+  as <- forAll $ genSmallList gen
+  let lhs = (as,"") `elem` readListDefault (showListWith shows as "")
+  let rhs = True
+  let ctx = contextualise $ LawContext
+        { lawContextLawName = "ShowListWith/ReadListDefault partial isomorphism", lawContextTcName = "Show/Read"
+        , lawContextLawBody = "(as,\"\") `elem` readListDefault (showListWith shows as \"\")" `congruency` "True"
+        , lawContextReduced = reduced lhs rhs
+        , lawContextTcProp =
+            let showAS = show as
+            in lawWhere
+              [ "(as,\"\") `elem` readListDefault (showListWith shows as \"\")" `congruency` "True, where"
+              , "as = " ++ showAS 
+              ]
+        } 
+  heqCtx lhs rhs ctx
+
diff --git a/src/Hedgehog/Classes/Storable.hs b/src/Hedgehog/Classes/Storable.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Storable.hs
@@ -0,0 +1,150 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Hedgehog.Classes.Storable (storableLaws) where
+
+import Hedgehog
+import Hedgehog.Classes.Common
+import Hedgehog.Internal.Gen (sample)
+
+import qualified Data.List as List
+import qualified Hedgehog.Gen as Gen
+import qualified Hedgehog.Range as Range
+
+import Foreign.Marshal.Alloc
+import Foreign.Marshal.Array
+import GHC.Ptr (Ptr(..), plusPtr)
+import Foreign.Storable (Storable(..))
+import System.IO.Unsafe (unsafePerformIO)
+
+-- | Tests the following 'Storable' laws:
+--
+-- [__ __]: @@ ≡ @@
+-- [__ __]: @@ ≡ @@
+-- [__ __]: @@ ≡ @@
+storableLaws :: (Eq a, Show a, Storable a) => Gen a -> Laws
+storableLaws gen = Laws "Storable"
+  [ ("Set-Get (you get back what you put in)", storableSetGet gen)
+  , ("Get-Set (putting back what you got out has no effect)", storableGetSet gen)
+  , ("List Conversion Roundtrips", storableList gen)
+  , ("peekElemOff a i ≡ peek (plusPtr a (i * sizeOf undefined))", storablePeekElem gen)
+  , ("peekElemOff a i x ≡ poke (plusPtr a (i * sizeOf undefined)) x ≡ id ", storablePokeElem gen)
+  , ("peekByteOff a i ≡ peek (plusPtr a i)", storablePeekByte gen)
+  , ("peekByteOff a i x ≡ poke (plusPtr a i) x ≡ id ", storablePokeByte gen)
+  ]
+
+genArray :: forall a. (Storable a) => Gen a -> Int -> IO (Ptr a)
+genArray gen len = do
+  let go ix xs = if ix == len
+        then pure xs
+        else do
+          x <- sample gen
+          go (ix + 1) (x : xs)
+  as <- go 0 []
+  newArray as
+
+storablePeekElem :: forall a. (Eq a, Show a, Storable a) => Gen a -> Property
+storablePeekElem gen = property $ do
+  as <- forAll $ genSmallNonEmptyList gen
+  let len = List.length as
+  ix <- forAll $ Gen.int (Range.linear 0 (len - 1))
+  unsafePerformIO $ do
+    addr <- genArray gen len
+    x <- peekElemOff addr ix
+    y <- peek (addr `plusPtr` (ix * sizeOf (undefined :: a)))
+    free addr
+    pure (x === y)
+
+storablePokeElem :: forall a. (Eq a, Show a, Storable a) => Gen a -> Property
+storablePokeElem gen = property $ do
+  as <- forAll $ genSmallNonEmptyList gen
+  x <- forAll gen
+  let len = List.length as
+  ix <- forAll $ Gen.int (Range.linear 0 (len - 1))
+  unsafePerformIO $ do
+    addr <- genArray gen len
+    pokeElemOff addr ix x
+    u <- peekElemOff addr ix
+    poke (addr `plusPtr` (ix * sizeOf x)) x
+    v <- peekElemOff addr ix
+    free addr
+    pure (u === v)
+
+storablePeekByte :: forall a. (Eq a, Show a, Storable a) => Gen a -> Property
+storablePeekByte gen = property $ do
+  as <- forAll $ genSmallNonEmptyList gen
+  let len = List.length as
+  off <- forAll $ Gen.int (Range.linear 0 (len - 1))
+  unsafePerformIO $ do
+    addr <- genArray gen len
+    x :: a <- peekByteOff addr off
+    y :: a <- peek (addr `plusPtr` off)
+    free addr
+    pure (x === y)
+
+storablePokeByte :: forall a. (Eq a, Show a, Storable a) => Gen a -> Property
+storablePokeByte gen = property $ do
+  as <- forAll $ genSmallNonEmptyList gen
+  x <- forAll gen
+  let len = List.length as
+  off <- forAll $ Gen.int (Range.linear 0 (len - 1))
+  unsafePerformIO $ do
+    addr <- genArray gen len
+    pokeByteOff addr off x
+    u :: a <- peekByteOff addr off
+    poke (addr `plusPtr` off) x
+    v :: a <- peekByteOff addr off
+    free addr
+    pure (u === v)
+
+storableSetGet :: forall a. (Eq a, Show a, Storable a) => Gen a -> Property
+storableSetGet gen = property $ do
+  a <- forAll gen
+  len <- forAll $ Gen.int (Range.linear 0 20)
+  ix <- forAll $ Gen.int (Range.linear 0 (len - 1))
+  unsafePerformIO $ do
+    ptr <- genArray gen len
+    pokeElemOff ptr ix a
+    a' <- peekElemOff ptr ix
+    free ptr
+    pure (a === a')
+
+storableGetSet :: forall a. (Eq a, Show a, Storable a) => Gen a -> Property
+storableGetSet gen = property $ do
+  as <- forAll $ genSmallNonEmptyList gen
+  let len = List.length as
+  ix <- forAll $ Gen.int (Range.linear 0 (len - 1))
+  unsafePerformIO $ do
+    ptrA <- newArray as
+    ptrB <- genArray gen len
+    copyArray ptrB ptrA len
+    a <- peekElemOff ptrA ix
+    pokeElemOff ptrA ix a
+    res <- arrayEq ptrA ptrB len
+    free ptrA
+    free ptrB
+    pure (res === True)
+
+storableList :: forall a. (Eq a, Show a, Storable a) => Gen a -> Property
+storableList gen = property $ do
+  as <- forAll $ genSmallNonEmptyList gen 
+  unsafePerformIO $ do
+    let len = List.length as
+    ptr <- newArray as
+    let rebuild :: Int -> IO [a]
+        rebuild ix = if ix < len
+          then (:) <$> peekElemOff ptr ix <*> rebuild (ix + 1)
+          else pure []
+    asNew <- rebuild 0
+    free ptr
+    pure (as === asNew)
+
+arrayEq :: forall a. (Eq a, Storable a) => Ptr a -> Ptr a -> Int -> IO Bool
+arrayEq ptrA ptrB len = go 0 where
+  go i = if i < len
+    then do
+      a <- peekElemOff ptrA i
+      b <- peekElemOff ptrB i
+      if a == b
+        then go (i + 1)
+        else pure False
+    else pure True
diff --git a/src/Hedgehog/Classes/Traversable.hs b/src/Hedgehog/Classes/Traversable.hs
new file mode 100644
--- /dev/null
+++ b/src/Hedgehog/Classes/Traversable.hs
@@ -0,0 +1,88 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE LambdaCase #-}
+
+module Hedgehog.Classes.Traversable (traversableLaws) where
+
+import Hedgehog
+import Hedgehog.Classes.Common
+
+import Data.Functor.Identity
+import Data.Functor.Compose
+import Data.Traversable (Traversable(..), foldMapDefault, fmapDefault)
+
+-- | Tests the following 'Traversable' laws:
+--
+-- [__Naturality__]: @t '.' 'traverse' f@ ≡ @'traverse' (t '.' f), for every applicative transformation t@
+-- [__Identity__]: @'traverse' 'Identity'@ ≡ @'Identity'@
+-- [__Composition__]: @'traverse' ('Compose' '.' 'fmap' g '.' f)@ ≡ @'Compose' '.' 'fmap' ('traverse' g) '.' 'traverse' f@
+-- [__SequenceA Naturality__]: @t '.' 'sequenceA'@ ≡ @'sequenceA' '.' 'fmap' t, for every applicative transformation t@
+-- [__SequenceA Identity__]: @'sequenceA' '.' 'fmap' 'Identity'@ ≡ @'Identity'@
+-- [__SequenceA Composition__]: @'sequenceA' '.' 'fmap' 'Compose'@ ≡ @'Compose' '.' 'fmap' 'sequenceA' '.' 'sequenceA'@
+-- [__FoldMap__]: @'foldMap'@ ≡ @'foldMapDefault'@
+-- [__Fmap__]: @'fmap'@ ≡ @'fmapDefault'@
+traversableLaws ::
+  ( Traversable f
+  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
+  ) => (forall x. Gen x -> Gen (f x)) -> Laws
+traversableLaws gen = Laws "Foldable"
+  [ ("Naturality", traversableNaturality gen)
+  , ("Identity", traversableIdentity gen)
+  , ("Composition", traversableComposition gen)
+  , ("Sequence Naturality", traversableSequenceNaturality gen)
+  , ("Sequence Identity", traversableSequenceIdentity gen)
+  , ("Sequence Composition", traversableSequenceComposition gen)
+  , ("foldMap", traversableFoldMap gen)
+  , ("fmap", traversableFmap gen)
+  ]
+
+type TraversableProp f =
+  ( Traversable f
+  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
+  ) => (forall x. Gen x -> Gen (f x)) -> Property
+
+traversableNaturality :: TraversableProp f
+traversableNaturality fgen = property $ do
+  a <- forAll $ fgen genSmallInteger
+  (apTrans (traverse func4 a)) `heq1` (traverse (apTrans . func4) a)
+
+traversableIdentity :: TraversableProp f
+traversableIdentity fgen = property $ do
+  t <- forAll $ fgen genSmallInteger
+  (traverse Identity t) `heq1` (Identity t)
+
+traversableComposition :: TraversableProp f
+traversableComposition fgen = property $ do
+  t <- forAll $ fgen genSmallInteger 
+  let lhs = (traverse (Compose . fmap func5 . func6) t)
+  let rhs = (Compose (fmap (traverse func5) (traverse func6 t)))
+  lhs `heq1` rhs
+
+traversableSequenceNaturality :: TraversableProp f
+traversableSequenceNaturality fgen = property $ do
+  x <- forAll $ fgen (genCompose genSmallInteger genTriple (genTuple genSetInteger))
+  let a = fmap toSpecialApplicative x
+  (apTrans (sequenceA a)) `heq1` (sequenceA (fmap apTrans a)) 
+
+traversableSequenceIdentity :: TraversableProp f
+traversableSequenceIdentity fgen = property $ do
+  t <- forAll $ fgen genSmallInteger
+  (sequenceA (fmap Identity t)) `heq1` (Identity t)
+
+traversableSequenceComposition :: TraversableProp f
+traversableSequenceComposition fgen = property $ do
+  let genTripleInteger = genTriple genSmallInteger
+  t <- forAll $ fgen (genTriple genTripleInteger)
+  (sequenceA (fmap Compose t)) `heq1` (Compose (fmap sequenceA (sequenceA t)))
+
+traversableFoldMap :: TraversableProp f
+traversableFoldMap fgen = property $ do
+  t <- forAll $ fgen genSmallInteger
+  foldMap func3 t `heq1` foldMapDefault func3 t  
+
+traversableFmap :: TraversableProp f
+traversableFmap fgen = property $ do
+  t <- forAll $ fgen genSmallInteger
+  fmap func3 t `heq1` fmapDefault func3 t
+