[ refactor ] Add equality as a parameter to Algebra.Consequences.Base

CHANGELOG.md

@@ -24,6 +24,11 @@ Non-backwards compatible changes
 Minor improvements
 ------------------
 
+* [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
 ------------------
 

src/Algebra/Consequences/Base.agda

@@ -7,26 +7,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

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
 
 
 ------------------------------------------------------------------------