From 4f1245b89badf18aaf8521136e8ded22a3c55027 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 20 Jan 2025 14:15:20 +0000
Subject: [PATCH 01/39] refactor: revise the definitions

---
 src/Algebra/Definitions.agda | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda
index 62528e5b70..80f46dd329 100644
--- a/src/Algebra/Definitions.agda
+++ b/src/Algebra/Definitions.agda
@@ -148,13 +148,22 @@ RightCancellative _•_ = ∀ x y z → (y • x) ≈ (z • x) → y ≈ z
 
 Cancellative : Op₂ A → Set _
 Cancellative _•_ = (LeftCancellative _•_) × (RightCancellative _•_)
-
+{-
 AlmostLeftCancellative : A → Op₂ A → Set _
 AlmostLeftCancellative e _•_ = ∀ x y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z
 
 AlmostRightCancellative : A → Op₂ A → Set _
 AlmostRightCancellative e _•_ = ∀ x y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z
 
+AlmostCancellative : A → Op₂ A → Set _
+AlmostCancellative e _•_ = AlmostLeftCancellative e _•_ × AlmostRightCancellative e _•_
+-}
+AlmostLeftCancellative : A → Op₂ A → Set _
+AlmostLeftCancellative e _•_ = ∀ x → x ≈ e ⊎ ∀ y z → (x • y) ≈ (x • z) → y ≈ z
+
+AlmostRightCancellative : A → Op₂ A → Set _
+AlmostRightCancellative e _•_ = ∀ x → x ≈ e ⊎ ∀ y z → (y • x) ≈ (z • x) → y ≈ z
+
 AlmostCancellative : A → Op₂ A → Set _
 AlmostCancellative e _•_ = AlmostLeftCancellative e _•_ × AlmostRightCancellative e _•_
 

From b64f1e17295f3e168036868db4c3b8a49aa2d2cb Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 20 Jan 2025 14:15:51 +0000
Subject: [PATCH 02/39] refactor: knock-on `Consequences`

---
 src/Algebra/Consequences/Setoid.agda | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda
index 66e441a9e0..24271b0a06 100644
--- a/src/Algebra/Consequences/Setoid.agda
+++ b/src/Algebra/Consequences/Setoid.agda
@@ -157,8 +157,9 @@ module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) {e : A} where
 
   comm∧almostCancelˡ⇒almostCancelʳ : AlmostLeftCancellative e _∙_ →
                                      AlmostRightCancellative e _∙_
-  comm∧almostCancelˡ⇒almostCancelʳ cancelˡ-nonZero x y z x≉e yx≈zx =
-    cancelˡ-nonZero x y z x≉e $ begin
+  comm∧almostCancelˡ⇒almostCancelʳ almostCancelˡ x with almostCancelˡ x
+  ... | inj₁ x≈e     = inj₁ x≈e
+  ... | inj₂ cancelˡ = inj₂ λ y z yx≈zx → cancelˡ y z $ begin
       x ∙ y ≈⟨ comm x y ⟩
       y ∙ x ≈⟨ yx≈zx ⟩
       z ∙ x ≈⟨ comm z x ⟩
@@ -166,8 +167,9 @@ module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) {e : A} where
 
   comm∧almostCancelʳ⇒almostCancelˡ : AlmostRightCancellative e _∙_ →
                                      AlmostLeftCancellative e _∙_
-  comm∧almostCancelʳ⇒almostCancelˡ cancelʳ-nonZero x y z x≉e xy≈xz =
-    cancelʳ-nonZero x y z x≉e $ begin
+  comm∧almostCancelʳ⇒almostCancelˡ almostCancelʳ x with almostCancelʳ x
+  ... | inj₁ x≈e     = inj₁ x≈e
+  ... | inj₂ cancelʳ = inj₂ λ y z xy≈xz → cancelʳ y z $ begin
       y ∙ x ≈⟨ comm y x ⟩
       x ∙ y ≈⟨ xy≈xz ⟩
       x ∙ z ≈⟨ comm x z ⟩

From a77cf6e0a88d3420ee44bf3a79fffbdd96977ee0 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 20 Jan 2025 14:17:19 +0000
Subject: [PATCH 03/39] update `README` to reflect intended milestone

---
 doc/README.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/README.agda b/doc/README.agda
index 78ad1cbbee..d2bd0b9caa 100644
--- a/doc/README.agda
+++ b/doc/README.agda
@@ -3,7 +3,7 @@
 module README where
 
 ------------------------------------------------------------------------
--- The Agda standard library, version 2.3-dev
+-- The Agda standard library, version 3.0-dev
 --
 -- Authors: Nils Anders Danielsson, Matthew Daggitt, Guillaume Allais
 -- with contributions from Andreas Abel, Stevan Andjelkovic,

From 7b09efd520ff94ab1ab6eb8e2036c12601173335 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 20 Jan 2025 14:32:50 +0000
Subject: [PATCH 04/39] refactor: knock-on
 `Algebra.Properties.CancellativeCommutativeSemiring`

---
 .../Properties/CancellativeCommutativeSemiring.agda    | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

diff --git a/src/Algebra/Properties/CancellativeCommutativeSemiring.agda b/src/Algebra/Properties/CancellativeCommutativeSemiring.agda
index e92fa5170e..a9702fcbf5 100644
--- a/src/Algebra/Properties/CancellativeCommutativeSemiring.agda
+++ b/src/Algebra/Properties/CancellativeCommutativeSemiring.agda
@@ -25,13 +25,9 @@ open import Relation.Binary.Reasoning.Setoid setoid
 *-almostCancelʳ = comm+almostCancelˡ⇒almostCancelʳ *-comm *-cancelˡ-nonZero
 
 xy≈0⇒x≈0∨y≈0 : Decidable _≈_ → ∀ {x y} → x * y ≈ 0# → x ≈ 0# ⊎ y ≈ 0#
