From 8693ddcc9283ac4f7d4e4abc11424bd77e050421 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 12 Nov 2025 17:33:01 +0000
Subject: [PATCH 1/2] refactor: put lemma in the right place

---
 CHANGELOG.md                                |  5 +++++
 src/Algebra/Consequences/Propositional.agda | 11 +----------
 src/Algebra/Consequences/Setoid.agda        | 10 +++++++++-
 3 files changed, 15 insertions(+), 11 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3eb803ac39..b68d6df09c 100644
--- a/CHANGELOG.md
+++ b/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))
   ```
diff --git a/src/Algebra/Consequences/Propositional.agda b/src/Algebra/Consequences/Propositional.agda
index f975cdef5e..36aa343b25 100644
--- a/src/Algebra/Consequences/Propositional.agda
+++ b/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
 
diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda
index 4d6bb4dbba..f2fdd9bba2 100644
--- a/src/Algebra/Consequences/Setoid.agda
+++ b/src/Algebra/Consequences/Setoid.agda
@@ -33,7 +33,7 @@ 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
 
@@ -41,6 +41,14 @@ 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
 

From 177e788af08c6fc854876008b31ed17b735d8662 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 12 Nov 2025 17:36:32 +0000
Subject: [PATCH 2/2] fix: uncommitted edits

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

diff --git a/src/Algebra/Consequences/Propositional.agda b/src/Algebra/Consequences/Propositional.agda
index 36aa343b25..9236791395 100644
--- a/src/Algebra/Consequences/Propositional.agda
+++ b/src/Algebra/Consequences/Propositional.agda
@@ -54,7 +54,7 @@ open Base public
   ; comm+distrʳ⇒distrˡ
   ; subst+comm⇒sym
   )
-test = {!sel⇒idem!}
+
 ------------------------------------------------------------------------
 -- Group-like structures