diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,16 @@
 # Revision history for group-theory
 
+## 0.2.0.0
+
+* Depend on the `groups` package ([#19](https://github.com/emilypi/group-theory/pull/19) - thanks to @taneb for providing the package!)
+* Added `FreeProduct` ([#13](https://github.com/emilypi/group-theory/pull/13))
+* Removed unsound `Group` instances ([#14](https://github.com/emilypi/group-theory/pull/14))
+* Add the `GroupOrder` typeclass for order calculations ([#20](https://github.com/emilypi/group-theory/pull/20))
+* Fixed 'Permutation' instances ([#21](https://github.com/emilypi/group-theory/pull/21))
+* Bugfixes for `FreeAbelianGroup`, allowing it to handle sparsity more robustly, as well as handling
+  `mempty` values on construction with a pattern synonym.
+* Typo fixes and documentation updates ([#16](https://github.com/emilypi/group-theory/pull/16), [#17](https://github.com/emilypi/group-theory/pull/17))
+
 ## 0.1.0.0
 
 * First version. Released on an unsuspecting world.
diff --git a/group-theory.cabal b/group-theory.cabal
--- a/group-theory.cabal
+++ b/group-theory.cabal
@@ -1,18 +1,28 @@
 cabal-version:   2.0
 name:            group-theory
-version:         0.1.0.0
+version:         0.2.0.0
 synopsis:        The theory of groups
 description:
-  This package includes definitions for Groups (monoids with invertibility), including
-  finite, fre, simple, cyclic, and permutation groups. Additionally, we add the concept
-  of 'Cancelative' functors, building upon 'Alternative' applicative functors.
+  This package includes definitions for Groups (Monoids with invertibility), including order calculations
+  as well as finite, free, cyclic, and permutation groups. Additionally, we add the concept
+  of 'Cancellative' functors, building upon 'Alternative' applicative functors.
+  .
+  There are other group theory related packages on Hackage:
+  .
+  * [groups](https://hackage.haskell.org/package/groups): A minimal, low-footprint definition
+  .
+  * [magmas](https://hackage.haskell.org/package/magmas): A pedagogical hierarchy of algebras, starting from Magmas, including Loops, and Inverse Semigroups.
+  .
+  * [arithmoi](https://hackage.haskell.org/package/arithmoi): Number theory, typelevel modular arithmetic, and cyclic groups.
+  .
+  This package, @group-theory@, tries to combine the best parts, while focusing on usability and intuitiveness.
 
 homepage:        https://github.com/emilypi/group-theory
 bug-reports:     https://github.com/emilypi/group-theory/issues
 license:         BSD3
 license-file:    LICENSE
 author:          Emily Pillmore
-maintainer:      emilypi@cohomolo.gy
+maintainer:      Emily Pillmore <emilypi@cohomolo.gy>, Reed Mullanix <reedmullanix@gmail.com>
 copyright:       (c) 2020 Emily Pillmore <emilypi@cohomolo.gy>
 category:        Algebra, Math, Permutations, Groups
 build-type:      Custom
@@ -34,20 +44,24 @@
 
 library
   exposed-modules:
-    Control.Applicative.Cancelative
+    Control.Applicative.Cancellative
     Data.Group
     Data.Group.Additive
     Data.Group.Cyclic
     Data.Group.Finite
     Data.Group.Foldable
     Data.Group.Free
+    Data.Group.Free.Internal
     Data.Group.Free.Church
+    Data.Group.Free.Product
     Data.Group.Multiplicative
+    Data.Group.Order
     Data.Group.Permutation
 
   build-depends:
       base        >=4.11 && <5
     , containers  >=0.5  && <0.7
+    , groups      ^>=0.5.2
 
   hs-source-dirs:   src
   default-language: Haskell2010
diff --git a/src/Control/Applicative/Cancelative.hs b/src/Control/Applicative/Cancelative.hs
deleted file mode 100644
--- a/src/Control/Applicative/Cancelative.hs
+++ /dev/null
@@ -1,107 +0,0 @@
-{-# language DefaultSignatures #-}
-{-# language Safe #-}
--- |
--- Module       : Control.Applicative.Cancelative
--- Copyright    : (c) 2020 Emily Pillmore
--- License      : BSD-style
---
--- Maintainer   : Emily Pillmore <emilypi@cohomolo.gy>,
---                Reed Mullanix <reedmullanix@gmail.com>
---
--- Stability    : stable
--- Portability  : non-portable
---
--- This module contains definitions for 'Cancelative' functors
--- along with the relevant combinators.
---
-module Control.Applicative.Cancelative
-( -- * Cancelative
-  Cancelative(..)
-  -- ** Cancelative combinators
-, cancel1
-, annihalate
-) where
-
-
-import Control.Applicative
-import Data.Group
-import Data.Group.Free
-import Data.Group.Free.Church
-import Data.Proxy
-
--- $setup
---
--- >>> import qualified Prelude
--- >>> import Data.Group
--- >>> import Data.Monoid
--- >>> import Data.Semigroup
--- >>> import Data.Word
--- >>> import Data.Group.Free
--- >>> import Data.Group.Foldable
--- >>> :set -XTypeApplications
--- >>> :set -XFlexibleContexts
-
--- -------------------------------------------------------------------- --
--- Cancelative functors
-
--- | A group on 'Applicative' functors.
---
--- 'Cancelative' functors have the following laws:
---
--- [Left Cancelation] @ 'cancel' a '<|>' a = 'empty' @
--- [Rigth Cancelation] @ a '<|>' 'cancel' a = 'empty' @
---
--- This is analogous to a group operation on applicative functors,
--- in the sense that 'Alternative' forms a monoid. A straight-
--- forward implementation exists whenever @f a@ forms a 'Group'
--- for all @a@, in which case, @cancel == invert@.
---
-class Alternative f => Cancelative f where
-  -- | Invert (or 'cancel') a 'Cancelative' functor, such that, if the
-  -- functor is also a 'Data.Group.Foldable.GroupFoldable', then @'Data.Group.Foldable.gold' '.' 'cancel'@
-  -- amounts to evaluating the inverse of a word in the functor.
-  --
-  -- === __Examples:__
-  --
-  -- >>> let x = FreeGroup [Left (Sum (2 :: Word8)), Right (Sum 3)]
-  -- >>> cancel x
-  -- FreeGroup {runFreeGroup = [Right (Sum {getSum = 2}),Left (Sum {getSum = 3})]}
-  --
-  cancel :: f a -> f a
-  default cancel :: Group (f a) => f a -> f a
-  cancel = invert
-  {-# minimal cancel #-}
-
-instance Cancelative FG where
-  cancel = invert
-
-instance Cancelative FA where
-  cancel = invert
-
-instance Cancelative FreeGroup where
-  cancel = invert
-
-instance Cancelative Proxy where
-  cancel _ = Proxy
-
--- -------------------------------------------------------------------- --
--- Cancelative functor combinators
-
--- | Cancel a single element in a 'Cancelative' functor.
---
--- === __Examples:__
---
--- >>> let x = FreeGroup [Left (Sum (2 :: Word8)), Right (Sum 3)]
--- >>> gold x
--- Sum {getSum = 1}
--- >>> gold $ cancel1 (Sum 1) x
--- Sum {getSum = 0}
---
-cancel1 :: (Group a, Cancelative f) => a -> f a -> f a
-cancel1 a f = cancel (pure a) <|> f
-
--- | Annihalate a 'Traversable''s worth of elements in a 'Cancelative'
--- functor.
---
-annihalate :: (Cancelative f, Traversable t) => (a -> f a) -> t a -> f (t a)
-annihalate f = traverse (cancel . f)
diff --git a/src/Control/Applicative/Cancellative.hs b/src/Control/Applicative/Cancellative.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Applicative/Cancellative.hs
@@ -0,0 +1,101 @@
+{-# language DefaultSignatures #-}
+{-# language Safe #-}
+-- |
+-- Module       : Control.Applicative.Cancellative
+-- Copyright    : (c) 2020 Emily Pillmore
+-- License      : BSD-style
+--
+-- Maintainer   : Emily Pillmore <emilypi@cohomolo.gy>,
+--                Reed Mullanix <reedmullanix@gmail.com>
+--
+-- Stability    : stable
+-- Portability  : non-portable
+--
+-- This module contains definitions for 'Cancellative' functors
+-- along with the relevant combinators.
+--
+module Control.Applicative.Cancellative
+( -- * Cancellative
+  Cancellative(..)
+  -- ** Cancellative combinators
+, cancel1
+, annihilate
+) where
+
+
+import Control.Applicative
+import Data.Group
+import Data.Group.Free
+import Data.Group.Free.Church
+import Data.Proxy
+
+-- $setup
+--
+-- >>> import qualified Prelude
+-- >>> import Data.Group
+-- >>> import Data.Monoid
+-- >>> import Data.Semigroup
+-- >>> import Data.Word
+-- >>> import Data.Group.Free
+-- >>> import Data.Group.Foldable
+-- >>> :set -XTypeApplications
+-- >>> :set -XFlexibleContexts
+
+-- -------------------------------------------------------------------- --
+-- Cancellative functors
+
+-- | A group on 'Applicative' functors.
+--
+-- 'Cancellative' functors have the following laws in addition to those of
+-- 'Alternative':
+--
+-- [Left Cancellation] @ 'cancel' a '<|>' a = 'empty' @
+-- [Rigth Cancellation] @ a '<|>' 'cancel' a = 'empty' @
+--
+-- This is analogous to a group operation on applicative functors,
+-- in the sense that 'Alternative' forms a monoid. A straight-
+-- forward implementation exists whenever @f a@ forms a 'Group'
+-- for all @a@, in which case, @cancel == invert@.
+--
+class Alternative f => Cancellative f where
+  -- | Invert (or 'cancel') a 'Cancellative' functor, such that, if the
+  -- functor is also a 'Data.Group.Foldable.GroupFoldable', then @'Data.Group.Foldable.gold' '.' 'cancel'@
+  -- amounts to evaluating the inverse of a word in the functor.
+  --
+  -- === __Examples:__
+  --
+  -- >>> let x = FreeGroup [Left (Sum (2 :: Word8)), Right (Sum 3)]
+  -- >>> cancel x
+  -- FreeGroup {runFreeGroup = [Left (Sum {getSum = 3}),Right (Sum {getSum = 2})]}
+  --
+  cancel :: f a -> f a
+  default cancel :: Group (f a) => f a -> f a
+  cancel = invert
+
+instance Cancellative FG
+instance Cancellative FA
+instance Cancellative FreeGroup
+instance Cancellative Proxy where
+  cancel _ = Proxy
+
+-- -------------------------------------------------------------------- --
+-- Cancellative functor combinators
+
+-- | Cancel a single element in a 'Cancellative' functor.
+--
+-- === __Examples:__
+--
+-- >>> let x = FreeGroup [Left (Sum (2 :: Word8)), Right (Sum 3)]
+-- >>> gold x
+-- Sum {getSum = 1}
+-- >>> gold $ cancel1 (Sum 1) x
+-- Sum {getSum = 0}
+--
+cancel1 :: (Group a, Cancellative f) => a -> f a -> f a
+cancel1 a f = cancel (pure a) <|> f
+
+-- | Annihilate a 'Traversable'\'s worth of elements in a 'Cancellative'
+-- functor.
+--
+annihilate :: (Cancellative f, Traversable t) => (a -> f a) -> t a -> f (t a)
+annihilate f = traverse (cancel . f)
diff --git a/src/Data/Group.hs b/src/Data/Group.hs
--- a/src/Data/Group.hs
+++ b/src/Data/Group.hs
@@ -1,7 +1,7 @@
-{-# language BangPatterns #-}
 {-# language CPP #-}
 {-# language DerivingStrategies #-}
 {-# language FlexibleInstances #-}
+{-# language PackageImports #-}
 {-# language PatternSynonyms #-}
 {-# language Safe #-}
 #if MIN_VERSION_base(4,12,0)
@@ -18,23 +18,24 @@
 -- Stability    : stable
 -- Portability  : non-portable
 --
--- This module contains definitions for 'Group' and 'AbelianGroup',
+-- This module contains definitions for 'Group' and 'Abelian',
 -- along with the relevant combinators.
 --
 module Data.Group
 ( -- * Groups
-  Group(..)
+  -- $groups
+  G.Group(..)
   -- * Group combinators
+, minus
+, gtimes
 , (><)
   -- ** Conjugation
 , conjugate
 , unconjugate
 , pattern Conjugate
-  -- ** Order
-, Order(..)
-, pattern Infinitary
-, pattern Finitary
-, order
+  -- ** Elements
+, pattern Inverse
+, pattern IdentityElem
   -- ** Abelianization
 , Abelianizer(..)
 , abelianize
@@ -42,32 +43,16 @@
 , pattern Abelianized
 , pattern Quotiented
   -- * Abelian groups
-, AbelianGroup
+  -- $abelian
+, G.Abelian
 ) where
 
 
 import Data.Bool
-import Data.Functor.Const
-#if __GLASGOW_HASKELL__ > 804
-import Data.Functor.Contravariant
-#endif
-import Data.Functor.Identity
-import Data.Semigroup (stimes)
-import Data.Int
+import "groups" Data.Group as G
 import Data.Monoid
-import Data.Ord
-import Data.Proxy
-import Data.Ratio
-import Data.Word
 
-import Numeric.Natural
-
-#if MIN_VERSION_base(4,12,0)
-import GHC.Generics
-#endif
-
 import Prelude hiding (negate, exponent)
-import qualified Prelude
 
 -- $setup
 --
@@ -75,299 +60,69 @@
 -- >>> import Data.Group
 -- >>> import Data.Monoid
 -- >>> import Data.Semigroup
+-- >>> import Data.Word
 -- >>> :set -XTypeApplications
 -- >>> :set -XFlexibleContexts
 
 infixr 6 ><
 
 -- -------------------------------------------------------------------- --
--- Groups
-
--- | The typeclass of groups (types with an associative binary operation that
--- has an identity, and all inverses, i.e. a 'Monoid' with all inverses),
--- representing the structural symmetries of a mathematical object.
---
--- Instances should satisfy the following:
---
--- [Right identity] @ x '<>' 'mempty' = x@
--- [Left identity]  @'mempty' '<>' x = x@
--- [Associativity]  @ x '<>' (y '<>' z) = (x '<>' y) '<>' z@
--- [Concatenation]  @ 'mconcat' = 'foldr' ('<>') 'mempty'@
--- [Right inverses] @ x '<>' 'invert' x = 'mempty' @
--- [Left inverses]  @ 'invert' x '<>' x = 'mempty' @
---
--- Some types can be viewed as a group in more than one way,
--- e.g. both addition and multiplication on numbers.
--- In such cases we often define @newtype@s and make those instances
--- of 'Group', e.g. 'Data.Semigroup.Sum' and 'Data.Semigroup.Product'.
--- Often in practice such differences between addition and
--- multiplication-like operations matter (e.g. when defining rings), and
--- so, classes "additive" (the underlying operation is addition-like) and
--- "multiplicative" group classes are provided in vis 'Data.Group.Additive.AdditiveGroup' and
--- 'Data.Group.Multiplicative.MultiplicativeGroup'.
---
--- Categorically, 'Group's may be viewed single-object groupoids.
---
-class Monoid a => Group a where
-  invert :: a -> a
-  invert a = mempty `minus` a
-  {-# inline invert #-}
-
-  -- | Similar to 'stimes' from 'Data.Semigroup', but handles
-  -- negative powers by using 'invert' appropriately.
-  --
-  -- === __Examples:__
-  --
-  -- >>> gtimes 2 (Sum 3)
-  -- Sum {getSum = 6}
-  -- >>> gtimes (-3) (Sum 3)
-  -- Sum {getSum = -9}
-  --
-  gtimes :: (Integral n) => n -> a -> a
-  gtimes n a
-    | n == 0 = mempty
-    | n > 0 = stimes n a
-    | otherwise = stimes (abs n) (invert a)
-  {-# inline gtimes #-}
-
-  -- | 'Group' subtraction.
-  --
-  -- This function denotes principled 'Group' subtraction, where
-  -- @a `minus` b@ translates into @a <> (invert b)@. This is because
-  -- subtraction as an operator is non-associative, but the operation
-  -- described in terms of addition and inversion is.
-  --
-  minus :: a -> a -> a
-  minus a b = a <> invert b
-  {-# inline minus #-}
-  {-# minimal invert | minus #-}
-
-
-instance Group () where
-  invert = id
-  {-# inline invert #-}
-
-instance Group b => Group (a -> b) where
-  invert f = invert . f
-  {-# inline invert #-}
-
-instance Group a => Group (Dual a) where
-  invert (Dual a) = Dual (invert a)
-  {-# inline invert #-}
-
-instance Group a => Group (Down a) where
-  invert (Down a) = Down (invert a)
-  {-# inline invert #-}
-
-instance Group a => Group (Endo a) where
-  invert (Endo a) = Endo (invert . a)
-  {-# inline invert #-}
-
-#if __GLASGOW_HASKELL__ > 804
-instance Group (Equivalence a) where
-  invert (Equivalence p) = Equivalence $ \a b -> not (p a b)
-  {-# inline invert #-}
-
-instance Group (Comparison a) where
-  invert (Comparison p) = Comparison $ \a b -> invert (p a b)
-  {-# inline invert #-}
-
-instance Group (Predicate a) where
-  invert (Predicate p) = Predicate $ \a -> not (p a)
-  {-# inline invert #-}
-
-instance Group a => Group (Op a b) where
-  invert (Op f) = Op $ invert . f
-  {-# inline invert #-}
-#endif
-
-instance Group Any where
-  invert (Any b) = Any $ bool True False b
-  {-# inline invert #-}
-
-instance Group All where
-  invert (All b) = All $ bool True False b
-  {-# inline invert #-}
-
-instance Group (Sum Integer) where
-  invert = Prelude.negate
-  {-# inline invert #-}
-
-instance Group (Sum Rational) where
-  invert = Prelude.negate
-  {-# inline invert #-}
-
-instance Group (Sum Int) where
-  invert = Prelude.negate
-  {-# inline invert #-}
-
-instance Group (Sum Int8) where
-  invert = Prelude.negate
-  {-# inline invert #-}
-
-instance Group (Sum Int16) where
-  invert = Prelude.negate
-  {-# inline invert #-}
-
-instance Group (Sum Int32) where
-  invert = Prelude.negate
-  {-# inline invert #-}
-
-instance Group (Sum Int64) where
-  invert = Prelude.negate
-  {-# inline invert #-}
-
-instance Group (Sum Word) where
-  invert = Prelude.negate
-  {-# inline invert #-}
-
-instance Group (Sum Word8) where
-  invert = Prelude.negate
-  {-# inline invert #-}
-
-instance Group (Sum Word16) where
-  invert = Prelude.negate
-  {-# inline invert #-}
-
-instance Group (Sum Word32) where
-  invert = Prelude.negate
-  {-# inline invert #-}
-
-instance Group (Sum Word64) where
-  invert = Prelude.negate
-  {-# inline invert #-}
-
-instance Group (Sum (Ratio Int)) where
-  invert = Sum . Prelude.negate . getSum
-  {-# inline invert #-}
-
-instance Group (Sum (Ratio Int8)) where
-  invert = Sum . Prelude.negate . getSum
-  {-# inline invert #-}
-
-instance Group (Sum (Ratio Int16)) where
-  invert = Sum . Prelude.negate . getSum
-  {-# inline invert #-}
-
-instance Group (Sum (Ratio Int32)) where
-  invert = Sum . Prelude.negate . getSum
-  {-# inline invert #-}
-
-instance Group (Sum (Ratio Int64)) where
-  invert = Sum . Prelude.negate . getSum
-  {-# inline invert #-}
-
-instance Group (Sum (Ratio Word)) where
-  invert = Sum . Prelude.negate . getSum
-  {-# inline invert #-}
-
-instance Group (Sum (Ratio Word8)) where
-  invert = Sum . Prelude.negate . getSum
-  {-# inline invert #-}
-
-instance Group (Sum (Ratio Word16)) where
-  invert = Sum . Prelude.negate . getSum
-  {-# inline invert #-}
-
-instance Group (Sum (Ratio Word32)) where
-  invert = Sum . Prelude.negate . getSum
-  {-# inline invert #-}
-
-instance Group (Sum (Ratio Word64)) where
-  invert = Sum . Prelude.negate . getSum
-  {-# inline invert #-}
-
-instance Group (Product Rational) where
-  invert = Product . Prelude.recip . getProduct
-  {-# inline invert #-}
-
-instance Group (Product (Ratio Natural)) where
-  invert = Product . Prelude.recip . getProduct
-  {-# inline invert #-}
-
-instance Group (Product (Ratio Int)) where
-  invert = Product . Prelude.recip . getProduct
-  {-# inline invert #-}
-
-instance Group (Product (Ratio Int8)) where
-  invert = Product . Prelude.recip . getProduct
-  {-# inline invert #-}
-
-instance Group (Product (Ratio Int16)) where
-  invert = Product . Prelude.recip . getProduct
-  {-# inline invert #-}
-
-instance Group (Product (Ratio Int32)) where
-  invert = Product . Prelude.recip . getProduct
-  {-# inline invert #-}
-
-instance Group (Product (Ratio Int64)) where
-  invert = Product . Prelude.recip . getProduct
-  {-# inline invert #-}
-
-instance Group (Product (Ratio Word)) where
-  invert = Product . Prelude.recip . getProduct
-  {-# inline invert #-}
-
-instance Group (Product (Ratio Word8)) where
-  invert = Product . Prelude.recip . getProduct
-  {-# inline invert #-}
-
-instance Group (Product (Ratio Word16)) where
-  invert = Product . Prelude.recip . getProduct
-  {-# inline invert #-}
-
-instance Group (Product (Ratio Word32)) where
-  invert = Product . Prelude.recip . getProduct
-  {-# inline invert #-}
-
-instance Group (Product (Ratio Word64)) where
-  invert = Product . Prelude.recip . getProduct
-  {-# inline invert #-}
-
-instance Group a => Group (Const a b) where
-  invert = Const . invert . getConst
-  {-# inline invert #-}
-
-instance Group a => Group (Identity a) where
-  invert = Identity . invert . runIdentity
-  {-# inline invert #-}
-
-instance Group Ordering where
-  invert LT = GT
-  invert EQ = EQ
-  invert GT = LT
-  {-# inline invert #-}
+-- Group combinators
 
-instance (Group a, Group b) => Group (a,b) where
-  invert ~(a,b) = (invert a, invert b)
-  {-# inline invert #-}
+{- $groups
 
-instance Group a => Group (Proxy a) where
-  invert _ = Proxy
+The typeclass of groups (types with an associative binary operation that
+has an identity, and all inverses, i.e. a 'Monoid' with all inverses),
+representing the structural symmetries of a mathematical object.
 
-instance (Group a, Group b, Group c) => Group (a,b,c) where
-  invert ~(a,b,c) = (invert a, invert b, invert c)
-  {-# inline invert #-}
+Instances should satisfy the following:
 
-instance (Group a, Group b, Group c, Group d) => Group (a,b,c,d) where
-  invert ~(a,b,c,d) = (invert a, invert b, invert c, invert d)
-  {-# inline invert #-}
+[Right identity] @ x '<>' 'mempty' = x@
+[Left identity]  @'mempty' '<>' x = x@
+[Associativity]  @ x '<>' (y '<>' z) = (x '<>' y) '<>' z@
+[Concatenation]  @ 'mconcat' = 'foldr' ('<>') 'mempty'@
+[Right inverses] @ x '<>' 'invert' x = 'mempty' @
+[Left inverses]  @ 'invert' x '<>' x = 'mempty' @
 
-instance (Group a, Group b, Group c, Group d, Group e) => Group (a,b,c,d,e) where
-  invert ~(a,b,c,d,e) = (invert a, invert b, invert c, invert d, invert e)
-  {-# inline invert #-}
+Some types can be viewed as a group in more than one way,
+e.g. both addition and multiplication on numbers.
+In such cases we often define @newtype@s and make those instances
+of 'Group', e.g. 'Data.Semigroup.Sum' and 'Data.Semigroup.Product'.
+Often in practice such differences between addition and
+multiplication-like operations matter (e.g. when defining rings), and
+so, classes "additive" (the underlying operation is addition-like) and
+"multiplicative" group classes are provided in vis 'Data.Group.Additive.AdditiveGroup' and
+'Data.Group.Multiplicative.MultiplicativeGroup'.
 
-#if MIN_VERSION_base(4,12,0)
-instance (Group (f a), Group (g a)) => Group ((f :*: g) a) where
-  invert (f :*: g) = invert f :*: invert g
+Categorically, 'Group's may be viewed single-object groupoids.
+-}
 
-instance Group (f (g a)) => Group ((f :.: g) a) where
-  invert (Comp1 fg) = invert (Comp1 fg)
-#endif
+-- | An alias to 'pow'.
+--
+-- Similar to 'Data.Semigroup.stimes' from 'Data.Semigroup', but handles
+-- negative powers by using 'invert' appropriately.
+--
+-- === __Examples:__
+--
+-- >>> gtimes 2 (Sum 3)
+-- Sum {getSum = 6}
+-- >>> gtimes (-3) (Sum 3)
+-- Sum {getSum = -9}
+--
+gtimes :: (Group a, Integral n) => n -> a -> a
+gtimes = flip pow
+{-# inline gtimes #-}
 
--- -------------------------------------------------------------------- --
--- Group combinators
+-- | 'Group' subtraction.
+--
+-- This function denotes principled 'Group' subtraction, where
+-- @a `minus` b@ translates into @a <> invert b@. This is because
+-- subtraction as an operator is non-associative, but the operation
+-- described in terms of addition and inversion is.
+--
+minus :: Group a => a -> a -> a
+minus a b = a <> invert b
+{-# inline minus #-}
 
 -- | Apply @('<>')@, commuting its arguments. When the group is abelian,
 -- @a <> b@ is identically @b <> a@.
@@ -376,6 +131,9 @@
 a >< b = b <> a
 {-# inline (><) #-}
 
+-- -------------------------------------------------------------------- --
+-- Group conjugation
+
 -- | Conjugate an element of a group by another element.
 -- When the group is abelian, conjugation is the identity.
 --
@@ -387,10 +145,6 @@
 -- >>> conjugate x x
 -- Sum {getSum = 3}
 --
--- >>> let x = All True
--- >>> conjugate (All False) x
--- All {getAll = False}
---
 conjugate :: Group a => a -> a -> a
 conjugate g a = (g <> a) `minus` g
 {-# inline conjugate #-}
@@ -421,56 +175,15 @@
   Conjugate (g,a) = (g, unconjugate g a)
 {-# complete Conjugate #-}
 
--- -------------------------------------------------------------------- --
--- Group order
-
--- | The order of a group element.
---
--- The order of a group element can either be infinite,
--- as in the case of @All False@, or finite, as in the
--- case of @All True@.
---
-data Order = Infinite | Finite !Natural
-  deriving (Eq, Show)
-
--- | Unidirectional pattern synonym for the infinite order of a
--- group element.
---
-pattern Infinitary :: (Eq g, Group g) => g
-pattern Infinitary <- (order -> Infinite)
-
--- | Unidirectional pattern synonym for the finite order of a
--- group element.
---
-pattern Finitary :: (Eq g, Group g) => Natural -> g
-pattern Finitary n <- (order -> Finite n)
+-- | Bidirectional pattern for inverse elements.
+pattern Inverse :: (Group g) => g -> g
+pattern Inverse t <- (invert -> t) where
+    Inverse g = invert g
 
--- | Calculate the exponent of a particular element in a group.
---
--- __Warning:__ If 'order' expects a 'Data.Group.FiniteGroup', this is gauranteed
--- to terminate. However, this is not true of groups in general. This will
--- spin forever if you give it something like non-zero @Sum Integer@.
---
--- === __Examples__:
---
--- >>> order @(Sum Word8) 3
--- Finite 255
---
--- >>> order (Any False)
--- Finite 1
---
--- >>> order (All False)
--- Infinite
---
-order :: (Eq g, Group g) => g -> Order
-order a = go 0 a where
-  go !n g
-    -- guard against ().
-    | g == mempty, n > 0 = Finite n
-    -- guard against infinite cases like @All False@.
-    | g == a, n > 0 = Infinite
-    | otherwise = go (succ n) (g <> a)
-{-# inline order #-}
+-- | Bidirectional pattern for the identity element.
+pattern IdentityElem :: (Eq m, Monoid m) => m
+pattern IdentityElem <- ((== mempty) -> True) where
+  IdentityElem = mempty
 
 -- -------------------------------------------------------------------- --
 -- Abelianization
@@ -559,72 +272,10 @@
 -- -------------------------------------------------------------------- --
 -- Abelian (commutative) groups
 
--- | Commutative 'Group's.
---
--- Instances of 'AbelianGroup' satisfy the following laws:
---
--- [Commutativity] @x <> y = y <> x@
---
-class Group a => AbelianGroup a
-instance AbelianGroup ()
-instance AbelianGroup b => AbelianGroup (a -> b)
-instance AbelianGroup a => AbelianGroup (Dual a)
-instance AbelianGroup Any
-instance AbelianGroup All
-instance AbelianGroup (Sum Integer)
-instance AbelianGroup (Sum Int)
-instance AbelianGroup (Sum Int8)
-instance AbelianGroup (Sum Int16)
-instance AbelianGroup (Sum Int32)
-instance AbelianGroup (Sum Int64)
-instance AbelianGroup (Sum Word)
-instance AbelianGroup (Sum Word8)
-instance AbelianGroup (Sum Word16)
-instance AbelianGroup (Sum Word32)
-instance AbelianGroup (Sum Word64)
-instance AbelianGroup (Sum (Ratio Integer))
-instance AbelianGroup (Sum (Ratio Int))
-instance AbelianGroup (Sum (Ratio Int8))
-instance AbelianGroup (Sum (Ratio Int16))
-instance AbelianGroup (Sum (Ratio Int32))
-instance AbelianGroup (Sum (Ratio Int64))
-instance AbelianGroup (Sum (Ratio Word))
-instance AbelianGroup (Sum (Ratio Word8))
-instance AbelianGroup (Sum (Ratio Word16))
-instance AbelianGroup (Sum (Ratio Word32))
-instance AbelianGroup (Sum (Ratio Word64))
-instance AbelianGroup (Product (Ratio Integer))
-instance AbelianGroup (Product (Ratio Int))
-instance AbelianGroup (Product (Ratio Int8))
-instance AbelianGroup (Product (Ratio Int16))
-instance AbelianGroup (Product (Ratio Int32))
-instance AbelianGroup (Product (Ratio Int64))
-instance AbelianGroup (Product (Ratio Word))
-instance AbelianGroup (Product (Ratio Word8))
-instance AbelianGroup (Product (Ratio Word16))
-instance AbelianGroup (Product (Ratio Word32))
-instance AbelianGroup (Product (Ratio Word64))
-instance AbelianGroup (Product (Ratio Natural))
-instance AbelianGroup a => AbelianGroup (Const a b)
-instance AbelianGroup a => AbelianGroup (Identity a)
-instance AbelianGroup a => AbelianGroup (Proxy a)
-instance AbelianGroup Ordering
-instance (AbelianGroup a, AbelianGroup b) => AbelianGroup (a,b)
-instance (AbelianGroup a, AbelianGroup b, AbelianGroup c) => AbelianGroup (a,b,c)
-instance (AbelianGroup a, AbelianGroup b, AbelianGroup c, AbelianGroup d) => AbelianGroup (a,b,c,d)
-instance (AbelianGroup a, AbelianGroup b, AbelianGroup c, AbelianGroup d, AbelianGroup e) => AbelianGroup (a,b,c,d,e)
-instance AbelianGroup a => AbelianGroup (Down a)
-instance AbelianGroup a => AbelianGroup (Endo a)
-#if MIN_VERSION_base(4,12,0)
-instance (AbelianGroup (f a), AbelianGroup (g a)) => AbelianGroup ((f :*: g) a)
-instance AbelianGroup (f (g a)) => AbelianGroup ((f :.: g) a)
-#endif
+{- $abelian
+Commutative 'Group's.
 
-#if __GLASGOW_HASKELL__ > 804
-instance AbelianGroup (Equivalence a)
-instance AbelianGroup (Comparison a)
-instance AbelianGroup (Predicate a)
-instance AbelianGroup a => AbelianGroup (Op a b)
-#endif
+Instances of 'Abelian' satisfy the following laws:
 
-instance (Eq a, AbelianGroup a) => AbelianGroup (Abelianizer a)
+[Commutativity] @x <> y = y <> x@
+-}
diff --git a/src/Data/Group/Additive.hs b/src/Data/Group/Additive.hs
--- a/src/Data/Group/Additive.hs
+++ b/src/Data/Group/Additive.hs
@@ -34,12 +34,8 @@
 import Data.Functor.Const
 import Data.Functor.Identity
 import Data.Group
-import Data.Int
-import Data.Ord
 import Data.Proxy
-import Data.Ratio
 import Data.Semigroup
-import Data.Word
 
 import Prelude hiding ((-), (+))
 
@@ -67,30 +63,7 @@
 instance AdditiveGroup ()
 instance AdditiveGroup b => AdditiveGroup (a -> b)
 instance AdditiveGroup a => AdditiveGroup (Dual a)
-instance AdditiveGroup a => AdditiveGroup (Down a)
-instance AdditiveGroup Any
-instance AdditiveGroup (Sum Integer)
-instance AdditiveGroup (Sum Int)
-instance AdditiveGroup (Sum Int8)
-instance AdditiveGroup (Sum Int16)
-instance AdditiveGroup (Sum Int32)
-instance AdditiveGroup (Sum Int64)
-instance AdditiveGroup (Sum Word)
-instance AdditiveGroup (Sum Word8)
-instance AdditiveGroup (Sum Word16)
-instance AdditiveGroup (Sum Word32)
-instance AdditiveGroup (Sum Word64)
-instance AdditiveGroup (Sum (Ratio Integer))
-instance AdditiveGroup (Sum (Ratio Int))
-instance AdditiveGroup (Sum (Ratio Int8))
-instance AdditiveGroup (Sum (Ratio Int16))
-instance AdditiveGroup (Sum (Ratio Int32))
-instance AdditiveGroup (Sum (Ratio Int64))
-instance AdditiveGroup (Sum (Ratio Word))
-instance AdditiveGroup (Sum (Ratio Word8))
-instance AdditiveGroup (Sum (Ratio Word16))
-instance AdditiveGroup (Sum (Ratio Word32))
-instance AdditiveGroup (Sum (Ratio Word64))
+instance Num a => AdditiveGroup (Sum a)
 instance (AdditiveGroup a, AdditiveGroup b) => AdditiveGroup (a,b)
 instance (AdditiveGroup a, AdditiveGroup b, AdditiveGroup c) => AdditiveGroup (a,b,c)
 instance (AdditiveGroup a, AdditiveGroup b, AdditiveGroup c, AdditiveGroup d) => AdditiveGroup (a,b,c,d)
@@ -98,7 +71,6 @@
 instance AdditiveGroup a => AdditiveGroup (Const a b)
 instance AdditiveGroup a => AdditiveGroup (Identity a)
 instance AdditiveGroup a => AdditiveGroup (Proxy a)
-instance AdditiveGroup a => AdditiveGroup (Endo a)
 #if __GLASGOW_HASKELL__ > 804
 instance AdditiveGroup a => AdditiveGroup (Op a b)
 #endif
@@ -111,10 +83,6 @@
 -- >>> x - x
 -- Sum {getSum = 0}
 --
--- >>> let x = Any True
--- >>> x - x
--- Any {getAny = True}
---
 (-) :: AdditiveGroup a => a -> a -> a
 (-) = minus
 {-# inline (-) #-}
@@ -161,36 +129,14 @@
 -- -------------------------------------------------------------------- --
 -- Additive abelian groups
 
--- | An additive abelian group is an 'AbelianGroup' whose operation can be thought of
+-- | An additive abelian group is an 'Abelian' whose operation can be thought of
 -- as commutative addition in some sense. Almost all additive groups are abelian.
 --
-class (AbelianGroup g, AdditiveGroup g) => AdditiveAbelianGroup g
+class (Abelian g, AdditiveGroup g) => AdditiveAbelianGroup g
 instance AdditiveAbelianGroup ()
 instance AdditiveAbelianGroup b => AdditiveAbelianGroup (a -> b)
 instance AdditiveAbelianGroup a => AdditiveAbelianGroup (Dual a)
-instance AdditiveAbelianGroup Any
-instance AdditiveAbelianGroup (Sum Integer)
-instance AdditiveAbelianGroup (Sum Int)
-instance AdditiveAbelianGroup (Sum Int8)
-instance AdditiveAbelianGroup (Sum Int16)
-instance AdditiveAbelianGroup (Sum Int32)
-instance AdditiveAbelianGroup (Sum Int64)
-instance AdditiveAbelianGroup (Sum Word)
-instance AdditiveAbelianGroup (Sum Word8)
-instance AdditiveAbelianGroup (Sum Word16)
-instance AdditiveAbelianGroup (Sum Word32)
-instance AdditiveAbelianGroup (Sum Word64)
-instance AdditiveAbelianGroup (Sum (Ratio Integer))
-instance AdditiveAbelianGroup (Sum (Ratio Int))
-instance AdditiveAbelianGroup (Sum (Ratio Int8))
-instance AdditiveAbelianGroup (Sum (Ratio Int16))
-instance AdditiveAbelianGroup (Sum (Ratio Int32))
-instance AdditiveAbelianGroup (Sum (Ratio Int64))
-instance AdditiveAbelianGroup (Sum (Ratio Word))
-instance AdditiveAbelianGroup (Sum (Ratio Word8))
-instance AdditiveAbelianGroup (Sum (Ratio Word16))
-instance AdditiveAbelianGroup (Sum (Ratio Word32))
-instance AdditiveAbelianGroup (Sum (Ratio Word64))
+instance Num a => AdditiveAbelianGroup (Sum a)
 instance (AdditiveAbelianGroup a, AdditiveAbelianGroup b) => AdditiveAbelianGroup (a,b)
 instance (AdditiveAbelianGroup a, AdditiveAbelianGroup b, AdditiveAbelianGroup c) => AdditiveAbelianGroup (a,b,c)
 instance (AdditiveAbelianGroup a, AdditiveAbelianGroup b, AdditiveAbelianGroup c, AdditiveAbelianGroup d) => AdditiveAbelianGroup (a,b,c,d)
@@ -198,8 +144,6 @@
 instance AdditiveAbelianGroup a => AdditiveAbelianGroup (Const a b)
 instance AdditiveAbelianGroup a => AdditiveAbelianGroup (Identity a)
 instance AdditiveAbelianGroup a => AdditiveAbelianGroup (Proxy a)
-instance AdditiveAbelianGroup a => AdditiveAbelianGroup (Down a)
-instance AdditiveAbelianGroup a => AdditiveAbelianGroup (Endo a)
 #if __GLASGOW_HASKELL__ > 804
 instance AdditiveAbelianGroup a => AdditiveAbelianGroup (Op a b)
 #endif
diff --git a/src/Data/Group/Cyclic.hs b/src/Data/Group/Cyclic.hs
--- a/src/Data/Group/Cyclic.hs
+++ b/src/Data/Group/Cyclic.hs
@@ -1,5 +1,5 @@
-{-# language BangPatterns #-}
 {-# language FlexibleInstances #-}
+{-# language PackageImports #-}
 {-# language Safe #-}
 -- |
 -- Module       : Data.Group.Cyclic
@@ -11,26 +11,19 @@
 -- Stability    : stable
 -- Portability  : non-portable
 --
--- This module contains definitions for 'CyclicGroup'
+-- This module contains definitions for 'Cyclic' groups,
 -- along with the relevant combinators.
 --
 module Data.Group.Cyclic
 ( -- * Cyclic groups
-  CyclicGroup(..)
+  -- $cyclic
+  G.Cyclic(..)
   -- ** Combinators
-, generate
 , classify
+, G.generated
 ) where
 
-import Data.Functor.Const
-import Data.Functor.Identity
-import Data.Group
-import Data.Int
-import Data.List
-import Data.Monoid
-import Data.Ord
-import Data.Proxy
-import Data.Word
+import "groups" Data.Group as G
 
 -- $setup
 --
@@ -38,142 +31,33 @@
 -- >>> import Data.Group
 -- >>> import Data.Monoid
 -- >>> import Data.Semigroup
+-- >>> import Data.Word
 -- >>> :set -XTypeApplications
 
 -- -------------------------------------------------------------------- --
 -- Cyclic groups
 
--- | A 'CyclicGroup' is a 'Group' that is generated by a single element.
--- This element is called a /generator/ of the group. There can be many
--- generators for a group, e.g., any representative of an equivalence
--- class of prime numbers of the integers modulo @n@, but to make things
--- easy, we ask for only one generator.
---
-class Group g => CyclicGroup g where
-  generator :: g
-  {-# minimal generator #-}
 
-instance CyclicGroup () where
-  generator = ()
-  {-# inline generator #-}
-
--- instance CyclicGroup b => CyclicGroup (a -> b) where
---   generator = const generator
---   {-# inlinable generator #-}
-
-instance CyclicGroup a => CyclicGroup (Dual a) where
-  generator = Dual (invert generator)
-  {-# inlinable generator #-}
-
-instance CyclicGroup (Sum Integer) where
-  generator = 1
-  {-# inline generator #-}
-
-instance CyclicGroup (Sum Rational) where
-  generator = 1
-  {-# inline generator #-}
-
-instance CyclicGroup (Sum Int) where
-  generator = 1
-  {-# inline generator #-}
-
-instance CyclicGroup (Sum Int8) where
-  generator = 1
-  {-# inline generator #-}
-
-instance CyclicGroup (Sum Int16) where
-  generator = 1
-  {-# inline generator #-}
-
-instance CyclicGroup (Sum Int32) where
-  generator = 1
-  {-# inline generator #-}
-
-instance CyclicGroup (Sum Int64) where
-  generator = 1
-  {-# inline generator #-}
-
-instance CyclicGroup (Sum Word) where
-  generator = 1
-  {-# inline generator #-}
-
-instance CyclicGroup (Sum Word8) where
-  generator = 1
-  {-# inline generator #-}
-
-instance CyclicGroup (Sum Word16) where
-  generator = 1
-  {-# inline generator #-}
-
-instance CyclicGroup (Sum Word32) where
-  generator = 1
-  {-# inline generator #-}
-
-instance CyclicGroup (Sum Word64) where
-  generator = 1
-  {-# inline generator #-}
-
-instance CyclicGroup a => CyclicGroup (Const a b) where
-  generator = Const generator
-  {-# inlinable generator #-}
-
-instance CyclicGroup a => CyclicGroup (Identity a) where
-  generator = Identity generator
-  {-# inlinable generator #-}
-
-instance CyclicGroup a => CyclicGroup (Proxy a) where
-  generator = Proxy
-  {-# inlinable generator #-}
-
-instance (CyclicGroup a, CyclicGroup b) => CyclicGroup (a,b) where
-  generator = (generator, generator)
-  {-# inlinable generator #-}
-
-instance (CyclicGroup a, CyclicGroup b, CyclicGroup c) => CyclicGroup (a,b,c) where
-  generator = (generator, generator, generator)
-  {-# inlinable generator #-}
-
-instance (CyclicGroup a, CyclicGroup b, CyclicGroup c, CyclicGroup d) => CyclicGroup (a,b,c,d)  where
-  generator = (generator, generator, generator, generator)
-  {-# inlinable generator #-}
-
-instance (CyclicGroup a, CyclicGroup b, CyclicGroup c, CyclicGroup d, CyclicGroup e) => CyclicGroup (a,b,c,d,e) where
-  generator = (generator, generator, generator, generator, generator)
-  {-# inlinable generator #-}
-
-instance CyclicGroup a => CyclicGroup (Down a) where
-  generator = Down generator
-  {-# inline generator #-}
-
-instance CyclicGroup a => CyclicGroup (Endo a) where
-  generator = Endo $ const generator
-  {-# inline generator #-}
+{- $cyclic
 
--- -------------------------------------------------------------------- --
--- Cyclic group combinators
+'Cyclic' is a 'Group' that is generated by a single element.
+This element is called a /generator/ of the group. There can be many
+generators for a group, e.g., any representative of an equivalence
+class of prime numbers of the integers modulo @n@, but to make things
+easy, we ask for only one generator.
 
--- | Lazily generate all elements of a 'CyclicGroup' from its generator.
---
--- /Note/: fuses.
---
-generate :: (Eq a, CyclicGroup a) => [a]
-generate = unfoldr go (generator, 0 :: Integer)
-  where
-    go (a, !n)
-      | a == mempty, n > 0 = Nothing
-      | otherwise = Just (a, (a <> generator, succ n))
-{-# noinline generate #-}
+-}
 
--- | Classify elements of a 'CyclicGroup'.
+-- | Classify elements of a 'Cyclic' group.
 --
 -- Apply a classifying function @a -> Bool@ to the elements
--- of a 'CyclicGroup' as generated by its designated generator.
+-- of a 'Cyclic' group as generated by its designated generator.
 --
 -- === __Examples__:
 --
--- >>> classify (< (3 :: Sum Word8))
+-- >>> take 3 $ classify (< (3 :: Sum Word8))
 -- [Sum {getSum = 1},Sum {getSum = 2}]
 --
-classify :: (Eq a, CyclicGroup a) => (a -> Bool) -> [a]
-classify p = filter p generate
+classify :: (Eq a, G.Cyclic a) => (a -> Bool) -> [a]
+classify p = filter p G.generated'
 {-# inline classify #-}
diff --git a/src/Data/Group/Finite.hs b/src/Data/Group/Finite.hs
--- a/src/Data/Group/Finite.hs
+++ b/src/Data/Group/Finite.hs
@@ -1,5 +1,6 @@
 {-# language CPP #-}
 {-# language FlexibleInstances #-}
+{-# language BangPatterns #-}
 {-# language Safe #-}
 -- |
 -- Module       : Data.Group.Finite
@@ -19,7 +20,8 @@
 ( -- * Finite groups
   FiniteGroup
   -- ** Finite group combinators
-, safeOrder
+, finiteOrder
+, safeClassify
   -- * Finite abelian groups
 , FiniteAbelianGroup
 ) where
@@ -27,13 +29,10 @@
 import Data.Functor.Const
 import Data.Functor.Identity
 import Data.Group
-import Data.Int
 import Data.Monoid
-#if __GLASGOW_HASKELL__ >= 810
-import Data.Ord
-#endif
 import Data.Proxy
-import Data.Word
+import Data.Group.Cyclic
+import Numeric.Natural (Natural)
 
 -- $setup
 --
@@ -41,6 +40,7 @@
 -- >>> import Data.Group
 -- >>> import Data.Monoid
 -- >>> import Data.Semigroup
+-- >>> import Data.Word
 -- >>> :set -XTypeApplications
 
 -- -------------------------------------------------------------------- --
@@ -65,45 +65,40 @@
 instance (FiniteGroup a, FiniteGroup b, FiniteGroup c) => FiniteGroup (a,b,c)
 instance (FiniteGroup a, FiniteGroup b, FiniteGroup c, FiniteGroup d) => FiniteGroup (a,b,c,d)
 instance (FiniteGroup a, FiniteGroup b, FiniteGroup c, FiniteGroup d, FiniteGroup e) => FiniteGroup (a,b,c,d,e)
-instance FiniteGroup Any
-instance FiniteGroup All
-instance FiniteGroup (Sum Int)
-instance FiniteGroup (Sum Int8)
-instance FiniteGroup (Sum Int16)
-instance FiniteGroup (Sum Int32)
-instance FiniteGroup (Sum Int64)
-instance FiniteGroup (Sum Word)
-instance FiniteGroup (Sum Word8)
-instance FiniteGroup (Sum Word16)
-instance FiniteGroup (Sum Word32)
-instance FiniteGroup (Sum Word64)
-instance FiniteGroup Ordering
-
-#if __GLASGOW_HASKELL__ >= 810
-instance FiniteGroup a => FiniteGroup (Down a)
-#endif
+instance (Bounded a, Num a) => FiniteGroup (Sum a)
 
 -- -------------------------------------------------------------------- --
 -- Finite group combinators
 
--- | A safe version of 'order' for 'FiniteGroup's.
---
--- This is gauranteed to terminate with either @Infinite@ or @Finite@.
+-- | Calculate the exponent of a particular element in a finite group.
 --
 -- === __Examples__:
 --
--- >>> order @(Sum Word8) 3
--- Finite 255
+-- >>> finiteOrder @(Sum Word8) 3
+-- 256
 --
--- >>> order (Any False)
--- Finite 1
+finiteOrder :: (Eq g, FiniteGroup g) => g -> Natural
+finiteOrder a = go 1 a where
+  go !n g
+    | g == mempty = n
+    | otherwise   = go (succ n) (g <> a)
+{-# inline finiteOrder #-}
+
+-- | Classify elements of a finite 'Cyclic' group.
 --
--- >>> order (All False)
--- Infinite
+-- Apply a classifying function @a -> Bool@ to the elements
+-- of a 'Data.Group.Cyclic' group as generated by its designated generator.
+-- This is a safer version of 'classify', that is gauranteed
+-- to terminate.
 --
-safeOrder :: (Eq g, FiniteGroup g) => g -> Order
-safeOrder = order
-{-# inline safeOrder #-}
+-- === __Examples__:
+--
+-- >>> take 3 $ safeClassify (< (3 :: Sum Word8))
+-- [Sum {getSum = 1},Sum {getSum = 2}]
+--
+safeClassify :: (Eq a, Cyclic a, FiniteGroup a) => (a -> Bool) -> [a]
+safeClassify = classify
+{-# inline safeClassify #-}
 
 -- -------------------------------------------------------------------- --
 -- Finite abelian groups
@@ -114,16 +109,7 @@
 
 instance FiniteAbelianGroup ()
 instance FiniteAbelianGroup a => FiniteAbelianGroup (Dual a)
-instance FiniteAbelianGroup (Sum Int)
-instance FiniteAbelianGroup (Sum Int8)
-instance FiniteAbelianGroup (Sum Int16)
-instance FiniteAbelianGroup (Sum Int32)
-instance FiniteAbelianGroup (Sum Int64)
-instance FiniteAbelianGroup (Sum Word)
-instance FiniteAbelianGroup (Sum Word8)
-instance FiniteAbelianGroup (Sum Word16)
-instance FiniteAbelianGroup (Sum Word32)
-instance FiniteAbelianGroup (Sum Word64)
+instance (Num a, Bounded a) => FiniteAbelianGroup (Sum a)
 instance FiniteAbelianGroup a => FiniteAbelianGroup (Const a b)
 instance FiniteAbelianGroup a => FiniteAbelianGroup (Identity a)
 instance FiniteAbelianGroup a => FiniteAbelianGroup (Proxy a)
@@ -131,8 +117,3 @@
 instance (FiniteAbelianGroup a, FiniteAbelianGroup b, FiniteAbelianGroup c) => FiniteAbelianGroup (a,b,c)
 instance (FiniteAbelianGroup a, FiniteAbelianGroup b, FiniteAbelianGroup c, FiniteAbelianGroup d) => FiniteAbelianGroup (a,b,c,d)
 instance (FiniteAbelianGroup a, FiniteAbelianGroup b, FiniteAbelianGroup c, FiniteAbelianGroup d, FiniteAbelianGroup e) => FiniteAbelianGroup (a,b,c,d,e)
-instance FiniteAbelianGroup Ordering
-
-#if __GLASGOW_HASKELL__ >= 810
-instance FiniteAbelianGroup a => FiniteAbelianGroup (Down a)
-#endif
diff --git a/src/Data/Group/Foldable.hs b/src/Data/Group/Foldable.hs
--- a/src/Data/Group/Foldable.hs
+++ b/src/Data/Group/Foldable.hs
@@ -60,7 +60,7 @@
 -- 'GroupFoldable' has difficult-to-define laws in terms of Haskell,
 -- but is well-understood categorically: 'GroupFoldable's are
 -- functors (not necessarily 'Functor's) in the slice category \( [\mathcal{Hask}, \mathcal{Hask}] / F \),
--- where \( F \) is the free group functor in \( \mathcal{Hask} \). Hence, they are
+-- where \( F \) is the free group functor. Hence, they are
 -- defined by the natural transformations \( [\mathcal{Hask},\mathcal{Hask}](-, F) \) - i.e. 'toFG', or 'toFreeGroup'.
 --
 class GroupFoldable t where
diff --git a/src/Data/Group/Free.hs b/src/Data/Group/Free.hs
--- a/src/Data/Group/Free.hs
+++ b/src/Data/Group/Free.hs
@@ -1,6 +1,7 @@
-{-# language Safe #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# language Trustworthy #-}
 -- |
--- Module       : Data.Group
+-- Module       : Data.Group.Free
 -- Copyright    : (c) 2020 Reed Mullanix, Emily Pillmore
 -- License      : BSD-style
 --
@@ -10,7 +11,7 @@
 -- Stability    : stable
 -- Portability  : non-portable
 --
--- This module provides definitions for 'FreeGroup's and 'FreeAbelianGroup's,
+-- This module provides definitions for 'FreeGroup's and 'Data.Group.Free.FreeAbelianGroup's,
 -- along with useful combinators.
 --
 module Data.Group.Free
@@ -22,14 +23,19 @@
 , interpret'
 , present
   -- * Free abelian groups
-, FreeAbelianGroup(..)
+, FreeAbelianGroup
+, pattern FreeAbelianGroup
+, mkFreeAbelianGroup
+, runFreeAbelianGroup
   -- ** Free abelian group combinators
+, abfoldMap
 , abmap
 , abjoin
 , singleton
 , abInterpret
 ) where
 
+
 import Control.Applicative
 import Control.Monad
 
@@ -38,6 +44,9 @@
 import Data.Map (Map)
 import qualified Data.Map.Strict as Map
 import Data.Group
+import Data.Group.Free.Internal
+import Data.Group.Order
+import Data.Semigroup(Semigroup(..))
 
 -- $setup
 --
@@ -49,6 +58,9 @@
 -- >>> :set -XTypeApplications
 -- >>> :set -XFlexibleContexts
 
+-- -------------------------------------------------------------------- --
+-- Free groups
+
 -- | A representation of a free group over an alphabet @a@.
 --
 -- The intuition here is that @Left a@ represents a "negative" @a@,
@@ -67,12 +79,18 @@
     mempty = FreeGroup []
 
 instance Group (FreeGroup a) where
-    invert (FreeGroup g) = FreeGroup $ fmap inv g
-        where
-          inv :: Either a a -> Either a a
-          inv (Left a) = Right a
-          inv (Right a) = Left a
+    invert = FreeGroup
+      . fmap (either Right Left)
+      . reverse
+      . runFreeGroup
 
+instance Eq a => GroupOrder (FreeGroup a) where
+    -- TODO: It performs simplify each time @order@ is called.
+    --   Once "auto-simplify" is implemented, this
+    --   call of simplify should be removed.
+    order g | simplify g == mempty = Finite 1
+            | otherwise = Infinite
+
 instance Functor FreeGroup where
     fmap f (FreeGroup g) = FreeGroup $ fmap (bimap f f) g
 
@@ -84,7 +102,7 @@
     return = pure
     (FreeGroup g) >>= f = FreeGroup $ concatMap go g
         where
-          go (Left a)  = runFreeGroup $ invert $ f a
+          go (Left a)  = runFreeGroup $ invert (f a)
           go (Right a) = runFreeGroup $ f a
 
 instance Alternative FreeGroup where
@@ -127,45 +145,73 @@
 present = flip ($)
 {-# inline present #-}
 
--- | A representation of a free abelian group over an alphabet @a@.
---
--- The intuition here is group elements correspond with their positive
--- or negative multiplicities, and as such are simplified by construction.
---
-newtype FreeAbelianGroup a = FreeAbelianGroup { runFreeAbelian :: Map a Int }
-    deriving (Show, Eq, Ord)
-
-instance (Ord a) => Semigroup (FreeAbelianGroup a) where
-    (FreeAbelianGroup g) <> (FreeAbelianGroup g') =
-      FreeAbelianGroup $ Map.unionWith (+) g g'
+-- -------------------------------------------------------------------- --
+-- Free abelian groups
 
-instance (Ord a) => Monoid (FreeAbelianGroup a) where
-    mempty = FreeAbelianGroup mempty
+-- | /O(n)/ Constructs a 'Data.Group.Free.FreeAbelianGroup' from a finite 'Map' from
+-- the set of generators (@a@) to its multiplicities.
+mkFreeAbelianGroup :: Ord a => Map a Integer -> FreeAbelianGroup a
+mkFreeAbelianGroup = MkFreeAbelianGroup . Map.filter (/= 0)
 
-instance (Ord a) => Group (FreeAbelianGroup a) where
-    invert (FreeAbelianGroup g) = FreeAbelianGroup $ fmap negate g
+-- | /O(1)/ Gets a representation of 'Data.Group.Free.FreeAbelianGroup' as
+-- 'Map'. The returned map contains no records with
+-- multiplicity @0@ i.e. @'Map.lookup' a@ on the returned map
+-- never returns @Just 0@.
+--
+runFreeAbelianGroup :: FreeAbelianGroup a -> Map a Integer
+runFreeAbelianGroup (MkFreeAbelianGroup g) = g
 
 -- NOTE: We can't implement Functor/Applicative/Monad here
 -- due to the Ord constraint. C'est La Vie!
 
--- | Functorial 'fmap' for a 'FreeAbelianGroup'.
+-- | Given a function from generators to an abelian group @g@,
+-- lift that function to a group homomorphism from 'Data.Group.Free.FreeAbelianGroup' to @g@.
 --
+-- In other words, it's a function analogus to 'foldMap' for 'Monoid' or
+-- 'Data.Group.Foldable.goldMap' for @Group@.
+--
+abfoldMap :: (Abelian g) => (a -> g) -> FreeAbelianGroup a -> g
+abfoldMap f = Map.foldlWithKey' step mempty . runFreeAbelianGroup
+  where
+    step g a n = g <> pow (f a) n
+
+-- | Functorial 'fmap' for a 'Data.Group.Free.FreeAbelianGroup'.
+--
+-- === __Examples__:
+--
+-- >>> singleton 'a' <> singleton 'A'
+-- FreeAbelianGroup $ fromList [('A',1),('a',1)]
+-- >>> import Data.Char (toUpper)
+-- >>> abmap toUpper $ singleton 'a' <> singleton 'A'
+-- FreeAbelianGroup $ fromList [('A',2)]
+--
 abmap :: (Ord b) => (a -> b) -> FreeAbelianGroup a -> FreeAbelianGroup b
-abmap f (FreeAbelianGroup g) = FreeAbelianGroup $ Map.mapKeys f g
+abmap f = abfoldMap (singleton . f)
 
--- | Lift a singular value into a 'FreeAbelianGroup'. Analogous to 'pure'.
+-- | Lift a singular value into a 'Data.Group.Free.FreeAbelianGroup'. Analogous to 'pure'.
 --
+-- === __Examples__:
+--
+-- >>> singleton "foo"
+-- FreeAbelianGroup $ fromList [("foo",1)]
+--
 singleton :: a -> FreeAbelianGroup a
-singleton a = FreeAbelianGroup $ Map.singleton a 1
+singleton a = MkFreeAbelianGroup $ Map.singleton a 1
 
--- | Monadic 'join' for a 'FreeAbelianGroup'.
+-- | Monadic 'join' for a 'Data.Group.Free.FreeAbelianGroup'.
 --
 abjoin :: (Ord a) => FreeAbelianGroup (FreeAbelianGroup a) -> FreeAbelianGroup a
-abjoin (FreeAbelianGroup g) = FreeAbelianGroup $ Map.foldMapWithKey go g
-    where
-      go (FreeAbelianGroup g') n = fmap (*n) g'
+abjoin = abInterpret
 
 -- | Interpret a free group as a word in the underlying group @g@.
 --
-abInterpret :: (Group g) => FreeAbelianGroup g -> g
-abInterpret (FreeAbelianGroup g) = Map.foldMapWithKey (flip gtimes) g
+abInterpret :: (Abelian g) => FreeAbelianGroup g -> g
+abInterpret = abfoldMap id
+
+-- | Bidirectional pattern synonym for the construction of
+-- 'Data.Group.Free.Internal.FreeAbelianGroup's.
+--
+pattern FreeAbelianGroup :: Ord a => Map a Integer -> FreeAbelianGroup a
+pattern FreeAbelianGroup g <- MkFreeAbelianGroup g where
+    FreeAbelianGroup g = mkFreeAbelianGroup g
+{-# complete FreeAbelianGroup #-}
diff --git a/src/Data/Group/Free/Church.hs b/src/Data/Group/Free/Church.hs
--- a/src/Data/Group/Free/Church.hs
+++ b/src/Data/Group/Free/Church.hs
@@ -12,7 +12,7 @@
 -- Portability  : non-portable
 --
 -- This module provides definitions for Church-encoded
--- 'FreeGroup's, 'FreeAbelianGroup's, along with useful combinators.
+-- 'FreeGroup's, 'Data.Group.Free.Internal.FreeAbelianGroup's, along with useful combinators.
 --
 module Data.Group.Free.Church
 ( -- * Church-encoded free groups
@@ -34,18 +34,23 @@
 import Control.Applicative
 import Control.Monad
 
+import Data.Semigroup(Semigroup(..))
 import Data.Group
 import Data.Group.Free
 import qualified Data.Map.Strict as Map
 
 -- | The Church-encoding of a 'FreeGroup'.
 --
--- This datatype represents the free group on some @a@-valued
+-- This datatype represents the "true" free group in Haskell on some @a@-valued
 -- generators. For more information on why this encoding is preferred,
 -- see Dan Doel's <http://comonad.com/reader/2015/free-monoids-in-haskell/ article> in
 -- the Comonad Reader.
 --
-newtype FG a = FG { runFG :: forall g. (Group g) => (a -> g) -> g }
+-- While 'FreeGroup' et al are free in a strict language, and are more intuitive,
+-- they are not associative wtih respect to bottoms. 'FG' and 'FA' however, are,
+-- and should be preferred when working with possibly undefined data.
+--
+newtype FG a = FG { runFG :: forall g. Group g => (a -> g) -> g }
 
 instance Semigroup (FG a) where
   (FG g) <> (FG g') = FG $ \k -> g k <> g' k
@@ -101,22 +106,42 @@
 ----------------------------------------
 -- Free Abelian Groups
 
--- | The Church-encoding of a 'FreeAbelianGroup'.
+-- | The Church-encoding of a 'Data.Group.Free.Internal.FreeAbelianGroup'.
 --
 -- This datatype represents the free group on some @a@-valued
 -- generators, along with their exponents in the group.
 --
-newtype FA a = FA { runFA :: forall g. (Group g) => (a -> Int -> g) -> g }
+newtype FA a = FA { runFA :: forall g. Abelian g => (a -> Integer -> g) -> g }
 
 instance Semigroup (FA a) where
   (FA g) <> (FA g') = FA $ \k -> g k <> g' k
+  stimes = gtimes
 
 instance Monoid (FA a) where
   mempty = FA $ const mempty
 
 instance Group (FA a) where
-  invert (FA g) = FA (invert . g)
+  invert g = pow g (-1 :: Integer)
 
+  {-
+  Note: This implementation "optimizes" from the default implementation of
+  'pow', or more natural
+
+  > pow (FA g) n = FA $ \k -> gtimes n (g k)
+
+  by delaying the call of 'gtimes' as late as possible.
+
+  This is only possible because we expect 'Group g' to be an abelian group,
+  which implies the following equation hold:
+
+  > pow (x <> y) n = pow x n <> pow y n
+  -}
+  pow (FA g) n
+    | n == 0    = mempty
+    | otherwise = FA $ \k -> g (\a i -> k a (toInteger n * i))
+
+instance Abelian (FA a)
+
 instance Functor FA where
   fmap f (FA fa) = FA $ \k -> fa (k . f)
 
@@ -126,33 +151,35 @@
 
 instance Monad FA where
   return = pure
-  (FA fa) >>= f = FA $ \k -> fa (\a n -> gtimes n $ (runFA $ f a) k)
+  fa >>= f = interpretFA $ fmap f fa
 
 instance Alternative FA where
   empty = mempty
   (<|>) = (<>)
 
--- | Interpret a Church-encoded free abelian group as a concrete 'FreeAbelianGroup'.
+-- | Interpret a Church-encoded free abelian group as a concrete 'Data.Group.Free.Internal.FreeAbelianGroup'.
 --
-interpretFA :: Group g => FA g -> g
-interpretFA (FA fa) = fa (flip gtimes)
+interpretFA :: Abelian g => FA g -> g
+interpretFA (FA fa) = fa pow
 {-# inline interpretFA #-}
 
--- | Convert a Church-encoded free abelian group to a concrete 'FreeAbelianGroup'.
+-- | Convert a Church-encoded free abelian group to a concrete 'Data.Group.Free.Internal.FreeAbelianGroup'.
 --
 reifyFA :: Ord a => FA a -> FreeAbelianGroup a
 reifyFA = interpretFA . fmap singleton
 {-# inline reifyFA #-}
 
--- | Convert a concrete 'FreeAbelianGroup' to a Church-encoded free abelian group.
+-- | Convert a concrete 'Data.Group.Free.Internal.FreeAbelianGroup' to a Church-encoded free abelian group.
 --
-reflectFA :: Ord a => FreeAbelianGroup a -> FA a
-reflectFA (FreeAbelianGroup fa) = FA $ \k -> Map.foldMapWithKey k fa
+reflectFA :: FreeAbelianGroup a -> FA a
+reflectFA fa =
+  let g = runFreeAbelianGroup fa
+  in FA $ \k -> Map.foldMapWithKey k g
 {-# inline reflectFA #-}
 
 -- | Forget the commutative structure of a Church-encoded free abelian group,
 -- turning it into a standard free group.
---
-forgetFA :: Group a => FA a -> FG a
-forgetFA fa = FG ($ interpretFA fa)
+forgetFA :: (Ord a) => FA a -> FG a
+forgetFA fa = case reifyFA fa of
+  ~(FreeAbelianGroup fa') -> FG $ \t -> Map.foldMapWithKey (\a n -> t a `pow` n) fa'
 {-# inline forgetFA #-}
diff --git a/src/Data/Group/Free/Internal.hs b/src/Data/Group/Free/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Group/Free/Internal.hs
@@ -0,0 +1,101 @@
+{-# language Unsafe #-}
+-- |
+-- Module       : Data.Group.Free.Internal
+-- Copyright    : (c) 2020 Reed Mullanix, Emily Pillmore, Koji Miyazato
+-- License      : BSD-style
+--
+-- Maintainer   : Reed Mullanix <reedmullanix@gmail.com>,
+--                Emily Pillmore <emilypi@cohomolo.gy>
+--
+-- Stability    : stable
+-- Portability  : non-portable
+--
+-- This module exposes internals of 'FreeAbelianGroup'.
+--
+module Data.Group.Free.Internal
+( -- * Free abelian groups
+  FreeAbelianGroup(..)
+) where
+
+
+import Data.Map (Map)
+import qualified Data.Map.Strict as Map
+import qualified Data.Map.Merge.Strict as Map
+
+import Data.Semigroup(Semigroup(..))
+import Data.Group
+import Data.Group.Order
+
+
+-- $setup
+--
+-- >>> import qualified Prelude
+-- >>> import Data.Group
+-- >>> import Data.Monoid
+-- >>> import Data.Semigroup
+-- >>> import Data.Word
+-- >>> :set -XTypeApplications
+-- >>> :set -XFlexibleContexts
+
+-- | A representation of a free abelian group over an alphabet @a@.
+--
+-- The intuition here is group elements correspond with their positive
+-- or negative multiplicities, and as such are simplified by construction.
+--
+-- === __Examples__:
+--
+-- >>> let single a = MkFreeAbelianGroup $ Map.singleton a 1
+-- >>> a = single 'a'
+-- >>> b = single 'b'
+-- >>> a
+-- FreeAbelianGroup $ fromList [('a',1)]
+-- >>> a <> b
+-- FreeAbelianGroup $ fromList [('a',1),('b',1)]
+-- >>> a <> b == b <> a
+-- True
+-- >>> invert a
+-- FreeAbelianGroup $ fromList [('a',-1)]
+-- >>> a <> b <> invert a
+-- FreeAbelianGroup $ fromList [('b',1)]
+-- >>> gtimes 5 (a <> b)
+-- FreeAbelianGroup $ fromList [('a',5),('b',5)]
+--
+newtype FreeAbelianGroup a =
+  MkFreeAbelianGroup (Map a Integer)
+    -- ^ Unsafe "raw" constructor, which does not do normalization work.
+    -- Please use 'Data.Group.Free.mkFreeAbelianGroup' as it normalizes.
+    --
+  deriving (Eq, Ord)
+
+instance Show a => Show (FreeAbelianGroup a) where
+    showsPrec p (MkFreeAbelianGroup g) =
+        showParen (p > 0) $ ("FreeAbelianGroup $ " ++) . shows g
+
+instance (Ord a) => Semigroup (FreeAbelianGroup a) where
+    (MkFreeAbelianGroup g) <> (MkFreeAbelianGroup g') =
+      MkFreeAbelianGroup $ mergeG g g'
+      where
+        mergeG = Map.merge
+          Map.preserveMissing
+          Map.preserveMissing
+          (Map.zipWithMaybeMatched $ \_ m n -> nonZero $ m + n)
+        nonZero n = if n == 0 then Nothing else Just n
+
+    stimes = flip pow
+
+instance (Ord a) => Monoid (FreeAbelianGroup a) where
+    mempty = MkFreeAbelianGroup Map.empty
+
+instance (Ord a) => Group (FreeAbelianGroup a) where
+    invert (MkFreeAbelianGroup g) = MkFreeAbelianGroup $ Map.map negate g
+
+    pow _ 0 = mempty
+    pow (MkFreeAbelianGroup g) n
+      | n == 0    = mempty
+      | otherwise = MkFreeAbelianGroup $ Map.map (toInteger n *) g
+
+instance (Ord a) => Abelian (FreeAbelianGroup a)
+
+instance (Ord a) => GroupOrder (FreeAbelianGroup a) where
+    order g | g == mempty = Finite 1
+            | otherwise   = Infinite
diff --git a/src/Data/Group/Free/Product.hs b/src/Data/Group/Free/Product.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Group/Free/Product.hs
@@ -0,0 +1,97 @@
+-- |
+-- Module       : Data.Group.Free.Product
+-- Copyright    : (c) 2020 Reed Mullanix, Emily Pillmore
+-- License      : BSD-style
+--
+-- Maintainer   : Reed Mullanix <reedmullanix@gmail.com>,
+--                Emily Pillmore <emilypi@cohomolo.gy>
+--
+-- Stability    : stable
+-- Portability  : non-portable
+--
+-- This module provides definitions for the 'FreeProduct' of two groups,
+-- along with useful combinators.
+--
+module Data.Group.Free.Product
+( FreeProduct(..)
+, simplify
+, coproduct
+, injl
+, injr
+) where
+
+import Data.Bifunctor
+import Data.Group
+import Data.Group.Order
+
+import Data.Sequence (Seq(..))
+import qualified Data.Sequence as Seq
+
+
+-- -------------------------------------------------------------------- --
+-- Free products
+
+-- | The free product on two alphabets
+--
+-- __Note:__ This does not perform simplification upon multiplication or construction.
+-- To do this, one should use 'simplify'.
+--
+newtype FreeProduct g h = FreeProduct { runFreeProduct :: Seq (Either g h) }
+  deriving (Show, Eq, Ord)
+
+instance Functor (FreeProduct g) where
+  fmap f = FreeProduct . fmap (fmap f) . runFreeProduct
+
+instance Bifunctor FreeProduct where
+  bimap f g = FreeProduct . fmap (bimap f g) . runFreeProduct
+
+-- | /O(n)/ Simplifies a word in a 'FreeProduct'.
+-- This means that we get rid of any identity elements, and perform multiplication of neighboring @g@s and @h@s.
+--
+simplify :: (Eq g, Eq h, Monoid g, Monoid h) => FreeProduct g h -> FreeProduct g h
+simplify (FreeProduct fp) = FreeProduct $ go fp
+  where
+    go (Left IdentityElem :<| ghs) = go ghs
+    go (Right IdentityElem :<| ghs) = go ghs
+    go (Left g :<| Left g' :<| ghs) = go $ Left (g <> g') :<| ghs
+    go (Right h :<| Right h' :<| ghs) = go $ Right (h <> h') :<| ghs
+    go (gh :<| ghs) = gh :<| go ghs
+    go Empty = Empty
+
+instance Semigroup (FreeProduct g h) where
+  FreeProduct ghs <> FreeProduct ghs' = FreeProduct $ ghs <> ghs'
+
+instance Monoid (FreeProduct g h) where
+  mempty = FreeProduct Seq.empty
+
+instance (Group g, Group h) => Group (FreeProduct g h) where
+  invert (FreeProduct ghs) = FreeProduct $ bimap invert invert <$> Seq.reverse ghs
+
+instance (GroupOrder g, GroupOrder h) => GroupOrder (FreeProduct g h) where
+  -- TODO: It performs simplify each time @order@ is called.
+  --   Once "auto-simplify" is implemented, this
+  --   call of simplify should be removed.
+  order = go . runFreeProduct . simplify
+    where
+      go Seq.Empty         = Finite 1
+      go (x :<| Seq.Empty) = either order order x
+      go (Left g :<| (ghs :|> Left g'))
+        | g <> g' == mempty = go ghs
+      go (Right h :<| (ghs :|> Right h'))
+        | h <> h' == mempty = go ghs
+      go _ = Infinite
+
+-- | Left injection of an alphabet @a@ into a free product.
+--
+injl :: a -> FreeProduct a b
+injl a = FreeProduct $ Seq.singleton (Left a)
+
+-- | Right injection of an alphabet @b@ into a free product.
+--
+injr :: b -> FreeProduct a b
+injr b = FreeProduct $ Seq.singleton (Right b)
+
+-- | The 'FreeProduct' of two 'Monoid's is a coproduct in the category of monoids (and by extension, the category of groups).
+--
+coproduct :: Monoid m => (a -> m) -> (b -> m) -> FreeProduct a b -> m
+coproduct gi hi (FreeProduct ghs) = foldMap (either gi hi) ghs
diff --git a/src/Data/Group/Multiplicative.hs b/src/Data/Group/Multiplicative.hs
--- a/src/Data/Group/Multiplicative.hs
+++ b/src/Data/Group/Multiplicative.hs
@@ -29,14 +29,9 @@
 import Data.Functor.Const
 import Data.Functor.Identity
 import Data.Group
-import Data.Int
 import Data.Proxy
-import Data.Ratio
 import Data.Semigroup
-import Data.Word
 
-import Numeric.Natural
-
 import Prelude hiding ((^), (/), (*))
 
 infixl 7 /, *
@@ -63,19 +58,7 @@
 instance MultiplicativeGroup ()
 instance MultiplicativeGroup b => MultiplicativeGroup (a -> b)
 instance MultiplicativeGroup a => MultiplicativeGroup (Dual a)
-instance MultiplicativeGroup All
-instance MultiplicativeGroup (Product (Ratio Integer))
-instance MultiplicativeGroup (Product (Ratio Natural))
-instance MultiplicativeGroup (Product (Ratio Int))
-instance MultiplicativeGroup (Product (Ratio Int8))
-instance MultiplicativeGroup (Product (Ratio Int16))
-instance MultiplicativeGroup (Product (Ratio Int32))
-instance MultiplicativeGroup (Product (Ratio Int64))
-instance MultiplicativeGroup (Product (Ratio Word))
-instance MultiplicativeGroup (Product (Ratio Word8))
-instance MultiplicativeGroup (Product (Ratio Word16))
-instance MultiplicativeGroup (Product (Ratio Word32))
-instance MultiplicativeGroup (Product (Ratio Word64))
+instance Fractional a => MultiplicativeGroup (Product a)
 instance (MultiplicativeGroup a, MultiplicativeGroup b) => MultiplicativeGroup (a,b)
 instance (MultiplicativeGroup a, MultiplicativeGroup b, MultiplicativeGroup c) => MultiplicativeGroup (a,b,c)
 instance (MultiplicativeGroup a, MultiplicativeGroup b, MultiplicativeGroup c, MultiplicativeGroup d) => MultiplicativeGroup (a,b,c,d)
@@ -142,23 +125,11 @@
 -- as commutative multiplication in some sense. Almost all multiplicative groups
 -- are abelian.
 --
-class (MultiplicativeGroup g, AbelianGroup g) => MultiplicativeAbelianGroup g
+class (MultiplicativeGroup g, Abelian g) => MultiplicativeAbelianGroup g
 instance MultiplicativeAbelianGroup ()
 instance MultiplicativeAbelianGroup b => MultiplicativeAbelianGroup (a -> b)
 instance MultiplicativeAbelianGroup a => MultiplicativeAbelianGroup (Dual a)
-instance MultiplicativeAbelianGroup All
-instance MultiplicativeAbelianGroup (Product (Ratio Integer))
-instance MultiplicativeAbelianGroup (Product (Ratio Natural))
-instance MultiplicativeAbelianGroup (Product (Ratio Int))
-instance MultiplicativeAbelianGroup (Product (Ratio Int8))
-instance MultiplicativeAbelianGroup (Product (Ratio Int16))
-instance MultiplicativeAbelianGroup (Product (Ratio Int32))
-instance MultiplicativeAbelianGroup (Product (Ratio Int64))
-instance MultiplicativeAbelianGroup (Product (Ratio Word))
-instance MultiplicativeAbelianGroup (Product (Ratio Word8))
-instance MultiplicativeAbelianGroup (Product (Ratio Word16))
-instance MultiplicativeAbelianGroup (Product (Ratio Word32))
-instance MultiplicativeAbelianGroup (Product (Ratio Word64))
+instance Fractional a => MultiplicativeAbelianGroup (Product a)
 instance (MultiplicativeAbelianGroup a, MultiplicativeAbelianGroup b) => MultiplicativeAbelianGroup (a,b)
 instance (MultiplicativeAbelianGroup a, MultiplicativeAbelianGroup b, MultiplicativeAbelianGroup c) => MultiplicativeAbelianGroup (a,b,c)
 instance (MultiplicativeAbelianGroup a, MultiplicativeAbelianGroup b, MultiplicativeAbelianGroup c, MultiplicativeAbelianGroup d) => MultiplicativeAbelianGroup (a,b,c,d)
diff --git a/src/Data/Group/Order.hs b/src/Data/Group/Order.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Group/Order.hs
@@ -0,0 +1,197 @@
+{-# language Safe #-}
+{-# language FlexibleInstances #-}
+{-# language PatternSynonyms #-}
+{-# language ViewPatterns #-}
+-- |
+-- Module       : Data.Group.Order
+-- Copyright    : (c) 2020 Emily Pillmore
+--                Koji Miyazato <viercc@gmail.com>
+-- License      : BSD-style
+--
+-- Maintainer   : Emily Pillmore <emilypi@cohomolo.gy>,
+--                Reed Mullanix <reedmullanix@gmail.com>
+-- Stability    : stable
+-- Portability  : non-portable
+--
+-- This module contains definitions for 'GroupOrder'.
+module Data.Group.Order
+( -- * Group order
+  GroupOrder(..)
+  -- ** Order
+, Order(..)
+, pattern Infinitary
+, pattern Finitary
+, orderForBits
+, lcmOrder
+, FiniteGroup
+, finiteOrder
+) where
+
+
+import Data.Bits
+import Data.Functor.Const (Const(..))
+import Data.Functor.Identity (Identity(..))
+import Data.Group
+import Data.Group.Finite (FiniteGroup, finiteOrder)
+import Data.Int
+import Data.Monoid
+import Data.Ord (Down(..))
+import Data.Proxy (Proxy)
+import Data.Word
+
+
+import Numeric.Natural (Natural)
+
+
+-- -------------------------------------------------------------------- --
+-- Group order
+
+-- | The order of a group element.
+--
+-- The order of a group element can either be infinite,
+-- as in the case of @Sum Integer@, or finite, as in the
+-- case of @Sum Word8@.
+--
+data Order = Infinite | Finite !Natural
+  deriving (Eq, Show)
+
+-- | Unidirectional pattern synonym for the infinite order of a
+-- group element.
+--
+pattern Infinitary :: (GroupOrder g) => g
+pattern Infinitary <- (order -> Infinite)
+
+-- | Unidirectional pattern synonym for the finite order of a
+-- group element.
+--
+pattern Finitary :: (GroupOrder g) => Natural -> g
+pattern Finitary n <- (order -> Finite n)
+
+-- | @lcmOrder x y@ calculates the least common multiple of two 'Order's.
+--
+--   If both @x@ and @y@ are finite, it returns @'Finite' r@ where @r@
+--   is the least common multiple of them. Otherwise, it returns 'Infinite'.
+--
+-- === __Examples__:
+--
+-- >>> lcmOrder (Finite 2) (Finite 5)
+-- Finite 10
+-- >>> lcmOrder (Finite 2) (Finite 10)
+-- Finite 10
+-- >>> lcmOrder (Finite 1) Infinite
+-- Infinite
+--
+lcmOrder :: Order -> Order -> Order
+lcmOrder (Finite m) (Finite n) = Finite (lcm m n)
+lcmOrder _          _          = Infinite
+
+-- | The typeclass of groups, equipped with the function
+-- computing the order of a specific element of a group.
+--
+-- The order of @x@ is the smallest positive integer @k@
+-- such that @'Data.Group.gtimes' k x == 'mempty'@. If there are no such
+-- integers, the order of @x@ is defined to be infinity.
+--
+-- /Note:/ For any valid instances of 'GroupOrder',
+-- @order x == Finite 1@ holds if and only if @x == mempty@.
+--
+-- === __Examples__:
+--
+-- >>> order (3 :: Sum Word8)
+-- Finite 256
+-- >>> order (16 :: Sum Word8)
+-- Finite 16
+-- >>> order (0 :: Sum Integer)
+-- Finite 1
+-- >>> order (1 :: Sum Integer)
+-- Infinite
+--
+class (Eq g, Group g) => GroupOrder g where
+    -- | The order of an element of a group.
+    --
+    -- @order x@ must be @Finite k@ if the order of @x@ is
+    -- finite @k@, and must be @Infinite@ otherwise.
+    --
+    -- For a type which is also 'FiniteGroup',
+    -- @'Finite' . 'finiteOrder'@ is a valid implementation of 'order',
+    -- if not efficient.
+    order :: g -> Order
+
+instance GroupOrder () where
+    order _ = Finite 1
+
+instance GroupOrder (Proxy a) where
+    order _ = Finite 1
+
+instance GroupOrder (Sum Integer) where
+    order 0 = Finite 1
+    order _ = Infinite
+
+instance GroupOrder (Sum Rational) where
+    order 0 = Finite 1
+    order _ = Infinite
+
+instance GroupOrder (Sum Int) where order = orderForBits
+instance GroupOrder (Sum Int8) where order = orderForBits
+instance GroupOrder (Sum Int16) where order = orderForBits
+instance GroupOrder (Sum Int32) where order = orderForBits
+instance GroupOrder (Sum Int64) where order = orderForBits
+instance GroupOrder (Sum Word) where order = orderForBits
+instance GroupOrder (Sum Word8) where order = orderForBits
+instance GroupOrder (Sum Word16) where order = orderForBits
+instance GroupOrder (Sum Word32) where order = orderForBits
+instance GroupOrder (Sum Word64) where order = orderForBits
+
+
+-- | Given a number @x :: a@ represented by fixed-width binary integers,
+-- return the minimum positive integer @2^n@ such that
+-- @(fromInteger (2^n) * x :: a) == 0@.
+--
+zeroFactor :: FiniteBits a => a -> Natural
+zeroFactor a = bit (finiteBitSize a - countTrailingZeros a)
+
+-- | An efficient implementation of 'order' for additive group of
+--   fixed-width integers, like 'Int' or 'Word8'.
+--
+orderForBits :: (Integral a, FiniteBits a) => Sum a -> Order
+orderForBits (Sum a) = Finite (zeroFactor a)
+
+instance GroupOrder (Product Rational) where
+    order 1 = Finite 1
+    order _ = Infinite
+
+instance (GroupOrder a, GroupOrder b) => GroupOrder (a,b) where
+    order (a,b) = order a `lcmOrder` order b
+
+instance (GroupOrder a, GroupOrder b, GroupOrder c) => GroupOrder (a,b,c) where
+    order (a,b,c) = order ((a,b),c)
+
+instance (GroupOrder a, GroupOrder b, GroupOrder c, GroupOrder d)
+        => GroupOrder (a,b,c,d) where
+    order (a,b,c,d) = order ((a,b),(c,d))
+instance (GroupOrder a, GroupOrder b, GroupOrder c, GroupOrder d, GroupOrder e)
+        => GroupOrder (a,b,c,d,e) where
+    order (a,b,c,d,e) = order ((a,b,c),(d,e))
+
+{- Safe Haskell doesn't allow GND, at least for now.
+{-# language
+  GeneralizedNewtypeDeriving,
+  StandaloneDeriving,
+  DerivingStrategies
+#-}
+deriving newtype instance GroupOrder a => GroupOrder (Down a)
+deriving newtype instance GroupOrder a => GroupOrder (Dual a)
+deriving newtype instance GroupOrder a => GroupOrder (Const a b)
+deriving newtype instance GroupOrder a => GroupOrder (Identity a)
+-}
+instance GroupOrder a => GroupOrder (Down a) where
+    order (Down a) = order a
+
+instance GroupOrder a => GroupOrder (Dual a) where
+    order = order . getDual
+
+instance GroupOrder a => GroupOrder (Const a b) where
+    order = order . getConst
+
+instance GroupOrder a => GroupOrder (Identity a) where
+    order = order . runIdentity
diff --git a/src/Data/Group/Permutation.hs b/src/Data/Group/Permutation.hs
--- a/src/Data/Group/Permutation.hs
+++ b/src/Data/Group/Permutation.hs
@@ -1,5 +1,8 @@
+{-# language BangPatterns #-}
 {-# language PatternSynonyms #-}
 {-# language Safe #-}
+{-# language ScopedTypeVariables #-}
+{-# language TypeApplications #-}
 {-# language ViewPatterns #-}
 -- |
 -- Module       : Data.Group
@@ -31,20 +34,43 @@
 
 
 import Data.Group
-import Data.Group.Additive
-import Data.Group.Multiplicative
+import Data.Group.Order
 
+import qualified Data.IntSet as ISet
+import Data.Function (on)
+import Numeric.Natural (Natural)
+
 infixr 0 $-, -$
 
 -- -------------------------------------------------------------------- --
 -- Permutations
 
--- | Isomorphism of a finite set onto itself. Each entry consists of one
+-- | Isomorphism of a type onto itself. Each entry consists of one
 -- half of the isomorphism.
 --
 -- /Note/: It is the responsibility of the user to provide inverse proofs
 -- for 'to' and 'from'. Be responsible!
 --
+-- === __Examples:__
+--
+-- >>> p1 = permute succ pred :: Permutation Integer
+-- >>> p2 = permute negate negate :: Permutation Integer
+-- >>> to (p1 <> p2) 2
+-- -1
+-- >>> from (p1 <> p2) (-1)
+-- 2
+-- >>> to (p2 <> p1) 2
+-- -3
+--
+-- Permutations on a finite set @a@ (, indicated by satisfying
+-- @(Bounded a, Enum a)@ constraint,) can be tested their equality
+-- and computed their 'order's.
+--
+-- >>> c1 = permute not not :: Permutation Bool
+-- >>> c1 <> c1 == mempty
+-- True
+-- >>> order c1
+-- Finite 2
 data Permutation a = Permutation
   { to :: a -> a
     -- ^ The forward half of the bijection
@@ -55,20 +81,49 @@
 -- instance Profunctor Permutation where
 --   dimap = :'(
 
-instance Semigroup a => Semigroup (Permutation a) where
-  a <> b = Permutation (to a <> to b) (from a <> from b)
+instance Semigroup (Permutation a) where
+  a <> b = Permutation (to a . to b) (from b . from a)
 
-instance Monoid a => Monoid (Permutation a) where
+instance Monoid (Permutation a) where
   mempty = Permutation id id
 
-instance Group a => Group (Permutation a) where
-  invert (Permutation t f) = Permutation (f . t) (t . f)
+instance Group (Permutation a) where
+  invert (Permutation t f) = Permutation f t
 
-instance AbelianGroup a => AbelianGroup (Permutation a)
-instance AdditiveGroup a => AdditiveGroup (Permutation a)
-instance AdditiveAbelianGroup a => AdditiveAbelianGroup (Permutation a)
-instance MultiplicativeGroup a => MultiplicativeGroup (Permutation a)
+instance (Enum a, Bounded a) => Eq (Permutation a) where
+  (==) = (==) `on` (functionRepr . to)
 
+instance (Enum a, Bounded a) => Ord (Permutation a) where
+  compare = compare `on` (functionRepr . to)
+
+instance (Enum a, Bounded a) => GroupOrder (Permutation a) where
+  order Permutation{to = f} = Finite (go 1 fullSet)
+    where
+      n = 1 + fromEnum (maxBound @a)
+      fullSet = ISet.fromDistinctAscList [0 .. n - 1]
+
+      f' :: Int -> Int
+      f' = fromEnum . f . toEnum
+
+      go :: Natural -> ISet.IntSet -> Natural
+      go !ord elements = case ISet.minView elements of
+        Nothing -> ord
+        Just (k, elements') ->
+          let (period, elements'') = takeCycle k elements'
+          in go (lcm period ord) elements''
+
+      takeCycle :: Int -> ISet.IntSet -> (Natural, ISet.IntSet)
+      takeCycle k = loop 1 (f' k)
+        where
+          loop !period j elements
+            | j `ISet.member` elements = loop (succ period) (f' j) (ISet.delete j elements)
+            | {- j ∉ elements && -} j == k = (period, elements)
+            | otherwise = error $ "Non-bijective: witness=toEnum " ++ show j
+
+-- | Apply a function to all enumerated elements of a bounded enumerable type
+--
+functionRepr :: (Enum a, Bounded a) => (a -> a) -> [Int]
+functionRepr f = fromEnum . f <$> [minBound .. maxBound]
 
 -- -------------------------------------------------------------------- --
 -- Permutation group combinators