-xy≈0⇒x≈0∨y≈0 _≟_ {x} {y} xy≈0 with x ≟ 0# | y ≟ 0#
-... | yes x≈0 | _       = inj₁ x≈0
-... | no  _   | yes y≈0 = inj₂ y≈0
-... | no  x≉0 | no  y≉0 = contradiction y≈0 y≉0
-  where
-  xy≈x*0 = trans xy≈0 (sym (zeroʳ x))
-  y≈0    = *-cancelˡ-nonZero _ y 0# x≉0 xy≈x*0
+xy≈0⇒x≈0∨y≈0 _≟_ {x} {y} xy≈0 with *-cancelˡ-nonZero x
+... | inj₁ x≈0     = inj₁ x≈0
+... | inj₂ cancelˡ = inj₂ (cancelˡ y 0# (trans xy≈0 (sym (zeroʳ x))))
 
 x≉0∧y≉0⇒xy≉0 : Decidable _≈_ → ∀ {x y} → x ≉ 0# → y ≉ 0# → x * y ≉ 0#
 x≉0∧y≉0⇒xy≉0 _≟_ x≉0 y≉0 xy≈0 with xy≈0⇒x≈0∨y≈0 _≟_ xy≈0

From 776ff3da760fc504ec26585e6ff0cef4f6dbd256 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 20 Jan 2025 15:23:41 +0000
Subject: [PATCH 05/39] refactor: tighten imports

---
 src/Algebra/Properties/Semiring/Primality.agda | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/Algebra/Properties/Semiring/Primality.agda b/src/Algebra/Properties/Semiring/Primality.agda
index 210d9fb1a0..dd8f821134 100644
--- a/src/Algebra/Properties/Semiring/Primality.agda
+++ b/src/Algebra/Properties/Semiring/Primality.agda
@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Some theory for CancellativeCommutativeSemiring.
+-- Properties of Coprimality and Irreducibility for Semiring.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
@@ -15,8 +15,11 @@ module Algebra.Properties.Semiring.Primality
   {a ℓ} (R : Semiring a ℓ)
   where
 
-open Semiring R renaming (Carrier to A)
+open Semiring R
+  using (_≉_; sym; trans; 0#; 1#; zeroˡ; rawSemiring)
+  renaming (Carrier to A)
 open import Algebra.Properties.Semiring.Divisibility R
+  using (_∣_; ∣-trans; 0∤1)
 
 ------------------------------------------------------------------------
 -- Re-export primality definitions

From 7e11c2629961363c7d5b18b2373f0e806f00a803 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 20 Jan 2025 15:25:05 +0000
Subject: [PATCH 06/39] tidy up

---
 src/Algebra/Definitions.agda | 9 ---------
 1 file changed, 9 deletions(-)

diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda
index 80f46dd329..8869e43119 100644
--- a/src/Algebra/Definitions.agda
+++ b/src/Algebra/Definitions.agda
@@ -148,16 +148,7 @@ RightCancellative _•_ = ∀ x y z → (y • x) ≈ (z • x) → y ≈ z
 
 Cancellative : Op₂ A → Set _
 Cancellative _•_ = (LeftCancellative _•_) × (RightCancellative _•_)
-{-
-AlmostLeftCancellative : A → Op₂ A → Set _
-AlmostLeftCancellative e _•_ = ∀ x y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z
-
-AlmostRightCancellative : A → Op₂ A → Set _
-AlmostRightCancellative e _•_ = ∀ x y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z
 
-AlmostCancellative : A → Op₂ A → Set _
-AlmostCancellative e _•_ = AlmostLeftCancellative e _•_ × AlmostRightCancellative e _•_
--}
 AlmostLeftCancellative : A → Op₂ A → Set _
 AlmostLeftCancellative e _•_ = ∀ x → x ≈ e ⊎ ∀ y z → (x • y) ≈ (x • z) → y ≈ z
 

From a3168a2734eb291a70ae1106b42a27ed90f9a070 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 6 Feb 2025 09:18:59 +0000
Subject: [PATCH 07/39] refactor: cosmetic redefinition

---
 src/Algebra/Definitions.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda
index 8869e43119..d1ec43ee17 100644
--- a/src/Algebra/Definitions.agda
+++ b/src/Algebra/Definitions.agda
@@ -37,10 +37,10 @@ Congruent₂ : Op₂ A → Set _
 Congruent₂ ∙ = ∙ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_
 
 LeftCongruent : Op₂ A → Set _
-LeftCongruent _∙_ = ∀ {x} → (x ∙_) Preserves _≈_ ⟶ _≈_
+LeftCongruent _∙_ = ∀ {x} → Congruent₁ (x ∙_)
 
 RightCongruent : Op₂ A → Set _
-RightCongruent _∙_ = ∀ {x} → (_∙ x) Preserves _≈_ ⟶ _≈_
+RightCongruent _∙_ = ∀ {x} → Congruent₁ (_∙ x)
 
 Associative : Op₂ A → Set _
 Associative _∙_ = ∀ x y z → ((x ∙ y) ∙ z) ≈ (x ∙ (y ∙ z))

From 1aa78f31133083afb691069a82d741c75f387fc8 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 6 Feb 2025 16:34:46 +0000
Subject: [PATCH 08/39] refactor: add definitions and consequences

---
 src/Algebra/Consequences/Base.agda | 34 ++++++++++++++++++++++++++++++
 src/Algebra/Definitions.agda       | 27 +++++++++++++++++++-----
 2 files changed, 56 insertions(+), 5 deletions(-)

diff --git a/src/Algebra/Consequences/Base.agda b/src/Algebra/Consequences/Base.agda
index 574ad48a16..f60e97207a 100644
--- a/src/Algebra/Consequences/Base.agda
+++ b/src/Algebra/Consequences/Base.agda
@@ -13,14 +13,48 @@ module Algebra.Consequences.Base
 open import Algebra.Core
 open import Algebra.Definitions
 open import Data.Sum.Base
+open import Function.Base using (const)
 open import Relation.Binary.Core
 open import Relation.Binary.Definitions using (Reflexive)
+open import Relation.Nullary.Decidable.Core using (yes; no)
+open import Relation.Nullary.Negation.Core using (contradiction)
+open import Relation.Unary using (Pred; Decidable)
+
 
 module _ {ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) where
 
   sel⇒idem : Selective _≈_ _•_ → Idempotent _≈_ _•_
   sel⇒idem sel x = reduce (sel x x)
 
+module _ {p ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) (P : Pred A p) where
+
+  almost⇒exceptˡ : _-AlmostLeftCancellative_ _≈_ P _•_ →
+                   Except_-LeftCancellative_ _≈_ P _•_
+  almost⇒exceptˡ cancelˡ {x} with cancelˡ x
+  ... | inj₁ px     = contradiction px
+  ... | inj₂ cancel = const cancel
+
+  almost⇒exceptʳ : _-AlmostRightCancellative_ _≈_ P _•_ →
+                   Except_-RightCancellative_ _≈_ P _•_
+  almost⇒exceptʳ cancelʳ {x} with cancelʳ x
+  ... | inj₁ px     = contradiction px
+  ... | inj₂ cancel = const cancel
+
+module _ {p ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ)
+         {P : Pred A p} (dec : Decidable P) where
+
+  except⇒almostˡ : Except_-LeftCancellative_ _≈_ P _•_ →
+                   _-AlmostLeftCancellative_ _≈_ P _•_
+  except⇒almostˡ cancelˡ x with dec x
+  ... | yes px = inj₁ px
+  ... | no ¬px = inj₂ (cancelˡ ¬px)
+
+  except⇒almostʳ : Except_-RightCancellative_ _≈_ P _•_ →
+                   _-AlmostRightCancellative_ _≈_ P _•_
+  except⇒almostʳ cancelʳ x with dec x
+  ... | yes px = inj₁ px
+  ... | no ¬px = inj₂ (cancelʳ ¬px)
+
 module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) where
 
   reflexive∧selfInverse⇒involutive : Reflexive _≈_ →
diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda
index d1ec43ee17..8a45720427 100644
--- a/src/Algebra/Definitions.agda
+++ b/src/Algebra/Definitions.agda
@@ -16,7 +16,6 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Relation.Binary.Core using (Rel; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
-open import Relation.Nullary.Negation.Core using (¬_)
 
 module Algebra.Definitions
   {a ℓ} {A : Set a}   -- The underlying set
@@ -26,6 +25,8 @@ module Algebra.Definitions
 open import Algebra.Core using (Op₁; Op₂)
 open import Data.Product.Base using (_×_; ∃-syntax)
 open import Data.Sum.Base using (_⊎_)
+open import Relation.Nullary.Negation.Core using (¬_)
+open import Relation.Unary using (Pred)
 
 ------------------------------------------------------------------------
 -- Properties of operations
@@ -140,20 +141,36 @@ SelfInverse f = ∀ {x y} → f x ≈ y → f y ≈ x
 Involutive : Op₁ A → Set _
 Involutive f = ∀ x → f (f x) ≈ x
 
+LeftCancellativeAt : A → Op₂ A → Set _
+LeftCancellativeAt x _•_ = ∀ y z → (x • y) ≈ (x • z) → y ≈ z
+
 LeftCancellative : Op₂ A → Set _
-LeftCancellative _•_ = ∀ x y z → (x • y) ≈ (x • z) → y ≈ z
+LeftCancellative _•_ = ∀ x → LeftCancellativeAt x _•_
+
+RightCancellativeAt : A → Op₂ A → Set _
+RightCancellativeAt x _•_ = ∀ y z → (y • x) ≈ (z • x) → y ≈ z
 
 RightCancellative : Op₂ A → Set _
-RightCancellative _•_ = ∀ x y z → (y • x) ≈ (z • x) → y ≈ z
+RightCancellative _•_ = ∀ x → RightCancellativeAt x _•_
 
 Cancellative : Op₂ A → Set _
 Cancellative _•_ = (LeftCancellative _•_) × (RightCancellative _•_)
 
+_-AlmostLeftCancellative_ Except_-LeftCancellative_ : ∀ {p} (P : Pred A p) →
+                                                      Op₂ A → Set _
+P -AlmostLeftCancellative _•_ = ∀ x → P x ⊎ LeftCancellativeAt x _•_
+Except P -LeftCancellative _•_ = ∀ {x} → ¬ (P x) → LeftCancellativeAt x _•_
+
 AlmostLeftCancellative : A → Op₂ A → Set _
-AlmostLeftCancellative e _•_ = ∀ x → x ≈ e ⊎ ∀ y z → (x • y) ≈ (x • z) → y ≈ z
+AlmostLeftCancellative e = (_≈ e) -AlmostLeftCancellative_
+
+_-AlmostRightCancellative_ Except_-RightCancellative_ : ∀ {p} (P : Pred A p) →
+                                                         Op₂ A → Set _
+P -AlmostRightCancellative _•_ = ∀ x → P x ⊎ RightCancellativeAt x _•_
+Except P -RightCancellative _•_ = ∀ {x} → ¬ (P x) → RightCancellativeAt x _•_
 
 AlmostRightCancellative : A → Op₂ A → Set _
-AlmostRightCancellative e _•_ = ∀ x → x ≈ e ⊎ ∀ y z → (y • x) ≈ (z • x) → y ≈ z
+AlmostRightCancellative e = (_≈ e) -AlmostLeftCancellative_
 
 AlmostCancellative : A → Op₂ A → Set _
 AlmostCancellative e _•_ = AlmostLeftCancellative e _•_ × AlmostRightCancellative e _•_

From c75c12a135d607969fe283cbd0bf55f8144bc79d Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 6 Feb 2025 16:43:36 +0000
Subject: [PATCH 09/39] fix: oops!

---
 src/Algebra/Definitions.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda
index 8a45720427..3cf1e2848a 100644
--- a/src/Algebra/Definitions.agda
+++ b/src/Algebra/Definitions.agda
@@ -170,7 +170,7 @@ P -AlmostRightCancellative _•_ = ∀ x → P x ⊎ RightCancellativeAt x _•_
 Except P -RightCancellative _•_ = ∀ {x} → ¬ (P x) → RightCancellativeAt x _•_
 
 AlmostRightCancellative : A → Op₂ A → Set _
-AlmostRightCancellative e = (_≈ e) -AlmostLeftCancellative_
+AlmostRightCancellative e = (_≈ e) -AlmostRightCancellative_
 
 AlmostCancellative : A → Op₂ A → Set _
 AlmostCancellative e _•_ = AlmostLeftCancellative e _•_ × AlmostRightCancellative e _•_

From 8d9f167ccfd9ed5e16ad00ca6f47621d6325f227 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 6 Feb 2025 17:25:30 +0000
Subject: [PATCH 10/39] =?UTF-8?q?refactor:=20add=20`*-almostCancel=CA=B3-?=
 =?UTF-8?q?=E2=89=A1`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Data/Nat/Properties.agda | 20 ++++++++++++++------
 1 file changed, 14 insertions(+), 6 deletions(-)

diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 3537b3298a..76b6b7fb0b 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -16,8 +16,6 @@ open import Algebra.Bundles using (Magma; Semigroup; CommutativeSemigroup;
   CommutativeMonoid; Monoid; Semiring; CommutativeSemiring; CommutativeSemiringWithoutOne)
 open import Algebra.Definitions.RawMagma using (_,_)
 open import Algebra.Morphism
-open import Algebra.Consequences.Propositional
-  using (comm+cancelˡ⇒cancelʳ; comm∧distrʳ⇒distrˡ; comm∧distrˡ⇒distrʳ)
 open import Algebra.Construct.NaturalChoice.Base
   using (MinOperator; MaxOperator)
 import Algebra.Construct.NaturalChoice.MinMaxOp as MinMaxOp
@@ -46,6 +44,10 @@ open import Relation.Nullary.Decidable using (True; via-injection; map′; recom
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Reflects using (fromEquivalence)
 
+open import Algebra.Consequences.Propositional {A = ℕ}
+  using ( comm∧cancelˡ⇒cancelʳ
+        ; comm∧distrʳ⇒distrˡ; comm∧distrˡ⇒distrʳ
+        ; almost⇒exceptʳ)
 open import Algebra.Definitions {A = ℕ} _≡_
   hiding (LeftCancellative; RightCancellative; Cancellative)
 open import Algebra.Definitions
@@ -561,7 +563,7 @@ open ≤-Reasoning
 +-cancelˡ-≡ (suc m) _ _ eq = +-cancelˡ-≡ m _ _ (cong pred eq)
 
 +-cancelʳ-≡ : RightCancellative _≡_ _+_
-+-cancelʳ-≡ = comm+cancelˡ⇒cancelʳ +-comm +-cancelˡ-≡
++-cancelʳ-≡ = comm∧cancelˡ⇒cancelʳ +-comm +-cancelˡ-≡
 
 +-cancel-≡ : Cancellative _≡_ _+_
 +-cancel-≡ = +-cancelˡ-≡ , +-cancelʳ-≡
@@ -908,10 +910,16 @@ m+n≮m m n = subst (_≮ m) (+-comm n m) (m+n≮n n m)
 ------------------------------------------------------------------------
 -- Other properties of _*_ and _≡_
 
+*-almostCancelʳ-≡ : AlmostRightCancellative 0 _*_
+*-almostCancelʳ-≡ zero    = inj₁ refl
+*-almostCancelʳ-≡ o@(suc _) = inj₂ lemma
+  module *-AlmostRightCancellative where
+  lemma : RightCancellativeAt o _*_
+  lemma zero    zero    _  = refl
+  lemma (suc m) (suc n) eq = cong suc (lemma m n (+-cancelˡ-≡ o (m * o) (n * o) eq))
+
 *-cancelʳ-≡ : ∀ m n o .{{_ : NonZero o}} → m * o ≡ n * o → m ≡ n
-*-cancelʳ-≡ zero    zero    (suc o) eq = refl
-*-cancelʳ-≡ (suc m) (suc n) (suc o) eq =
-  cong suc (*-cancelʳ-≡ m n (suc o) (+-cancelˡ-≡ (suc o) (m * suc o) (n * suc o) eq))
+*-cancelʳ-≡ m n o = almost⇒exceptʳ _ _ *-almostCancelʳ-≡ (≢-nonZero⁻¹ _) m n
 
 *-cancelˡ-≡ : ∀ m n o .{{_ : NonZero o}} → o * m ≡ o * n → m ≡ n
 *-cancelˡ-≡ m n o rewrite *-comm o m | *-comm o n = *-cancelʳ-≡ m n o

From cbc33e8ad8f2d04009c2766de47a00a6d9aa6be2 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 6 Feb 2025 18:09:22 +0000
Subject: [PATCH 11/39] refactor: tweak `import`s

---
 src/Data/Integer/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda
index f89d3164f6..da837014c8 100644
--- a/src/Data/Integer/Properties.agda
+++ b/src/Data/Integer/Properties.agda
@@ -44,7 +44,7 @@ open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 import Relation.Nullary.Decidable as Dec
 
 open import Algebra.Definitions {A = ℤ} _≡_
-open import Algebra.Consequences.Propositional
+open import Algebra.Consequences.Propositional {A = ℤ}
 open import Algebra.Structures {A = ℤ} _≡_
 module ℤtoℕ = Morphism.Definitions ℤ ℕ _≡_
 module ℕtoℤ = Morphism.Definitions ℕ ℤ _≡_

From 63694db511005122ed23b2f5d207c01bb858e05b Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 6 Feb 2025 18:10:03 +0000
Subject: [PATCH 12/39] refactor: `breaking` rectify lemma statement

---
 src/Data/Rational/Unnormalised/Properties.agda | 16 ++++++----------
 1 file changed, 6 insertions(+), 10 deletions(-)

diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda
index 181e4a6189..401a996542 100644
--- a/src/Data/Rational/Unnormalised/Properties.agda
+++ b/src/Data/Rational/Unnormalised/Properties.agda
@@ -13,7 +13,6 @@ open import Algebra
 open import Algebra.Apartness
 open import Algebra.Lattice
 import Algebra.Consequences.Setoid as Consequences
-open import Algebra.Consequences.Propositional
 open import Algebra.Construct.NaturalChoice.Base
 import Algebra.Construct.NaturalChoice.MinMaxOp as MinMaxOp
 import Algebra.Lattice.Construct.NaturalChoice.MinMaxOp as LatticeMinMaxOp
@@ -44,6 +43,7 @@ import Relation.Binary.Properties.Poset as PosetProperties
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 open import Relation.Binary.Reasoning.Syntax
 
+open import Algebra.Consequences.Propositional {A = ℚᵘ}
 open import Algebra.Properties.CommutativeSemigroup ℤ.*-commutativeSemigroup
 
 private
@@ -746,7 +746,7 @@ neg⇒nonZero (mkℚᵘ (-[1+ _ ]) _) = _
 +-identityˡ p = ≃-reflexive (+-identityˡ-≡ p)
 
 +-identityʳ-≡ : RightIdentity _≡_ 0ℚᵘ _+_
-+-identityʳ-≡ = comm+idˡ⇒idʳ +-comm-≡ {e = 0ℚᵘ} +-identityˡ-≡
++-identityʳ-≡ = comm∧idˡ⇒idʳ +-comm-≡ {e = 0ℚᵘ} +-identityˡ-≡
 
 +-identityʳ : RightIdentity _≃_ 0ℚᵘ _+_
 +-identityʳ p = ≃-reflexive (+-identityʳ-≡ p)
@@ -774,8 +774,8 @@ neg⇒nonZero (mkℚᵘ (-[1+ _ ]) _) = _
 +-inverse : Inverse _≃_ 0ℚᵘ -_ _+_
 +-inverse = +-inverseˡ , +-inverseʳ
 
-+-cancelˡ : ∀ {r p q} → r + p ≃ r + q → p ≃ q
-+-cancelˡ {r} {p} {q} r+p≃r+q = begin-equality
++-cancelˡ : LeftCancellative _≃_ _+_
++-cancelˡ r p q r+p≃r+q = begin-equality
   p            ≃⟨ +-identityʳ p ⟨
   p + 0ℚᵘ      ≃⟨ +-congʳ p (+-inverseʳ r) ⟨
   p + (r - r)  ≃⟨ +-assoc p r (- r) ⟨
@@ -787,12 +787,8 @@ neg⇒nonZero (mkℚᵘ (-[1+ _ ]) _) = _
   q + 0ℚᵘ      ≃⟨ +-identityʳ q ⟩
   q            ∎ where open ≤-Reasoning
 
-+-cancelʳ : ∀ {r p q} → p + r ≃ q + r → p ≃ q
-+-cancelʳ {r} {p} {q} p+r≃q+r = +-cancelˡ {r} $ begin-equality
-  r + p ≃⟨ +-comm r p ⟩
-  p + r ≃⟨ p+r≃q+r ⟩
-  q + r ≃⟨ +-comm q r ⟩
-  r + q ∎ where open ≤-Reasoning
++-cancelʳ : RightCancellative _≃_ _+_
++-cancelʳ = Consequences.comm∧cancelˡ⇒cancelʳ ≃-setoid +-comm +-cancelˡ
 
 p+p≃0⇒p≃0 : ∀ p → p + p ≃ 0ℚᵘ → p ≃ 0ℚᵘ
 p+p≃0⇒p≃0 (mkℚᵘ ℤ.+0 _) (*≡* _) = *≡* refl

From 4049a7be94c69ed246e1913253437a9e9333cde6 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 6 Feb 2025 18:18:42 +0000
Subject: [PATCH 13/39] refactor: cosmetic

---
 src/Data/Rational/Properties.agda | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index 0341f53c45..6db9625c99 100644
--- a/src/Data/Rational/Properties.agda
+++ b/src/Data/Rational/Properties.agda
@@ -13,7 +13,6 @@ open import Algebra.Apartness
 open import Algebra.Construct.NaturalChoice.Base
 import Algebra.Construct.NaturalChoice.MinMaxOp as MinMaxOp
 import Algebra.Lattice.Construct.NaturalChoice.MinMaxOp as LatticeMinMaxOp
-open import Algebra.Consequences.Propositional
 open import Algebra.Morphism
 open import Algebra.Bundles
 import Algebra.Morphism.MagmaMonomorphism  as MagmaMonomorphisms
@@ -64,6 +63,7 @@ open import Relation.Nullary.Decidable.Core as Dec
   using (yes; no; recompute; map′; _×-dec_)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 
+open import Algebra.Consequences.Propositional {A = ℚ}
 open import Algebra.Definitions {A = ℚ} _≡_
 open import Algebra.Structures  {A = ℚ} _≡_
 
@@ -168,9 +168,9 @@ drop-*≡* (*≡* eq) = eq
       ℤ.∣ n₁ ∣ ℕ.* suc d₂    ∎)
 
   helper : mkℚ n₁ d₁ c₁ ≡ mkℚ n₂ d₂ c₂
-  helper with ∣-antisym 1+d₁∣1+d₂ 1+d₂∣1+d₁
-  ... | refl with ℤ.*-cancelʳ-≡ n₁ n₂ (+ suc d₁) eq
-  ...   | refl = refl
+  helper with refl ← ∣-antisym 1+d₁∣1+d₂ 1+d₂∣1+d₁
+         with refl ← ℤ.*-cancelʳ-≡ n₁ n₂ (+ suc d₁) eq
+    = refl
 
 ≃-sym : Symmetric _≃_
 ≃-sym = ≡⇒≃ ∘′ sym ∘′ ≃⇒≡
@@ -857,14 +857,14 @@ toℚᵘ-homo-+ p@record{} q@record{} with +-nf p q ℤ.≟ 0ℤ
   eq : ↥ (p + q) ≡ 0ℤ
   eq rewrite eq2 = cong ↥_ (0/n≡0 (↧ₙ p ℕ.* ↧ₙ q))
 
-... | no  nf[p,q]≢0 = *≡* (ℤ.*-cancelʳ-≡ _ _ (+-nf p q) {{ℤ.≢-nonZero nf[p,q]≢0}} $ begin
+... | no  nf[p,q]≢0 = *≡* $ ℤ.*-cancelʳ-≡ _ _ (+-nf p q) {{ℤ.≢-nonZero nf[p,q]≢0}} $ begin
     (↥ᵘ (toℚᵘ (p + q))) ℤ.* ↧+ᵘ p q  ℤ.* +-nf p q ≡⟨ cong (λ v → v ℤ.* ↧+ᵘ p q ℤ.* +-nf p q) (↥ᵘ-toℚᵘ (p + q)) ⟩
     ↥ (p + q) ℤ.* ↧+ᵘ p q ℤ.* +-nf p q            ≡⟨ xy∙z≈xz∙y (↥ (p + q)) _ _ ⟩
     ↥ (p + q) ℤ.* +-nf p q ℤ.* ↧+ᵘ p q            ≡⟨ cong (ℤ._* ↧+ᵘ p q) (↥-+ p q) ⟩
     ↥+ᵘ p q ℤ.* ↧+ᵘ p q                           ≡⟨ cong (↥+ᵘ p q ℤ.*_) (sym (↧-+ p q)) ⟩
     ↥+ᵘ p q ℤ.* (↧ (p + q) ℤ.* +-nf p q)          ≡⟨ x∙yz≈xy∙z (↥+ᵘ p q) _ _ ⟩
     ↥+ᵘ p q ℤ.* ↧ (p + q)  ℤ.* +-nf p q           ≡⟨ cong (λ v → ↥+ᵘ p q ℤ.* v ℤ.* +-nf p q) (↧ᵘ-toℚᵘ (p + q)) ⟨
-    ↥+ᵘ p q ℤ.* ↧ᵘ (toℚᵘ (p + q)) ℤ.* +-nf p q    ∎)
+    ↥+ᵘ p q ℤ.* ↧ᵘ (toℚᵘ (p + q)) ℤ.* +-nf p q    ∎
   where open ≡-Reasoning; open CommSemigroupProperties ℤ.*-commutativeSemigroup
 
 toℚᵘ-isMagmaHomomorphism-+ : IsMagmaHomomorphism +-rawMagma ℚᵘ.+-rawMagma toℚᵘ
@@ -1092,14 +1092,14 @@ toℚᵘ-homo-* p@record{} q@record{} with *-nf p q ℤ.≟ 0ℤ
 
   eq : ↥ (p * q) ≡ 0ℤ
   eq rewrite eq2 = cong ↥_ (0/n≡0 (↧ₙ p ℕ.* ↧ₙ q))
-... | no nf[p,q]≢0 = *≡* (ℤ.*-cancelʳ-≡ _ _ (*-nf p q) {{ℤ.≢-nonZero nf[p,q]≢0}} $ begin
+... | no nf[p,q]≢0 = *≡* $ ℤ.*-cancelʳ-≡ _ _ (*-nf p q) {{ℤ.≢-nonZero nf[p,q]≢0}} $ begin
   ↥ᵘ (toℚᵘ (p * q)) ℤ.* (↧ p ℤ.* ↧ q) ℤ.* *-nf p q     ≡⟨ cong (λ v → v ℤ.* (↧ p ℤ.* ↧ q) ℤ.* *-nf p q) (↥ᵘ-toℚᵘ (p * q)) ⟩
   ↥ (p * q)         ℤ.* (↧ p ℤ.* ↧ q) ℤ.* *-nf p q     ≡⟨ xy∙z≈xz∙y (↥ (p * q)) _ _ ⟩
   ↥ (p * q)         ℤ.* *-nf p q ℤ.* (↧ p ℤ.* ↧ q)     ≡⟨ cong (ℤ._* (↧ p ℤ.* ↧ q)) (↥-* p q) ⟩
   (↥ p ℤ.* ↥ q)     ℤ.* (↧ p ℤ.* ↧ q)                  ≡⟨ cong ((↥ p ℤ.* ↥ q) ℤ.*_) (sym (↧-* p q)) ⟩
   (↥ p ℤ.* ↥ q)     ℤ.* (↧ (p * q) ℤ.* *-nf p q)       ≡⟨ x∙yz≈xy∙z (↥ p ℤ.* ↥ q) _ _ ⟩
   (↥ p ℤ.* ↥ q)     ℤ.* ↧ (p * q)  ℤ.* *-nf p q        ≡⟨ cong (λ v → (↥ p ℤ.* ↥ q) ℤ.* v ℤ.* *-nf p q) (↧ᵘ-toℚᵘ (p * q)) ⟨
-  (↥ p ℤ.* ↥ q)     ℤ.* ↧ᵘ (toℚᵘ (p * q)) ℤ.* *-nf p q ∎)
+  (↥ p ℤ.* ↥ q)     ℤ.* ↧ᵘ (toℚᵘ (p * q)) ℤ.* *-nf p q ∎
   where open ≡-Reasoning; open CommSemigroupProperties ℤ.*-commutativeSemigroup
 
 toℚᵘ-homo-1/ : ∀ p .{{_ : NonZero p}} → toℚᵘ (1/ p) ℚᵘ.≃ (ℚᵘ.1/ toℚᵘ p)

From a46af5b18e0062e9faaf941c369ca1c2714abfe6 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 6 Feb 2025 18:24:39 +0000
Subject: [PATCH 14/39] refactor: cosmetic; dollar application slows down
 typechecker considerably

---
 src/Data/Rational/Properties.agda | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index 6db9625c99..6c476d2ddb 100644
--- a/src/Data/Rational/Properties.agda
+++ b/src/Data/Rational/Properties.agda
@@ -857,14 +857,14 @@ toℚᵘ-homo-+ p@record{} q@record{} with +-nf p q ℤ.≟ 0ℤ
   eq : ↥ (p + q) ≡ 0ℤ
   eq rewrite eq2 = cong ↥_ (0/n≡0 (↧ₙ p ℕ.* ↧ₙ q))
 
-... | no  nf[p,q]≢0 = *≡* $ ℤ.*-cancelʳ-≡ _ _ (+-nf p q) {{ℤ.≢-nonZero nf[p,q]≢0}} $ begin
+... | no  nf[p,q]≢0 = *≡* (ℤ.*-cancelʳ-≡ _ _ (+-nf p q) {{ℤ.≢-nonZero nf[p,q]≢0}} (begin
     (↥ᵘ (toℚᵘ (p + q))) ℤ.* ↧+ᵘ p q  ℤ.* +-nf p q ≡⟨ cong (λ v → v ℤ.* ↧+ᵘ p q ℤ.* +-nf p q) (↥ᵘ-toℚᵘ (p + q)) ⟩
     ↥ (p + q) ℤ.* ↧+ᵘ p q ℤ.* +-nf p q            ≡⟨ xy∙z≈xz∙y (↥ (p + q)) _ _ ⟩
     ↥ (p + q) ℤ.* +-nf p q ℤ.* ↧+ᵘ p q            ≡⟨ cong (ℤ._* ↧+ᵘ p q) (↥-+ p q) ⟩
     ↥+ᵘ p q ℤ.* ↧+ᵘ p q                           ≡⟨ cong (↥+ᵘ p q ℤ.*_) (sym (↧-+ p q)) ⟩
     ↥+ᵘ p q ℤ.* (↧ (p + q) ℤ.* +-nf p q)          ≡⟨ x∙yz≈xy∙z (↥+ᵘ p q) _ _ ⟩
     ↥+ᵘ p q ℤ.* ↧ (p + q)  ℤ.* +-nf p q           ≡⟨ cong (λ v → ↥+ᵘ p q ℤ.* v ℤ.* +-nf p q) (↧ᵘ-toℚᵘ (p + q)) ⟨
-    ↥+ᵘ p q ℤ.* ↧ᵘ (toℚᵘ (p + q)) ℤ.* +-nf p q    ∎
+    ↥+ᵘ p q ℤ.* ↧ᵘ (toℚᵘ (p + q)) ℤ.* +-nf p q    ∎))
   where open ≡-Reasoning; open CommSemigroupProperties ℤ.*-commutativeSemigroup
 
 toℚᵘ-isMagmaHomomorphism-+ : IsMagmaHomomorphism +-rawMagma ℚᵘ.+-rawMagma toℚᵘ
@@ -1092,14 +1092,14 @@ toℚᵘ-homo-* p@record{} q@record{} with *-nf p q ℤ.≟ 0ℤ
 
   eq : ↥ (p * q) ≡ 0ℤ
   eq rewrite eq2 = cong ↥_ (0/n≡0 (↧ₙ p ℕ.* ↧ₙ q))
-... | no nf[p,q]≢0 = *≡* $ ℤ.*-cancelʳ-≡ _ _ (*-nf p q) {{ℤ.≢-nonZero nf[p,q]≢0}} $ begin
+... | no nf[p,q]≢0 = *≡* (ℤ.*-cancelʳ-≡ _ _ (*-nf p q) {{ℤ.≢-nonZero nf[p,q]≢0}} (begin
   ↥ᵘ (toℚᵘ (p * q)) ℤ.* (↧ p ℤ.* ↧ q) ℤ.* *-nf p q     ≡⟨ cong (λ v → v ℤ.* (↧ p ℤ.* ↧ q) ℤ.* *-nf p q) (↥ᵘ-toℚᵘ (p * q)) ⟩
   ↥ (p * q)         ℤ.* (↧ p ℤ.* ↧ q) ℤ.* *-nf p q     ≡⟨ xy∙z≈xz∙y (↥ (p * q)) _ _ ⟩
   ↥ (p * q)         ℤ.* *-nf p q ℤ.* (↧ p ℤ.* ↧ q)     ≡⟨ cong (ℤ._* (↧ p ℤ.* ↧ q)) (↥-* p q) ⟩
   (↥ p ℤ.* ↥ q)     ℤ.* (↧ p ℤ.* ↧ q)                  ≡⟨ cong ((↥ p ℤ.* ↥ q) ℤ.*_) (sym (↧-* p q)) ⟩
   (↥ p ℤ.* ↥ q)     ℤ.* (↧ (p * q) ℤ.* *-nf p q)       ≡⟨ x∙yz≈xy∙z (↥ p ℤ.* ↥ q) _ _ ⟩
   (↥ p ℤ.* ↥ q)     ℤ.* ↧ (p * q)  ℤ.* *-nf p q        ≡⟨ cong (λ v → (↥ p ℤ.* ↥ q) ℤ.* v ℤ.* *-nf p q) (↧ᵘ-toℚᵘ (p * q)) ⟨
-  (↥ p ℤ.* ↥ q)     ℤ.* ↧ᵘ (toℚᵘ (p * q)) ℤ.* *-nf p q ∎
+  (↥ p ℤ.* ↥ q)     ℤ.* ↧ᵘ (toℚᵘ (p * q)) ℤ.* *-nf p q ∎))
   where open ≡-Reasoning; open CommSemigroupProperties ℤ.*-commutativeSemigroup
 
 toℚᵘ-homo-1/ : ∀ p .{{_ : NonZero p}} → toℚᵘ (1/ p) ℚᵘ.≃ (ℚᵘ.1/ toℚᵘ p)

From d06f0a9f2cfa6fc452ce93833c6da164c40a0dc1 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 9 Feb 2025 11:11:35 +0000
Subject: [PATCH 15/39] refactor: avoid `with` if possible

---
 src/Algebra/Consequences/Base.agda | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

diff --git a/src/Algebra/Consequences/Base.agda b/src/Algebra/Consequences/Base.agda
index f60e97207a..57bbc4b1b1 100644
--- a/src/Algebra/Consequences/Base.agda
+++ b/src/Algebra/Consequences/Base.agda
@@ -30,15 +30,11 @@ module _ {p ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) (P : Pred A p) where
 
   almost⇒exceptˡ : _-AlmostLeftCancellative_ _≈_ P _•_ →
                    Except_-LeftCancellative_ _≈_ P _•_
-  almost⇒exceptˡ cancelˡ {x} with cancelˡ x
-  ... | inj₁ px     = contradiction px
-  ... | inj₂ cancel = const cancel
+  almost⇒exceptˡ cancel = [ contradiction , const ]′ (cancel _)
 
   almost⇒exceptʳ : _-AlmostRightCancellative_ _≈_ P _•_ →
                    Except_-RightCancellative_ _≈_ P _•_
-  almost⇒exceptʳ cancelʳ {x} with cancelʳ x
-  ... | inj₁ px     = contradiction px
-  ... | inj₂ cancel = const cancel
+  almost⇒exceptʳ cancel = [ contradiction , const ]′ (cancel _)
 
 module _ {p ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ)
          {P : Pred A p} (dec : Decidable P) where

From 4bd8a7f38770af04e5c4274d918cf314f2b0b96d Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 9 Feb 2025 11:12:13 +0000
Subject: [PATCH 16/39] refactor: introduce `At` lemma factorisation

---
 src/Algebra/Consequences/Setoid.agda | 36 +++++++++++++---------------
 1 file changed, 17 insertions(+), 19 deletions(-)

diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda
index 24271b0a06..6414978b93 100644
--- a/src/Algebra/Consequences/Setoid.agda
+++ b/src/Algebra/Consequences/Setoid.agda
@@ -17,7 +17,7 @@ module Algebra.Consequences.Setoid {a ℓ} (S : Setoid a ℓ) where
 open Setoid S renaming (Carrier to A)
 open import Algebra.Core
 open import Algebra.Definitions _≈_
-open import Data.Sum.Base using (inj₁; inj₂)
+open import Data.Sum.Base using (inj₁; inj₂; [_,_])
 open import Data.Product.Base using (_,_)
 open import Function.Base using (_$_; id; _∘_)
 open import Function.Definitions
@@ -100,20 +100,28 @@ module _ {f : Op₁ A} (self : SelfInverse f) where
 
 module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) where
 
-  comm∧cancelˡ⇒cancelʳ : LeftCancellative _∙_ → RightCancellative _∙_
-  comm∧cancelˡ⇒cancelʳ cancelˡ x y z eq = cancelˡ x y z $ begin
+  comm∧cancelAtˡ⇒cancelAtʳ : ∀ {x} → LeftCancellativeAt x _∙_ →
+                             RightCancellativeAt x _∙_
+  comm∧cancelAtˡ⇒cancelAtʳ {x = x} cancel y z eq = cancel y z $ begin
     x ∙ y ≈⟨ comm x y ⟩
     y ∙ x ≈⟨ eq ⟩
     z ∙ x ≈⟨ comm z x ⟩
     x ∙ z ∎
 
-  comm∧cancelʳ⇒cancelˡ : RightCancellative _∙_ → LeftCancellative _∙_
-  comm∧cancelʳ⇒cancelˡ cancelʳ x y z eq = cancelʳ x y z $ begin
+  comm∧cancelˡ⇒cancelʳ : LeftCancellative _∙_ → RightCancellative _∙_
+  comm∧cancelˡ⇒cancelʳ cancel = comm∧cancelAtˡ⇒cancelAtʳ ∘ cancel
+
+  comm∧cancelAtʳ⇒cancelAtˡ : ∀ {x} → RightCancellativeAt x _∙_ →
+                             LeftCancellativeAt x _∙_
+  comm∧cancelAtʳ⇒cancelAtˡ {x = x} cancel y z eq = cancel y z $ begin
     y ∙ x ≈⟨ comm y x ⟩
     x ∙ y ≈⟨ eq ⟩
     x ∙ z ≈⟨ comm x z ⟩
     z ∙ x ∎
 
+  comm∧cancelʳ⇒cancelˡ : RightCancellative _∙_ → LeftCancellative _∙_
+  comm∧cancelʳ⇒cancelˡ cancel = comm∧cancelAtʳ⇒cancelAtˡ ∘ cancel
+
 ------------------------------------------------------------------------
 -- Monoid-like structures
 
@@ -157,23 +165,13 @@ module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) {e : A} where
 
   comm∧almostCancelˡ⇒almostCancelʳ : AlmostLeftCancellative e _∙_ →
                                      AlmostRightCancellative e _∙_
