diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 74492dd..c14c8a6 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -24,7 +24,7 @@ jobs:
           ghc-version: ${{ matrix.ghc }}
           cabal-version: 'latest'
       - name: Configure
-        run: cabal new-configure
+        run: cabal new-configure --enable-tests
       - name: Freeze
         run: cabal freeze
       - name: Cache
@@ -35,3 +35,5 @@ jobs:
           restore-keys: ${{ runner.os }}-${{ matrix.ghc }}-
       - name: Build
         run: cabal build
+      - name: Run tests
+        run: cabal test
diff --git a/Control/Monad/Accum.hs b/Control/Monad/Accum.hs
index 7be9140..5a019a2 100644
--- a/Control/Monad/Accum.hs
+++ b/Control/Monad/Accum.hs
@@ -140,7 +140,7 @@ import Data.Kind (Type)
 -- These are also the default definitions.
 --
 -- 1. @'look'@ @=@ @'accum' '$' \acc -> (acc, mempty)@
--- 2. @'add' x@ @=@ @'accum' '$' \acc -> ('()', x)@
+-- 2. @'add' x@ @=@ @'accum' '$' \_ -> ('()', x)@
 -- 3. @'accum' f@ @=@ @'look' >>= \acc -> let (res, v) = f acc in 'add' v '$>' res@
 --
 -- @since 2.3
diff --git a/cabal.project b/cabal.project
index f243510..f419e1b 100644
--- a/cabal.project
+++ b/cabal.project
@@ -1,4 +1,6 @@
 packages: ./mtl.cabal
 
+test-show-details: direct
+
 package mtl
   ghc-options: -Werror
diff --git a/mtl.cabal b/mtl.cabal
index 6174624..d9d56a8 100644
--- a/mtl.cabal
+++ b/mtl.cabal
@@ -28,7 +28,18 @@ source-repository head
   type: git
   location: https://github.com/haskell/mtl.git
 
+common common-lang
+  build-depends: 
+    , base >= 4.12 && < 5
+    , transformers >= 0.5.6 && < 0.7
+  ghc-options:
+    -Wall -Wcompat -Wincomplete-record-updates
+    -Wincomplete-uni-patterns -Wredundant-constraints
+    -Wmissing-export-lists
+  default-language: Haskell2010
+
 Library
+  import: common-lang
   exposed-modules:
     Control.Monad.Cont
     Control.Monad.Cont.Class
@@ -54,14 +65,18 @@ Library
     Control.Monad.Writer.Strict
     Control.Monad.Accum
     Control.Monad.Select
+  
+test-suite properties
+  import: common-lang
+  type: exitcode-stdio-1.0
+  main-is: Main.hs
+  other-modules: Accum
+  build-depends: 
+    , mtl
+    , QuickCheck ^>= 2.14.0
+    , tasty ^>= 1.4.0.0
+    , tasty-quickcheck ^>= 0.10.0
+    , pretty-show ^>= 1.10
 
