diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,17 @@
+## [0.6.0]
+
+* [Enhance `traversable` checks](https://github.com/haskell-checkers/checkers/pull/61)
+
+* [Remove redundant constraint from instance CoArbitrary Array](https://github.com/haskell-checkers/checkers/pull/65)
+
+[0.6.0]: https://github.com/haskell-checkers/checkers/compare/v0.5.7...v0.6.0
+
+## [0.5.7]
+
+* [Add `bifoldable` and `bifoldableBifunctor` tests](https://github.com/haskell-checkers/checkers/pull/62)
+
+* [Restore `verboseBatch` functionality](https://github.com/haskell-checkers/checkers/pull/59)
+
+* [Drop support for GHC < 8.2](https://github.com/haskell-checkers/checkers/pull/63)
+
+[0.5.7]: https://github.com/haskell-checkers/checkers/compare/v0.5.6...v0.5.7
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,2 @@
+**checkers** is a library for reusable QuickCheck properties, particularly for standard type classes (class laws and [class morphisms](http://conal.net/papers/type-class-morphisms)).
+Checkers also has lots of support for randomly generating data values (thanks to Thomas Davie).
diff --git a/checkers.cabal b/checkers.cabal
--- a/checkers.cabal
+++ b/checkers.cabal
@@ -1,6 +1,6 @@
 Name:                checkers
-Version:             0.4.14
-Cabal-Version:       >= 1.6
+Version:             0.6.0
+Cabal-Version:       >= 1.10
 Synopsis:            Check properties on standard classes and data structures.
 Category:            Testing
 Description:
@@ -17,19 +17,18 @@
 License-File:        COPYING
 Stability:           experimental
 build-type:          Simple
-tested-with:         GHC==8.6.4, GHC==8.4.4, GHC==8.2.2, GHC==8.0.2, GHC==7.10.3
-homepage:            https://github.com/conal/checkers
+tested-with:         GHC==9.2.1, GHC==9.0.2, GHC==8.10.7, GHC==8.8.4, GHC==8.6.5, GHC==8.4.4, GHC==8.2.2
+homepage:            https://github.com/haskell-checkers/checkers
+extra-source-files:  README.md CHANGELOG.md
+
 source-repository head
   type:     git
-  location: git://github.com/conal/checkers.git
+  location: git://github.com/haskell-checkers/checkers.git
 
 Library
   hs-Source-Dirs:      src
   Extensions:
-  Build-Depends:       base >= 4 && < 5, random, QuickCheck>=2.3, array >= 0.1, semigroupoids >= 5 && < 6
-  if !impl(ghc >= 8.0)
-    build-depends:
-      semigroups          >= 0.18.2  && < 0.19
+  Build-Depends:       base >= 4.10 && < 5, random, QuickCheck>=2.3, array >= 0.1, semigroupoids >= 5 && < 6
 
   Exposed-Modules:
                        Test.QuickCheck.Utils
@@ -48,6 +47,5 @@
                        Test.QuickCheck.Later
   Other-modules:
                        Control.Monad.Extensions
-  ghc-options:         -Wall
-  if impl(ghc >= 8.0)
-    ghc-options:       -Wredundant-constraints
+  ghc-options:         -Wall -Wredundant-constraints
+  Default-Language:    Haskell2010
diff --git a/src/Test/QuickCheck/Checkers.hs b/src/Test/QuickCheck/Checkers.hs
--- a/src/Test/QuickCheck/Checkers.hs
+++ b/src/Test/QuickCheck/Checkers.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances
            , FlexibleContexts, TypeSynonymInstances, GeneralizedNewtypeDeriving
-           , UndecidableInstances, ScopedTypeVariables
+           , UndecidableInstances, ScopedTypeVariables, DefaultSignatures
+           , TypeOperators, CPP
   #-}
 {-# OPTIONS_GHC -Wall -fno-warn-orphans #-}
 
@@ -33,7 +34,7 @@
   -- * Model-based (semantics-based) testing
   , Model(..)
   , meq, meq1, meq2, meq3, meq4, meq5
-  , eqModels
+  , eqModels, denotationFor
   , Model1(..)
   -- * Some handy testing types
   -- , Positive, NonZero(..), NonNegative(..)
@@ -44,11 +45,25 @@
   ) where
 
 import Data.Function (on)
-import Data.Monoid (Monoid (mempty, mappend))
 import Control.Applicative
 import Control.Arrow ((***),first)
 import qualified Control.Exception as Ex
 import Data.List (foldl')
+import Data.List.NonEmpty (NonEmpty (..))
+import Data.Monoid hiding (First, Last)
+
+import Data.Complex
+import Data.Proxy
+import Data.Ratio
+import Data.Functor.Identity
+
+#if __GLASGOW_HASKELL__ >= 800
+import Data.Functor.Compose
+import qualified Data.Functor.Product as F
+import qualified Data.Functor.Sum as F
+#endif
+import Data.Semigroup
+import GHC.Generics
 import System.Random
 import Test.QuickCheck hiding (generate)
 import Test.QuickCheck.Random (QCGen, newQCGen)
@@ -83,17 +98,21 @@
 
 -- TODO: consider a tree structure so that flattening is unnecessary.
 
+type QuickCheckRunner = Args -> Property -> IO ()
+
 -- | Run a batch of tests.  See 'quickBatch' and 'verboseBatch'.
-checkBatch :: Args -> TestBatch -> IO ()
-checkBatch args (name,tests) =
+checkBatch' :: QuickCheckRunner -> Args -> TestBatch -> IO ()
+checkBatch' runner args (name,tests) =
   do putStrLn $ "\n" ++ name ++ ":"
      mapM_ pr tests
  where
    pr (s,p) = do putStr (padTo (width + 4) ("  "++s ++ ":"))
-                 Ex.catch (quickCheckWith args p)
+                 Ex.catch (runner args p)
                           (print :: Ex.SomeException -> IO ())
    width    = foldl' max 0 (map (length.fst) tests)
 
+checkBatch :: Args -> TestBatch -> IO ()
+checkBatch = checkBatch' quickCheckWith
 
 padTo :: Int -> String -> String
 padTo n = take n . (++ repeat ' ')
@@ -104,15 +123,11 @@
 
 -- | Check a batch verbosely.
 verboseBatch :: TestBatch -> IO ()
-verboseBatch = checkBatch verbose'
+verboseBatch = checkBatch' verboseCheckWith quick'
 
-quick', verbose' :: Args
+quick' :: Args
 quick'   = stdArgs { maxSuccess = 500 }
-verbose' = quick'
-           -- quick' { configEvery = \ n args -> show n ++ ":\n" ++ unlines args }
 
--- TODO: Restore verbose functionality.  How in QC2?
-
 {-
 
 -- TODO: change TestBatch to be hierarchical/recursive, rather than
@@ -174,51 +189,107 @@
 
 -- | Types of values that can be tested for equality, perhaps through
 -- random sampling.
-class EqProp a where (=-=) :: a -> a -> Property
+class EqProp a where
+  (=-=) :: a -> a -> Property
+  default (=-=) :: (Generic a, GEqProp (Rep a)) => a -> a -> Property
+  (=-=) = geq `on` from
+  {-# INLINEABLE (=-=) #-}
 
+class GEqProp g where
+  geq :: g x -> g x -> Property
+
+instance GEqProp g => GEqProp (M1 _1 _2 g) where
+  geq = geq `on` unM1
+  {-# INLINEABLE geq #-}
+
+instance (GEqProp g1, GEqProp g2) => GEqProp (g1 :*: g2) where
+  geq (g1a :*: g1b) (g2a :*: g2b) = geq g1a g2a .&&. geq g1b g2b
+  {-# INLINEABLE geq #-}
+
+instance (GEqProp g1, GEqProp g2) => GEqProp (g1 :+: g2) where
+  geq (L1 g1) (L1 g2) = geq g1 g2
+  geq (R1 g1) (R1 g2) = geq g1 g2
+  geq _ _             = property False
+  {-# INLINEABLE geq #-}
+
+instance EqProp a => GEqProp (K1 _1 a) where
+  geq = (=-=) `on` unK1
+  {-# INLINEABLE geq #-}
+
+instance GEqProp U1 where
+  geq U1 U1 = property True
+  {-# INLINEABLE geq #-}
+
+instance GEqProp V1 where
+  geq _ _ = property True
+  {-# INLINEABLE geq #-}
+
 -- | For 'Eq' types as 'EqProp' types
 eq :: Eq a => a -> a -> Property
 a `eq` a' = property (a == a')
 
+
 -- Template: fill in with Eq types for a
 --   instance EqProp a where (=-=) = eq
 -- E.g.,
 
-instance EqProp ()     where (=-=) = eq
-instance EqProp Bool   where (=-=) = eq
-instance EqProp Char   where (=-=) = eq
-instance EqProp Int    where (=-=) = eq
-instance EqProp Float  where (=-=) = eq
-instance EqProp Double where (=-=) = eq
+instance EqProp ()
+instance EqProp Bool
+instance EqProp Char where (=-=) = eq
+instance EqProp Ordering
 
+-- Numeric
+instance EqProp Int     where (=-=) = eq
+instance EqProp Float   where (=-=) = eq
+instance EqProp Double  where (=-=) = eq
+instance EqProp Integer where (=-=) = eq
+instance Eq a => EqProp (Complex a) where (=-=) = eq
+instance Eq a => EqProp (Ratio a) where (=-=) = eq
+
+-- Semigroups
+instance EqProp a => EqProp (Min a)
+instance EqProp a => EqProp (Max a)
+instance EqProp a => EqProp (First a)
+instance EqProp a => EqProp (Last a)
+
+-- Monoids
+instance EqProp a => EqProp (Dual a)
+instance (Show a, Arbitrary a, EqProp a) => EqProp (Endo a)
+instance EqProp All
+instance EqProp Any
+instance EqProp a => EqProp (Sum a)
+instance EqProp a => EqProp (Product a)
+instance EqProp (f a) => EqProp (Alt f a)
+#if __GLASGOW_HASKELL__ >= 806
+instance EqProp (f a) => EqProp (Ap f a)
+#endif
+
 -- Lists
-instance EqProp a => EqProp [a] where
-    [] =-= [] = property True
-    x:xs =-= y:ys = x =-= y .&. xs =-= ys
-    _ =-= _ = property False
+instance EqProp a => EqProp [a]
+instance EqProp a => EqProp (NonEmpty a)
+instance EqProp a => EqProp (ZipList a)
 
 -- Maybe
-instance EqProp a => EqProp (Maybe a) where
-    Nothing =-= Nothing = property True
-    Just x =-= Just y = x =-= y
-    _ =-= _ = property False
+instance EqProp a => EqProp (Maybe a)
 
 -- Pairing
-instance (EqProp a, EqProp b) => EqProp (a,b) where
-  (a,b) =-= (a',b') = a =-= a' .&. b =-= b'
-
-instance (EqProp a, EqProp b, EqProp c) => EqProp (a,b,c) where
-  (a,b,c) =-=(a',b',c') = a =-= a' .&. b =-= b' .&. c =-= c'
-
-instance (EqProp a, EqProp b, EqProp c, EqProp d) => EqProp (a,b,c,d) where
-  (a,b,c,d) =-=(a',b',c',d') = a =-= a' .&. b =-= b' .&. c =-= c' .&. d =-= d'
+instance (EqProp a, EqProp b) => EqProp (a,b)
+instance (EqProp a, EqProp b, EqProp c) => EqProp (a,b,c)
+instance (EqProp a, EqProp b, EqProp c, EqProp d) => EqProp (a,b,c,d)
 
 -- Either
-instance (EqProp a, EqProp b) => EqProp (Either a b) where
-  (Left x)  =-=  (Left x') = x =-= x'
-  (Right x) =-= (Right x') = x =-= x'
-  _         =-=          _ = property False
+instance (EqProp a, EqProp b) => EqProp (Either a b)
 
+-- Functors
+#if __GLASGOW_HASKELL__ >= 800
+instance EqProp (f (g a)) => EqProp (Compose f g a)
+instance (EqProp (f a), EqProp (g a)) => EqProp (F.Sum f g a)
+instance (EqProp (f a), EqProp (g a)) => EqProp (F.Product f g a)
+#endif
+instance EqProp a => EqProp (Identity a)
+instance EqProp a => EqProp (Const a b)
+instance EqProp (Proxy a)
+
 -- Function equality
 instance (Show a, Arbitrary a, EqProp b) => EqProp (a -> b) where
   f =-= f' = property (liftA2 (=-=) f f')
@@ -230,6 +301,19 @@
 eqModels :: (Model a b, EqProp b) => a -> a -> Property
 eqModels = (=-=) `on` model
 
+
+-- | @f `'denotationFor'` g@ proves that @f@ is a model for @g@, ie that
+-- @'model' . g '=-=' f@.
+denotationFor
+    :: (Model b b', Arbitrary a, EqProp b', Show a)
+    => (a -> b')
+    -> (a -> b)
+    -> TestBatch
+denotationFor f g =
+  ( "denotation"
+  , [("eq", model . g =-= f)]
+  )
+
 -- Other types
 -- instance EqProp a => EqProp (S.Stream a) where (=-=) = eqModels
 
@@ -262,18 +346,13 @@
     forAll (gen a) $ \ b ->
       (a `rel` b) ==> (b `rel` a)
 
--- | Symmetric property: @a `rel` b && b `rel` a ==> a == b@.  Generate
--- @a@ randomly, but use @gen a@ to generate @b@.  @gen@ ought to satisfy
--- both @rel@ directions fairly often but not always.
+-- | Antisymmetric property: @(a `rel` b) && (a /= b) ==> not (b `rel` a)@.
+--
+-- @since 0.5.0
 antiSymmetric :: (Arbitrary a, Show a, Eq a) =>
-                 BinRel a -> (a -> Gen a) -> Property
-antiSymmetric rel gen =
-  property $ \ a ->
-    forAll (gen a) $ \ b ->
-      (a `rel` b) && (b `rel` a) ==> a == b
-
-
-
+                 BinRel a -> Property
+antiSymmetric rel =
+  property $ \ a b -> (a `rel` b) && (a /= b) ==> not (b `rel` a)
 
 -- | Has a given left identity, according to '(=-=)'
 leftId :: (Show a, Arbitrary a, EqProp a) => (i -> a -> a) -> i -> Property
@@ -409,9 +488,12 @@
 instance Model Double Double where model = id
 instance Model String String where model = id
 
--- This next one requires UndecidableInstances
+-- These next two require UndecidableInstances
 instance (Model a b, Model a' b') => Model (a,a') (b,b') where
   model = model *** model
+
+instance Model b b' => Model (a -> b) (a -> b') where
+  model f = model . f
 
 -- instance Model (S.Stream a) (NonNegative Int -> a) where
 --   model s (NonNegative i) = s S.!! i
diff --git a/src/Test/QuickCheck/Classes.hs b/src/Test/QuickCheck/Classes.hs
--- a/src/Test/QuickCheck/Classes.hs
+++ b/src/Test/QuickCheck/Classes.hs
@@ -1,8 +1,7 @@
 {-# LANGUAGE ScopedTypeVariables, FlexibleContexts, KindSignatures
-           , Rank2Types, TypeOperators, CPP
+           , Rank2Types, TypeApplications, TypeOperators, CPP
   #-}
 
-{-# OPTIONS_GHC -Wall #-}
 ----------------------------------------------------------------------
 -- |
 -- Module      :  Test.QuickCheck.Classes
@@ -24,21 +23,25 @@
   , applicative, applicativeMorphism, semanticApplicative
   , bind, bindMorphism, semanticBind, bindApply
   , monad, monadMorphism, semanticMonad, monadFunctor
-  , monadApplicative, arrow, arrowChoice, foldable, foldableFunctor, traversable
+  , monadApplicative, arrow, arrowChoice, foldable, foldableFunctor, bifoldable, bifoldableBifunctor, traversable
   , monadPlus, monadOr, alt, alternative
   )
   where
 
-import Control.Applicative ((<$>))
+import Data.Bifoldable (Bifoldable (..))
+import Data.Bifunctor hiding (first, second)
 import Data.Foldable (Foldable(..))
 import Data.Functor.Apply (Apply ((<.>)))
 import Data.Functor.Alt (Alt ((<!>)))
 import Data.Functor.Bind (Bind ((>>-)), apDefault)
 import qualified Data.Functor.Bind as B (Bind (join))
-import Data.Semigroup (Semigroup ((<>)))
-import Data.Monoid (Monoid (mappend, mempty), Endo(..), Dual(..), Sum(..), Product(..))
-import Data.Traversable (Traversable (..), fmapDefault, foldMapDefault)
-import Control.Applicative
+import Data.Functor.Compose (Compose (..))
+import Data.Functor.Identity (Identity (..))
+import Data.List.NonEmpty (NonEmpty(..))
+import Data.Semigroup (Semigroup (..))
+import Data.Monoid (Endo(..), Dual(..), Sum(..), Product(..))
+import Data.Traversable (fmapDefault, foldMapDefault)
+import Control.Applicative (Alternative(..))
 import Control.Monad (MonadPlus (..), ap, join)
 import Control.Arrow (Arrow,ArrowChoice,first,second,left,right,(>>>),arr)
 import Test.QuickCheck
@@ -48,24 +51,44 @@
 import Test.QuickCheck.Instances.Char ()
 
 
--- | Total ordering.  @gen a@ ought to generate values @b@ satisfying @a
--- `rel` b@ fairly often.
+-- | Total ordering.
+--
+-- @gen a@ ought to generate values @b@ satisfying @a `rel` b@ fairly often.
 ordRel :: forall a. (Ord a, Show a, Arbitrary a) =>
           BinRel a -> (a -> Gen a) -> TestBatch
 ordRel rel gen =
   ( "ord"
   , [ ("reflexive"    , reflexive     rel    )
     , ("transitive"   , transitive    rel gen)
-    , ("antiSymmetric", antiSymmetric rel gen)
+    , ("antiSymmetric", antiSymmetric rel    )
     ]
   )
 
--- | Total ordering
+-- | 'Ord' laws.
+--
+-- @gen a@ ought to generate values @b@ satisfying @a `rel` b@ fairly often.
 ord :: forall a. (Ord a, Show a, Arbitrary a) =>
        (a -> Gen a) -> TestBatch
-ord = ordRel (<=)
-
-
+ord gen =
+    ( "Ord"
+    , [ ("Reflexivity of (<=)", reflexive le)
+      , ("Transitivity of (<=)", transitive le gen)
+      , ("Antisymmetry of (<=)", antiSymmetric le)
+      , ("x >= y = y <= x", p (\x y -> (x >= y) === (y <= x)))
+      , ("x < y = x <= y && x /= y", p (\x y -> (x < y) === (x <= y && x /= y)))
+      , ("x > y = y < x", p (\x y -> (x > y) === (y < x)))
+      , ("x < y = compare x y == LT", p (\x y -> (x < y) === (compare x y == LT)))
+      , ("x > y = compare x y == GT", p (\x y -> (x > y) === (compare x y == GT)))
+      , ("x == y = compare x y == EQ", p (\x y -> (x == y) === (compare x y == EQ)))
+      , ("min x y == if x <= y then x else y = True", p (\x y -> min x y === if x <= y then x else y))
+      , ("max x y == if x >= y then x else y = True", p (\x y -> max x y === if x >= y then x else y))
+      ]
+    )
+  where
+    le :: a -> a -> Bool
+    le = (<=)
+    p :: (a -> a -> Property) -> Property
+    p = property
 
 -- | 'Ord' morphism properties.  @h@ is an 'Ord' morphism iff:
 --
@@ -111,18 +134,40 @@
                , [ ("left  identity", leftId  mappend (mempty :: a))
                  , ("right identity", rightId mappend (mempty :: a))
                  , ("associativity" , isAssoc (mappend :: Binop a))
+#if MIN_VERSION_base(4,11,0)
+                 , ("mappend = (<>)", property monoidSemigroupP)
+#endif
+                 , ("mconcat", property mconcatP)
                  ]
                )
+  where
+#if MIN_VERSION_base(4,11,0)
+    monoidSemigroupP :: a -> a -> Property
+    monoidSemigroupP x y = mappend x y =-= x <> y
+#endif
+    mconcatP :: [a] -> Property
+    mconcatP as = mconcat as =-= foldr mappend mempty as
 
 -- | Properties to check that the 'Semigroup' 'a' satisfies the semigroup
 -- properties.  The argument value is ignored and is present only for its
 -- type.
-semigroup :: forall a. (Semigroup a, Show a, Arbitrary a, EqProp a) =>
-             a -> TestBatch
+--
+-- @since 0.5.0
+semigroup :: forall a n.
+             ( Semigroup a, Show a, Arbitrary a, EqProp a
+             , Integral n, Show n, Arbitrary n) =>
+             (a, n) -> TestBatch
 semigroup = const ( "semigroup"
                   , [("associativity", isAssoc ((<>) :: Binop a))
+                    ,("sconcat", property sconcatP)
+                    ,("stimes", property stimesP)
                     ]
                   )
+  where
+    sconcatP :: a -> [a] -> Property
+    sconcatP a as = sconcat (a :| as) =-= foldr1 (<>) (a :| as)
+    stimesP :: Positive n -> a -> Property
+    stimesP (Positive n) a = stimes n a =-= foldr1 (<>) (replicate (fromIntegral n) a)
 
 -- | Monoid homomorphism properties.  See also 'homomorphism'.
 monoidMorphism :: (Monoid a, Monoid b, EqProp b, Show a, Arbitrary a) =>
@@ -429,24 +474,34 @@
          , Arbitrary (m a), EqProp (m a), Show (m a)
          , Arbitrary (m b), EqProp (m b)
          , Arbitrary (m c), EqProp (m c)
+         , Show (m (a -> b)), Arbitrary (m (a -> b))
          ) =>
          m (a,b,c) -> TestBatch
 monad = const ( "monad laws"
               , [ ("left  identity", property leftP)
                 , ("right identity", property rightP)
                 , ("associativity" , property assocP)
+                , ("pure", property pureP)
+                , ("ap", property apP)
                 ]
               )
  where
    leftP  :: (a -> m b) -> a -> Property
    rightP :: m a -> Property
    assocP :: m a -> (a -> m b) -> (b -> m c) -> Property
+   pureP :: a -> Property
+   apP :: m (a -> b) -> m a -> Property
 
    leftP f a    = (return a >>= f)  =-= f a
    rightP m     = (m >>= return)    =-=  m
    assocP m f g = ((m >>= f) >>= g) =-= (m >>= (\x -> f x >>= g))
+   pureP x = (pure x :: m a) =-= return x
+   apP f x = (f <*> x) =-= (f `ap` x)
 
 -- | Law for monads that are also instances of 'Functor'.
+--
+-- Note that instances that satisfy 'applicative' and 'monad'
+-- are implied to satisfy this property too.
 monadFunctor :: forall m a b.
                 ( Monad m
                 , Arbitrary b, CoArbitrary a
@@ -458,6 +513,7 @@
    bindReturnP :: (a -> b) -> m a -> Property
    bindReturnP f xs = fmap f xs =-= (xs >>= return . f)
 
+-- | Note that 'monad' also contains these properties.
 monadApplicative :: forall m a b.
                     ( Monad m
                     , EqProp (m a), EqProp (m b)
@@ -665,29 +721,63 @@
     rightMovesP f g = (left f >>> right (arr g))
                         =-= ((right (arr g)) >>> left f)
 
-traversable :: forall f a b m.
-               ( Traversable f, Monoid m, Show (f a)
-               , Arbitrary (f a), Arbitrary b, Arbitrary m
-               , CoArbitrary a
-               , EqProp (f b), EqProp m) =>
-               f (a, b, m) -> TestBatch
-traversable = const ( "traversable"
-                    , [ ("fmap", property fmapP)
+traversable :: forall t a b c m f g.
+               ( Traversable t, Applicative f, Applicative g, Monoid m
+               , Arbitrary (t a), Arbitrary (t b), Arbitrary (f b), Arbitrary (g c)
+               , Arbitrary (t (f (g a)))
+               , Arbitrary m, Arbitrary b
+               , CoArbitrary a, CoArbitrary b
+               , Show (t a), Show (t b), Show (t (f (g a)))
+               , EqProp (t b), EqProp m, EqProp (f (g (t a))), EqProp (f (g (t c)))) => t (f a, g b, c, m)
+  -> TestBatch
+traversable = const ( "Traversable"
+                    , [ ("identity", property identityP)
+                      , ("composition", property compositionP)
+                      -- , ("naturality", property $ \(f :: f Int -> g Int) -> naturalityP f)
+                      , ("fmap", property fmapP)
                       , ("foldMap", property foldMapP)
+                      , ("sequenceA identity", property sequenceIdentityP)
+                      , ("sequenceA composition", property sequenceCompositionP)
+                      -- , ("sequenceA naturality", property $ \(f :: f a -> g a) -> sequenceNaturalityP f)
                       ]
                     )
  where
-   fmapP :: (a -> b) -> f a -> Property
-   foldMapP :: (a -> m) -> f a -> Property
+   identityP :: Property
+   identityP = traverse @t @_ @b Identity =-= Identity
 
+   compositionP :: (a -> f b) -> (b -> g c) -> Property
+   compositionP f g = traverse @t (Compose . fmap g . f) =-= Compose . fmap (traverse g) . traverse f
+
+   --FIXME: Does not compile due to rank2 type.
+   --naturalityP :: (forall x. (f x -> g x)) -> (a -> f b) -> Property
+   --naturalityP t f = t . traverse @t f =-= traverse (t . f)
+
+   fmapP :: (a -> b) -> t a -> Property
    fmapP f x = f `fmap` x =-= f `fmapDefault` x
-   foldMapP f x = f `foldMap` x =-= f `foldMapDefault` x
 
+   foldMapP :: (a -> m) -> t a -> Property
+   foldMapP f x = f `foldMap` x =-= (f `foldMapDefault` x :: m)
+
+   sequenceIdentityP :: Property
+   sequenceIdentityP = sequenceA @t @_ @b . fmap Identity =-= Identity
+
+   sequenceCompositionP :: Property
+   sequenceCompositionP = sequenceA @t @(Compose f g) @a . fmap Compose =-= Compose . fmap sequenceA . sequenceA
+
+   --FIXME: Does not compile due to rank2 type.
+   --sequenceNaturalityP :: (forall x. (f x -> g x)) -> Property
+   --sequenceNaturalityP t = t . sequenceA @t @_ @a =-= sequenceA . fmap t
+
 -- | Note that 'foldable' doesn't check the strictness of 'foldl'', `foldr'' and `foldMap''.
+--
+-- @since 0.4.13
+
+-- The (Arbitrary m) constraint is required with base >= 4.13, where we have an
+-- additional property for checking foldMap'.
 foldable :: forall t a b m n o.
             ( Foldable t
             , CoArbitrary a, CoArbitrary b
-            , Arbitrary a, Arbitrary b, Arbitrary o, Arbitrary (t a), Arbitrary (t m), Arbitrary (t n), Arbitrary (t o)
+            , Arbitrary a, Arbitrary b, Arbitrary m, Arbitrary o, Arbitrary (t a), Arbitrary (t m), Arbitrary (t n), Arbitrary (t o)
             , Monoid m
             , Num n
             , Ord o
@@ -754,6 +844,7 @@
     elemP :: o -> t o -> Property
     elemP o t = elem o t =-= elem o (toList t)
 
+-- | @since 0.4.13
 foldableFunctor :: forall t a m.
                    ( Functor t, Foldable t
                    , CoArbitrary a
@@ -768,3 +859,42 @@
   where
     foldMapP :: (a -> m) -> t a -> Property
     foldMapP f t = foldMap f t =-= fold (fmap f t)
+
+-- | @since 0.5.7
+bifoldable :: forall p a b c m.
+               ( Bifoldable p, Monoid m
+               , Show (p a b), Show (p m m)
+               , Arbitrary (p a b), Arbitrary (p m m), Arbitrary m
+               , CoArbitrary a, CoArbitrary b
+               , EqProp m, EqProp c, CoArbitrary c, Arbitrary c, Show c) =>
+               p a (b, c, m)  -> TestBatch
+bifoldable = const ( "Bifoldable"
+                    , [ ("identity", property identityP)
+                      , ("bifoldMap f g ≡ bifoldr (mappend . f) (mappend . g) mempty", property bifoldMapBifoldrP)
+                      , ("bifoldr f g z t ≡ appEndo (bifoldMap (Endo . f) (Endo . g) t) z", property bifoldrBifoldMapP)
+                      ]
+                    )
+ where
+   identityP :: Property
+   identityP = bifold =-= (bifoldMap id id :: p m m -> m)
+
+   bifoldMapBifoldrP :: (a -> m) -> (b -> m) -> Property
+   bifoldMapBifoldrP f g = bifoldMap f g =-= (bifoldr (mappend . f) (mappend . g) mempty :: p a b -> m)
+
+   bifoldrBifoldMapP :: (a -> c -> c) -> (b -> c -> c) -> c -> p a b -> Property
+   bifoldrBifoldMapP f g z t = bifoldr f g z t =-= appEndo (bifoldMap (Endo . f) (Endo . g) t) z
+
+-- | @since 0.5.7
+bifoldableBifunctor :: forall p a b m.
+                       ( Bifoldable p, Bifunctor p, Monoid m
+                       , Show (p a b)
+                       , Arbitrary (p a b), Arbitrary m, CoArbitrary a, CoArbitrary b
+                       , EqProp m) =>
+                       p a (b, m) -> TestBatch
+bifoldableBifunctor = const ( "Bifoldable Bifunctor"
+                            , [ ("bifoldMap f g ≡  bifold . bimap f g", property bifoldBimapP) ]
+                            )
+  where
+    bifoldBimapP :: (a -> m) -> (b -> m) -> Property
+    bifoldBimapP f g = bifoldMap f g =-= (bifold . bimap f g :: p a b -> m)
+    
diff --git a/src/Test/QuickCheck/Instances/Array.hs b/src/Test/QuickCheck/Instances/Array.hs
--- a/src/Test/QuickCheck/Instances/Array.hs
+++ b/src/Test/QuickCheck/Instances/Array.hs
@@ -1,4 +1,6 @@
+{-# LANGUAGE CPP #-}
 {-# OPTIONS_GHC -Wall -fno-warn-orphans #-}
+
 module Test.QuickCheck.Instances.Array where
 
 import Test.QuickCheck
@@ -8,5 +10,5 @@
   arbitrary   =
     (\x -> listArray (0,fromIntegral (length x - 1)) x) <$> arbitrary
 
-instance (Ix a, CoArbitrary b) => CoArbitrary (Array a b) where
+instance (CoArbitrary b) => CoArbitrary (Array a b) where
   coarbitrary = coarbitrary . elems
diff --git a/src/Test/QuickCheck/Instances/Maybe.hs b/src/Test/QuickCheck/Instances/Maybe.hs
--- a/src/Test/QuickCheck/Instances/Maybe.hs
+++ b/src/Test/QuickCheck/Instances/Maybe.hs
@@ -1,6 +1,5 @@
 module Test.QuickCheck.Instances.Maybe (maybeGen) where
 
-import Control.Applicative (pure, (<$>))
 import Test.QuickCheck
 
 maybeGen :: Gen a -> Gen (Maybe a)
diff --git a/src/Test/QuickCheck/Instances/Num.hs b/src/Test/QuickCheck/Instances/Num.hs
--- a/src/Test/QuickCheck/Instances/Num.hs
+++ b/src/Test/QuickCheck/Instances/Num.hs
@@ -4,7 +4,6 @@
        ,nonZero,nonZero_
        ) where
 
-import Control.Applicative ((<$>))
 import Test.QuickCheck
 import Control.Monad.Extensions