From ff6f7770b848d011fb24b2a1ef6d086a06199612 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 6 Feb 2025 11:33:14 +0000
Subject: [PATCH 1/7] refactor: change top-level parameterisation, plus local
 `variable`s to fix syntax

---
 src/Algebra/Consequences/Base.agda | 35 +++++++++++++++++++-----------
 1 file changed, 22 insertions(+), 13 deletions(-)

diff --git a/src/Algebra/Consequences/Base.agda b/src/Algebra/Consequences/Base.agda
index 574ad48a16..780726f3b0 100644
--- a/src/Algebra/Consequences/Base.agda
+++ b/src/Algebra/Consequences/Base.agda
@@ -1,3 +1,4 @@
+
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
@@ -7,26 +8,34 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
+open import Relation.Binary.Core using (Rel)
+
 module Algebra.Consequences.Base
-  {a} {A : Set a} where
+  {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) where
 
-open import Algebra.Core
-open import Algebra.Definitions
-open import Data.Sum.Base
-open import Relation.Binary.Core
+open import Algebra.Core using (Op₁; Op₂)
+open import Algebra.Definitions _≈_
+open import Data.Sum.Base using (reduce)
 open import Relation.Binary.Definitions using (Reflexive)
 
-module _ {ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) where
+private
+  variable
+    f : Op₁ A
+    _∙_ : Op₂ A
+
+------------------------------------------------------------------------
+-- Selective
+
+sel⇒idem : Selective _∙_ → Idempotent _∙_
+sel⇒idem sel x = reduce (sel x x)
 
-  sel⇒idem : Selective _≈_ _•_ → Idempotent _≈_ _•_
-  sel⇒idem sel x = reduce (sel x x)
+------------------------------------------------------------------------
+-- SelfInverse
 
-module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) where
+reflexive∧selfInverse⇒involutive : Reflexive _≈_ → SelfInverse f →
+                                   Involutive f
+reflexive∧selfInverse⇒involutive refl inv _ = inv refl
 
-  reflexive∧selfInverse⇒involutive : Reflexive _≈_ →
-                                     SelfInverse _≈_ f →
-                                     Involutive _≈_ f
-  reflexive∧selfInverse⇒involutive refl inv _ = inv refl
 
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES

From b920bef97c9642477e0ac48d725796242e9c0b31 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 6 Feb 2025 11:34:17 +0000
Subject: [PATCH 2/7] refactor: propagate changes

---
 src/Algebra/Consequences/Setoid.agda | 125 +++++++++++++--------------
 1 file changed, 62 insertions(+), 63 deletions(-)

diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda
index 66e441a9e0..304bd8e004 100644
--- a/src/Algebra/Consequences/Setoid.agda
+++ b/src/Algebra/Consequences/Setoid.agda
@@ -7,10 +7,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles using (Setoid)
-open import Relation.Binary.Definitions
-  using (Substitutive; Symmetric; Total)
 
 module Algebra.Consequences.Setoid {a ℓ} (S : Setoid a ℓ) where
 
@@ -21,47 +18,55 @@ open import Data.Sum.Base using (inj₁; inj₂)
 open import Data.Product.Base using (_,_)
 open import Function.Base using (_$_; id; _∘_)
 open import Function.Definitions
-import Relation.Binary.Consequences as Bin
+import Relation.Binary.Consequences as BinaryConsequences
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Definitions
+  using (Substitutive; Symmetric; Total)
 open import Relation.Binary.Reasoning.Setoid S
 open import Relation.Unary using (Pred)
 
+private
+  variable
+    e 0# : A
+    f _⁻¹ : Op₁ A
+    _∙_ _◦_ _+_ _*_ : Op₂ A
+
 ------------------------------------------------------------------------
 -- Re-exports
 
 -- Export base lemmas that don't require the setoid
 
-open import Algebra.Consequences.Base public
+open import Algebra.Consequences.Base _≈_ public
 
 ------------------------------------------------------------------------
 -- MiddleFourExchange
 
-module _ {_∙_ : Op₂ A} (cong : Congruent₂ _∙_) where
+module _ (cong : Congruent₂ _∙_) where
 
   comm∧assoc⇒middleFour : Commutative _∙_ → Associative _∙_ →
                           _∙_ MiddleFourExchange _∙_
   comm∧assoc⇒middleFour comm assoc w x y z = begin
     (w ∙ x) ∙ (y ∙ z) ≈⟨ assoc w x (y ∙ z) ⟩