-  build-depends:
-    , base >=4.12 && < 5
-    , transformers >= 0.5.6 && <0.7
-
-  ghc-options:
-    -Wall -Wcompat -Wincomplete-record-updates
-    -Wincomplete-uni-patterns -Wredundant-constraints
-    -Wmissing-export-lists
-
-  default-language: Haskell2010
+  hs-source-dirs: test/properties
+  ghc-options: -O2 -threaded -rtsopts -with-rtsopts=-N
diff --git a/test/properties/Accum.hs b/test/properties/Accum.hs
new file mode 100644
index 0000000..33698bc
--- /dev/null
+++ b/test/properties/Accum.hs
@@ -0,0 +1,307 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE DerivingVia #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Accum
+  ( M (..),
+    N (..),
+    AccumArb (..),
+    accumLaws,
+    accumLawsCont,
+    accumLawsSelect,
+  )
+where
+
+import Control.Monad (guard)
+import Control.Monad.Accum (MonadAccum (accum, add, look))
+import Data.Functor (($>))
+import Data.Kind (Type)
+import Test.QuickCheck
+  ( Arbitrary (arbitrary, shrink),
+    Blind (Blind),
+    CoArbitrary (coarbitrary),
+    Property,
+    chooseInt,
+    forAllShrinkShow,
+    property,
+    shrinkList,
+    sized,
+    (===),
+  )
+import Test.QuickCheck.Poly (A, B)
+import Test.Tasty (TestTree)
+import Test.Tasty.QuickCheck (testProperties)
+import Text.Show.Pretty (ppShow)
+import Type.Reflection
+  ( Typeable,
+    tyConModule,
+    tyConName,
+    typeRep,
+    typeRepTyCon,
+  )
+
+newtype M = M [Int]
+  deriving (Eq, Semigroup, Monoid) via [Int]
+  deriving stock (Show)
+
+instance Arbitrary M where
+  arbitrary = M . pure <$> sized (\size -> chooseInt (0, abs size))
+  shrink (M xs) =
+    M <$> do
+      xs' <- shrinkList (const []) xs
+      guard (not . null $ xs')
+      pure xs'
+
+instance CoArbitrary M where
+  coarbitrary (M xs) = coarbitrary xs
+
+newtype N = N M
+  deriving (Eq, Semigroup, Monoid, Arbitrary) via M
+  deriving stock (Show)
+
+newtype AccumArb (w :: Type) (a :: Type)
+  = AccumArb (w -> (a, w))
+  deriving (Arbitrary) via (w -> (a, w))
+
+runAccumArb :: AccumArb w a -> w -> (a, w)
+runAccumArb (AccumArb f) = f
+
+accumLawsSelect ::
+  forall (m :: Type -> Type) (t :: Type).
+  (MonadAccum M m, Typeable m, Arbitrary t, Show t) =>
+  (forall (a :: Type). t -> m a -> (a -> AccumArb M B) -> AccumArb M a) ->
+  TestTree
+accumLawsSelect lowerSelect =
+  testProperties
+    testName
+    [ ("look *> look = look", lookLookProp),
+      ("add mempty = pure ()", addMemptyProp),
+      ("add x *> add y = add (x <> y)", addAddProp),
+      ("add x *> look = look >>= \\w -> add x $> w <> x", addLookProp),
+      ("accum (const (x, mempty)) = pure x", accumPureProp),
+      ("accum f *> accum g law (too long)", accumFGProp),
+      ("look = accum $ \\acc -> (acc, mempty)", lookAccumProp),
+      ("add x = accum $ \\acc -> ((), x)", addAccumProp),
+      ("accum f = look >>= \\acc -> let (res, v) = f acc in add v $> res", accumAddProp)
+    ]
+  where
+    testName :: String
+    testName = "MonadAccum laws for " <> typeName @(m A)
+    addAccumProp :: Property
+    addAccumProp = theNeedful $ \(w, arg, x, Blind f) ->
+      let lhs = lowerSelect arg (add x) f
+          rhs = lowerSelect arg (accum $ const ((), x)) f
+       in runAccumArb lhs w === runAccumArb rhs w
+    accumAddProp :: Property
+    accumAddProp = theNeedful $ \(w, arg, Blind (f :: M -> (A, M)), Blind g) ->
+      let lhs = lowerSelect arg (accum f) g
+          rhs = lowerSelect arg (look >>= \acc -> let (res, v) = f acc in add v $> res) g
+       in runAccumArb lhs w === runAccumArb rhs w
+    lookAccumProp :: Property
+    lookAccumProp = theNeedful $ \(w, arg, Blind f) ->
+      let lhs = lowerSelect arg look f
+          rhs = lowerSelect arg (accum (,mempty)) f
+       in runAccumArb lhs w === runAccumArb rhs w
+    lookLookProp :: Property
+    lookLookProp = theNeedful $ \(w, arg, Blind f) ->
+      let lhs = lowerSelect arg look f
+          rhs = lowerSelect arg (look *> look) f
+       in runAccumArb lhs w === runAccumArb rhs w
+    addMemptyProp :: Property
+    addMemptyProp = theNeedful $ \(w, arg, Blind f) ->
+      let lhs = lowerSelect arg (add mempty) f
+          rhs = lowerSelect arg (pure ()) f
+       in runAccumArb lhs w === runAccumArb rhs w
+    addAddProp :: Property
+    addAddProp = theNeedful $ \(w, arg, x, y, Blind f) ->
+      let lhs = lowerSelect arg (add x *> add y) f
+          rhs = lowerSelect arg (add (x <> y)) f
+       in runAccumArb lhs w === runAccumArb rhs w
+    addLookProp :: Property
+    addLookProp = theNeedful $ \(w, arg, x, Blind f) ->
+      let lhs = lowerSelect arg (add x *> look) f
+          rhs = lowerSelect arg (look >>= \w' -> add x $> w' <> x) f
+       in runAccumArb lhs w === runAccumArb rhs w
+    accumPureProp :: Property
+    accumPureProp = theNeedful $ \(w, arg, x :: A, Blind f) ->
+      let lhs = lowerSelect arg (accum (const (x, mempty))) f
+          rhs = lowerSelect arg (pure x) f
+       in runAccumArb lhs w === runAccumArb rhs w
+    accumFGProp :: Property
+    accumFGProp = theNeedful $ \(w', arg, Blind (f :: M -> (A, M)), Blind (g :: M -> (M, M)), Blind h) ->
+      let lhs = lowerSelect arg (accum f *> accum g) h
+          rhs =
+            lowerSelect
+              arg
+              ( accum $ \acc ->
+                  let (_, v) = f acc
+                      (res, w) = g (acc <> v)
+                   in (res, v <> w)
+              )
+              h
+       in runAccumArb lhs w' === runAccumArb rhs w'
+
+accumLawsCont ::
+  forall (m :: Type -> Type) (t :: Type).
+  (MonadAccum M m, Typeable m, Arbitrary t, Show t) =>
+  (forall (a :: Type). t -> m a -> (a -> AccumArb M B) -> AccumArb M B) ->
+  TestTree
+accumLawsCont lowerCont =
+  testProperties
+    testName
+    [ ("look *> look = look", lookLookProp),
+      ("add mempty = pure ()", addMemptyProp),
+      ("add x *> add y = add (x <> y)", addAddProp),
+      ("add x *> look = look >>= \\w -> add x $> w <> x", addLookProp),
+      ("accum (const (x, mempty)) = pure x", accumPureProp),
+      ("accum f *> accum g law (too long)", accumFGProp),
+      ("look = accum $ \\acc -> (acc, mempty)", lookAccumProp),
+      ("add x = accum $ \\acc -> ((), x)", addAccumProp),
+      ("accum f = look >>= \\acc -> let (res, v) = f acc in add v $> res", accumAddProp)
+    ]
+  where
+    testName :: String
+    testName = "MonadAccum laws for " <> typeName @(m A)
+    addAccumProp :: Property
+    addAccumProp = theNeedful $ \(w, arg, x, Blind f) ->
+      let lhs = lowerCont arg (add x) f
+          rhs = lowerCont arg (accum $ const ((), x)) f
+       in runAccumArb lhs w === runAccumArb rhs w
+    accumAddProp :: Property
+    accumAddProp = theNeedful $ \(w, arg, Blind (f :: M -> (A, M)), Blind g) ->
+      let lhs = lowerCont arg (accum f) g
+          rhs = lowerCont arg (look >>= \acc -> let (res, v) = f acc in add v $> res) g
+       in runAccumArb lhs w === runAccumArb rhs w
+    lookAccumProp :: Property
+    lookAccumProp = theNeedful $ \(w, arg, Blind f) ->
+      let lhs = lowerCont arg look f
+          rhs = lowerCont arg (accum (,mempty)) f
+       in runAccumArb lhs w === runAccumArb rhs w
+    lookLookProp :: Property
+    lookLookProp = theNeedful $ \(w, arg, Blind f) ->
+      let lhs = lowerCont arg look f
+          rhs = lowerCont arg (look *> look) f
+       in runAccumArb lhs w === runAccumArb rhs w
+    addMemptyProp :: Property
+    addMemptyProp = theNeedful $ \(w, arg, Blind f) ->
+      let lhs = lowerCont arg (add mempty) f
+          rhs = lowerCont arg (pure ()) f
+       in runAccumArb lhs w === runAccumArb rhs w
+    addAddProp :: Property
+    addAddProp = theNeedful $ \(w, arg, x, y, Blind f) ->
+      let lhs = lowerCont arg (add x *> add y) f
+          rhs = lowerCont arg (add (x <> y)) f
+       in runAccumArb lhs w === runAccumArb rhs w
+    addLookProp :: Property
+    addLookProp = theNeedful $ \(w, arg, x, Blind f) ->
+      let lhs = lowerCont arg (add x *> look) f
+          rhs = lowerCont arg (look >>= \w' -> add x $> w' <> x) f
+       in runAccumArb lhs w === runAccumArb rhs w
+    accumPureProp :: Property
+    accumPureProp = theNeedful $ \(w, arg, x :: A, Blind f) ->
+      let lhs = lowerCont arg (accum (const (x, mempty))) f
+          rhs = lowerCont arg (pure x) f
+       in runAccumArb lhs w === runAccumArb rhs w
+    accumFGProp :: Property
+    accumFGProp = theNeedful $ \(w', arg, Blind (f :: M -> (A, M)), Blind (g :: M -> (M, M)), Blind h) ->
+      let lhs = lowerCont arg (accum f *> accum g) h
+          rhs =
+            lowerCont
+              arg
+              ( accum $ \acc ->
+                  let (_, v) = f acc
+                      (res, w) = g (acc <> v)
+                   in (res, v <> w)
+              )
+              h
+       in runAccumArb lhs w' === runAccumArb rhs w'
+
+accumLaws ::
+  forall (m :: Type -> Type) (t :: Type).
+  (MonadAccum M m, Typeable m, Arbitrary t, Show t) =>
+  (forall (a :: Type). (Eq a) => t -> m a -> m a -> Bool) ->
+  TestTree
+accumLaws runAndCompare =
+  testProperties
+    testName
+    [ ("look *> look = look", lookLookProp),
+      ("add mempty = pure ()", addMemptyProp),
+      ("add x *> add y = add (x <> y)", addAddProp),
+      ("add x *> look = look >>= \\w -> add x $> w <> x", addLookProp),
+      ("accum (const (x, mempty)) = pure x", accumPureProp),
+      ("accum f *> accum g law (too long)", accumFGProp),
+      ("look = accum $ \\acc -> (acc, mempty)", lookAccumProp),
+      ("add x = accum $ \\acc -> ((), x)", addAccumProp),
+      ("accum f = look >>= \\acc -> let (res, v) = f acc in add v $> res", accumAddProp)
+    ]
+  where
+    testName :: String
+    testName = "MonadAccum laws for " <> typeName @(m A)
+    addAccumProp :: Property
+    addAccumProp = theNeedful $ \(w, x) ->
+      let lhs = add x
+          rhs = accum $ const ((), x)
+       in property . runAndCompare w lhs $ rhs
+    accumAddProp :: Property
+    accumAddProp = theNeedful $ \(w, Blind (f :: M -> (A, M))) ->
+      let lhs = accum f
+          rhs = look >>= \acc -> let (res, v) = f acc in add v $> res
+       in property . runAndCompare w lhs $ rhs
+    lookLookProp :: Property
+    lookLookProp = theNeedful $ \w ->
+      let lhs = look *> look
+          rhs = look
+       in property . runAndCompare w lhs $ rhs
+    addMemptyProp :: Property
+    addMemptyProp = theNeedful $ \w ->
+      let lhs = add mempty
+          rhs = pure ()
+       in property . runAndCompare w lhs $ rhs
+    addAddProp :: Property
+    addAddProp = theNeedful $ \(w, x, y) ->
+      let lhs = add x *> add y
+          rhs = add (x <> y)
+       in property . runAndCompare w lhs $ rhs
+    addLookProp :: Property
+    addLookProp = theNeedful $ \(w, x) ->
+      let lhs = add x *> look
+          rhs = look >>= \w' -> add x $> w' <> x
+       in property . runAndCompare w lhs $ rhs
+    accumPureProp :: Property
+    accumPureProp = theNeedful $ \(w, x :: A) ->
+      let lhs = accum (const (x, mempty))
+          rhs = pure x
+       in property . runAndCompare w lhs $ rhs
+    accumFGProp :: Property
+    accumFGProp = theNeedful $ \(w', Blind (f :: M -> (A, M)), Blind (g :: M -> (M, M))) ->
+      let lhs = accum f *> accum g
+          rhs = accum $ \acc ->
+            let (_, v) = f acc
+                (res, w) = g (acc <> v)
+             in (res, v <> w)
+       in property . runAndCompare w' lhs $ rhs
+    lookAccumProp :: Property
+    lookAccumProp = theNeedful $ \w ->
+      let lhs = look
+          rhs = accum (,mempty)
+       in property . runAndCompare w lhs $ rhs
+
+-- Helpers
+
+typeName :: forall (a :: Type). (Typeable a) => String
+typeName =
+  let ourTyCon = typeRepTyCon $ typeRep @a
+   in tyConModule ourTyCon <> "." <> tyConName ourTyCon
+
+theNeedful ::
+  forall (a :: Type).
+  (Arbitrary a, Show a) =>
+  (a -> Property) ->
+  Property
+theNeedful = forAllShrinkShow arbitrary shrink ppShow
diff --git a/test/properties/Main.hs b/test/properties/Main.hs
new file mode 100644
index 0000000..d33ac3a
--- /dev/null
+++ b/test/properties/Main.hs
@@ -0,0 +1,247 @@
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE NumericUnderscores #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Main (main) where
+
+import Accum
+  ( AccumArb (AccumArb),
+    M,
+    N,
+    accumLaws,
+    accumLawsCont,
+    accumLawsSelect,
+  )
+import Control.Monad.Trans.Accum (Accum, AccumT (AccumT), accum, runAccum)
+import Control.Monad.Trans.Cont (ContT, runContT)
+import Control.Monad.Trans.Except (ExceptT, runExceptT)
+import Control.Monad.Trans.Identity (IdentityT, runIdentityT)
+import Control.Monad.Trans.Maybe (MaybeT, runMaybeT)
+import qualified Control.Monad.Trans.RWS.CPS as RWSCPS
+import qualified Control.Monad.Trans.RWS.Lazy as RWSLazy
+import qualified Control.Monad.Trans.RWS.Strict as RWSStrict
+import Control.Monad.Trans.Reader (ReaderT, runReaderT)
+import Control.Monad.Trans.Select (SelectT, runSelectT)
+import qualified Control.Monad.Trans.State.Lazy as StateLazy
+import qualified Control.Monad.Trans.State.Strict as StateStrict
+import qualified Control.Monad.Trans.Writer.CPS as WriterCPS
+import qualified Control.Monad.Trans.Writer.Lazy as WriterLazy
+import qualified Control.Monad.Trans.Writer.Strict as WriterStrict
+import Data.Functor.Identity (Identity, runIdentity)
+import Data.Kind (Type)
+import GHC.IO.Encoding (setLocaleEncoding, utf8)
+import Test.QuickCheck.Poly (A, B)
+import Test.Tasty (adjustOption, defaultMain, testGroup)
+import Test.Tasty.QuickCheck (QuickCheckTests)
+
+main :: IO ()
+main = do
+  setLocaleEncoding utf8
+  defaultMain . adjustOption go . testGroup "Laws" $
+    [ testGroup
+        "Accum"
+        [ accumLaws lowerBase,
+          accumLaws lowerMaybe,
+          accumLaws lowerExcept,
+          accumLaws lowerIdentity,
+          accumLaws lowerRWSLazy,
+          accumLaws lowerRWSStrict,
+          accumLaws lowerRWSCPS,
+          accumLaws lowerReader,
+          accumLaws lowerStateLazy,
+          accumLaws lowerStateStrict,
+          accumLaws lowerWriterLazy,
+          accumLaws lowerWriterStrict,
+          accumLaws lowerWriterCPS,
+          accumLawsCont lowerCont,
+          accumLawsSelect lowerSelect
+        ]
+    ]
+  where
+    go :: QuickCheckTests -> QuickCheckTests
+    go = max 1_000_000
+
+-- Lowerings
+
+lowerSelect ::
+  forall (a :: Type).
+  () ->
+  SelectT B (Accum M) a ->
+  (a -> AccumArb M B) ->
+  AccumArb M a
+lowerSelect _ comp handler =
+  demote . runSelectT comp $ (promote . handler)
+
+lowerCont ::
+  forall (a :: Type).
+  () ->
+  ContT B (Accum M) a ->
+  (a -> AccumArb M B) ->
+  AccumArb M B
+lowerCont _ comp handler =
+  demote . runContT comp $ (promote . handler)
+
+promote ::
+  forall (w :: Type) (a :: Type).
+  AccumArb w a ->
+  Accum w a
+promote (AccumArb f) = accum f
+
+demote ::
+  forall (w :: Type) (a :: Type).
+  Accum w a ->
+  AccumArb w a
+demote (AccumT f) = AccumArb $ \w -> runIdentity . f $ w
+
+lowerBase ::
+  forall (a :: Type).
+  (Eq a) =>
+  M ->
+  AccumT M Identity a ->
+  AccumT M Identity a ->
+  Bool
+lowerBase w lhs rhs = runAccum lhs w == runAccum rhs w
+
+lowerMaybe ::
+  forall (a :: Type).
+  (Eq a) =>
+  M ->
+  MaybeT (Accum M) a ->
+  MaybeT (Accum M) a ->
+  Bool
+lowerMaybe w lhs rhs =
+  let leftRun = runAccum (runMaybeT lhs) w
+      rightRun = runAccum (runMaybeT rhs) w
+   in leftRun == rightRun
+
+lowerExcept ::
+  forall (a :: Type).
+  (Eq a) =>
+  M ->
+  ExceptT A (Accum M) a ->
+  ExceptT A (Accum M) a ->
+  Bool
+lowerExcept w lhs rhs =
+  let leftRun = runAccum (runExceptT lhs) w
+      rightRun = runAccum (runExceptT rhs) w
+   in leftRun == rightRun
+
+lowerIdentity ::
+  forall (a :: Type).
+  (Eq a) =>
+  M ->
+  IdentityT (Accum M) a ->
+  IdentityT (Accum M) a ->
+  Bool
+lowerIdentity w lhs rhs =
+  let leftRun = runAccum (runIdentityT lhs) w
+      rightRun = runAccum (runIdentityT rhs) w
+   in leftRun == rightRun
+
+lowerRWSLazy ::
+  forall (a :: Type).
+  (Eq a) =>
+  (M, A, B) ->
+  RWSLazy.RWST A M B (Accum M) a ->
+  RWSLazy.RWST A M B (Accum M) a ->
+  Bool
+lowerRWSLazy (w, r, s) lhs rhs =
+  let leftRun = runAccum (RWSLazy.runRWST lhs r s) w
+      rightRun = runAccum (RWSLazy.runRWST rhs r s) w
+   in leftRun == rightRun
+
+lowerRWSStrict ::
+  forall (a :: Type).
+  (Eq a) =>
+  (M, A, B) ->
+  RWSStrict.RWST A M B (Accum M) a ->
+  RWSStrict.RWST A M B (Accum M) a ->
+  Bool
+lowerRWSStrict (w, r, s) lhs rhs =
+  let leftRun = runAccum (RWSStrict.runRWST lhs r s) w
+      rightRun = runAccum (RWSStrict.runRWST rhs r s) w
+   in leftRun == rightRun
+
+lowerRWSCPS ::
+  forall (a :: Type).
+  (Eq a) =>
+  (M, A, B) ->
+  RWSCPS.RWST A M B (Accum M) a ->
+  RWSCPS.RWST A M B (Accum M) a ->
+  Bool
+lowerRWSCPS (w, r, s) lhs rhs =
+  let leftRun = runAccum (RWSCPS.runRWST lhs r s) w
+      rightRun = runAccum (RWSCPS.runRWST rhs r s) w
+   in leftRun == rightRun
+
+lowerReader ::
+  forall (a :: Type).
+  (Eq a) =>
+  (M, A) ->
+  ReaderT A (Accum M) a ->
+  ReaderT A (Accum M) a ->
+  Bool
+lowerReader (w, r) lhs rhs =
+  let leftRun = runAccum (runReaderT lhs r) w
+      rightRun = runAccum (runReaderT rhs r) w
+   in leftRun == rightRun
+
+lowerStateLazy ::
+  forall (a :: Type).
+  (Eq a) =>
+  (M, A) ->
+  StateLazy.StateT A (Accum M) a ->
+  StateLazy.StateT A (Accum M) a ->
+  Bool
+lowerStateLazy (w, s) lhs rhs =
+  let leftRun = runAccum (StateLazy.runStateT lhs s) w
+      rightRun = runAccum (StateLazy.runStateT rhs s) w
+   in leftRun == rightRun
+
+lowerStateStrict ::
+  forall (a :: Type).
+  (Eq a) =>
+  (M, A) ->
+  StateStrict.StateT A (Accum M) a ->
+  StateStrict.StateT A (Accum M) a ->
+  Bool
+lowerStateStrict (w, s) lhs rhs =
+  let leftRun = runAccum (StateStrict.runStateT lhs s) w
+      rightRun = runAccum (StateStrict.runStateT rhs s) w
+   in leftRun == rightRun
+
+lowerWriterLazy ::
+  forall (a :: Type).
+  (Eq a) =>
+  M ->
+  WriterLazy.WriterT N (Accum M) a ->
+  WriterLazy.WriterT N (Accum M) a ->
+  Bool
+lowerWriterLazy w lhs rhs =
+  let leftRun = runAccum (WriterLazy.runWriterT lhs) w
+      rightRun = runAccum (WriterLazy.runWriterT rhs) w
+   in leftRun == rightRun
+
+lowerWriterStrict ::
+  forall (a :: Type).
+  (Eq a) =>
+  M ->
+  WriterStrict.WriterT N (Accum M) a ->
+  WriterStrict.WriterT N (Accum M) a ->
+  Bool
+lowerWriterStrict w lhs rhs =
+  let leftRun = runAccum (WriterStrict.runWriterT lhs) w
+      rightRun = runAccum (WriterStrict.runWriterT rhs) w
+   in leftRun == rightRun
+
+lowerWriterCPS ::
+  forall (a :: Type).
+  (Eq a) =>
+  M ->
+  WriterCPS.WriterT N (Accum M) a ->
+  WriterCPS.WriterT N (Accum M) a ->
+  Bool
+lowerWriterCPS w lhs rhs =
+  let leftRun = runAccum (WriterCPS.runWriterT lhs) w
+      rightRun = runAccum (WriterCPS.runWriterT rhs) w
+   in leftRun == rightRun