-  comm∧almostCancelˡ⇒almostCancelʳ almostCancelˡ x with almostCancelˡ x
-  ... | inj₁ x≈e     = inj₁ x≈e
-  ... | inj₂ cancelˡ = inj₂ λ y z yx≈zx → cancelˡ y z $ begin
-      x ∙ y ≈⟨ comm x y ⟩
-      y ∙ x ≈⟨ yx≈zx ⟩
-      z ∙ x ≈⟨ comm z x ⟩
-      x ∙ z ∎
+  comm∧almostCancelˡ⇒almostCancelʳ almostCancel =
+    [ inj₁ , inj₂ ∘ comm∧cancelAtˡ⇒cancelAtʳ comm ] ∘ almostCancel
 
   comm∧almostCancelʳ⇒almostCancelˡ : AlmostRightCancellative e _∙_ →
                                      AlmostLeftCancellative e _∙_
-  comm∧almostCancelʳ⇒almostCancelˡ almostCancelʳ x with almostCancelʳ x
-  ... | inj₁ x≈e     = inj₁ x≈e
-  ... | inj₂ cancelʳ = inj₂ λ y z xy≈xz → cancelʳ y z $ begin
-      y ∙ x ≈⟨ comm y x ⟩
-      x ∙ y ≈⟨ xy≈xz ⟩
-      x ∙ z ≈⟨ comm x z ⟩
-      z ∙ x ∎
+  comm∧almostCancelʳ⇒almostCancelˡ almostCancel  =
+    [ inj₁ , inj₂ ∘ comm∧cancelAtʳ⇒cancelAtˡ comm ] ∘ almostCancel
 
 ------------------------------------------------------------------------
 -- Group-like structures