-    w ∙ (x ∙ (y ∙ z)) ≈⟨ cong refl (sym (assoc x y z)) ⟩
+    w ∙ (x ∙ (y ∙ z)) ≈⟨ cong refl (assoc x y z) ⟨
     w ∙ ((x ∙ y) ∙ z) ≈⟨ cong refl (cong (comm x y) refl) ⟩
     w ∙ ((y ∙ x) ∙ z) ≈⟨ cong refl (assoc y x z) ⟩
-    w ∙ (y ∙ (x ∙ z)) ≈⟨ sym (assoc w y (x ∙ z)) ⟩
+    w ∙ (y ∙ (x ∙ z)) ≈⟨ assoc w y (x ∙ z) ⟨
     (w ∙ y) ∙ (x ∙ z) ∎
 
-  identity∧middleFour⇒assoc : {e : A} → Identity e _∙_ →
-                              _∙_ MiddleFourExchange _∙_ →
+  identity∧middleFour⇒assoc : Identity e _∙_ → _∙_ MiddleFourExchange _∙_ →
                               Associative _∙_
-  identity∧middleFour⇒assoc {e} (identityˡ , identityʳ) middleFour x y z = begin
-    (x ∙ y) ∙ z       ≈⟨ cong refl (sym (identityˡ z)) ⟩
+  identity∧middleFour⇒assoc {e = e} (identityˡ , identityʳ) middleFour x y z
+    = begin
+    (x ∙ y) ∙ z       ≈⟨ cong refl (identityˡ z) ⟨
     (x ∙ y) ∙ (e ∙ z) ≈⟨ middleFour x y e z ⟩
     (x ∙ e) ∙ (y ∙ z) ≈⟨ cong (identityʳ x) refl ⟩
     x ∙ (y ∙ z)       ∎
 
-  identity∧middleFour⇒comm : {_+_ : Op₂ A} {e : A} → Identity e _+_ →
-                             _∙_ MiddleFourExchange _+_ →
+  identity∧middleFour⇒comm : Identity e _+_ → _∙_ MiddleFourExchange _+_ →
                              Commutative _∙_
-  identity∧middleFour⇒comm {_+_} {e} (identityˡ , identityʳ) middleFour x y
+  identity∧middleFour⇒comm {e = e} {_+_ = _+_} (identityˡ , identityʳ) middleFour x y
     = begin
-    x ∙ y             ≈⟨ sym (cong (identityˡ x) (identityʳ y)) ⟩
+    x ∙ y             ≈⟨ cong (identityˡ x) (identityʳ y) ⟨
     (e + x) ∙ (y + e) ≈⟨ middleFour e x y e ⟩
     (e + y) ∙ (x + e) ≈⟨ cong (identityˡ y) (identityʳ x) ⟩
     y ∙ x             ∎
@@ -69,12 +74,12 @@ module _ {_∙_ : Op₂ A} (cong : Congruent₂ _∙_) where
 ------------------------------------------------------------------------
 -- SelfInverse
 
-module _ {f : Op₁ A} (self : SelfInverse f) where
+module _ (self : SelfInverse f) where
 
   selfInverse⇒involutive : Involutive f
-  selfInverse⇒involutive = reflexive∧selfInverse⇒involutive _≈_ refl self
+  selfInverse⇒involutive = reflexive∧selfInverse⇒involutive refl self
 
-  selfInverse⇒congruent : Congruent _≈_ _≈_ f
+  selfInverse⇒congruent : Congruent₁ f
   selfInverse⇒congruent {x} {y} x≈y = sym (self (begin
     f (f x) ≈⟨ selfInverse⇒involutive x ⟩
     x       ≈⟨ x≈y ⟩
@@ -98,7 +103,7 @@ module _ {f : Op₁ A} (self : SelfInverse f) where
 ------------------------------------------------------------------------
 -- Magma-like structures
 
-module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) where
+module _ (comm : Commutative _∙_) where
 
   comm∧cancelˡ⇒cancelʳ : LeftCancellative _∙_ → RightCancellative _∙_
   comm∧cancelˡ⇒cancelʳ cancelˡ x y z eq = cancelˡ x y z $ begin
@@ -117,16 +122,16 @@ module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) where
 ------------------------------------------------------------------------
 -- Monoid-like structures
 
-module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) {e : A} where
+module _ (comm : Commutative _∙_) where
 
   comm∧idˡ⇒idʳ : LeftIdentity e _∙_ → RightIdentity e _∙_
