diff --git a/src/Algebra/Solver/CommutativeMonoid.agda b/src/Algebra/Solver/CommutativeMonoid.agda
index 04d4d372e6..55ed56a539 100644
--- a/src/Algebra/Solver/CommutativeMonoid.agda
+++ b/src/Algebra/Solver/CommutativeMonoid.agda
@@ -8,196 +8,43 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra
+open import Algebra.Bundles using (CommutativeMonoid)
 
-module Algebra.Solver.CommutativeMonoid {m₁ m₂} (M : CommutativeMonoid m₁ m₂) where
+module Algebra.Solver.CommutativeMonoid {c ℓ} (M : CommutativeMonoid c ℓ) where
 
-open import Data.Fin.Base using (Fin; zero; suc)
-open import Data.Maybe.Base as Maybe
-  using (Maybe; From-just; from-just)
-open import Data.Nat as ℕ using (ℕ; zero; suc; _+_)
-open import Data.Nat.GeneralisedArithmetic using (fold)
-open import Data.Product.Base using (_×_; uncurry)
-open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate)
+import Algebra.Solver.CommutativeMonoid.Normal as Normal
+import Algebra.Solver.Monoid.Tactic as Tactic
 
-open import Function.Base using (_∘_)
+open CommutativeMonoid M using (monoid)
 
-import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
-import Relation.Binary.Reflection as Reflection
-import Relation.Nullary.Decidable as Dec
-import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
-
-open import Relation.Binary.Consequences using (dec⇒weaklyDec)
-open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
-open import Relation.Nullary.Decidable as Dec using (Dec)
-
-open CommutativeMonoid M
-open ≈-Reasoning setoid
-
-private
-  variable
-    n : ℕ
 
 ------------------------------------------------------------------------
--- Monoid expressions
-
--- There is one constructor for every operation, plus one for
--- variables; there may be at most n variables.
-
-infixr 5 _⊕_
-infixr 10 _•_
-
-data Expr (n : ℕ) : Set where
-  var : Fin n → Expr n
-  id  : Expr n
-  _⊕_ : Expr n → Expr n → Expr n
+-- Expressions and Normal forms
 
--- An environment contains one value for every variable.
+open module N = Normal M public
+-- for deprecation below
+  renaming (∙-homo to comp-correct; correct to normalise-correct)
+  hiding (module Expr)
 
-Env : ℕ → Set _
-Env n = Vec Carrier n
-
--- The semantics of an expression is a function from an environment to
--- a value.
-
-⟦_⟧ : Expr n → Env n → Carrier
-⟦ var x   ⟧ ρ = lookup ρ x
-⟦ id      ⟧ ρ = ε
-⟦ e₁ ⊕ e₂ ⟧ ρ = ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ
+open N.Expr public
+-- for backwards compatibility
+  renaming (‵var to var; ‵ε to id; _‵∙_ to _⊕_)
 
 ------------------------------------------------------------------------
--- Normal forms
-
--- A normal form is a vector of multiplicities (a bag).
+-- Tactic
 
-Normal : ℕ → Set
-Normal n = Vec ℕ n
+open Tactic monoid normal public
 
--- The semantics of a normal form.
-
-⟦_⟧⇓ : Normal n → Env n → Carrier
-⟦ []    ⟧⇓ _ = ε
-⟦ n ∷ v ⟧⇓ (a ∷ ρ) = fold (⟦ v ⟧⇓ ρ) (a ∙_) n
 
 ------------------------------------------------------------------------
--- Constructions on normal forms
-
--- The empty bag.
-
-empty : Normal n
-empty = replicate _ 0
-
--- A singleton bag.
-
-sg : (i : Fin n) → Normal n
-sg zero    = 1 ∷ empty
-sg (suc i) = 0 ∷ sg i
-
--- The composition of normal forms.
-
-_•_  : (v w : Normal n) → Normal n
-[]      • []      = []
-(l ∷ v) • (m ∷ w) = l + m ∷ v • w
-
+-- DEPRECATED NAMES
 ------------------------------------------------------------------------
--- Correctness of the constructions on normal forms
-
--- The empty bag stands for the unit ε.
-
-empty-correct : (ρ : Env n) → ⟦ empty ⟧⇓ ρ ≈ ε
-empty-correct [] = refl
-empty-correct (a ∷ ρ) = empty-correct ρ
-
--- The singleton bag stands for a single variable.
-
-sg-correct : (x : Fin n) (ρ : Env n) →  ⟦ sg x ⟧⇓ ρ ≈ lookup ρ x
-sg-correct zero (x ∷ ρ) = begin
-    x ∙ ⟦ empty ⟧⇓ ρ   ≈⟨ ∙-congˡ (empty-correct ρ) ⟩
-    x ∙ ε              ≈⟨ identityʳ _ ⟩
-    x                  ∎
-sg-correct (suc x) (m ∷ ρ) = sg-correct x ρ
-
--- Normal form composition corresponds to the composition of the monoid.
-
-comp-correct : (v w : Normal n) (ρ : Env n) →
-              ⟦ v • w ⟧⇓ ρ ≈ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ)
-comp-correct [] [] ρ =  sym (identityˡ _)
-comp-correct (l ∷ v) (m ∷ w) (a ∷ ρ) = lemma l m (comp-correct v w ρ)
-  where
-    flip12 : ∀ a b c → a ∙ (b ∙ c) ≈ b ∙ (a ∙ c)
-    flip12 a b c = begin
-        a ∙ (b ∙ c)  ≈⟨ sym (assoc _ _ _) ⟩
-        (a ∙ b) ∙ c  ≈⟨ ∙-congʳ (comm _ _) ⟩
-        (b ∙ a) ∙ c  ≈⟨ assoc _ _ _ ⟩
-        b ∙ (a ∙ c)  ∎
-    lemma : ∀ l m {d b c} (p : d ≈ b ∙ c) →
-      fold d (a ∙_) (l + m) ≈ fold b (a ∙_) l ∙ fold c (a ∙_) m
-    lemma zero zero p = p
-    lemma zero (suc m) p = trans (∙-congˡ (lemma zero m p)) (flip12 _ _ _)
-    lemma (suc l) m p = trans (∙-congˡ (lemma l m p)) (sym (assoc a _ _))
-
-------------------------------------------------------------------------
--- Normalization
-
--- A normaliser.
-
-normalise : Expr n → Normal n
-normalise (var x)   = sg x
-normalise id        = empty
-normalise (e₁ ⊕ e₂) = normalise e₁ • normalise e₂
-
--- The normaliser preserves the semantics of the expression.
-
-normalise-correct : (e : Expr n) (ρ : Env n) →
-    ⟦ normalise e ⟧⇓ ρ ≈ ⟦ e ⟧ ρ
-normalise-correct (var x)   ρ = sg-correct x ρ
-normalise-correct id        ρ = empty-correct ρ
-normalise-correct (e₁ ⊕ e₂) ρ =  begin
-
-    ⟦ normalise e₁ • normalise e₂ ⟧⇓ ρ
-
-  ≈⟨ comp-correct (normalise e₁) (normalise e₂) ρ ⟩
-
-    ⟦ normalise e₁ ⟧⇓ ρ ∙ ⟦ normalise e₂ ⟧⇓ ρ
-
-  ≈⟨ ∙-cong (normalise-correct e₁ ρ) (normalise-correct e₂ ρ) ⟩
-
-    ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ
-  ∎
-
-------------------------------------------------------------------------
--- "Tactic.
-
-open module R = Reflection
-                  setoid var ⟦_⟧ (⟦_⟧⇓ ∘ normalise) normalise-correct
-  public using (solve; _⊜_)
-
--- We can decide if two normal forms are /syntactically/ equal.
-
-infix 5 _≟_
-
-_≟_ : (nf₁ nf₂ : Normal n) → Dec (nf₁ ≡ nf₂)
-nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable ℕ._≟_ nf₁ nf₂)
-  where open Pointwise
-
--- We can also give a sound, but not necessarily complete, procedure
--- for determining if two expressions have the same semantics.
-
-prove′ : (e₁ e₂ : Expr n) → Maybe (∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ)
-prove′ e₁ e₂ =
-  Maybe.map lemma (dec⇒weaklyDec _≟_ (normalise e₁) (normalise e₂))
-  where
-  lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ
-  lemma eq ρ =
-    R.prove ρ e₁ e₂ (begin
-      ⟦ normalise e₁ ⟧⇓ ρ  ≡⟨ ≡.cong (λ e → ⟦ e ⟧⇓ ρ) eq ⟩
-      ⟦ normalise e₂ ⟧⇓ ρ  ∎)
-
--- This procedure can be combined with from-just.
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
 