From 05a11e92c25b7f4e4ae97cd0ed59302731d45bce Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 9 Feb 2025 11:32:16 +0000
Subject: [PATCH 17/39] `CHANGELOG`

---
 CHANGELOG.md | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4940047ba8..5fd8b25293 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -67,6 +67,12 @@ New modules
 Additions to existing modules
 -----------------------------
 
+* In `Algebra.Consequences.Setoid`:
+  ```agda
+  comm∧cancelAtˡ⇒cancelAtʳ : LeftCancellativeAt x _∙_ → RightCancellativeAt x _∙_
+  comm∧cancelAtʳ⇒cancelAtˡ : RightCancellativeAt x _∙_ → LeftCancellativeAt x _∙_
+  ```
+
 * In `Algebra.Construct.Pointwise`:
   ```agda
   isNearSemiring                  : IsNearSemiring _≈_ _+_ _*_ 0# →

From 5e9ac7c063a039dc2a35827b1645940c5a371c08 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 10 Feb 2025 05:14:33 +0000
Subject: [PATCH 18/39] refactor: use `instance`s

---
 src/Algebra/Consequences/Base.agda | 20 ++++++++++++--------
 src/Algebra/Definitions.agda       | 22 +++++++++++++---------
 2 files changed, 25 insertions(+), 17 deletions(-)

diff --git a/src/Algebra/Consequences/Base.agda b/src/Algebra/Consequences/Base.agda
index 57bbc4b1b1..18f1a45cc4 100644
--- a/src/Algebra/Consequences/Base.agda
+++ b/src/Algebra/Consequences/Base.agda
@@ -13,11 +13,12 @@ module Algebra.Consequences.Base
 open import Algebra.Core
 open import Algebra.Definitions
 open import Data.Sum.Base
-open import Function.Base using (const)
+open import Function.Base using (id; const; flip)
 open import Relation.Binary.Core
 open import Relation.Binary.Definitions using (Reflexive)
 open import Relation.Nullary.Decidable.Core using (yes; no)
 open import Relation.Nullary.Negation.Core using (contradiction)
+open import Relation.Nullary.Recomputable using (¬-recompute)
 open import Relation.Unary using (Pred; Decidable)
 
 
@@ -26,30 +27,33 @@ module _ {ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) where
   sel⇒idem : Selective _≈_ _•_ → Idempotent _≈_ _•_
   sel⇒idem sel x = reduce (sel x x)
 
-module _ {p ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) (P : Pred A p) where
+module _ {p ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ)
+         {P : Pred A p} where
 
   almost⇒exceptˡ : _-AlmostLeftCancellative_ _≈_ P _•_ →
                    Except_-LeftCancellative_ _≈_ P _•_
-  almost⇒exceptˡ cancel = [ contradiction , const ]′ (cancel _)
+  almost⇒exceptˡ cancel x {{¬px}} =
+    [ flip contradiction (¬-recompute ¬px) , id ]′ (cancel x)
 
   almost⇒exceptʳ : _-AlmostRightCancellative_ _≈_ P _•_ →
                    Except_-RightCancellative_ _≈_ P _•_
-  almost⇒exceptʳ cancel = [ contradiction , const ]′ (cancel _)
+  almost⇒exceptʳ cancel x {{¬px}} =
+    [ flip contradiction (¬-recompute ¬px) , id ]′ (cancel x)
 
 module _ {p ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ)
          {P : Pred A p} (dec : Decidable P) where
 
   except⇒almostˡ : Except_-LeftCancellative_ _≈_ P _•_ →
                    _-AlmostLeftCancellative_ _≈_ P _•_
-  except⇒almostˡ cancelˡ x with dec x
+  except⇒almostˡ cancel x with dec x
   ... | yes px = inj₁ px
-  ... | no ¬px = inj₂ (cancelˡ ¬px)
+  ... | no ¬px = inj₂ (cancel x {{¬px}})
 
   except⇒almostʳ : Except_-RightCancellative_ _≈_ P _•_ →
                    _-AlmostRightCancellative_ _≈_ P _•_
-  except⇒almostʳ cancelʳ x with dec x
+  except⇒almostʳ cancel x with dec x
   ... | yes px = inj₁ px
-  ... | no ¬px = inj₂ (cancelʳ ¬px)
+  ... | no ¬px = inj₂ (cancel x {{¬px}})
 
 module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) where
 
diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda
index 3cf1e2848a..085a34b13f 100644
--- a/src/Algebra/Definitions.agda
+++ b/src/Algebra/Definitions.agda
@@ -26,7 +26,7 @@ open import Algebra.Core using (Op₁; Op₂)
 open import Data.Product.Base using (_×_; ∃-syntax)
 open import Data.Sum.Base using (_⊎_)
 open import Relation.Nullary.Negation.Core using (¬_)
-open import Relation.Unary using (Pred)
+open import Relation.Unary using (Pred; ∁)
 
 ------------------------------------------------------------------------
 -- Properties of operations
@@ -156,18 +156,22 @@ RightCancellative _•_ = ∀ x → RightCancellativeAt x _•_
 Cancellative : Op₂ A → Set _
 Cancellative _•_ = (LeftCancellative _•_) × (RightCancellative _•_)
 
-_-AlmostLeftCancellative_ Except_-LeftCancellative_ : ∀ {p} (P : Pred A p) →
-                                                      Op₂ A → Set _
-P -AlmostLeftCancellative _•_ = ∀ x → P x ⊎ LeftCancellativeAt x _•_
-Except P -LeftCancellative _•_ = ∀ {x} → ¬ (P x) → LeftCancellativeAt x _•_
+_-AlmostLeftCancellative_ Provided_-LeftCancellative_
+  Except_-LeftCancellative_ : ∀ {p} (P : Pred A p) → Op₂ A → Set _
+
+P -AlmostLeftCancellative _•_    = ∀ x → P x ⊎ LeftCancellativeAt x _•_
+Provided P -LeftCancellative _•_ = ∀ x → .{{P x}} → LeftCancellativeAt x _•_
+Except_-LeftCancellative_ P      = Provided (∁ P) -LeftCancellative_
 
 AlmostLeftCancellative : A → Op₂ A → Set _
 AlmostLeftCancellative e = (_≈ e) -AlmostLeftCancellative_
 
-_-AlmostRightCancellative_ Except_-RightCancellative_ : ∀ {p} (P : Pred A p) →
-                                                         Op₂ A → Set _
-P -AlmostRightCancellative _•_ = ∀ x → P x ⊎ RightCancellativeAt x _•_
-Except P -RightCancellative _•_ = ∀ {x} → ¬ (P x) → RightCancellativeAt x _•_
+_-AlmostRightCancellative_ Provided_-RightCancellative_
+  Except_-RightCancellative_ : ∀ {p} (P : Pred A p) → Op₂ A → Set _
+
+P -AlmostRightCancellative _•_    = ∀ x → P x ⊎ RightCancellativeAt x _•_
+Provided P -RightCancellative _•_ = ∀ x → .{{P x}} → RightCancellativeAt x _•_
+Except_-RightCancellative_ P      = Provided (∁ P) -RightCancellative_
 
 AlmostRightCancellative : A → Op₂ A → Set _
 AlmostRightCancellative e = (_≈ e) -AlmostRightCancellative_

From 8eea4566a267c5f41e50266fdeaefd0f577ec0c8 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 10 Feb 2025 05:15:10 +0000
Subject: [PATCH 19/39] refactor: knock-on

---
 src/Data/Nat/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 76b6b7fb0b..69f62ad891 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -919,7 +919,7 @@ m+n≮m m n = subst (_≮ m) (+-comm n m) (m+n≮n n m)
   lemma (suc m) (suc n) eq = cong suc (lemma m n (+-cancelˡ-≡ o (m * o) (n * o) eq))
 
 *-cancelʳ-≡ : ∀ m n o .{{_ : NonZero o}} → m * o ≡ n * o → m ≡ n
-*-cancelʳ-≡ m n o = almost⇒exceptʳ _ _ *-almostCancelʳ-≡ (≢-nonZero⁻¹ _) m n
+*-cancelʳ-≡ m n o = almost⇒exceptʳ _ *-almostCancelʳ-≡ o {{≢-nonZero⁻¹ o}} m n
 
 *-cancelˡ-≡ : ∀ m n o .{{_ : NonZero o}} → o * m ≡ o * n → m ≡ n
 *-cancelˡ-≡ m n o rewrite *-comm o m | *-comm o n = *-cancelʳ-≡ m n o

From 30299f1fc3d56591a3e1c7a14f030f4d8900c7b3 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 10 Feb 2025 06:27:49 +0000
Subject: [PATCH 20/39] refactor: use `Data.Sum.Base` operations instead of
 `with`

---
 .../CancellativeCommutativeSemiring.agda      | 21 ++++++++-----------
 1 file changed, 9 insertions(+), 12 deletions(-)

diff --git a/src/Algebra/Properties/CancellativeCommutativeSemiring.agda b/src/Algebra/Properties/CancellativeCommutativeSemiring.agda
index a9702fcbf5..edc277ceb3 100644
--- a/src/Algebra/Properties/CancellativeCommutativeSemiring.agda
+++ b/src/Algebra/Properties/CancellativeCommutativeSemiring.agda
@@ -7,29 +7,26 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra using (CancellativeCommutativeSemiring)
-open import Algebra.Definitions using (AlmostRightCancellative)
-open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
-open import Relation.Binary.Definitions using (Decidable)
-open import Relation.Nullary.Decidable using (yes; no)
-open import Relation.Nullary.Negation using (contradiction)
 
 module Algebra.Properties.CancellativeCommutativeSemiring
   {a ℓ} (R : CancellativeCommutativeSemiring a ℓ)
   where
 
+open import Algebra.Definitions using (AlmostRightCancellative)
+open import Data.Sum.Base using (_⊎_; [_,_]′; map₂)
+open import Relation.Binary.Definitions using (Decidable)
+
 open CancellativeCommutativeSemiring R
 open import Algebra.Consequences.Setoid setoid
 open import Relation.Binary.Reasoning.Setoid setoid
 
 *-almostCancelʳ : AlmostRightCancellative _≈_ 0# _*_
-*-almostCancelʳ = comm+almostCancelˡ⇒almostCancelʳ *-comm *-cancelˡ-nonZero
+*-almostCancelʳ = comm∧almostCancelˡ⇒almostCancelʳ *-comm *-cancelˡ-nonZero
 
 xy≈0⇒x≈0∨y≈0 : Decidable _≈_ → ∀ {x y} → x * y ≈ 0# → x ≈ 0# ⊎ y ≈ 0#
-xy≈0⇒x≈0∨y≈0 _≟_ {x} {y} xy≈0 with *-cancelˡ-nonZero x
-... | inj₁ x≈0     = inj₁ x≈0
-... | inj₂ cancelˡ = inj₂ (cancelˡ y 0# (trans xy≈0 (sym (zeroʳ x))))
+xy≈0⇒x≈0∨y≈0 _≟_ {x} {y} xy≈0 =
+  map₂ (λ cancel → cancel y 0# (trans xy≈0 (sym (zeroʳ x)))) (*-cancelˡ-nonZero x)
 
 x≉0∧y≉0⇒xy≉0 : Decidable _≈_ → ∀ {x y} → x ≉ 0# → y ≉ 0# → x * y ≉ 0#
-x≉0∧y≉0⇒xy≉0 _≟_ x≉0 y≉0 xy≈0 with xy≈0⇒x≈0∨y≈0 _≟_ xy≈0
-... | inj₁ x≈0 = x≉0 x≈0
-... | inj₂ y≈0 = y≉0 y≈0
+x≉0∧y≉0⇒xy≉0 _≟_ x≉0 y≉0 xy≈0 = [ x≉0 , y≉0 ]′ (xy≈0⇒x≈0∨y≈0 _≟_ xy≈0)
+

From 1fbd51a1c701000a870583bbe963259f9edbd0fd Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 10 Feb 2025 06:37:06 +0000
Subject: [PATCH 21/39] fix: take these edits to a separate PR

---
 src/Algebra/Properties/Semiring/Primality.agda | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/src/Algebra/Properties/Semiring/Primality.agda b/src/Algebra/Properties/Semiring/Primality.agda
index dd8f821134..fc2d1c36c9 100644
--- a/src/Algebra/Properties/Semiring/Primality.agda
+++ b/src/Algebra/Properties/Semiring/Primality.agda
@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Properties of Coprimality and Irreducibility for Semiring.
+-- Some theory for CancellativeCommutativeSemiring.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
@@ -11,15 +11,12 @@ open import Data.Sum.Base using (reduce)
 open import Function.Base using (flip)
 open import Relation.Binary.Definitions using (Symmetric)
 
-module Algebra.Properties.Semiring.Primality
+module Algebra.Properties.Semiring.PrimalityMASTER
   {a ℓ} (R : Semiring a ℓ)
   where
 
-open Semiring R
-  using (_≉_; sym; trans; 0#; 1#; zeroˡ; rawSemiring)
-  renaming (Carrier to A)
+open Semiring R renaming (Carrier to A)
 open import Algebra.Properties.Semiring.Divisibility R
-  using (_∣_; ∣-trans; 0∤1)
 
 ------------------------------------------------------------------------
 -- Re-export primality definitions

From d6a461b35768da5932a6da3810da065d0161db37 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 10 Feb 2025 06:38:15 +0000
Subject: [PATCH 22/39] fix: take these edits to a separate PR

---
 src/Algebra/Properties/Semiring/Primality.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Algebra/Properties/Semiring/Primality.agda b/src/Algebra/Properties/Semiring/Primality.agda
index fc2d1c36c9..210d9fb1a0 100644
--- a/src/Algebra/Properties/Semiring/Primality.agda
+++ b/src/Algebra/Properties/Semiring/Primality.agda
@@ -11,7 +11,7 @@ open import Data.Sum.Base using (reduce)
 open import Function.Base using (flip)
 open import Relation.Binary.Definitions using (Symmetric)
 
-module Algebra.Properties.Semiring.PrimalityMASTER
+module Algebra.Properties.Semiring.Primality
   {a ℓ} (R : Semiring a ℓ)
   where
 

From c2e14ef2a6e3a5f5322e9c97c96c4edcfd22d687 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 10 Feb 2025 19:19:34 +0000
Subject: [PATCH 23/39] refactor: change order of parametrisation

---
 src/Algebra/Consequences/Base.agda | 12 ++++++------
 src/Algebra/Definitions.agda       |  4 ++--
 src/Data/Nat/Properties.agda       |  2 +-
 3 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/src/Algebra/Consequences/Base.agda b/src/Algebra/Consequences/Base.agda
index 18f1a45cc4..8bb6f49fc8 100644
--- a/src/Algebra/Consequences/Base.agda
+++ b/src/Algebra/Consequences/Base.agda
@@ -32,13 +32,13 @@ module _ {p ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ)
 
   almost⇒exceptˡ : _-AlmostLeftCancellative_ _≈_ P _•_ →
                    Except_-LeftCancellative_ _≈_ P _•_
-  almost⇒exceptˡ cancel x {{¬px}} =
-    [ flip contradiction (¬-recompute ¬px) , id ]′ (cancel x)
+  almost⇒exceptˡ cancel x y z {{¬px}} =
+    [ flip contradiction (¬-recompute ¬px) , (λ cancel → cancel y z) ]′ (cancel x)
 
   almost⇒exceptʳ : _-AlmostRightCancellative_ _≈_ P _•_ →
                    Except_-RightCancellative_ _≈_ P _•_
-  almost⇒exceptʳ cancel x {{¬px}} =
-    [ flip contradiction (¬-recompute ¬px) , id ]′ (cancel x)
+  almost⇒exceptʳ cancel x y z {{¬px}} =
+    [ flip contradiction (¬-recompute ¬px) , (λ cancel → cancel y z) ]′ (cancel x)
 
 module _ {p ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ)
          {P : Pred A p} (dec : Decidable P) where
@@ -47,13 +47,13 @@ module _ {p ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ)
                    _-AlmostLeftCancellative_ _≈_ P _•_
   except⇒almostˡ cancel x with dec x
   ... | yes px = inj₁ px
-  ... | no ¬px = inj₂ (cancel x {{¬px}})
+  ... | no ¬px = inj₂ (λ y z → cancel x y z {{¬px}})
 
   except⇒almostʳ : Except_-RightCancellative_ _≈_ P _•_ →
                    _-AlmostRightCancellative_ _≈_ P _•_
   except⇒almostʳ cancel x with dec x
   ... | yes px = inj₁ px
-  ... | no ¬px = inj₂ (cancel x {{¬px}})
+  ... | no ¬px = inj₂ (λ y z → cancel x y z {{¬px}})
 
 module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) where
 
diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda
index 085a34b13f..37b5106374 100644
--- a/src/Algebra/Definitions.agda
+++ b/src/Algebra/Definitions.agda
@@ -160,7 +160,7 @@ _-AlmostLeftCancellative_ Provided_-LeftCancellative_
   Except_-LeftCancellative_ : ∀ {p} (P : Pred A p) → Op₂ A → Set _
 
 P -AlmostLeftCancellative _•_    = ∀ x → P x ⊎ LeftCancellativeAt x _•_
-Provided P -LeftCancellative _•_ = ∀ x → .{{P x}} → LeftCancellativeAt x _•_
+Provided P -LeftCancellative _•_ = ∀ x y z → .{{P x}} → (x • y) ≈ (x • z) → y ≈ z
 Except_-LeftCancellative_ P      = Provided (∁ P) -LeftCancellative_
 
 AlmostLeftCancellative : A → Op₂ A → Set _
@@ -170,7 +170,7 @@ _-AlmostRightCancellative_ Provided_-RightCancellative_
   Except_-RightCancellative_ : ∀ {p} (P : Pred A p) → Op₂ A → Set _
 
 P -AlmostRightCancellative _•_    = ∀ x → P x ⊎ RightCancellativeAt x _•_
-Provided P -RightCancellative _•_ = ∀ x → .{{P x}} → RightCancellativeAt x _•_
+Provided P -RightCancellative _•_ = ∀ x y z → .{{P x}} → (y • x) ≈ (z • x) → y ≈ z
 Except_-RightCancellative_ P      = Provided (∁ P) -RightCancellative_
 
 AlmostRightCancellative : A → Op₂ A → Set _
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index aaddb7f189..9e00552dcf 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -921,7 +921,7 @@ m+n≮m m n = subst (_≮ m) (+-comm n m) (m+n≮n n m)
   lemma (suc m) (suc n) eq = cong suc (lemma m n (+-cancelˡ-≡ o (m * o) (n * o) eq))
 
 *-cancelʳ-≡ : ∀ m n o .{{_ : NonZero o}} → m * o ≡ n * o → m ≡ n
-*-cancelʳ-≡ m n o = almost⇒exceptʳ _ *-almostCancelʳ-≡ o {{≢-nonZero⁻¹ o}} m n
+*-cancelʳ-≡ m n o = almost⇒exceptʳ _ *-almostCancelʳ-≡ o m n {{≢-nonZero⁻¹ _}}
 
 *-cancelˡ-≡ : ∀ m n o .{{_ : NonZero o}} → o * m ≡ o * n → m ≡ n
 *-cancelˡ-≡ m n o rewrite *-comm o m | *-comm o n = *-cancelʳ-≡ m n o

From 6ceb7a73f6266f159de09b6317149f71a318f44e Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 10 Feb 2025 19:29:56 +0000
Subject: [PATCH 24/39] fix: `CHANGELOG`

---
 CHANGELOG.md | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index ed9073889b..892ce372cd 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -114,3 +114,8 @@ Additions to existing modules
   quasiring                       : Quasiring c ℓ → Quasiring (a ⊔ c) (a ⊔ ℓ)
   commutativeRing                 : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ)
   ```
