[ bug/refactor ] put Algebra.Consequence.Propositional.sel⇒idem in the right place (#2881)

* refactor: put lemma in the right place

* fix: uncommitted edits

* fix: `CHANGELOG`

* fix: qualified module name

Author: jamesmckinna

CHANGELOG.md

@@ -133,6 +133,7 @@ Additions to existing modules
 
 * In `Algebra.Consequences.Setoid`:
   ```agda
+  sel⇒idem : Selective _∙_ → Idempotent _∙_
   binomial-expansion : Congruent₂ _∙_  → Associative _∙_ → _◦_ DistributesOver _∙_ →
     ∀ w x y z → ((w ∙ x) ◦ (y ∙ z)) ≈ ((((w ◦ y) ∙ (w ◦ z)) ∙ (x ◦ y)) ∙ (x ◦ z))
   identity⇒central   : Identity e _∙_ → Central _∙_ e

src/Algebra/Consequences/Propositional.agda

@@ -22,12 +22,12 @@ open import Relation.Binary.PropositionalEquality.Properties
 open import Relation.Unary using (Pred)
 
 open import Algebra.Definitions {A = A} _≡_
-import Algebra.Consequences.Setoid (setoid A) as Base
+import Algebra.Consequences.Setoid (setoid A) as SetoidConsequences
 
 ------------------------------------------------------------------------
 -- Re-export all proofs that don't require congruence or substitutivity
 
-open Base public
+open SetoidConsequences public
   hiding
   ( comm∧assoc⇒middleFour
   ; identity∧middleFour⇒assoc
@@ -41,7 +41,6 @@ open Base public
   ; comm⇒sym[distribˡ]
   ; subst∧comm⇒sym
   ; wlog
-  ; sel⇒idem
   ; binomial-expansion
 -- plus all the deprecated versions of the above
   ; comm+assoc⇒middleFour
@@ -64,12 +63,12 @@ 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 = SetoidConsequences.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 = SetoidConsequences.assoc∧id∧invˡ⇒invʳ-unique (cong₂ _)
 
 ------------------------------------------------------------------------
 -- Ring-like structures
@@ -80,27 +79,27 @@ module _ {_+_ _*_ -_ 0#} where
                                 RightIdentity 0# _+_ → RightInverse 0# -_ _+_ →
                                 LeftZero 0# _*_
   assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ =
-    Base.assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ (cong₂ _+_) (cong₂ _*_)
+    SetoidConsequences.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₂ _*_)
+    SetoidConsequences.assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ (cong₂ _+_) (cong₂ _*_)
 
 ------------------------------------------------------------------------
 -- Bisemigroup-like structures
 
 module _ {_∙_ _◦_ : Op₂ A} (∙-comm : Commutative _∙_) where
 
   comm∧distrˡ⇒distrʳ : _∙_ DistributesOverˡ _◦_ → _∙_ DistributesOverʳ _◦_
-  comm∧distrˡ⇒distrʳ = Base.comm+distrˡ⇒distrʳ (cong₂ _) ∙-comm
+  comm∧distrˡ⇒distrʳ = SetoidConsequences.comm+distrˡ⇒distrʳ (cong₂ _) ∙-comm
 
   comm∧distrʳ⇒distrˡ : _∙_ DistributesOverʳ _◦_ → _∙_ DistributesOverˡ _◦_
-  comm∧distrʳ⇒distrˡ = Base.comm∧distrʳ⇒distrˡ (cong₂ _) ∙-comm
+  comm∧distrʳ⇒distrˡ = SetoidConsequences.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ˡ] = SetoidConsequences.comm⇒sym[distribˡ] (cong₂ _◦_) ∙-comm
 
 module _ {_∙_ _◦_ : Op₂ A}
          (∙-assoc : Associative _∙_)
@@ -109,15 +108,7 @@ module _ {_∙_ _◦_ : Op₂ A}
 
   binomial-expansion : ∀ w x y z →
              ((w ∙ x) ◦ (y ∙ z)) ≡ ((((w ◦ y) ∙ (w ◦ z)) ∙ (x ◦ y)) ∙ (x ◦ z))
-  binomial-expansion = Base.binomial-expansion {_∙_} {_◦_} (cong₂ _) ∙-assoc distrib
-
-------------------------------------------------------------------------
--- Selectivity
-
-module _ {_∙_ : Op₂ A} where
-
-  sel⇒idem : Selective _∙_ → Idempotent _∙_
-  sel⇒idem = Base.sel⇒idem _≡_
+  binomial-expansion = SetoidConsequences.binomial-expansion {_∙_} {_◦_} (cong₂ _) ∙-assoc distrib
 
 ------------------------------------------------------------------------
 -- Middle-Four Exchange
@@ -126,17 +117,17 @@ module _ {_∙_ : Op₂ A} where
 
   comm∧assoc⇒middleFour : Commutative _∙_ → Associative _∙_ →
                           _∙_ MiddleFourExchange _∙_
-  comm∧assoc⇒middleFour = Base.comm∧assoc⇒middleFour (cong₂ _∙_)
+  comm∧assoc⇒middleFour = SetoidConsequences.comm∧assoc⇒middleFour (cong₂ _∙_)
 
   identity∧middleFour⇒assoc : {e : A} → Identity e _∙_ →
                               _∙_ MiddleFourExchange _∙_ →
                               Associative _∙_
-  identity∧middleFour⇒assoc = Base.identity∧middleFour⇒assoc (cong₂ _∙_)
+  identity∧middleFour⇒assoc = SetoidConsequences.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 = SetoidConsequences.identity∧middleFour⇒comm (cong₂ _∙_)
 
 ------------------------------------------------------------------------
 -- Without Loss of Generality
@@ -145,13 +136,13 @@ module _ {p} {P : Pred A p} 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 = SetoidConsequences.subst∧comm⇒sym {P = P} subst
 
   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 = SetoidConsequences.wlog {P = P} subst
 
 
 ------------------------------------------------------------------------

src/Algebra/Consequences/Setoid.agda

@@ -33,14 +33,22 @@ open import Relation.Binary.Reasoning.Setoid S
 -- Export base lemmas that don't require the setoid
 
 open Base public
-  hiding (module Congruence)
+  hiding (module Congruence; sel⇒idem)
 
 -- Export congruence lemmas using reflexivity
 
 module Congruence {_∙_ : Op₂ A} (cong : Congruent₂ _∙_) where
 
   open Base.Congruence _≈_ cong refl public
 
+------------------------------------------------------------------------
+-- Selectivity
+
+module _ {_∙_ : Op₂ A} where
+
+  sel⇒idem : Selective _∙_ → Idempotent _∙_
+  sel⇒idem = Base.sel⇒idem _≈_
+
 ------------------------------------------------------------------------
 -- MiddleFourExchange