From 7bf4fa240ff7e265b378c7922a18db0dbd58c294 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 19 Nov 2025 08:05:40 +0000
Subject: [PATCH] fix: #2882

---
 CHANGELOG.md                       |  5 ++++
 src/Algebra/Properties/Monoid.agda | 41 ++++++++++++++++++++++++------
 2 files changed, 38 insertions(+), 8 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 52fc3d6984..7929850e71 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -53,6 +53,11 @@ Deprecated names
   interchange  ↦   medial
   ```
 
+* In `Algebra.Properties.Monoid`:
+  ```agda
+  ε-comm  ↦   ε-central
+  ```
+
 * In `Data.Fin.Properties`:
   ```agda
   ¬∀⟶∃¬-smallest  ↦   ¬∀⇒∃¬-smallest
diff --git a/src/Algebra/Properties/Monoid.agda b/src/Algebra/Properties/Monoid.agda
index a93480d9ba..882a8879b7 100644
--- a/src/Algebra/Properties/Monoid.agda
+++ b/src/Algebra/Properties/Monoid.agda
@@ -8,26 +8,37 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra.Bundles using (Monoid)
-open import Function using (_∘_)
 
 module Algebra.Properties.Monoid {o ℓ} (M : Monoid o ℓ) where
 
+open import Function using (_∘_)
+
 open Monoid M
-  using (Carrier; _∙_; _≈_; setoid; isMagma; semigroup; ε; sym; identityˡ
-  ; identityʳ ; ∙-cong; refl; assoc; ∙-congˡ; ∙-congʳ; trans)
+  using (Carrier; _∙_; ε; _≈_; refl; sym; trans; setoid
+        ; ∙-cong; ∙-congˡ; ∙-congʳ; isMagma
+        ; assoc; semigroup; identity; identityˡ; identityʳ)
+
+open import Algebra.Consequences.Setoid setoid using (identity⇒central)
+open import Algebra.Definitions _≈_ using (Central)
 open import Relation.Binary.Reasoning.Setoid setoid
 
+private
+  variable
+    a b c d : Carrier
+
+------------------------------------------------------------------------
+-- Re-export `Semigroup` properties
+
 open import Algebra.Properties.Semigroup semigroup public
 
-private
-    variable
-        a b c d : Carrier
+------------------------------------------------------------------------
+-- Properties of identity
 
 ε-unique : ∀ a → (∀ b → b ∙ a ≈ b) → a ≈ ε
 ε-unique a b∙a≈b = trans (sym (identityˡ a)) (b∙a≈b ε)
 
-ε-comm : ∀ a → a ∙ ε ≈ ε ∙ a
-ε-comm a = trans (identityʳ a) (sym (identityˡ a))
+ε-central : Central _∙_ ε
+ε-central = identity⇒central {_∙_ = _∙_} identity
 
 module _ (a≈ε : a ≈ ε) where
   elimʳ : ∀ b → b ∙ a ≈ b
@@ -65,3 +76,17 @@ module _ (inv : a ∙ c ≈ ε) where
   insertᶜ : ∀ b d → b ∙ d ≈ (b ∙ a) ∙ (c ∙ d)
   insertᶜ = λ b d → sym (cancelᶜ b d)
 
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.4
+
+ε-comm = ε-central
+{-# WARNING_ON_USAGE ε-comm
+"Warning: ε-comm was deprecated in v2.4.
+Please use ε-central instead."
+#-}