-  comm∧idˡ⇒idʳ idˡ x = begin
+  comm∧idˡ⇒idʳ {e = e} idˡ x = begin
     x ∙ e ≈⟨ comm x e ⟩
     e ∙ x ≈⟨ idˡ x ⟩
     x     ∎
 
   comm∧idʳ⇒idˡ : RightIdentity e _∙_ → LeftIdentity e _∙_
-  comm∧idʳ⇒idˡ idʳ x = begin
+  comm∧idʳ⇒idˡ {e = e} idʳ x = begin
     e ∙ x ≈⟨ comm e x ⟩
     x ∙ e ≈⟨ idʳ x ⟩
     x     ∎
@@ -138,13 +143,13 @@ module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) {e : A} where
   comm∧idʳ⇒id idʳ = comm∧idʳ⇒idˡ idʳ , idʳ
 
   comm∧zeˡ⇒zeʳ : LeftZero e _∙_ → RightZero e _∙_
-  comm∧zeˡ⇒zeʳ zeˡ x = begin
+  comm∧zeˡ⇒zeʳ  {e = e} zeˡ x = begin
     x ∙ e ≈⟨ comm x e ⟩
     e ∙ x ≈⟨ zeˡ x ⟩
     e     ∎
 
   comm∧zeʳ⇒zeˡ : RightZero e _∙_ → LeftZero e _∙_
-  comm∧zeʳ⇒zeˡ zeʳ x = begin
+  comm∧zeʳ⇒zeˡ {e = e} zeʳ x = begin
     e ∙ x ≈⟨ comm e x ⟩
     x ∙ e ≈⟨ zeʳ x ⟩
     e     ∎
@@ -157,7 +162,7 @@ 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 =
+  comm∧almostCancelˡ⇒almostCancelʳ {e = e} cancelˡ-nonZero x y z x≉e yx≈zx =
     cancelˡ-nonZero x y z x≉e $ begin
       x ∙ y ≈⟨ comm x y ⟩
       y ∙ x ≈⟨ yx≈zx ⟩
@@ -166,7 +171,7 @@ 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 =
+  comm∧almostCancelʳ⇒almostCancelˡ {e = e} cancelʳ-nonZero x y z x≉e xy≈xz =
     cancelʳ-nonZero x y z x≉e $ begin
       y ∙ x ≈⟨ comm y x ⟩
       x ∙ y ≈⟨ xy≈xz ⟩
@@ -176,10 +181,10 @@ module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) {e : A} where
 ------------------------------------------------------------------------
 -- Group-like structures
 
-module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (comm : Commutative _∙_) where
+module _ (comm : Commutative _∙_) where
 
   comm∧invˡ⇒invʳ : LeftInverse e _⁻¹ _∙_ → RightInverse e _⁻¹ _∙_
-  comm∧invˡ⇒invʳ invˡ x = begin
+  comm∧invˡ⇒invʳ {e = e} {_⁻¹ = _⁻¹} invˡ x = begin
     x ∙ (x ⁻¹) ≈⟨ comm x (x ⁻¹) ⟩
     (x ⁻¹) ∙ x ≈⟨ invˡ x ⟩
     e          ∎
@@ -188,7 +193,7 @@ module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (comm : Commutative _∙_) whe
   comm∧invˡ⇒inv invˡ = invˡ , comm∧invˡ⇒invʳ invˡ
 
   comm∧invʳ⇒invˡ : RightInverse e _⁻¹ _∙_ → LeftInverse e _⁻¹ _∙_
-  comm∧invʳ⇒invˡ invʳ x = begin
+  comm∧invʳ⇒invˡ {e = e} {_⁻¹ = _⁻¹} invʳ x = begin
     (x ⁻¹) ∙ x ≈⟨ comm (x ⁻¹) x ⟩
     x ∙ (x ⁻¹) ≈⟨ invʳ x ⟩
     e          ∎
@@ -196,15 +201,15 @@ module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (comm : Commutative _∙_) whe
   comm∧invʳ⇒inv : RightInverse e _⁻¹ _∙_ → Inverse e _⁻¹ _∙_
   comm∧invʳ⇒inv invʳ = comm∧invʳ⇒invˡ invʳ , invʳ
 
-module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (cong : Congruent₂ _∙_) where
+module _ (cong : Congruent₂ _∙_) where
 
   assoc∧id∧invʳ⇒invˡ-unique : Associative _∙_ →
                               Identity e _∙_ → RightInverse e _⁻¹ _∙_ →
                               ∀ x y → (x ∙ y) ≈ e → x ≈ (y ⁻¹)