+
+* In `Data.Nat.Properties`:
+  ```agda
+  *-almostCancelʳ-≡ : AlmostRightCancellative 0 _*_
+  ```

From 44ba20cc0c7fb48e50bc9097402503ad8d60b518 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 11 Feb 2025 01:53:37 +0000
Subject: [PATCH 25/39] refactor: `import`s

---
 src/Algebra/Consequences/Base.agda | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/Algebra/Consequences/Base.agda b/src/Algebra/Consequences/Base.agda
index 8bb6f49fc8..cab896cb6a 100644
--- a/src/Algebra/Consequences/Base.agda
+++ b/src/Algebra/Consequences/Base.agda
@@ -10,11 +10,11 @@
 module Algebra.Consequences.Base
   {a} {A : Set a} where
 
-open import Algebra.Core
+open import Algebra.Core using (Op₁; Op₂)
 open import Algebra.Definitions
-open import Data.Sum.Base
+open import Data.Sum.Base using (inj₁; inj₂; reduce; [_,_]′)
 open import Function.Base using (id; const; flip)
-open import Relation.Binary.Core
+open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions using (Reflexive)
 open import Relation.Nullary.Decidable.Core using (yes; no)
 open import Relation.Nullary.Negation.Core using (contradiction)
@@ -53,7 +53,7 @@ module _ {p ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ)
                    _-AlmostRightCancellative_ _≈_ P _•_
   except⇒almostʳ cancel x with dec x
   ... | yes px = inj₁ px