-prove : ∀ n (e₁ e₂ : Expr n) → From-just (prove′ e₁ e₂)
-prove _ e₁ e₂ = from-just (prove′ e₁ e₂)
+-- Version 2.2
 
--- prove : ∀ n (es : Expr n × Expr n) →
---         From-just (uncurry prove′ es)
--- prove _ = from-just ∘ uncurry prove′
+{-# WARNING_ON_USAGE normalise-correct
+"Warning: normalise-correct was deprecated in v2.2.
+Please use Algebra.Solver.CommutativeMonoid.Normal.correct instead."
+#-}
diff --git a/src/Algebra/Solver/CommutativeMonoid/Normal.agda b/src/Algebra/Solver/CommutativeMonoid/Normal.agda
new file mode 100644
index 0000000000..d1810bcb8a
--- /dev/null
+++ b/src/Algebra/Solver/CommutativeMonoid/Normal.agda
@@ -0,0 +1,145 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Normal forms in commutative monoids
+--
+-- Adapted from Algebra.Solver.Monoid.Normal
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Algebra.Bundles using (CommutativeMonoid)
+
+module Algebra.Solver.CommutativeMonoid.Normal
+  {c ℓ} (M : CommutativeMonoid c ℓ) where
+
+open import Algebra.Bundles.Raw using (RawMonoid)
+import Algebra.Properties.CommutativeSemigroup as CommutativeSemigroupProperties
+import Algebra.Properties.Monoid.Mult as MonoidMultProperties
+open import Data.Fin.Base using (Fin; zero; suc)
+open import Data.Nat as ℕ using (ℕ; zero; suc; _+_)
+open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate; zipWith)
+open import Data.Vec.Relation.Binary.Equality.DecPropositional using (_≡?_)
+open import Relation.Binary.Definitions using (DecidableEquality)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+
+open CommutativeMonoid M
+open MonoidMultProperties monoid using (_×_; ×-homo-1; ×-homo-+)
+open CommutativeSemigroupProperties commutativeSemigroup using (interchange)
+open ≈-Reasoning setoid
+
+private
+  variable
+    n : ℕ
+
+
+------------------------------------------------------------------------
+-- Monoid expressions
+
+open import Algebra.Solver.Monoid.Expression monoid public
+
+------------------------------------------------------------------------
+-- Normal forms
+
+-- A normal form is a vector of multiplicities (a bag).
+
+private
+  N : ℕ → Set
+  N n = Vec ℕ n
+
+-- Constructions on normal forms
+
+-- The empty bag.
+
+  empty : N n
+  empty = replicate _ 0
+
+-- A singleton bag.
+
+  sg : (i : Fin n) → N n
+  sg zero    = 1 ∷ empty
+  sg (suc i) = 0 ∷ sg i
+
+-- The composition of normal forms: bag union.
+  infixr 10 _•_
+
+  _•_  : (v w : N n) → N n
+  _•_ = zipWith _+_
+
+-- Packaging up the normal forms
+
+NF : ℕ → RawMonoid _ _
+NF n = record { Carrier = N n ; _≈_ = _≡_ ; _∙_ = _•_ ; ε = empty }
+
+-- The semantics of a normal form.
+
+⟦_⟧⇓ : N n → Env n → Carrier
+⟦ []    ⟧⇓ _       = ε
+⟦ n ∷ v ⟧⇓ (a ∷ ρ) = (n × a) ∙ (⟦ v ⟧⇓ ρ)
+
+-- We can decide if two normal forms are /syntactically/ equal.
+
+infix 5 _≟_
+
+_≟_ : DecidableEquality (N n)
+_≟_ = _≡?_ ℕ._≟_
+
+------------------------------------------------------------------------
+-- Correctness of the constructions on normal forms
+
+-- The empty bag stands for the unit ε.
+
+ε-homo : (ρ : Env n) → ⟦ empty ⟧⇓ ρ ≈ ε
+ε-homo [] = refl
+ε-homo (a ∷ ρ) = begin
+    ε ∙ ⟦ empty ⟧⇓ ρ   ≈⟨ identityˡ _ ⟩
+    ⟦ empty ⟧⇓ ρ       ≈⟨ ε-homo ρ ⟩
+    ε                  ∎
+
+-- The singleton bag stands for a single variable.
+
+sg-correct : (x : Fin n) (ρ : Env n) →  ⟦ sg x ⟧⇓ ρ ≈ lookup ρ x
+sg-correct zero (x ∷ ρ) = begin
+    (1 × x) ∙ ⟦ empty ⟧⇓ ρ   ≈⟨ ∙-congʳ (×-homo-1 _) ⟩
+    x ∙ ⟦ empty ⟧⇓ ρ         ≈⟨ ∙-congˡ (ε-homo ρ) ⟩
+    x ∙ ε                    ≈⟨ identityʳ _ ⟩
+    x                        ∎
+sg-correct (suc x) (_ ∷ ρ) = begin
+    ε ∙ ⟦ sg x ⟧⇓ ρ   ≈⟨ identityˡ _ ⟩
+    ⟦ sg x ⟧⇓ ρ       ≈⟨ sg-correct x ρ ⟩
+    lookup ρ x        ∎
+
+-- Normal form composition corresponds to the composition of the monoid.
+
+∙-homo : ∀ v w (ρ : Env n) →
+         ⟦ v • w ⟧⇓ ρ ≈ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ)
+∙-homo [] [] _ =  sym (identityˡ _)
+∙-homo (l ∷ v) (m ∷ w) (a ∷ ρ) = begin
+  ((l + m) × a) ∙ ⟦ v • w ⟧⇓ ρ              ≈⟨ ∙-congʳ  (×-homo-+ a l m) ⟩
+  (l × a) ∙ (m × a) ∙ ⟦ v • w ⟧⇓ ρ          ≈⟨ ∙-congˡ  (∙-homo v w ρ) ⟩
+  (l × a) ∙ (m × a) ∙ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ) ≈⟨ interchange _ _ _ _ ⟩
+  ⟦ l ∷ v ⟧⇓ (a ∷ ρ) ∙ ⟦ m ∷ w ⟧⇓ (a ∷ ρ)   ∎
+
+------------------------------------------------------------------------
+-- Packaging everything up
+
+normal : NormalAPI
+normal = record
+  { NF       = NF
+  ; var      = sg
+  ; _≟_      = _≟_
+  ; ⟦_⟧⇓     = ⟦_⟧⇓
+  ; ⟦var_⟧⇓  = sg-correct
+  ; ⟦⟧⇓-homo = λ ρ → record
+    { isMagmaHomomorphism = record
+      { isRelHomomorphism = record
+        { cong = λ where ≡.refl → refl }
+      ; homo = λ v w → ∙-homo v w ρ
+      }
+    ; ε-homo = ε-homo ρ
+    }
+  }
+
+open NormalAPI normal public
+  using (normalise; correct)
diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda
index 00b8824975..dfb8f50ab5 100644
--- a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda
+++ b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda
@@ -10,208 +10,41 @@
 
 open import Algebra.Bundles using (IdempotentCommutativeMonoid)
 
