refactor: put lemma in the right place

Author: jamesmckinna

CHANGELOG.md

@@ -11,6 +11,10 @@ Bug-fixes
 
 * Fix a type error in `README.Data.Fin.Relation.Unary.Top` within the definition of `>-weakInduction`.
 
+* Remove spurious definition of `Algebra.Consequences.Propositional.sel⇒idem`,
+  which duplicated lemma from `Algebra.Consequences.Base`, instead of importing
+  from `Algebra.Consequences.Setoid`.
+
 * Fix a typo in `Algebra.Morphism.Construct.DirectProduct`.
 
 * Fix a typo in `Function.Construct.Constant`.
@@ -122,6 +126,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))
   ```

src/Algebra/Consequences/Propositional.agda

@@ -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
@@ -55,7 +54,7 @@ open Base public
   ; comm+distrʳ⇒distrˡ
   ; subst+comm⇒sym
   )
-
+test = {!sel⇒idem!}
 ------------------------------------------------------------------------
 -- Group-like structures
 
@@ -111,14 +110,6 @@ module _ {_∙_ _◦_ : Op₂ A}
              ((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 _≡_
-
 ------------------------------------------------------------------------
 -- Middle-Four Exchange
 

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