-  ... | no ¬px = inj₂ (λ y z → cancel x y z {{¬px}})
+  ... | no ¬px = inj₂ λ y z → cancel x y z {{¬px}}
 
 module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) where
 
@@ -62,6 +62,7 @@ module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) where
                                      Involutive _≈_ f
   reflexive∧selfInverse⇒involutive refl inv _ = inv refl
 
+
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
 ------------------------------------------------------------------------

From 770b223410e3e1bc2d5705efadb031c4e375cec2 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 11 Feb 2025 01:55:17 +0000
Subject: [PATCH 26/39] =?UTF-8?q?refactor:=20streamline,=20using=20`Data.S?=
 =?UTF-8?q?um.Base.map=E2=82=82`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Algebra/Consequences/Setoid.agda | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda
index 6414978b93..108dc7d6a5 100644
--- a/src/Algebra/Consequences/Setoid.agda
+++ b/src/Algebra/Consequences/Setoid.agda
@@ -17,7 +17,7 @@ module Algebra.Consequences.Setoid {a ℓ} (S : Setoid a ℓ) where
 open Setoid S renaming (Carrier to A)
 open import Algebra.Core
 open import Algebra.Definitions _≈_
-open import Data.Sum.Base using (inj₁; inj₂; [_,_])
+open import Data.Sum.Base using (map₂)
 open import Data.Product.Base using (_,_)
 open import Function.Base using (_$_; id; _∘_)
 open import Function.Definitions
@@ -165,13 +165,13 @@ module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) {e : A} where
 
   comm∧almostCancelˡ⇒almostCancelʳ : AlmostLeftCancellative e _∙_ →
                                      AlmostRightCancellative e _∙_
-  comm∧almostCancelˡ⇒almostCancelʳ almostCancel =
-    [ inj₁ , inj₂ ∘ comm∧cancelAtˡ⇒cancelAtʳ comm ] ∘ almostCancel
+  comm∧almostCancelˡ⇒almostCancelʳ cancel =
+    map₂ (comm∧cancelAtˡ⇒cancelAtʳ comm) ∘ cancel
 
   comm∧almostCancelʳ⇒almostCancelˡ : AlmostRightCancellative e _∙_ →
                                      AlmostLeftCancellative e _∙_
-  comm∧almostCancelʳ⇒almostCancelˡ almostCancel  =
-    [ inj₁ , inj₂ ∘ comm∧cancelAtʳ⇒cancelAtˡ comm ] ∘ almostCancel
+  comm∧almostCancelʳ⇒almostCancelˡ cancel  =
+    map₂ (comm∧cancelAtʳ⇒cancelAtˡ comm) ∘ cancel
 
 ------------------------------------------------------------------------
 -- Group-like structures

From 0747e48457d2aa446b0e0059602f62c0f1000642 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 11 Feb 2025 02:16:45 +0000
Subject: [PATCH 27/39] refactor: streamline; deprecate already exported
 definition

---
 .../CancellativeCommutativeSemiring.agda      | 37 ++++++++++++++-----
 1 file changed, 27 insertions(+), 10 deletions(-)

diff --git a/src/Algebra/Properties/CancellativeCommutativeSemiring.agda b/src/Algebra/Properties/CancellativeCommutativeSemiring.agda
index edc277ceb3..81433cd28b 100644
--- a/src/Algebra/Properties/CancellativeCommutativeSemiring.agda
+++ b/src/Algebra/Properties/CancellativeCommutativeSemiring.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra using (CancellativeCommutativeSemiring)
+open import Algebra.Bundles using (CancellativeCommutativeSemiring)
 
 module Algebra.Properties.CancellativeCommutativeSemiring
   {a ℓ} (R : CancellativeCommutativeSemiring a ℓ)
@@ -16,17 +16,34 @@ open import Algebra.Definitions using (AlmostRightCancellative)
 open import Data.Sum.Base using (_⊎_; [_,_]′; map₂)
 open import Relation.Binary.Definitions using (Decidable)
 
-open CancellativeCommutativeSemiring R
+open CancellativeCommutativeSemiring R renaming (Carrier to A)
 open import Algebra.Consequences.Setoid setoid
-open import Relation.Binary.Reasoning.Setoid setoid
 
-*-almostCancelʳ : AlmostRightCancellative _≈_ 0# _*_
-*-almostCancelʳ = comm∧almostCancelˡ⇒almostCancelʳ *-comm *-cancelˡ-nonZero
+private
+  variable
+    x y : A
 