-open import Data.Bool as Bool using (Bool; true; false; if_then_else_; _∨_)
-open import Data.Fin.Base using (Fin; zero; suc)
-open import Data.Maybe.Base as Maybe
-  using (Maybe; From-just; from-just)
-open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _+_)
-open import Data.Product.Base using (_×_; uncurry)
-open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate)
-
-open import Function.Base using (_∘_)
-
-import Relation.Binary.Reasoning.Setoid  as ≈-Reasoning
-import Relation.Binary.Reflection            as Reflection
-import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
-
-open import Relation.Binary.Consequences using (dec⇒weaklyDec)
-open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
-open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
-open import Relation.Nullary.Decidable as Dec using (Dec)
-
-
 module Algebra.Solver.IdempotentCommutativeMonoid
-  {m₁ m₂} (M : IdempotentCommutativeMonoid m₁ m₂) where
+  {c ℓ} (M : IdempotentCommutativeMonoid c ℓ) where
 
-open IdempotentCommutativeMonoid M
-open ≈-Reasoning setoid
+import Algebra.Solver.IdempotentCommutativeMonoid.Normal as Normal
+import Algebra.Solver.Monoid.Tactic as Tactic
 
-private
-  variable
-    n : ℕ
+open IdempotentCommutativeMonoid M using (monoid)
 
 ------------------------------------------------------------------------
--- Monoid expressions
-
--- There is one constructor for every operation, plus one for
--- variables; there may be at most n variables.
+-- Expressions and Normal forms
 
-infixr 5 _⊕_
-infixr 10 _•_
+open module N = Normal M public
+-- for deprecation below
+  renaming (∙-homo to comp-correct; correct to normalise-correct)
+  hiding (module Expr)
 
-data Expr (n : ℕ) : Set where
-  var : Fin n → Expr n
-  id  : Expr n
-  _⊕_ : Expr n → Expr n → Expr n
-
--- An environment contains one value for every variable.
-
-Env : ℕ → Set _
-Env n = Vec Carrier n
-
--- The semantics of an expression is a function from an environment to
--- a value.
-
-⟦_⟧ : ∀ {n} → Expr n → Env n → Carrier
-⟦ var x   ⟧ ρ = lookup ρ x
-⟦ id      ⟧ ρ = ε
-⟦ e₁ ⊕ e₂ ⟧ ρ = ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ
+open N.Expr public
+-- for backwards compatibility
+  renaming (‵var to var; ‵ε to id; _‵∙_ to _⊕_)
 
 ------------------------------------------------------------------------
--- Normal forms
-
--- A normal form is a vector of bits (a set).
-
-Normal : ℕ → Set
-Normal n = Vec Bool n
+-- Tactic
 
--- The semantics of a normal form.
+open Tactic monoid normal public
 
-⟦_⟧⇓ : Normal n → Env n → Carrier
-⟦ []    ⟧⇓ _ = ε
-⟦ b ∷ v ⟧⇓ (a ∷ ρ) = if b then a ∙ (⟦ v ⟧⇓ ρ) else (⟦ v ⟧⇓ ρ)
 
 ------------------------------------------------------------------------
--- Constructions on normal forms
-
--- The empty set.
-
-empty : Normal n
-empty = replicate _ false
-
--- A singleton set.
-
-sg : (i : Fin n) → Normal n
-sg zero    = true ∷ empty
-sg (suc i) = false ∷ sg i
-
--- The composition of normal forms.
-
-_•_ : (v w : Normal n) → Normal n
-[]      • []      = []
-(l ∷ v) • (m ∷ w) = (l ∨ m) ∷ v • w
-
+-- DEPRECATED NAMES
 ------------------------------------------------------------------------