-  assoc∧id∧invʳ⇒invˡ-unique assoc (idˡ , idʳ) invʳ x y eq = begin
-    x                ≈⟨ sym (idʳ x) ⟩
+  assoc∧id∧invʳ⇒invˡ-unique {e = e} {_⁻¹ = _⁻¹} assoc (idˡ , idʳ) invʳ x y eq = begin
+    x                ≈⟨ idʳ x ⟨
     x ∙ e            ≈⟨ cong refl (sym (invʳ y)) ⟩
-    x ∙ (y ∙ (y ⁻¹)) ≈⟨ sym (assoc x y (y ⁻¹)) ⟩
+    x ∙ (y ∙ (y ⁻¹)) ≈⟨ assoc x y (y ⁻¹) ⟨
     (x ∙ y) ∙ (y ⁻¹) ≈⟨ cong eq refl ⟩
     e ∙ (y ⁻¹)       ≈⟨ idˡ (y ⁻¹) ⟩
     y ⁻¹             ∎
@@ -212,9 +217,9 @@ module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (cong : Congruent₂ _∙_) wh
   assoc∧id∧invˡ⇒invʳ-unique : Associative _∙_ →
                               Identity e _∙_ → LeftInverse e _⁻¹ _∙_ →
                               ∀ x y → (x ∙ y) ≈ e → y ≈ (x ⁻¹)
-  assoc∧id∧invˡ⇒invʳ-unique assoc (idˡ , idʳ) invˡ x y eq = begin
-    y                ≈⟨ sym (idˡ y) ⟩
-    e ∙ y            ≈⟨ cong (sym (invˡ x)) refl ⟩
+  assoc∧id∧invˡ⇒invʳ-unique {e = e} {_⁻¹ = _⁻¹} assoc (idˡ , idʳ) invˡ x y eq = begin
+    y                ≈⟨ idˡ y ⟨
+    e ∙ y            ≈⟨ cong (invˡ x) refl ⟨
     ((x ⁻¹) ∙ x) ∙ y ≈⟨ assoc (x ⁻¹) x y ⟩
     (x ⁻¹) ∙ (x ∙ y) ≈⟨ cong refl eq ⟩
     (x ⁻¹) ∙ e       ≈⟨ idʳ (x ⁻¹) ⟩
@@ -223,10 +228,7 @@ module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (cong : Congruent₂ _∙_) wh
 ------------------------------------------------------------------------
 -- Bisemigroup-like structures
 
-module _ {_∙_ _◦_ : Op₂ A}
-         (◦-cong : Congruent₂ _◦_)
-         (∙-comm : Commutative _∙_)
-         where
+module _ (◦-cong : Congruent₂ _◦_) (∙-comm : Commutative _∙_) where
 
   comm∧distrˡ⇒distrʳ :  _∙_ DistributesOverˡ _◦_ → _∙_ DistributesOverʳ _◦_
   comm∧distrˡ⇒distrʳ distrˡ x y z = begin
@@ -256,8 +258,7 @@ module _ {_∙_ _◦_ : Op₂ A}
     (x ◦ z) ∙ (x ◦ y) ∎
 
 
-module _ {_∙_ _◦_ : Op₂ A}
-         (∙-cong  : Congruent₂ _∙_)
+module _ (∙-cong  : Congruent₂ _∙_)
          (∙-assoc : Associative _∙_)
          (◦-comm  : Commutative _◦_)
          where
@@ -278,20 +279,17 @@ module _ {_∙_ _◦_ : Op₂ A}
 ------------------------------------------------------------------------
 -- Ring-like structures
 
