From cbfc19e161e4402fc32ff704bb29ce095e18eda0 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 12 Nov 2025 16:54:34 +0000
Subject: [PATCH 1/2] add: `Algebra.Definitions.Central`

---
 CHANGELOG.md                 | 5 +++++
 src/Algebra/Definitions.agda | 3 +++
 2 files changed, 8 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3eb803ac39..c3ea84a1cc 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -126,6 +126,11 @@ Additions to existing modules
     ∀ w x y z → ((w ∙ x) ◦ (y ∙ z)) ≈ ((((w ◦ y) ∙ (w ◦ z)) ∙ (x ◦ y)) ∙ (x ◦ z))
   ```
 
+* In `Algebra.Definitions`:
+  ```agda
+  Central : Op₂ A → A → Set _
+  ```
+
 * In `Algebra.Lattice.Properties.BooleanAlgebra.XorRing`:
   ```agda
   ⊕-∧-isBooleanRing : IsBooleanRing _⊕_ _∧_ id ⊥ ⊤
diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda
index e42958da4d..3123ef976d 100644
--- a/src/Algebra/Definitions.agda
+++ b/src/Algebra/Definitions.agda
@@ -50,6 +50,9 @@ Associative _∙_ = ∀ x y z → ((x ∙ y) ∙ z) ≈ (x ∙ (y ∙ z))
 Commutative : Op₂ A → Set _
 Commutative _∙_ = ∀ x y → (x ∙ y) ≈ (y ∙ x)
 
+Central : Op₂ A → A → Set _
+Central _∙_ x = ∀ y → (x ∙ y) ≈ (y ∙ x)
+
 LeftIdentity : A → Op₂ A → Set _
 LeftIdentity e _∙_ = ∀ x → (e ∙ x) ≈ x
 

From 80388380ac948acea844caa6bb81bd6607929fb3 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 12 Nov 2025 17:11:02 +0000
Subject: [PATCH 2/2] add: `Identity` and `Zero` elements are `Central`

---
 CHANGELOG.md                         | 4 ++++
 src/Algebra/Consequences/Setoid.agda | 9 +++++++++
 2 files changed, 13 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index c3ea84a1cc..52fc3d6984 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -118,12 +118,16 @@ Additions to existing modules
   ```agda
   binomial-expansion : Associative _∙_ → _◦_ DistributesOver _∙_ →
     ∀ w x y z → ((w ∙ x) ◦ (y ∙ z)) ≡ ((((w ◦ y) ∙ (w ◦ z)) ∙ (x ◦ y)) ∙ (x ◦ z))
+  identity⇒central   : Identity e _∙_ → Central _∙_ e
+  zero⇒central       : Zero e _∙_ → Central _∙_ e
   ```
 
 * In `Algebra.Consequences.Setoid`:
   ```agda
   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
+  zero⇒central       : Zero e _∙_ → Central _∙_ e
   ```
 
 * In `Algebra.Definitions`:
diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda
index 4d6bb4dbba..8ace8652ed 100644
--- a/src/Algebra/Consequences/Setoid.agda
+++ b/src/Algebra/Consequences/Setoid.agda
@@ -184,6 +184,15 @@ module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) {e : A} where
       x ∙ z ≈⟨ comm x z ⟩
       z ∙ x ∎
 
+module _ {_∙_ : Op₂ A} {e : A} where
+
+  identity⇒central : Identity e _∙_ → Central _∙_ e
+  identity⇒central (identityˡ , identityʳ) x = trans (identityˡ x) (sym (identityʳ x))
+
+  zero⇒central : Zero e _∙_ → Central _∙_ e
+  zero⇒central (zeroˡ , zeroʳ) x = trans (zeroˡ x) (sym (zeroʳ x))
+
+
 ------------------------------------------------------------------------
 -- Group-like structures