-xy≈0⇒x≈0∨y≈0 : Decidable _≈_ → ∀ {x y} → x * y ≈ 0# → x ≈ 0# ⊎ y ≈ 0#
-xy≈0⇒x≈0∨y≈0 _≟_ {x} {y} xy≈0 =
-  map₂ (λ cancel → cancel y 0# (trans xy≈0 (sym (zeroʳ x)))) (*-cancelˡ-nonZero x)
 
-x≉0∧y≉0⇒xy≉0 : Decidable _≈_ → ∀ {x y} → x ≉ 0# → y ≉ 0# → x * y ≉ 0#
-x≉0∧y≉0⇒xy≉0 _≟_ x≉0 y≉0 xy≈0 = [ x≉0 , y≉0 ]′ (xy≈0⇒x≈0∨y≈0 _≟_ xy≈0)
+module _ (_≟_ : Decidable _≈_) where
 
+  xy≈0⇒x≈0∨y≈0 : x * y ≈ 0# → x ≈ 0# ⊎ y ≈ 0#
+  xy≈0⇒x≈0∨y≈0 {x} {y} xy≈0 =
+    map₂ (λ cancel → cancel _ _ (trans xy≈0 (sym (zeroʳ x)))) (*-cancelˡ-nonZero x)
+
+  x≉0∧y≉0⇒xy≉0 : x ≉ 0# → y ≉ 0# → x * y ≉ 0#
+  x≉0∧y≉0⇒xy≉0 x≉0 y≉0 xy≈0 = [ x≉0 , y≉0 ]′ (xy≈0⇒x≈0∨y≈0 xy≈0)
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.3
+
+*-almostCancelʳ = *-cancelʳ-nonZero
+{-# WARNING_ON_USAGE *-almostCancelʳ
+"Warning: *-almostCancelʳ was deprecated in v2.3.
+Please use Algebra.Structures.IsCancellativeCommutativeSemiring.*-cancelʳ-nonZero instead."
+#-}

From e12eeb5b61c57fb999d36f1eab29c1d60e89f1e3 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 11 Feb 2025 02:22:33 +0000
Subject: [PATCH 28/39] refactor: remove one more `import`

---
 src/Algebra/Properties/CancellativeCommutativeSemiring.agda | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/Algebra/Properties/CancellativeCommutativeSemiring.agda b/src/Algebra/Properties/CancellativeCommutativeSemiring.agda
index 81433cd28b..0a4dda8fdd 100644
--- a/src/Algebra/Properties/CancellativeCommutativeSemiring.agda
+++ b/src/Algebra/Properties/CancellativeCommutativeSemiring.agda
@@ -12,12 +12,10 @@ module Algebra.Properties.CancellativeCommutativeSemiring
   {a ℓ} (R : CancellativeCommutativeSemiring a ℓ)
   where
 
-open import Algebra.Definitions using (AlmostRightCancellative)
 open import Data.Sum.Base using (_⊎_; [_,_]′; map₂)
 open import Relation.Binary.Definitions using (Decidable)
 
 open CancellativeCommutativeSemiring R renaming (Carrier to A)
-open import Algebra.Consequences.Setoid setoid
 
 private
   variable

From e5c47f33ebd0e29e693688a172293782ea1ae03e Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 11 Feb 2025 04:31:15 +0000
Subject: [PATCH 29/39] refactor: remove one more `import`

---
 src/Algebra/Definitions.agda | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda
index 37b5106374..2be653788a 100644
--- a/src/Algebra/Definitions.agda
+++ b/src/Algebra/Definitions.agda
@@ -25,7 +25,6 @@ module Algebra.Definitions
 open import Algebra.Core using (Op₁; Op₂)
 open import Data.Product.Base using (_×_; ∃-syntax)
 open import Data.Sum.Base using (_⊎_)
-open import Relation.Nullary.Negation.Core using (¬_)
 open import Relation.Unary using (Pred; ∁)
 
 ------------------------------------------------------------------------

From ad0f4b77e423c93bd94b3b7b739837cb2a81c95b Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 11 Feb 2025 04:31:54 +0000
Subject: [PATCH 30/39] fix: add missing deprecation

---
 CHANGELOG.md | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 892ce372cd..2f6c48ded5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -40,6 +40,11 @@ Deprecated names
   *ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc   ↦  *ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc
   ```
 
+* In `Algebra.Properties.CancellativeCommutativeSemiring`:
+  ```agda
+  *-almostCancelʳ  ↦  Algebra.Structures.IsCancellativeCommutativeSemiring.*-cancelʳ-nonZero
+  ```
+
 * In `Algebra.Properties.Magma.Divisibility`:
   ```agda
   ∣∣-sym       ↦  ∥-sym

From 80a9aeac59fe8ed128b274d9bddf7a378182cdc9 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 27 Feb 2025 09:25:12 +0000
Subject: [PATCH 31/39] fix: explicit `import` policy returns to bite!

---
 src/Algebra/Consequences/Base.agda | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/Algebra/Consequences/Base.agda b/src/Algebra/Consequences/Base.agda
index cc37978aab..7dff568d8c 100644
--- a/src/Algebra/Consequences/Base.agda
+++ b/src/Algebra/Consequences/Base.agda
@@ -12,7 +12,9 @@ module Algebra.Consequences.Base
 
 open import Algebra.Core using (Op₁; Op₂)
 open import Algebra.Definitions
-  using (Selective; Idempotent; SelfInverse; Involutive)
+  using (Selective; Idempotent; SelfInverse; Involutive
+        ; _-AlmostLeftCancellative_; Except_-LeftCancellative_
+        ; _-AlmostRightCancellative_; Except_-RightCancellative_)
 open import Data.Sum.Base using (inj₁; inj₂; reduce; [_,_]′)
 open import Function.Base using (id; const; flip)
 open import Relation.Binary.Core using (Rel)

From e27d1cb9da4a5d0bdc23a87ce5672768aac7b8e1 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 24 Mar 2025 10:19:17 +0000
Subject: [PATCH 32/39] fix: reverted change

---
 doc/README.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/README.agda b/doc/README.agda
index d2bd0b9caa..78ad1cbbee 100644
--- a/doc/README.agda
+++ b/doc/README.agda
@@ -3,7 +3,7 @@
 module README where
 
 ------------------------------------------------------------------------
--- The Agda standard library, version 3.0-dev
+-- The Agda standard library, version 2.3-dev
 --
 -- Authors: Nils Anders Danielsson, Matthew Daggitt, Guillaume Allais
 -- with contributions from Andreas Abel, Stevan Andjelkovic,

From c1cf532356494d5515074e9c0bc2deb8640a7749 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 27 Mar 2025 13:52:28 +0000
Subject: [PATCH 33/39] fix: imports

---
 src/Data/Rational/Properties.agda              |  3 +--
 src/Data/Rational/Unnormalised/Properties.agda | 12 ++++++------
 2 files changed, 7 insertions(+), 8 deletions(-)

diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index b53ec38f06..b045d3d827 100644
--- a/src/Data/Rational/Properties.agda
+++ b/src/Data/Rational/Properties.agda
@@ -67,7 +67,6 @@ open import Relation.Nullary.Decidable.Core as Dec
   using (yes; no; recompute; map′; _×-dec_)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 
-open import Algebra.Consequences.Propositional {A = ℚ}
 open import Algebra.Definitions {A = ℚ} _≡_
 open import Algebra.Structures  {A = ℚ} _≡_
 
@@ -352,7 +351,7 @@ normalize-injective-≃ m n c d eq = ℕ./-cancelʳ-≡
     gcd[m,c]*gcd[n,d]≢0 = ℕ.m*n≢0 gcd[m,c] gcd[n,d]
     gcd[n,d]*gcd[m,c]≢0 = ℕ.m*n≢0 gcd[n,d] gcd[m,c]
 
-  div = mkℚ+-injective eq
+  div = {!mkℚ+-injective eq!}
   m/gcd[m,c]≡n/gcd[n,d] = proj₁ div
   c/gcd[m,c]≡d/gcd[n,d] = proj₂ div
 
diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda
index 31f90b05c6..0bbda20f8f 100644
--- a/src/Data/Rational/Unnormalised/Properties.agda
+++ b/src/Data/Rational/Unnormalised/Properties.agda
@@ -11,16 +11,16 @@ module Data.Rational.Unnormalised.Properties where
 
 open import Algebra.Definitions
 open import Algebra.Structures
-  using (IsMagma; IsSemigroup; IsBand; IsSelectiveMagma; IsMonoid
-        ; IsCommutativeMonoid; IsGroup; IsAbelianGroup; IsRing
-        ; IsCommutativeRing)
+  using (IsMagma; IsSemigroup; IsBand; IsSelectiveMagma
+        ; IsMonoid; IsCommutativeMonoid; IsGroup; IsAbelianGroup
+        ; IsRing; IsCommutativeRing)
 open import Algebra.Bundles
 open import Algebra.Apartness
   using (IsHeytingCommutativeRing; IsHeytingField
         ; HeytingCommutativeRing; HeytingField)
 open import Algebra.Lattice
-  using (IsLattice; IsDistributiveLattice; IsSemilattice
-        ; Semilattice; Lattice; DistributiveLattice; RawLattice)
+  using (IsSemilattice; IsLattice; IsDistributiveLattice
+        ; RawLattice; Semilattice; Lattice; DistributiveLattice)
 import Algebra.Consequences.Setoid as Consequences
 open import Algebra.Construct.NaturalChoice.Base
   using (MaxOperator; MinOperator)
@@ -764,7 +764,7 @@ neg⇒nonZero (mkℚᵘ (-[1+ _ ]) _) = _
 +-identityˡ p = ≃-reflexive (+-identityˡ-≡ p)
 
 +-identityʳ-≡ : RightIdentity _≡_ 0ℚᵘ _+_
-+-identityʳ-≡ = comm∧idˡ⇒idʳ +-comm-≡ {e = 0ℚᵘ} +-identityˡ-≡
++-identityʳ-≡ = comm∧idˡ⇒idʳ +-comm-≡ +-identityˡ-≡
 
 +-identityʳ : RightIdentity _≃_ 0ℚᵘ _+_
 +-identityʳ p = ≃-reflexive (+-identityʳ-≡ p)

From 011340341b92d817e8ba2730a08d318ba9b92797 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 27 Mar 2025 13:53:07 +0000
Subject: [PATCH 34/39] fix: names and `CHANGELOG`

---
 CHANGELOG.md                 | 18 ++++++++++++++++++
 src/Algebra/Definitions.agda | 26 ++++++++++++++------------
 2 files changed, 32 insertions(+), 12 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 51ce4e79e4..d7f5521f34 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -25,6 +25,12 @@ Non-backwards compatible changes
   significantly faster. However, its reduction behaviour on open terms may have
   changed.
 
+* The definitions of `LeftCancellative`/`RightCancellative` in `Algebra.Definitions`
+  have been altered to make the quantification for each argument explicit. The
+  definitions of `AlmostLeftCancellative`/`AlmostRightCancellative` have also been
+  changed to rephrase them in 'positive' logical terms. These definitions have been
+  propagated through the numeric types `X` in `Data.X.Properties`.
+
 Minor improvements
 ------------------
 
@@ -166,6 +172,18 @@ Additions to existing modules
   commutativeRing                 : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ)
   ```
 
+* In `Algebra.Definitions`:
+  ```agda
+  LeftCancellativeAt           : A → Op₂ A → Set _
+  RightCancellativeAt          : A → Op₂ A → Set _
+  _AlmostLeftCancellative′_    : (P : Pred A p) → Op₂ A → Set _
+  Provided_LeftCancellative_   : (P : Pred A p) → Op₂ A → Set _
+  Except_LeftCancellative_     : (P : Pred A p) → Op₂ A → Set _
+  _AlmostRightCancellative′_   : (P : Pred A p) → Op₂ A → Set _
+  Provided_RightCancellative_  : (P : Pred A p) → Op₂ A → Set _
+  Except_RightCancellative_    : (P : Pred A p) → Op₂ A → Set _
+  ```
+
 * In `Algebra.Properties.Magma.Divisibility`:
   ```agda
   ∣ˡ-respʳ-≈  : _∣ˡ_ Respectsʳ _≈_
diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda
index 2be653788a..4ba97341e8 100644
--- a/src/Algebra/Definitions.agda
+++ b/src/Algebra/Definitions.agda
@@ -155,25 +155,27 @@ RightCancellative _•_ = ∀ x → RightCancellativeAt x _•_
 Cancellative : Op₂ A → Set _
 Cancellative _•_ = (LeftCancellative _•_) × (RightCancellative _•_)
 
-_-AlmostLeftCancellative_ Provided_-LeftCancellative_
-  Except_-LeftCancellative_ : ∀ {p} (P : Pred A p) → Op₂ A → Set _
+_AlmostLeftCancellative′_    : ∀ {p} (P : Pred A p) → Op₂ A → Set _
+Provided_LeftCancellative_  : ∀ {p} (P : Pred A p) → Op₂ A → Set _
+Except_LeftCancellative_    : ∀ {p} (P : Pred A p) → Op₂ A → Set _
 
-P -AlmostLeftCancellative _•_    = ∀ x → P x ⊎ LeftCancellativeAt x _•_
-Provided P -LeftCancellative _•_ = ∀ x y z → .{{P x}} → (x • y) ≈ (x • z) → y ≈ z
-Except_-LeftCancellative_ P      = Provided (∁ P) -LeftCancellative_
+P AlmostLeftCancellative′ _•_   = ∀ x → P x ⊎ LeftCancellativeAt x _•_
+Provided P LeftCancellative _•_ = ∀ x y z → .{{P x}} → (x • y) ≈ (x • z) → y ≈ z
+Except P LeftCancellative _•_   = Provided (∁ P) LeftCancellative _•_
 
 AlmostLeftCancellative : A → Op₂ A → Set _
-AlmostLeftCancellative e = (_≈ e) -AlmostLeftCancellative_
+AlmostLeftCancellative e = (_≈ e) AlmostLeftCancellative′_
 
-_-AlmostRightCancellative_ Provided_-RightCancellative_
-  Except_-RightCancellative_ : ∀ {p} (P : Pred A p) → Op₂ A → Set _
+_AlmostRightCancellative′_  : ∀ {p} (P : Pred A p) → Op₂ A → Set _
+Provided_RightCancellative_ : ∀ {p} (P : Pred A p) → Op₂ A → Set _
+Except_RightCancellative_   : ∀ {p} (P : Pred A p) → Op₂ A → Set _
 
-P -AlmostRightCancellative _•_    = ∀ x → P x ⊎ RightCancellativeAt x _•_
-Provided P -RightCancellative _•_ = ∀ x y z → .{{P x}} → (y • x) ≈ (z • x) → y ≈ z
-Except_-RightCancellative_ P      = Provided (∁ P) -RightCancellative_
+P AlmostRightCancellative′ _•_    = ∀ x → P x ⊎ RightCancellativeAt x _•_
+Provided P RightCancellative _•_ = ∀ x y z → .{{P x}} → (y • x) ≈ (z • x) → y ≈ z
+Except_RightCancellative_ P      = Provided (∁ P) RightCancellative_
 
 AlmostRightCancellative : A → Op₂ A → Set _
-AlmostRightCancellative e = (_≈ e) -AlmostRightCancellative_
+AlmostRightCancellative e = (_≈ e) AlmostRightCancellative′_
 
 AlmostCancellative : A → Op₂ A → Set _
 AlmostCancellative e _•_ = AlmostLeftCancellative e _•_ × AlmostRightCancellative e _•_

From 6ad84adf7c98fed84ce906bec54f12380b8b2849 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 27 Mar 2025 13:56:47 +0000
Subject: [PATCH 35/39] fix: names

---
 src/Algebra/Consequences/Base.agda | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/Algebra/Consequences/Base.agda b/src/Algebra/Consequences/Base.agda
index 7dff568d8c..4953781a6a 100644
--- a/src/Algebra/Consequences/Base.agda
+++ b/src/Algebra/Consequences/Base.agda
@@ -13,8 +13,8 @@ module Algebra.Consequences.Base
 open import Algebra.Core using (Op₁; Op₂)
 open import Algebra.Definitions
   using (Selective; Idempotent; SelfInverse; Involutive
-        ; _-AlmostLeftCancellative_; Except_-LeftCancellative_
-        ; _-AlmostRightCancellative_; Except_-RightCancellative_)
+        ; _AlmostLeftCancellative′_; Except_LeftCancellative_
+        ; _AlmostRightCancellative′_; Except_RightCancellative_)
 open import Data.Sum.Base using (inj₁; inj₂; reduce; [_,_]′)
 open import Function.Base using (id; const; flip)
 open import Relation.Binary.Core using (Rel)