-module _ {_+_ _*_ : Op₂ A}
-         {_⁻¹ : Op₁ A} {0# : A}
-         (+-cong : Congruent₂ _+_)
-         (*-cong : Congruent₂ _*_)
-         where
+module _ (+-cong : Congruent₂ _+_) (*-cong : Congruent₂ _*_) where
 
   assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ : Associative _+_ → _*_ DistributesOverʳ _+_ →
                                 RightIdentity 0# _+_ → RightInverse 0# _⁻¹ _+_ →
                                 LeftZero 0# _*_
-  assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ +-assoc distribʳ idʳ invʳ  x = begin
-    0# * x                                 ≈⟨ sym (idʳ _) ⟩
+  assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ {0# = 0#} {_⁻¹ = _⁻¹} +-assoc distribʳ idʳ invʳ  x
+    = begin
+    0# * x                                 ≈⟨ idʳ _ ⟨
     (0# * x) + 0#                          ≈⟨ +-cong refl (sym (invʳ _)) ⟩
-    (0# * x) + ((0# * x)  + ((0# * x)⁻¹))  ≈⟨ sym (+-assoc _ _ _) ⟩
-    ((0# * x) +  (0# * x)) + ((0# * x)⁻¹)  ≈⟨ +-cong (sym (distribʳ _ _ _)) refl ⟩
+    (0# * x) + ((0# * x)  + ((0# * x)⁻¹))  ≈⟨ +-assoc _ _ _ ⟨
+    ((0# * x) +  (0# * x)) + ((0# * x)⁻¹)  ≈⟨ +-cong (distribʳ _ _ _) refl ⟨
     ((0# + 0#) * x) + ((0# * x)⁻¹)         ≈⟨ +-cong (*-cong (idʳ _) refl) refl ⟩
     (0# * x) + ((0# * x)⁻¹)                ≈⟨ invʳ _ ⟩
     0#                                     ∎
@@ -299,11 +297,12 @@ module _ {_+_ _*_ : Op₂ A}
   assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ : Associative _+_ → _*_ DistributesOverˡ _+_ →
                                 RightIdentity 0# _+_ → RightInverse 0# _⁻¹ _+_ →
                                 RightZero 0# _*_
-  assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ +-assoc distribˡ idʳ invʳ  x = begin
-     x * 0#                                ≈⟨ sym (idʳ _) ⟩
+  assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ {0# = 0#} {_⁻¹ = _⁻¹} +-assoc distribˡ idʳ invʳ  x
+    = begin
+     x * 0#                                ≈⟨ idʳ _ ⟨
      (x * 0#) + 0#                         ≈⟨ +-cong refl (sym (invʳ _)) ⟩
-     (x * 0#) + ((x * 0#) + ((x * 0#)⁻¹))  ≈⟨ sym (+-assoc _ _ _) ⟩
-     ((x * 0#) + (x * 0#)) + ((x * 0#)⁻¹)  ≈⟨ +-cong (sym (distribˡ _ _ _)) refl ⟩
+     (x * 0#) + ((x * 0#) + ((x * 0#)⁻¹))  ≈⟨ +-assoc _ _ _ ⟨
+     ((x * 0#) + (x * 0#)) + ((x * 0#)⁻¹)  ≈⟨ +-cong (distribˡ _ _ _) refl ⟨
      (x * (0# + 0#)) + ((x * 0#)⁻¹)        ≈⟨ +-cong (*-cong refl (idʳ _)) refl ⟩
      ((x * 0#) + ((x * 0#)⁻¹))             ≈⟨ invʳ _ ⟩
      0#                                    ∎
@@ -311,18 +310,18 @@ module _ {_+_ _*_ : Op₂ A}
 ------------------------------------------------------------------------
 -- Without Loss of Generality
 
-module _ {p} {f : Op₂ A} {P : Pred A p}
+module _ {p} {P : Pred A p}
          (≈-subst : Substitutive _≈_ p)
-         (comm : Commutative f)
+         (∙-comm : Commutative _∙_)
          where
 
-  subst∧comm⇒sym : Symmetric (λ a b → P (f a b))
-  subst∧comm⇒sym = ≈-subst P (comm _ _)
+  subst∧comm⇒sym : Symmetric (λ a b → P (a ∙ b))
+  subst∧comm⇒sym = ≈-subst P (∙-comm _ _)
 
   wlog : ∀ {r} {_R_ : Rel _ r} → Total _R_ →
-         (∀ a b → a R b → P (f a b)) →
-         ∀ a b → P (f a b)
-  wlog r-total = Bin.wlog r-total subst∧comm⇒sym
+         (∀ a b → a R b → P (a ∙ b)) →
+         ∀ a b → P (a ∙ b)
+  wlog r-total = BinaryConsequences.wlog r-total subst∧comm⇒sym
 
 
 ------------------------------------------------------------------------

From 1e25c10bd5cf98cfb72d0b6c886af7e47201fe02 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 6 Feb 2025 11:37:18 +0000
Subject: [PATCH 3/7] refactor: propagate changes; remove spurious anonymous
 modules

---
 src/Algebra/Consequences/Propositional.agda | 104 +++++++++-----------
 1 file changed, 47 insertions(+), 57 deletions(-)

diff --git a/src/Algebra/Consequences/Propositional.agda b/src/Algebra/Consequences/Propositional.agda
index 29490cbd0c..14451e6e3e 100644
--- a/src/Algebra/Consequences/Propositional.agda
+++ b/src/Algebra/Consequences/Propositional.agda
@@ -20,10 +20,17 @@ open import Relation.Binary.PropositionalEquality.Properties
   using (setoid)
 open import Relation.Unary using (Pred)
 
-open import Algebra.Core
+open import Algebra.Core using (Op₁; Op₂)
 open import Algebra.Definitions {A = A} _≡_
 import Algebra.Consequences.Setoid (setoid A) as Base
 
+private
+  variable
+    e ε 0# : A
+    f _⁻¹ -_ : Op₁ A
+    _∙_ _◦_ _+_ _*_ : Op₂ A
+
+
 ------------------------------------------------------------------------
 -- Re-export all proofs that don't require congruence or substitutivity
 
@@ -41,7 +48,6 @@ open Base public
   ; comm⇒sym[distribˡ]
   ; subst∧comm⇒sym
   ; wlog
-  ; sel⇒idem
 -- plus all the deprecated versions of the above
   ; comm+assoc⇒middleFour
   ; identity+middleFour⇒assoc
@@ -58,39 +64,35 @@ open Base public
 ------------------------------------------------------------------------
 -- Group-like structures
 
-module _ {_∙_ _⁻¹ ε} where
-
-  assoc∧id∧invʳ⇒invˡ-unique : Associative _∙_ → Identity ε _∙_ →
-                              RightInverse ε _⁻¹ _∙_ →
-                              ∀ x y → (x ∙ y) ≡ ε → x ≡ (y ⁻¹)
-  assoc∧id∧invʳ⇒invˡ-unique = Base.assoc∧id∧invʳ⇒invˡ-unique (cong₂ _)
+assoc∧id∧invʳ⇒invˡ-unique : Associative _∙_ → Identity ε _∙_ →
+                            RightInverse ε _⁻¹ _∙_ →
+                            ∀ x y → (x ∙ y) ≡ ε → x ≡ (y ⁻¹)
+assoc∧id∧invʳ⇒invˡ-unique = Base.assoc∧id∧invʳ⇒invˡ-unique (cong₂ _)
 
-  assoc∧id∧invˡ⇒invʳ-unique : Associative _∙_ → Identity ε _∙_ →
-                              LeftInverse ε _⁻¹ _∙_ →
-                              ∀ x y → (x ∙ y) ≡ ε → y ≡ (x ⁻¹)
-  assoc∧id∧invˡ⇒invʳ-unique = Base.assoc∧id∧invˡ⇒invʳ-unique (cong₂ _)
+assoc∧id∧invˡ⇒invʳ-unique : Associative _∙_ → Identity ε _∙_ →
+                            LeftInverse ε _⁻¹ _∙_ →
+                            ∀ x y → (x ∙ y) ≡ ε → y ≡ (x ⁻¹)
+assoc∧id∧invˡ⇒invʳ-unique = Base.assoc∧id∧invˡ⇒invʳ-unique (cong₂ _)
 
 ------------------------------------------------------------------------
 -- Ring-like structures
 
-module _ {_+_ _*_ -_ 0#} where
+assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ : Associative _+_ → _*_ DistributesOverʳ _+_ →
+                              RightIdentity 0# _+_ → RightInverse 0# -_ _+_ →
+                              LeftZero 0# _*_
+assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ {_+_ = _+_} {_*_ = _*_} =
+  Base.assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ (cong₂ _+_) (cong₂ _*_)
 
-  assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ : Associative _+_ → _*_ DistributesOverʳ _+_ →
-                                RightIdentity 0# _+_ → RightInverse 0# -_ _+_ →
-                                LeftZero 0# _*_
-  assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ =
-    Base.assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ (cong₂ _+_) (cong₂ _*_)
-
-  assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ : Associative _+_ → _*_ DistributesOverˡ _+_ →
-                                RightIdentity 0# _+_ → RightInverse 0# -_ _+_ →
-                                RightZero 0# _*_
-  assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ =
-    Base.assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ (cong₂ _+_) (cong₂ _*_)
+assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ : Associative _+_ → _*_ DistributesOverˡ _+_ →
+                              RightIdentity 0# _+_ → RightInverse 0# -_ _+_ →
+                              RightZero 0# _*_
+assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ {_+_ = _+_} {_*_ = _*_} =
+  Base.assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ (cong₂ _+_) (cong₂ _*_)
 
 ------------------------------------------------------------------------
 -- Bisemigroup-like structures
 
-module _ {_∙_ _◦_ : Op₂ A} (∙-comm : Commutative _∙_) where
+module _ (∙-comm : Commutative _∙_) where
 
   comm∧distrˡ⇒distrʳ : _∙_ DistributesOverˡ _◦_ → _∙_ DistributesOverʳ _◦_
   comm∧distrˡ⇒distrʳ = Base.comm+distrˡ⇒distrʳ (cong₂ _) ∙-comm
@@ -99,49 +101,37 @@ module _ {_∙_ _◦_ : Op₂ A} (∙-comm : Commutative _∙_) where
   comm∧distrʳ⇒distrˡ = Base.comm∧distrʳ⇒distrˡ (cong₂ _) ∙-comm
 
   comm⇒sym[distribˡ] : ∀ x → Symmetric (λ y z → (x ◦ (y ∙ z)) ≡ ((x ◦ y) ∙ (x ◦ z)))
-  comm⇒sym[distribˡ] = Base.comm⇒sym[distribˡ] (cong₂ _◦_) ∙-comm
+  comm⇒sym[distribˡ] = Base.comm⇒sym[distribˡ] (cong₂ _) ∙-comm
 
 ------------------------------------------------------------------------
--- Selectivity
-
-module _ {_∙_ : Op₂ A} where
-
-  sel⇒idem : Selective _∙_ → Idempotent _∙_
-  sel⇒idem = Base.sel⇒idem _≡_
-
-------------------------------------------------------------------------
--- Middle-Four Exchange
-
-module _ {_∙_ : Op₂ A} where
+-- MiddleFourExchange
 
-  comm∧assoc⇒middleFour : Commutative _∙_ → Associative _∙_ →
-                          _∙_ MiddleFourExchange _∙_
-  comm∧assoc⇒middleFour = Base.comm∧assoc⇒middleFour (cong₂ _∙_)
+comm∧assoc⇒middleFour : Commutative _∙_ → Associative _∙_ →
+                        _∙_ MiddleFourExchange _∙_
+comm∧assoc⇒middleFour = Base.comm∧assoc⇒middleFour (cong₂ _)
 
-  identity∧middleFour⇒assoc : {e : A} → Identity e _∙_ →
-                              _∙_ MiddleFourExchange _∙_ →
-                              Associative _∙_
-  identity∧middleFour⇒assoc = Base.identity∧middleFour⇒assoc (cong₂ _∙_)
+identity∧middleFour⇒assoc : Identity e _∙_ →
+                            _∙_ MiddleFourExchange _∙_ →
+                            Associative _∙_
+identity∧middleFour⇒assoc {_∙_ = _∙_} = Base.identity∧middleFour⇒assoc (cong₂ _∙_)
 
-  identity∧middleFour⇒comm : {_+_ : Op₂ A} {e : A} → Identity e _+_ →
-                             _∙_ MiddleFourExchange _+_ →
-                             Commutative _∙_
-  identity∧middleFour⇒comm = Base.identity∧middleFour⇒comm (cong₂ _∙_)
+identity∧middleFour⇒comm : Identity e _+_ →
+                           _∙_ MiddleFourExchange _+_ →
+                           Commutative _∙_
+identity∧middleFour⇒comm = Base.identity∧middleFour⇒comm (cong₂ _)
 
 ------------------------------------------------------------------------
 -- Without Loss of Generality
 
-module _ {p} {P : Pred A p} where
+module _ {p} {P : Pred A p} (∙-comm : Commutative _∙_) where
 
-  subst∧comm⇒sym : ∀ {f} (f-comm : Commutative f) →
-                   Symmetric (λ a b → P (f a b))
-  subst∧comm⇒sym = Base.subst∧comm⇒sym {P = P} subst
+  subst∧comm⇒sym : Symmetric (λ a b → P (a ∙ b))
+  subst∧comm⇒sym = Base.subst∧comm⇒sym {P = P} subst ∙-comm
 
-  wlog : ∀ {f} (f-comm : Commutative f) →
-         ∀ {r} {_R_ : Rel _ r} → Total _R_ →
-         (∀ a b → a R b → P (f a b)) →
-         ∀ a b → P (f a b)
-  wlog = Base.wlog {P = P} subst
+  wlog : ∀ {r} {_R_ : Rel _ r} → Total _R_ →
+         (∀ a b → a R b → P (a ∙ b)) →
+         ∀ a b → P (a ∙ b)
+  wlog = Base.wlog {P = P} subst ∙-comm
 
 
 ------------------------------------------------------------------------

From 6eab5f223e71e60c599bba3522df7c60287cd5b2 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 6 Feb 2025 11:53:17 +0000
Subject: [PATCH 4/7] fix: `CHANGELOG`

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4940047ba8..7556f36d34 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -15,6 +15,12 @@ Non-backwards compatible changes
 Minor improvements
 ------------------
 
+* [Issue #2502](https://github.com/agda/agda-stdlib/issues/2502) The top-level
+  module `Algebra.Consequences.Base` now takes the underlying equality relation
+  as an additional parameter, with slightly improved ergonomics wrt subsequent
+  imports; additionally, its internal implicit module parameters capturing the
+  signature of various algebraic operations, have now been lifted out as `variable`s.
+
 Deprecated modules
 ------------------
 

From 2433c3c7ac1154d7644e9cbcd8b1b75f958340e9 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 6 Feb 2025 12:04:17 +0000
Subject: [PATCH 5/7] fix: deprecated names from #2206 / #2168

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

diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda
index 181e4a6189..3d7c84554c 100644
--- a/src/Data/Rational/Unnormalised/Properties.agda
+++ b/src/Data/Rational/Unnormalised/Properties.agda
@@ -1144,7 +1144,7 @@ p≤q⇒0≤q-p {p} {q} p≤q = begin
 *-zeroˡ p@record{} = *≡* refl
 
 *-zeroʳ : RightZero _≃_ 0ℚᵘ _*_
-*-zeroʳ = Consequences.comm+zeˡ⇒zeʳ ≃-setoid *-comm *-zeroˡ
+*-zeroʳ = Consequences.comm∧zeˡ⇒zeʳ ≃-setoid *-comm *-zeroˡ
 
 *-zero : Zero _≃_ 0ℚᵘ _*_
 *-zero = *-zeroˡ , *-zeroʳ
@@ -1171,7 +1171,7 @@ invertible⇒≄ {p} {q} (1/p-q , 1/x*x≃1 , x*1/x≃1) p≃q = 0≄1 (begin
   in *≡* eq where open ℤ-solver
 
 *-distribʳ-+ : _DistributesOverʳ_ _≃_ _*_ _+_
-*-distribʳ-+ = Consequences.comm+distrˡ⇒distrʳ ≃-setoid +-cong *-comm *-distribˡ-+
+*-distribʳ-+ = Consequences.comm∧distrˡ⇒distrʳ ≃-setoid +-cong *-comm *-distribˡ-+
 
 *-distrib-+ : _DistributesOver_ _≃_ _*_ _+_
 *-distrib-+ = *-distribˡ-+ , *-distribʳ-+

From d19dac94ae3984c777a1be42598185ea97f313a6 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 6 Feb 2025 12:24:10 +0000
Subject: [PATCH 6/7] fix: remove spurious blank line introduced by mistake

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

diff --git a/src/Algebra/Consequences/Base.agda b/src/Algebra/Consequences/Base.agda
index 780726f3b0..2cedb9a5aa 100644
--- a/src/Algebra/Consequences/Base.agda
+++ b/src/Algebra/Consequences/Base.agda
@@ -1,4 +1,3 @@
-
 ------------------------------------------------------------------------
 -- The Agda standard library
 --

From 0f720f873637cf42b0a3f860da6f3604e136b893 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 19 Feb 2025 18:39:06 +0000
Subject: [PATCH 7/7] fix: `CHANGELOG` entry

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index fb7b64a703..895cbe789c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -24,11 +24,10 @@ Non-backwards compatible changes
 Minor improvements
 ------------------
 
-* [Issue #2502](https://github.com/agda/agda-stdlib/issues/2502) The top-level
-  module `Algebra.Consequences.Base` now takes the underlying equality relation
-  as an additional parameter, with slightly improved ergonomics wrt subsequent
-  imports; additionally, its internal implicit module parameters capturing the
-  signature of various algebraic operations, have now been lifted out as `variable`s.
+* [Issue #2502](https://github.com/agda/agda-stdlib/issues/2502) The module
+  `Algebra.Consequences.Base` now takes the underlying equality relation as
+  an additional top-level parameter, with slightly improved ergonomics wrt
+  subsequent imports by clients, as well as streamlined internals.
 
 Deprecated modules
 ------------------