--- Correctness of the constructions on normal forms
-
--- The empty set stands for the unit ε.
-
-empty-correct : (ρ : Env n) → ⟦ empty ⟧⇓ ρ ≈ ε
-empty-correct []      = refl
-empty-correct (a ∷ ρ) = empty-correct ρ
-
--- The singleton set stands for a single variable.
-
-sg-correct : (x : Fin n) (ρ : Env n) → ⟦ sg x ⟧⇓ ρ ≈ lookup ρ x
-sg-correct zero (x ∷ ρ) = begin
-    x ∙ ⟦ empty ⟧⇓ ρ   ≈⟨ ∙-congˡ (empty-correct ρ) ⟩
-    x ∙ ε              ≈⟨ identityʳ _ ⟩
-    x                  ∎
-sg-correct (suc x) (m ∷ ρ) = sg-correct x ρ
-
--- Normal form composition corresponds to the composition of the monoid.
-
-flip12 : ∀ a b c → a ∙ (b ∙ c) ≈ b ∙ (a ∙ c)
-flip12 a b c = begin
-    a ∙ (b ∙ c)  ≈⟨ sym (assoc _ _ _) ⟩
-    (a ∙ b) ∙ c  ≈⟨ ∙-congʳ (comm _ _) ⟩
-    (b ∙ a) ∙ c  ≈⟨ assoc _ _ _ ⟩
-    b ∙ (a ∙ c)  ∎
-
-distr : ∀ a b c → a ∙ (b ∙ c) ≈ (a ∙ b) ∙ (a ∙ c)
-distr a b c = begin
-    a ∙ (b ∙ c)        ≈⟨ ∙-cong (sym (idem a)) refl ⟩
-    (a ∙ a) ∙ (b ∙ c)  ≈⟨ assoc _ _ _ ⟩
-    a ∙ (a ∙ (b ∙ c))  ≈⟨ ∙-congˡ (sym (assoc _ _ _)) ⟩
-    a ∙ ((a ∙ b) ∙ c)  ≈⟨ ∙-congˡ (∙-congʳ (comm _ _)) ⟩
-    a ∙ ((b ∙ a) ∙ c)  ≈⟨ ∙-congˡ (assoc _ _ _) ⟩
-    a ∙ (b ∙ (a ∙ c))  ≈⟨ sym (assoc _ _ _) ⟩
-    (a ∙ b) ∙ (a ∙ c)  ∎
-
-comp-correct : ∀ (v w : Normal n) (ρ : Env n) →
-              ⟦ v • w ⟧⇓ ρ ≈ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ)
-comp-correct [] [] ρ = sym (identityˡ _)
-comp-correct (true ∷ v) (true ∷ w) (a ∷ ρ) =
-  trans (∙-congˡ (comp-correct v w ρ)) (distr _ _ _)
-comp-correct (true ∷ v) (false ∷ w) (a ∷ ρ) =
-  trans (∙-congˡ (comp-correct v w ρ)) (sym (assoc _ _ _))
-comp-correct (false ∷ v) (true ∷ w) (a ∷ ρ) =
-  trans (∙-congˡ (comp-correct v w ρ)) (flip12 _ _ _)
-comp-correct (false ∷ v) (false ∷ w) (a ∷ ρ) =
-  comp-correct v w ρ
-
-------------------------------------------------------------------------
--- Normalization
-
--- A normaliser.
-
-normalise : Expr n → Normal n
-normalise (var x)   = sg x
-normalise id        = empty
-normalise (e₁ ⊕ e₂) = normalise e₁ • normalise e₂
-
--- The normaliser preserves the semantics of the expression.
-
-normalise-correct : (e : Expr n) (ρ : Env n) →
-    ⟦ normalise e ⟧⇓ ρ ≈ ⟦ e ⟧ ρ
-normalise-correct (var x)   ρ = sg-correct x ρ
-normalise-correct id        ρ = empty-correct ρ
-normalise-correct (e₁ ⊕ e₂) ρ = begin
-
-    ⟦ normalise e₁ • normalise e₂ ⟧⇓ ρ
-
-  ≈⟨ comp-correct (normalise e₁) (normalise e₂) ρ ⟩
-
-    ⟦ normalise e₁ ⟧⇓ ρ ∙ ⟦ normalise e₂ ⟧⇓ ρ
-
-  ≈⟨ ∙-cong (normalise-correct e₁ ρ) (normalise-correct e₂ ρ) ⟩
-
-    ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ
-  ∎
-
-------------------------------------------------------------------------
--- "Tactic.
-
-open module R = Reflection
-                  setoid var ⟦_⟧ (⟦_⟧⇓ ∘ normalise) normalise-correct
-  public using (solve; _⊜_)
-
--- We can decide if two normal forms are /syntactically/ equal.
-
-infix 5 _≟_
-
-_≟_ : (nf₁ nf₂ : Normal n) → Dec (nf₁ ≡ nf₂)
-nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable Bool._≟_ nf₁ nf₂)
-  where open Pointwise
-
--- We can also give a sound, but not necessarily complete, procedure
--- for determining if two expressions have the same semantics.
-
-prove′ : (e₁ e₂ : Expr n) → Maybe (∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ)
-prove′ e₁ e₂ =
-  Maybe.map lemma (dec⇒weaklyDec _≟_ (normalise e₁) (normalise e₂))
-  where
-  lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ
-  lemma eq ρ =
-    R.prove ρ e₁ e₂ (begin
-      ⟦ normalise e₁ ⟧⇓ ρ  ≡⟨ ≡.cong (λ e → ⟦ e ⟧⇓ ρ) eq ⟩
-      ⟦ normalise e₂ ⟧⇓ ρ  ∎)
-
--- This procedure can be combined with from-just.
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
 
-prove : ∀ n (e₁ e₂ : Expr n) → From-just (prove′ e₁ e₂)
-prove _ e₁ e₂ = from-just (prove′ e₁ e₂)
+-- Version 2.2
 