@@ -33,27 +33,27 @@ module _ {ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) where
 module _ {p ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ)
          {P : Pred A p} where
 
-  almost⇒exceptˡ : _-AlmostLeftCancellative_ _≈_ P _•_ →
-                   Except_-LeftCancellative_ _≈_ P _•_
+  almost⇒exceptˡ : _AlmostLeftCancellative′_ _≈_ P _•_ →
+                   Except_LeftCancellative_ _≈_ P _•_
   almost⇒exceptˡ cancel x y z {{¬px}} =
     [ flip contradiction (¬-recompute ¬px) , (λ cancel → cancel y z) ]′ (cancel x)
 
-  almost⇒exceptʳ : _-AlmostRightCancellative_ _≈_ P _•_ →
-                   Except_-RightCancellative_ _≈_ P _•_
+  almost⇒exceptʳ : _AlmostRightCancellative′_ _≈_ P _•_ →
+                   Except_RightCancellative_ _≈_ P _•_
   almost⇒exceptʳ cancel x y z {{¬px}} =
     [ flip contradiction (¬-recompute ¬px) , (λ cancel → cancel y z) ]′ (cancel x)
 
 module _ {p ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ)
          {P : Pred A p} (dec : Decidable P) where
 
-  except⇒almostˡ : Except_-LeftCancellative_ _≈_ P _•_ →
-                   _-AlmostLeftCancellative_ _≈_ P _•_
+  except⇒almostˡ : Except_LeftCancellative_ _≈_ P _•_ →
+                   _AlmostLeftCancellative′_ _≈_ P _•_
   except⇒almostˡ cancel x with dec x
   ... | yes px = inj₁ px
   ... | no ¬px = inj₂ (λ y z → cancel x y z {{¬px}})
 
-  except⇒almostʳ : Except_-RightCancellative_ _≈_ P _•_ →
-                   _-AlmostRightCancellative_ _≈_ P _•_
+  except⇒almostʳ : Except_RightCancellative_ _≈_ P _•_ →
+                   _AlmostRightCancellative′_ _≈_ P _•_
   except⇒almostʳ cancel x with dec x
   ... | yes px = inj₁ px
   ... | no ¬px = inj₂ λ y z → cancel x y z {{¬px}}

From 1fcf44bae16d815a49e73234d5e7c80dd1206b15 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 27 Mar 2025 14:15:04 +0000
Subject: [PATCH 36/39] add: more `CHANGELOG` entries

---
 CHANGELOG.md | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d7f5521f34..9f4f48ea13 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -137,6 +137,18 @@ New modules
 Additions to existing modules
 -----------------------------
 
+* In `Algebra.Consequences.Base`:
+  ```agda
+  almost⇒exceptˡ : _AlmostLeftCancellative′_ _≈_ P _•_ →
+                   Except_LeftCancellative_ _≈_ P _•_
+  almost⇒exceptʳ : _AlmostRightCancellative′_ _≈_ P _•_ →
+                   Except_RightCancellative_ _≈_ P _•_
+  except⇒almostˡ : Decidable P → Except_LeftCancellative_ _≈_ P _•_ →
+                   _AlmostLeftCancellative′_ _≈_ P _•_
+  except⇒almostʳ : Decidable P → Except_RightCancellative_ _≈_ P _•_ →
+                   _AlmostRightCancellative′_ _≈_ P _•_
+  ```
+
 * In `Algebra.Consequences.Setoid`:
   ```agda
   comm∧cancelAtˡ⇒cancelAtʳ : LeftCancellativeAt x _∙_ → RightCancellativeAt x _∙_

From c1f8b9a5d6f311ddc658870677087559f9f15de2 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 27 Mar 2025 14:17:22 +0000
Subject: [PATCH 37/39] fix: whitespace

---
 src/Algebra/Definitions.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda
index 4ba97341e8..43892028d9 100644
--- a/src/Algebra/Definitions.agda
+++ b/src/Algebra/Definitions.agda
@@ -155,7 +155,7 @@ RightCancellative _•_ = ∀ x → RightCancellativeAt x _•_
 Cancellative : Op₂ A → Set _
 Cancellative _•_ = (LeftCancellative _•_) × (RightCancellative _•_)
 
-_AlmostLeftCancellative′_    : ∀ {p} (P : Pred A p) → Op₂ A → Set _
+_AlmostLeftCancellative′_   : ∀ {p} (P : Pred A p) → Op₂ A → Set _
 Provided_LeftCancellative_  : ∀ {p} (P : Pred A p) → Op₂ A → Set _
 Except_LeftCancellative_    : ∀ {p} (P : Pred A p) → Op₂ A → Set _
 

From 38e4a12729bbf9d899e72e0175337366f5ae3525 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 27 Mar 2025 14:32:39 +0000
Subject: [PATCH 38/39] fix: unsaved commit

---
 src/Data/Rational/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index b045d3d827..d04293ae1f 100644
--- a/src/Data/Rational/Properties.agda
+++ b/src/Data/Rational/Properties.agda
@@ -351,7 +351,7 @@ normalize-injective-≃ m n c d eq = ℕ./-cancelʳ-≡
     gcd[m,c]*gcd[n,d]≢0 = ℕ.m*n≢0 gcd[m,c] gcd[n,d]
     gcd[n,d]*gcd[m,c]≢0 = ℕ.m*n≢0 gcd[n,d] gcd[m,c]
 
-  div = {!mkℚ+-injective eq!}
+  div = mkℚ+-injective eq
   m/gcd[m,c]≡n/gcd[n,d] = proj₁ div
   c/gcd[m,c]≡d/gcd[n,d] = proj₂ div
 

From c2d6088ba5e1a867818811d1d2539cfc67bf8cb5 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 7 Apr 2025 09:32:40 +0100
Subject: [PATCH 39/39] fix: order of declaration/definition

---
 src/Algebra/Definitions.agda | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda
index 43892028d9..d468ce943d 100644
--- a/src/Algebra/Definitions.agda
+++ b/src/Algebra/Definitions.agda
@@ -156,22 +156,25 @@ Cancellative : Op₂ A → Set _
 Cancellative _•_ = (LeftCancellative _•_) × (RightCancellative _•_)
 
 _AlmostLeftCancellative′_   : ∀ {p} (P : Pred A p) → Op₂ A → Set _
-Provided_LeftCancellative_  : ∀ {p} (P : Pred A p) → Op₂ A → Set _
-Except_LeftCancellative_    : ∀ {p} (P : Pred A p) → Op₂ A → Set _
 
 P AlmostLeftCancellative′ _•_   = ∀ x → P x ⊎ LeftCancellativeAt x _•_
+
+Provided_LeftCancellative_  : ∀ {p} (P : Pred A p) → Op₂ A → Set _
 Provided P LeftCancellative _•_ = ∀ x y z → .{{P x}} → (x • y) ≈ (x • z) → y ≈ z
+
+Except_LeftCancellative_    : ∀ {p} (P : Pred A p) → Op₂ A → Set _
 Except P LeftCancellative _•_   = Provided (∁ P) LeftCancellative _•_
 
 AlmostLeftCancellative : A → Op₂ A → Set _
 AlmostLeftCancellative e = (_≈ e) AlmostLeftCancellative′_
 
 _AlmostRightCancellative′_  : ∀ {p} (P : Pred A p) → Op₂ A → Set _
-Provided_RightCancellative_ : ∀ {p} (P : Pred A p) → Op₂ A → Set _
-Except_RightCancellative_   : ∀ {p} (P : Pred A p) → Op₂ A → Set _
-
 P AlmostRightCancellative′ _•_    = ∀ x → P x ⊎ RightCancellativeAt x _•_
+
+Provided_RightCancellative_ : ∀ {p} (P : Pred A p) → Op₂ A → Set _
 Provided P RightCancellative _•_ = ∀ x y z → .{{P x}} → (y • x) ≈ (z • x) → y ≈ z
+
+Except_RightCancellative_   : ∀ {p} (P : Pred A p) → Op₂ A → Set _
 Except_RightCancellative_ P      = Provided (∁ P) RightCancellative_
 
 AlmostRightCancellative : A → Op₂ A → Set _