--- prove : ∀ n (es : Expr n × Expr n) →
---         From-just (uncurry prove′ es)
--- prove _ = from-just ∘ uncurry prove′
+{-# WARNING_ON_USAGE normalise-correct
+"Warning: normalise-correct was deprecated in v2.2.
+Please use Algebra.Solver.IdempotentCommutativeMonoid.Normal.correct instead."
+#-}
diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda
new file mode 100644
index 0000000000..0c09a42c4e
--- /dev/null
+++ b/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda
@@ -0,0 +1,164 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Normal forms in commutative monoids
+--
+-- Adapted from Algebra.Solver.Monoid.Normal
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Algebra.Bundles using (IdempotentCommutativeMonoid)
+
+module Algebra.Solver.IdempotentCommutativeMonoid.Normal
+  {c ℓ} (M : IdempotentCommutativeMonoid c ℓ) where
+
+open import Algebra.Bundles.Raw using (RawMonoid)
+import Algebra.Properties.CommutativeSemigroup as CommutativeSemigroupProperties
+import Algebra.Properties.IdempotentCommutativeMonoid as IdempotentCommutativeMonoidProperties
+open import Data.Bool as Bool using (Bool; true; false; if_then_else_; _∨_)
+open import Data.Fin.Base using (Fin; zero; suc)
+open import Data.Nat.Base using (ℕ; zero; suc; _+_)
+open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate; zipWith)
+open import Data.Vec.Relation.Binary.Equality.DecPropositional using (_≡?_)
+open import Relation.Binary.Definitions using (DecidableEquality)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+
+open IdempotentCommutativeMonoid M
+open IdempotentCommutativeMonoidProperties M using (∙-distrˡ-∙)
+open CommutativeSemigroupProperties commutativeSemigroup
+  using  (x∙yz≈xy∙z; x∙yz≈y∙xz)
+open ≈-Reasoning setoid
+
+private
+  variable
+    n : ℕ
+
+
+------------------------------------------------------------------------
+-- Monoid expressions
+
+open import Algebra.Solver.Monoid.Expression monoid public
+
+------------------------------------------------------------------------
+-- Normal forms
+
+-- A normal form is a vector of Booleans (a set of variable occurrences).
+
+private
+  N : ℕ → Set
+  N n = Vec Bool n
+
+-- Constructions on normal forms
+
+-- The empty set.
+
+  empty : N n
+  empty = replicate _ false
+
+-- A singleton set.
+
+  sg : (i : Fin n) → N n
+  sg zero    = true ∷ empty
+  sg (suc i) = false ∷ sg i
+
+-- The composition of normal forms: set union.
+  infixr 10 _•_
+
+  _•_  : (v w : N n) → N n
+  _•_ = zipWith _∨_
+
+-- Packaging up the normal forms
+
+NF : ℕ → RawMonoid _ _
+NF n = record { Carrier = N n ; _≈_ = _≡_ ; _∙_ = _•_ ; ε = empty }
+
+-- The semantics of a normal form.
+
+⟦_⟧⇓ : N n → Env n → Carrier
+⟦ []    ⟧⇓ _       = ε
+⟦ b ∷ v ⟧⇓ (a ∷ ρ) = if b then a ∙ (⟦ v ⟧⇓ ρ) else (⟦ v ⟧⇓ ρ)
+
+-- We can decide if two normal forms are /syntactically/ equal.
+
+infix 5 _≟_
+
+_≟_ : DecidableEquality (N n)
+_≟_ = _≡?_ Bool._≟_
+
+------------------------------------------------------------------------
+-- Correctness of the constructions on normal forms
+
+-- The empty bag stands for the unit ε.
+
+ε-homo : (ρ : Env n) → ⟦ empty ⟧⇓ ρ ≈ ε
+ε-homo [] = refl
+ε-homo (a ∷ ρ) = ε-homo ρ
+
+-- The singleton bag stands for a single variable.
+
+sg-correct : (x : Fin n) (ρ : Env n) →  ⟦ sg x ⟧⇓ ρ ≈ lookup ρ x
+sg-correct zero (x ∷ ρ) = begin
+    x ∙ ⟦ empty ⟧⇓ ρ  ≈⟨ ∙-congˡ (ε-homo ρ) ⟩
+    x ∙ ε             ≈⟨ identityʳ _ ⟩
+    x                 ∎
+sg-correct (suc x) (_ ∷ ρ) = sg-correct x ρ
+
+-- Normal form composition corresponds to the composition of the monoid.
+
+∙-homo : ∀ v w (ρ : Env n) →
+         ⟦ v • w ⟧⇓ ρ ≈ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ)
+∙-homo [] [] ρ = sym (identityˡ _)
+∙-homo (true ∷ v) (true ∷ w) (a ∷ ρ) =
+  trans (∙-congˡ (∙-homo v w ρ)) (∙-distrˡ-∙ _ _ _)
+∙-homo (true ∷ v) (false ∷ w) (a ∷ ρ) =
+  trans (∙-congˡ (∙-homo v w ρ)) (x∙yz≈xy∙z _ _ _)
+∙-homo (false ∷ v) (true ∷ w) (a ∷ ρ) =
+  trans (∙-congˡ (∙-homo v w ρ)) (x∙yz≈y∙xz _ _ _)
+∙-homo (false ∷ v) (false ∷ w) (a ∷ ρ) =
+  ∙-homo v w ρ
+
+------------------------------------------------------------------------
+-- Packaging everything up
+
+normal : NormalAPI
+normal = record
+  { NF       = NF
+  ; var      = sg
+  ; _≟_      = _≟_
+  ; ⟦_⟧⇓     = ⟦_⟧⇓
+  ; ⟦var_⟧⇓  = sg-correct
+  ; ⟦⟧⇓-homo = λ ρ → record
+    { isMagmaHomomorphism = record
+      { isRelHomomorphism = record
+        { cong = λ where ≡.refl → refl }
+      ; homo = λ v w → ∙-homo v w ρ
+      }
+    ; ε-homo = ε-homo ρ
+    }
+  }
+
+open NormalAPI normal public
+  using (normalise; correct)
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.2
+
+flip12 = x∙yz≈y∙xz
+{-# WARNING_ON_USAGE flip12
+"Warning: flip12 was deprecated in v2.2.
+Please use Algebra.Properties.CommutativeSemigroup.x∙yz≈y∙xz instead."
+#-}
+
+distr = ∙-distrˡ-∙
+{-# WARNING_ON_USAGE distr
+"Warning: distr was deprecated in v2.2.
+Please use Algebra.Properties.IdempotentCommutativeMonoid.∙-distrˡ-∙ instead."
+#-}
diff --git a/src/Algebra/Solver/Monoid.agda b/src/Algebra/Solver/Monoid.agda
index 7debc4e1aa..9524236c05 100644
--- a/src/Algebra/Solver/Monoid.agda
+++ b/src/Algebra/Solver/Monoid.agda
@@ -6,133 +6,70 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra
+open import Algebra.Bundles using (Monoid)
 
-module Algebra.Solver.Monoid {m₁ m₂} (M : Monoid m₁ m₂) where
+module Algebra.Solver.Monoid {c ℓ} (M : Monoid c ℓ) where
 
-open import Data.Fin.Base as Fin
-import Data.Fin.Properties as Fin
-open import Data.List.Base hiding (lookup)
-import Data.List.Relation.Binary.Equality.DecPropositional as ListEq
+import Algebra.Solver.Monoid.Normal as Normal
+import Algebra.Solver.Monoid.Tactic as Tactic
 open import Data.Maybe.Base as Maybe
-  using (Maybe; From-just; from-just)
-open import Data.Nat.Base using (ℕ)
+  using (From-just; from-just)
 open import Data.Product.Base using (_×_; uncurry)
-open import Data.Vec.Base using (Vec; lookup)
-open import Function.Base using (_∘_; _$_)
-open import Relation.Binary.Consequences using (dec⇒weaklyDec)
-open import Relation.Binary.Definitions using (DecidableEquality)
+open import Function.Base using (_∘_)
 
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
-import Relation.Binary.Reflection
-import Relation.Nullary.Decidable.Core as Dec
-
-open Monoid M
-open import Relation.Binary.Reasoning.Setoid setoid
 
 ------------------------------------------------------------------------
--- Monoid expressions
-
--- There is one constructor for every operation, plus one for
--- variables; there may be at most n variables.
-
-infixr 5 _⊕_
-
-data Expr (n : ℕ) : Set where
-  var : Fin n → Expr n
-  id  : Expr n
-  _⊕_ : Expr n → Expr n → Expr n
-
--- An environment contains one value for every variable.
+-- Expressions and Normal forms
 
-Env : ℕ → Set _
-Env n = Vec Carrier n
+open module N = Normal M public
+-- for deprecation below
+  renaming (∙-homo to homomorphic; correct to normalise-correct)
+  hiding (module Expr)
 
--- The semantics of an expression is a function from an environment to
--- a value.
-
-⟦_⟧ : ∀ {n} → Expr n → Env n → Carrier
-⟦ var x   ⟧ ρ = lookup ρ x
-⟦ id      ⟧ ρ = ε
-⟦ e₁ ⊕ e₂ ⟧ ρ = ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ
+open N.Expr public
+-- for backwards compatibility
+  renaming (‵var to var; ‵ε to id; _‵∙_ to _⊕_)
 
 ------------------------------------------------------------------------
--- Normal forms
-
--- A normal form is a list of variables.
-
-Normal : ℕ → Set
-Normal n = List (Fin n)
-
--- The semantics of a normal form.
+-- Tactic
 
-⟦_⟧⇓ : ∀ {n} → Normal n → Env n → Carrier
-⟦ []     ⟧⇓ ρ = ε
-⟦ x ∷ nf ⟧⇓ ρ = lookup ρ x ∙ ⟦ nf ⟧⇓ ρ
+open module T = Tactic M normal public
+  hiding (prove)
 
--- A normaliser.
-
-normalise : ∀ {n} → Expr n → Normal n
-normalise (var x)   = x ∷ []
-normalise id        = []
-normalise (e₁ ⊕ e₂) = normalise e₁ ++ normalise e₂
-
--- The normaliser is homomorphic with respect to _++_/_∙_.
-
-homomorphic : ∀ {n} (nf₁ nf₂ : Normal n) (ρ : Env n) →
-              ⟦ nf₁ ++ nf₂ ⟧⇓ ρ ≈ (⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ)
-homomorphic [] nf₂ ρ = begin
-  ⟦ nf₂ ⟧⇓ ρ      ≈⟨ sym $ identityˡ _ ⟩
-  ε ∙ ⟦ nf₂ ⟧⇓ ρ  ∎
-homomorphic (x ∷ nf₁) nf₂ ρ = begin
-  lookup ρ x ∙ ⟦ nf₁ ++ nf₂ ⟧⇓ ρ          ≈⟨ ∙-congˡ (homomorphic nf₁ nf₂ ρ) ⟩
-  lookup ρ x ∙ (⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ)  ≈⟨ sym $ assoc _ _ _ ⟩
-  lookup ρ x ∙ ⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ    ∎
-
--- The normaliser preserves the semantics of the expression.
+prove : ∀ n (es : Expr n × Expr n) → From-just (uncurry prove′ es)
+prove _ = from-just ∘ uncurry prove′
 
-normalise-correct :
-  ∀ {n} (e : Expr n) (ρ : Env n) → ⟦ normalise e ⟧⇓ ρ ≈ ⟦ e ⟧ ρ
-normalise-correct (var x) ρ = begin
-  lookup ρ x ∙ ε  ≈⟨ identityʳ _ ⟩
-  lookup ρ x      ∎
-normalise-correct id ρ = begin
-  ε  ∎
-normalise-correct (e₁ ⊕ e₂) ρ = begin
-  ⟦ normalise e₁ ++ normalise e₂ ⟧⇓ ρ        ≈⟨ homomorphic (normalise e₁) (normalise e₂) ρ ⟩
-  ⟦ normalise e₁ ⟧⇓ ρ ∙ ⟦ normalise e₂ ⟧⇓ ρ  ≈⟨ ∙-cong (normalise-correct e₁ ρ) (normalise-correct e₂ ρ) ⟩
-  ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ                        ∎
 
 ------------------------------------------------------------------------
--- "Tactic.
-
-open module R = Relation.Binary.Reflection
-                  setoid var ⟦_⟧ (⟦_⟧⇓ ∘ normalise) normalise-correct
-  public using (solve; _⊜_)
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
 
--- We can decide if two normal forms are /syntactically/ equal.
+-- Version 2.2
 
-infix 5 _≟_
+{-# WARNING_ON_USAGE homomorphic
+"Warning: homomorphic was deprecated in v2.2.
+Please use (relevant field `homo` of) Algebra.Solver.Monoid.Normal.⟦⟧⇓-homo instead."
+#-}
 
-_≟_ : ∀ {n} → DecidableEquality (Normal n)
-nf₁ ≟ nf₂ = Dec.map′ ≋⇒≡ ≡⇒≋ (nf₁ ≋? nf₂)
-  where open ListEq Fin._≟_
+{-# WARNING_ON_USAGE normalise-correct
+"Warning: normalise-correct was deprecated in v2.2.
+Please use Algebra.Solver.Monoid.Normal.correct instead."
+#-}
 
--- We can also give a sound, but not necessarily complete, procedure
--- for determining if two expressions have the same semantics.
+{-# WARNING_ON_USAGE var
+"Warning: var was deprecated in v2.2.
+Please use Algebra.Solver.Monoid.Expression.‵var instead."
+#-}
 
-prove′ : ∀ {n} (e₁ e₂ : Expr n) → Maybe (∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ)
-prove′ e₁ e₂ =
-  Maybe.map lemma $ dec⇒weaklyDec _≟_ (normalise e₁) (normalise e₂)
-  where
-  lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ
-  lemma eq ρ =
-    R.prove ρ e₁ e₂ (begin
-      ⟦ normalise e₁ ⟧⇓ ρ  ≡⟨ cong (λ e → ⟦ e ⟧⇓ ρ) eq ⟩
-      ⟦ normalise e₂ ⟧⇓ ρ  ∎)
+{-# WARNING_ON_USAGE id
+"Warning: id was deprecated in v2.2.
+Please use Algebra.Solver.Monoid.Expression.‵ε instead."
+#-}
 
--- This procedure can be combined with from-just.
+{-# WARNING_ON_USAGE _⊕_
+"Warning: _⊕_ was deprecated in v2.2.
+Please use Algebra.Solver.Monoid.Expression._‵∙_ instead."
+#-}
 
-prove : ∀ n (es : Expr n × Expr n) →
-        From-just (uncurry prove′ es)
-prove _ = from-just ∘ uncurry prove′
diff --git a/src/Algebra/Solver/Monoid/Expression.agda b/src/Algebra/Solver/Monoid/Expression.agda
new file mode 100644
index 0000000000..c460cc2e01
--- /dev/null
+++ b/src/Algebra/Solver/Monoid/Expression.agda
@@ -0,0 +1,126 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- A solver for equations over monoids
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Algebra.Bundles using (Monoid)
+
+module Algebra.Solver.Monoid.Expression {c ℓ} (M : Monoid c ℓ) where
+
+open import Algebra.Bundles.Raw using (RawMonoid)
+open import Algebra.Morphism.Structures using (IsMonoidHomomorphism)
+open import Algebra.Structures using (IsMonoid)
+open import Data.Fin.Base using (Fin)
+open import Data.Maybe.Base as Maybe using (Maybe)
+open import Data.Nat.Base using (ℕ)
+open import Data.Vec.Base using (Vec; lookup)
+open import Level using (suc; _⊔_)
+open import Relation.Binary.Consequences using (dec⇒weaklyDec)
+open import Relation.Binary.Definitions using (DecidableEquality)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+
+private
+  variable
+    n : ℕ
+
+open Monoid M using (Carrier; _≈_; ε; _∙_; rawMonoid; isMonoid)
+
+
+------------------------------------------------------------------------
+-- Monoid expressions
+
+-- There is one constructor for every operation, plus one for
+-- variables; there may be at most n variables.
+
+infixr 5 _‵∙_
+
+data Expr (n : ℕ) : Set where
+  ‵var : Fin n → Expr n
+  ‵ε   : Expr n
+  _‵∙_ : Expr n → Expr n → Expr n
+
+-- An environment contains one value for every variable.
+
+Env : ℕ → Set _
+Env n = Vec Carrier n
+
+-- The semantics of an expression is a function from an environment to
+-- a value.
+
+⟦_⟧ : Expr n → Env n → Carrier
+⟦ ‵var x   ⟧ ρ = lookup ρ x
+⟦ ‵ε       ⟧ ρ = ε
+⟦ e₁ ‵∙ e₂ ⟧ ρ = ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ
+
+------------------------------------------------------------------------
+-- API for normal expressions
+
+record NormalAPI {a r} : Set (suc (a ⊔ r) ⊔ c ⊔ ℓ) where
+  infix 5 _≟_
+
+  field
+
+    NF        : ℕ → RawMonoid a r
+
+  private
+    N : ℕ → Set a
+    N n = RawMonoid.Carrier (NF n)
+
+  field
+
+    var       : Fin n → N n
+
+-- We can decide if two normal forms are /syntactically/ equal.
+
+    _≟_       : DecidableEquality (N n)
+
+-- The semantics of a normal form.
+    ⟦_⟧⇓     : N n → Env n → Carrier
+
+-- Which "agrees with the environment on variables".
+    ⟦var_⟧⇓  : ∀ x ρ → ⟦ var x ⟧⇓ ρ ≈ lookup {n = n} ρ x
+
+-- And which is a monoid homomorphism between NF and M
+    ⟦⟧⇓-homo : ∀ ρ → IsMonoidHomomorphism (NF n) rawMonoid λ e → ⟦ e ⟧⇓ ρ
+
+------------------------------------------------------------------------
+-- The normaliser and its correctness proof, as manifest fields of `Normal`
+
+  module _ {n} where
+
+    private module N = RawMonoid (NF n)
+
+-- Definition
+
+    normalise : Expr n → N n
+    normalise (‵var x)   = var x
+    normalise ‵ε         = N.ε
+    normalise (e₁ ‵∙ e₂) = (normalise e₁) N.∙ (normalise e₂)
+
+-- The normaliser preserves the semantics of the expression.
+
+    correct : ∀ e ρ → ⟦ normalise e ⟧⇓ ρ ≈ ⟦ e ⟧ ρ
+    correct (‵var x)   ρ = ⟦var x ⟧⇓ ρ
+    correct ‵ε         ρ = ε-homo
+      where open IsMonoidHomomorphism (⟦⟧⇓-homo ρ)
+    correct (e₁ ‵∙ e₂) ρ = begin
+      ⟦ normalise e₁ N.∙ normalise e₂ ⟧⇓ ρ
+        ≈⟨ homo (normalise e₁) (normalise e₂) ⟩
+      ⟦ normalise e₁ ⟧⇓ ρ ∙ ⟦ normalise e₂ ⟧⇓ ρ
+        ≈⟨ ∙-cong (correct e₁ ρ) (correct e₂ ρ) ⟩
+      ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ
+        ∎
+      where
+      open IsMonoid isMonoid using (∙-cong; setoid)
+      open ≈-Reasoning setoid
+      open IsMonoidHomomorphism (⟦⟧⇓-homo ρ)
+
+-- Semi-decision procedure for equality of normalised expressions
+
+    _semi≟_ : ∀ e₁ e₂ → Maybe (normalise e₁ ≡ normalise e₂)
+    e₁ semi≟ e₂ = dec⇒weaklyDec _≟_ (normalise e₁) (normalise e₂)
+
diff --git a/src/Algebra/Solver/Monoid/Normal.agda b/src/Algebra/Solver/Monoid/Normal.agda
new file mode 100644
index 0000000000..0d93f1a68e
--- /dev/null
+++ b/src/Algebra/Solver/Monoid/Normal.agda
@@ -0,0 +1,102 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Normal forms in commutative monoids
+--
+-- Adapted from Algebra.Solver.Monoid.Normal
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Algebra.Bundles using (Monoid)
+
+module Algebra.Solver.Monoid.Normal {c ℓ} (M : Monoid c ℓ) where
+
+open import Algebra.Bundles.Raw using (RawMonoid)
+import Algebra.Properties.Semigroup as SemigroupProperties
+open import Data.Fin as Fin using (Fin)
+open import Data.List.Base using (List; []; _∷_; [_]; _++_; ++-[]-rawMonoid)
+open import Data.List.Relation.Binary.Equality.DecPropositional using (_≡?_)
+open import Data.Nat.Base using (ℕ)
+open import Data.Vec.Base using (lookup)
+open import Relation.Binary.Definitions using (DecidableEquality)
+import Relation.Binary.PropositionalEquality.Core as ≡
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+
+open Monoid M
+open SemigroupProperties semigroup using (x∙yz≈xy∙z)
+open ≈-Reasoning setoid
+
+private
+  variable
+    n : ℕ
+
+
+------------------------------------------------------------------------
+-- Monoid expressions
+
+open import Algebra.Solver.Monoid.Expression M public
+
+------------------------------------------------------------------------
+-- Normal forms
+
+-- A normal form is a list of variables.
+
+NF : ℕ → RawMonoid _ _
+NF n = ++-[]-rawMonoid (Fin n)
+
+private
+
+  module NF {n} = RawMonoid (NF n)
+
+  N : ℕ → Set _
+  N n = NF.Carrier {n}
+
+-- The semantics of a normal form.
+
+⟦_⟧⇓ : N n → Env n → Carrier
+⟦ []     ⟧⇓ ρ = ε
+⟦ x ∷ nf ⟧⇓ ρ = lookup ρ x ∙ ⟦ nf ⟧⇓ ρ
+
+-- The normaliser is homomorphic with respect to _++_ =def NF._∙_.
+
+∙-homo : (nf₁ nf₂ : N n) (ρ : Env n) →
+         ⟦ nf₁ NF.∙ nf₂ ⟧⇓ ρ ≈ ⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ
+∙-homo [] nf₂ ρ = begin
+  ⟦ nf₂ ⟧⇓ ρ      ≈⟨ identityˡ _ ⟨
+  ε ∙ ⟦ nf₂ ⟧⇓ ρ  ∎
+∙-homo (x ∷ nf₁) nf₂ ρ = begin
+  lookup ρ x ∙ ⟦ nf₁ NF.∙ nf₂ ⟧⇓ ρ        ≈⟨ ∙-congˡ (∙-homo nf₁ nf₂ ρ) ⟩
+  lookup ρ x ∙ (⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ)  ≈⟨ x∙yz≈xy∙z _ _ _ ⟩
+  lookup ρ x ∙ ⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ    ∎
+
+-- We can decide if two normal forms are /syntactically/ equal.
+
+infix 5 _≟_
+
+_≟_ : DecidableEquality (N n)
+_≟_ = _≡?_ Fin._≟_
+
+------------------------------------------------------------------------
+-- Packaging everything up
+
+normal : NormalAPI
+normal = record
+  { NF       = NF
+  ; var      = [_]
+  ; _≟_      = _≟_
+  ; ⟦_⟧⇓     = ⟦_⟧⇓
+  ; ⟦var_⟧⇓  = λ x ρ → identityʳ (lookup ρ x)
+  ; ⟦⟧⇓-homo = λ ρ → record
+     { isMagmaHomomorphism = record
+       { isRelHomomorphism = record
+         { cong = λ where ≡.refl → refl
+         }
+       ; homo = λ nf₁ nf₂ → ∙-homo nf₁ nf₂ ρ
+       }
+     ; ε-homo = refl
+     }
+  }
+
+open NormalAPI normal public
+  using (normalise; correct)
diff --git a/src/Algebra/Solver/Monoid/Tactic.agda b/src/Algebra/Solver/Monoid/Tactic.agda
new file mode 100644
index 0000000000..6f5e406b54
--- /dev/null
+++ b/src/Algebra/Solver/Monoid/Tactic.agda
@@ -0,0 +1,52 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- A solver for equations over monoids
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Algebra.Bundles using (Monoid)
+import Algebra.Solver.Monoid.Expression as Expression
+
+module Algebra.Solver.Monoid.Tactic {a r c ℓ}
+  (M : Monoid c ℓ)
+  (open Expression M)
+  (N : NormalAPI {a} {r})
+  where
+
+open import Data.Maybe.Base as Maybe using (Maybe; From-just; from-just)
+open import Function.Base using (_∘_; _$_)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+import Relation.Binary.Reflection as Reflection
+
+open Monoid M using (setoid; _≈_)
+open NormalAPI N
+
+
+------------------------------------------------------------------------
+-- Tactic
+
+-- Package the tactical behaviours
+
+open module R = Reflection setoid ‵var ⟦_⟧ (⟦_⟧⇓ ∘ normalise) correct public
+  using (solve; _⊜_)
+
+-- We can also give a sound, but not necessarily complete, procedure
+-- for determining if two expressions have the same semantics.
+
+prove′ : ∀ {n} e₁ e₂ → Maybe ((ρ : Env n) → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ)
+prove′ e₁ e₂ = Maybe.map lemma $ e₁ semi≟ e₂
+  where
+  open ≈-Reasoning setoid
+  lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ
+  lemma eq ρ = R.prove ρ e₁ e₂ $ begin
+    ⟦ normalise e₁ ⟧⇓ ρ  ≡⟨ cong (λ e → ⟦ e ⟧⇓ ρ) eq ⟩
+    ⟦ normalise e₂ ⟧⇓ ρ  ∎
+
+-- This procedure can be combined with from-just.
+
+prove : ∀ n (e₁ e₂ : Expr n) → From-just (prove′ e₁ e₂)
+prove _ e₁ e₂ = from-just $ prove′ e₁ e₂
+