From 0fc076fec1afbc15bea2061c82f5a8859ade10ec Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Tue, 1 Apr 2025 15:51:02 -0400
Subject: [PATCH 01/31]  Adds reasonig combinator for semigroup

---
 CHANGELOG.md                         |   2 +
 src/Algebra/Reasoning/SemiGroup.agda | 135 +++++++++++++++++++++++++++
 2 files changed, 137 insertions(+)
 create mode 100644 src/Algebra/Reasoning/SemiGroup.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2959d3d6ce..e38144b7f3 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -123,6 +123,8 @@ New modules
 
 * `Data.Sign.Show` to show a sign
 
+* `Algebra.Reasoning.SemiGroup` adding resaoning combinator for semigroup 
+
 Additions to existing modules
 -----------------------------
 
diff --git a/src/Algebra/Reasoning/SemiGroup.agda b/src/Algebra/Reasoning/SemiGroup.agda
new file mode 100644
index 0000000000..90ea09769a
--- /dev/null
+++ b/src/Algebra/Reasoning/SemiGroup.agda
@@ -0,0 +1,135 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Equational reasoning for semigroups
+-- (Utilities for associativity reasoning, pulling and pushing operations)
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Algebra using (Semigroup)
+
+module Algebra.Reasoning.SemiGroup {o ℓ} (S : Semigroup o ℓ) where
+
+open Semigroup S
+    using (Carrier; _∙_; _≈_; setoid; trans ; refl; sym; assoc; ∙-cong)
+open import Relation.Binary.Reasoning.Setoid setoid
+
+private
+ variable
+    a b c d e x y z : Carrier
+
+module Assoc4  {a b c d : Carrier} where
+    {-
+  Explanation of naming scheme:
+
+  Each successive association is given a Greek letter, from 'α' associated all
+  the way to the left, to 'ε' associated all the way to the right. Then,
+  'assoc²XY' is the proof that X is equal to Y. Explicitly:
+
+  α = ((a ∙ b) ∙ c) ∙ d
+  β = (a ∙ (b ∙ c)) ∙ d
+  γ = (a ∙ b) ∙ (c ∙ d)
+  δ = a ∙ ((b ∙ c) ∙ d)
+  ε = a ∙ (b ∙ (c ∙ d))
+
+  Only reassociations that need two assoc steps are defined here.
+  -}
+  assoc²αδ : ((a ∙ b) ∙ c) ∙ d ≈ a ∙ ((b ∙ c) ∙ d)
+  assoc²αδ = trans (∙-cong (assoc a b c) refl) (assoc a (b ∙ c) d)
+
+  assoc²αε : ((a ∙ b) ∙ c) ∙ d ≈ a ∙ (b ∙ (c ∙ d))
+  assoc²αε = trans (assoc (a ∙ b) c d) (assoc a b (c ∙ d))
+
+  assoc²βγ : (a ∙ (b ∙ c)) ∙ d ≈ (a ∙ b) ∙ (c ∙ d)
+  assoc²βγ = trans (sym (∙-cong (assoc a b c) refl)) (assoc (a ∙ b) c d)
+
+  assoc²βε : (a ∙ (b ∙ c)) ∙ d ≈ a ∙ (b ∙ (c ∙ d))
+  assoc²βε = trans (assoc a (b ∙ c) d) (∙-cong refl (assoc b c d))
+
+  assoc²γβ : (a ∙ b) ∙ (c ∙ d) ≈ (a ∙ (b ∙ c)) ∙ d
+  assoc²γβ = trans (sym (assoc (a ∙ b) c d)) (∙-cong (assoc a b c) refl)
+
+  assoc²γδ : (a ∙ b) ∙ (c ∙ d) ≈ a ∙ ((b ∙ c) ∙ d)
+  assoc²γδ = begin
+    (a ∙ b) ∙ (c ∙ d) ≈⟨ assoc a b (c ∙ d) ⟩
+    a ∙ (b ∙ (c ∙ d)) ≈⟨ ∙-cong refl (sym (assoc b c d)) ⟩
+    a ∙ ((b ∙ c) ∙ d) ∎
+
+  assoc²δα : a ∙ ((b ∙ c) ∙ d) ≈ ((a ∙ b) ∙ c) ∙ d
+  assoc²δα = sym (trans (∙-cong (assoc a b c) refl) (assoc a (b ∙ c) d))
+
+  assoc²δγ : a ∙ ((b ∙ c) ∙ d) ≈ (a ∙ b) ∙ (c ∙ d)
+  assoc²δγ = begin
+    a ∙ ((b ∙ c) ∙ d) ≈⟨ ∙-cong refl (assoc b c d) ⟩
+    a ∙ (b ∙ (c ∙ d)) ≈⟨ sym (assoc a b (c ∙ d)) ⟩
+    (a ∙ b) ∙ (c ∙ d) ∎
+
+  assoc²εα : a ∙ (b ∙ (c ∙ d)) ≈ ((a ∙ b) ∙ c) ∙ d
+  assoc²εα = sym (trans (assoc (a ∙ b) c d) (assoc a b (c ∙ d)))
+
+  assoc²εβ : a ∙ (b ∙ (c ∙ d)) ≈ (a ∙ (b ∙ c)) ∙ d
+  assoc²εβ = sym (trans (assoc a (b ∙ c) d) (∙-cong refl (assoc b c d)))
+
+open Assoc4 public
+
+module Pulls (ab≡c : a ∙ b ≈ c) where
+
+    pullʳ : ∀ {x} → (x ∙ a) ∙ b ≈ x ∙ c
+    pullʳ {x = x} = begin
+        (x ∙ a) ∙ b ≈⟨ assoc x a b ⟩
+        x ∙ (a ∙ b) ≈⟨ ∙-cong refl ab≡c ⟩
+        x ∙ c       ∎
+
+    pullˡ : ∀ {x} → a ∙ (b ∙ x) ≈ c ∙ x
+    pullˡ {x = x} = begin
+        a ∙ (b ∙ x) ≈⟨ sym (assoc a b x) ⟩
+        (a ∙ b) ∙ x ≈⟨ ∙-cong ab≡c refl ⟩
+        c ∙ x       ∎
+
+    pull-first : ∀ {x y} → a ∙ ((b ∙ x) ∙ y) ≈ c ∙ (x ∙ y)
+    pull-first {x = x} {y = y} = begin
+      a ∙ ((b ∙ x) ∙ y) ≈⟨ ∙-cong refl (assoc b x y) ⟩
+      a ∙ (b ∙ (x ∙ y)) ≈⟨ pullˡ ⟩
+      c ∙ (x ∙ y)       ∎
+
+    pull-center : ∀ {x y} → x ∙ (a ∙ (b ∙ y)) ≈ x ∙ (c ∙ y)
+    pull-center {x = x} {y = y} = ∙-cong refl (pullˡ)
+
+    -- could be called pull₃ʳ
+    pull-last : ∀ {x y} → (x ∙ (y ∙ a)) ∙ b ≈ x ∙ (y ∙ c)
+    pull-last {x = x} {y = y} = begin
+      (x ∙ (y ∙ a)) ∙ b ≈⟨ assoc x (y ∙ a) b ⟩
+      x ∙ ((y ∙ a) ∙ b) ≈⟨ ∙-cong refl (pullʳ {x = y}) ⟩
+      x ∙ (y ∙ c)       ∎
+
+open Pulls public
+
+module Pushes (ab≡c : a ∙ b ≈ c) where
+    pushʳ : x ∙ c ≈ (x ∙ a) ∙ b
+    pushʳ {x = x} = begin
+        x ∙ c       ≈⟨ sym (∙-cong refl ab≡c) ⟩
+        x ∙ (a ∙ b) ≈⟨ sym (assoc x a b) ⟩
+        (x ∙ a) ∙ b ∎
+
+    pushˡ : c ∙ x ≈ a ∙ (b ∙ x)
+    pushˡ {x = x} = begin
+        c ∙ x       ≈⟨ sym (∙-cong ab≡c refl) ⟩
+        (a ∙ b) ∙ x ≈⟨ assoc a b x ⟩
+        a ∙ (b ∙ x) ∎
+open Pushes public
+
+-- operate in the 'center' instead (like pull/push)
+center : a ∙ b ≈ c → (d ∙ a) ∙ (b ∙ e) ≈ d ∙ (c ∙ e)
+center eq = pullʳ (pullˡ eq)
+
+-- operate on the left part, then the right part
+center⁻¹ : a ∙ b ≈ c → x ∙ y ≈ z →  a ∙ ((b ∙ x) ∙ y) ≈ c ∙ z
+center⁻¹ {a = a} {b = b} {c = c} {x = x} {y = y} {z = z} eq eq′ = begin
+  a ∙ ((b ∙ x) ∙ y) ≈⟨ ∙-cong refl (pullʳ eq′) ⟩
+  a ∙ (b ∙ z)       ≈⟨ pullˡ eq ⟩
+  c ∙ z             ∎
+
+push-center : a ∙ b ≈ c → x ∙ (c ∙ y) ≈ x ∙ (a ∙ (b ∙ y))
+push-center eq = sym (pull-center eq)
+

From 3399c61043aeb1e20a6f2be42e08dafce95c4b5b Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Tue, 1 Apr 2025 15:51:24 -0400
Subject: [PATCH 02/31]  Adds reasonig combinator for semigroup

---
 CHANGELOG.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index e38144b7f3..74b8940856 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -123,7 +123,7 @@ New modules
 
 * `Data.Sign.Show` to show a sign
 
-* `Algebra.Reasoning.SemiGroup` adding resaoning combinator for semigroup 
+* `Algebra.Reasoning.SemiGroup` adding reasoning combinator for semigroup 
 
 Additions to existing modules
 -----------------------------

From 90fe27361eccffc1dce51717c560e7f6828e1aa7 Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Tue, 1 Apr 2025 15:56:05 -0400
Subject: [PATCH 03/31]  Adds reasonig combinator for semigroup

---
 src/Algebra/Reasoning/SemiGroup.agda | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/Algebra/Reasoning/SemiGroup.agda b/src/Algebra/Reasoning/SemiGroup.agda
index 90ea09769a..ab1346e00f 100644
--- a/src/Algebra/Reasoning/SemiGroup.agda
+++ b/src/Algebra/Reasoning/SemiGroup.agda
@@ -74,7 +74,6 @@ module Assoc4  {a b c d : Carrier} where
 open Assoc4 public
 
 module Pulls (ab≡c : a ∙ b ≈ c) where
-
     pullʳ : ∀ {x} → (x ∙ a) ∙ b ≈ x ∙ c
     pullʳ {x = x} = begin
         (x ∙ a) ∙ b ≈⟨ assoc x a b ⟩
@@ -132,4 +131,3 @@ center⁻¹ {a = a} {b = b} {c = c} {x = x} {y = y} {z = z} eq eq′ = begin
 
 push-center : a ∙ b ≈ c → x ∙ (c ∙ y) ≈ x ∙ (a ∙ (b ∙ y))
 push-center eq = sym (pull-center eq)
-

From ef3282f5ad694be842f1b09ab50e8d8861751190 Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Tue, 1 Apr 2025 15:56:20 -0400
Subject: [PATCH 04/31]  Adds reasonig combinator for semigroup

---
 CHANGELOG.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 74b8940856..ac8042caab 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -123,7 +123,7 @@ New modules
 
 * `Data.Sign.Show` to show a sign
 
-* `Algebra.Reasoning.SemiGroup` adding reasoning combinator for semigroup 
+* `Algebra.Reasoning.SemiGroup` adding reasoning combinator for semigroup
 
 Additions to existing modules
 -----------------------------

From 63e88cce57c92a59efc9886270390bcb678dd56a Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Tue, 1 Apr 2025 17:35:42 -0400
Subject: [PATCH 05/31] Add some more missing reasoning combinators

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

diff --git a/src/Algebra/Reasoning/SemiGroup.agda b/src/Algebra/Reasoning/SemiGroup.agda
index ab1346e00f..663becc068 100644
--- a/src/Algebra/Reasoning/SemiGroup.agda
+++ b/src/Algebra/Reasoning/SemiGroup.agda
@@ -9,7 +9,7 @@
 
 open import Algebra using (Semigroup)
 
-module Algebra.Reasoning.SemiGroup {o ℓ} (S : Semigroup o ℓ) where
+module Algebra.Reasoning.Semigroup {o ℓ} (S : Semigroup o ℓ) where
 
 open Semigroup S
     using (Carrier; _∙_; _≈_; setoid; trans ; refl; sym; assoc; ∙-cong)

From bb7ce151ce14f93bca26c7bc6a33af89746c5f08 Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Tue, 1 Apr 2025 18:06:12 -0400
Subject: [PATCH 06/31] add module Extends

---
 src/Algebra/Reasoning/SemiGroup.agda | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/src/Algebra/Reasoning/SemiGroup.agda b/src/Algebra/Reasoning/SemiGroup.agda
index 663becc068..e2290fc84d 100644
--- a/src/Algebra/Reasoning/SemiGroup.agda
+++ b/src/Algebra/Reasoning/SemiGroup.agda
@@ -131,3 +131,27 @@ center⁻¹ {a = a} {b = b} {c = c} {x = x} {y = y} {z = z} eq eq′ = begin
 
 push-center : a ∙ b ≈ c → x ∙ (c ∙ y) ≈ x ∙ (a ∙ (b ∙ y))
 push-center eq = sym (pull-center eq)
+
+module Extends {a b c d : Carrier} (s : a ∙ b ≈ c ∙ d) where
+  -- rewrite (x ∙ a) ∙ b to (x ∙ c) ∙ d
+  extendˡ : (x ∙ a) ∙ b ≈ (x ∙ c) ∙ d
+  extendˡ {x = x} = begin
+    (x ∙ a) ∙ b ≈⟨ pullʳ s ⟩
+    x ∙ (c ∙ d) ≈⟨ sym (assoc x c d) ⟩
+    (x ∙ c) ∙ d ∎
+
+  -- rewrite a ∙ (b ∙ x) to c ∙ (d ∙ x)
+  extendʳ : a ∙ (b ∙ x) ≈ c ∙ (d ∙ x)
+  extendʳ {x = x} = begin
+    a ∙ (b ∙ x) ≈⟨ pullˡ s ⟩
+    (c ∙ d) ∙ x ≈⟨ assoc c d x ⟩
+    c ∙ (d ∙ x) ∎
+
+  -- rewrite (x ∙ a) ∙ (b ∙ y) to (x ∙ c) ∙ (d ∙ y)
+  extend² : ∀ x y → (x ∙ a) ∙ (b ∙ y) ≈ (x ∙ c) ∙ (d ∙ y)
+  extend² x y = begin
+    (x ∙ a) ∙ (b ∙ y) ≈⟨ pullʳ (extendʳ {x = y}) ⟩
+    x ∙ (c ∙ (d ∙ y)) ≈⟨ sym (assoc x c (d ∙ y)) ⟩
+    (x ∙ c) ∙ (d ∙ y) ∎
+
+open Extends public

From 885d7a0bd44eb569e7181d106bf1a2458f206d18 Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Tue, 1 Apr 2025 18:29:34 -0400
Subject: [PATCH 07/31] rename SemiGroup to Semigroup

---
 src/Algebra/Reasoning/{SemiGroup.agda => Semigroup.agda} | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)
 rename src/Algebra/Reasoning/{SemiGroup.agda => Semigroup.agda} (99%)

diff --git a/src/Algebra/Reasoning/SemiGroup.agda b/src/Algebra/Reasoning/Semigroup.agda
similarity index 99%
rename from src/Algebra/Reasoning/SemiGroup.agda
rename to src/Algebra/Reasoning/Semigroup.agda
index e2290fc84d..3d9b758836 100644
--- a/src/Algebra/Reasoning/SemiGroup.agda
+++ b/src/Algebra/Reasoning/Semigroup.agda
@@ -154,4 +154,4 @@ module Extends {a b c d : Carrier} (s : a ∙ b ≈ c ∙ d) where
     x ∙ (c ∙ (d ∙ y)) ≈⟨ sym (assoc x c (d ∙ y)) ⟩
     (x ∙ c) ∙ (d ∙ y) ∎
 
-open Extends public
+open Extends public
\ No newline at end of file

From ad54a5b083391e334388098521ecc012ecc46647 Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Tue, 1 Apr 2025 18:31:49 -0400
Subject: [PATCH 08/31] fix-whitespace

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

diff --git a/src/Algebra/Reasoning/Semigroup.agda b/src/Algebra/Reasoning/Semigroup.agda
index 3d9b758836..e2290fc84d 100644
--- a/src/Algebra/Reasoning/Semigroup.agda
+++ b/src/Algebra/Reasoning/Semigroup.agda
@@ -154,4 +154,4 @@ module Extends {a b c d : Carrier} (s : a ∙ b ≈ c ∙ d) where
     x ∙ (c ∙ (d ∙ y)) ≈⟨ sym (assoc x c (d ∙ y)) ⟩
     (x ∙ c) ∙ (d ∙ y) ∎
 
-open Extends public
\ No newline at end of file
+open Extends public

From 2b511c2b9343a747584cb622cde9bc25a560747a Mon Sep 17 00:00:00 2001
From: Jacques <149587529+jmougeot@users.noreply.github.com>
Date: Wed, 2 Apr 2025 13:36:47 -0400
Subject: [PATCH 09/31] Update CHANGELOG.md

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
---
 CHANGELOG.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index ac8042caab..404194cf78 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -123,7 +123,7 @@ New modules
 
 * `Data.Sign.Show` to show a sign
 
-* `Algebra.Reasoning.SemiGroup` adding reasoning combinator for semigroup
+* `Algebra.Reasoning.Semigroup` adding reasoning combinators for semigroups
 
 Additions to existing modules
 -----------------------------

From 8151123dd9a6d7b0bdb9b89377eba61eb9cbaded Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Thu, 3 Apr 2025 17:44:24 -0400
Subject: [PATCH 10/31] New names

---
 CHANGELOG.md                                  |   2 +-
 .../Properties/Semigroup/Reasoning.agda       | 144 ++++++++++++++++
 src/Algebra/Reasoning/Semigroup.agda          | 157 ------------------
 3 files changed, 145 insertions(+), 158 deletions(-)
 create mode 100644 src/Algebra/Properties/Semigroup/Reasoning.agda
 delete mode 100644 src/Algebra/Reasoning/Semigroup.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 404194cf78..03e4631c65 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -123,7 +123,7 @@ New modules
 
 * `Data.Sign.Show` to show a sign
 
-* `Algebra.Reasoning.Semigroup` adding reasoning combinators for semigroups
+* `AlgebraPropreties.Semigroup.Reasoning` adding reasoning combinators for semigroups
 
 Additions to existing modules
 -----------------------------
diff --git a/src/Algebra/Properties/Semigroup/Reasoning.agda b/src/Algebra/Properties/Semigroup/Reasoning.agda
new file mode 100644
index 0000000000..58c35f6699
--- /dev/null
+++ b/src/Algebra/Properties/Semigroup/Reasoning.agda
@@ -0,0 +1,144 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Equational reasoning for semigroups
+-- (Utilities for associativity reasoning, pulling and pushing operations)
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Algebra.Bundles using (Semigroup)
+
+module Algebra.Properties.Semigroup.Reasoning {o ℓ} (S : Semigroup o ℓ) where
+
+open import Algebra.Structures using (IsMagma)
+
+open Semigroup S
+    using (Carrier; _∙_; _≈_; setoid; trans; refl; sym; assoc; ∙-cong; isMagma)
+open import Relation.Binary.Reasoning.Setoid setoid
+open IsMagma isMagma using (∙-congˡ; ∙-congʳ)
+
+private
+ variable
+    u v w x y z : Carrier
+
+module Assoc4  {u v w x : Carrier} where
+  [[u∙v]∙w]∙x≈u∙[[v∙w]∙x] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ ((v ∙ w) ∙ x)
+  [[u∙v]∙w]∙x≈u∙[[v∙w]∙x] = trans (∙-congʳ (assoc u v w)) (assoc u (v ∙ w) x)
+
+  [[u∙v]∙w]∙x≈u∙[v∙[w∙x]] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ (v ∙ (w ∙ x))
+  [[u∙v]∙w]∙x≈u∙[v∙[w∙x]] = trans (assoc (u ∙ v) w x) (assoc u v (w ∙ x))
+
+  [u∙[v∙w]]∙x≈[u∙v]∙[w∙x] : (u ∙ (v ∙ w)) ∙ x ≈ (u ∙ v) ∙ (w ∙ x)
+  [u∙[v∙w]]∙x≈[u∙v]∙[w∙x] = trans (sym (∙-congʳ (assoc u v w))) (assoc (u ∙ v) w x)
+
+  [u∙[v∙w]]∙x≈u∙[v∙[w∙x]] : (u ∙ (v ∙ w)) ∙ x ≈ u ∙ (v ∙ (w ∙ x))
+  [u∙[v∙w]]∙x≈u∙[v∙[w∙x]] = trans (assoc u (v ∙ w) x) (∙-congˡ (assoc v w x))
+
+  [u∙v]∙[w∙x]≈[u∙[v∙w]]∙x : (u ∙ v) ∙ (w ∙ x) ≈ (u ∙ (v ∙ w)) ∙ x
+  [u∙v]∙[w∙x]≈[u∙[v∙w]]∙x = trans (sym (assoc (u ∙ v) w x)) (∙-congʳ (assoc u v w))
+
+  [u∙v]∙[w∙x]≈u∙[[v∙w]]∙x] : (u ∙ v) ∙ (w ∙ x) ≈ u ∙ ((v ∙ w) ∙ x)
+  [u∙v]∙[w∙x]≈u∙[[v∙w]]∙x] = begin
+    (u ∙ v) ∙ (w ∙ x) ≈⟨ assoc u v (w ∙ x) ⟩
+    u ∙ (v ∙ (w ∙ x)) ≈⟨ ∙-congˡ (sym (assoc v w x)) ⟩
+    u ∙ ((v ∙ w) ∙ x) ∎
+
+  u∙[[v∙w]∙x]≈[[u∙v]∙w]∙x : u ∙ ((v ∙ w) ∙ x) ≈ ((u ∙ v) ∙ w) ∙ x
+  u∙[[v∙w]∙x]≈[[u∙v]∙w]∙x = sym (trans (∙-congʳ (assoc u v w)) (assoc u (v ∙ w) x))
+
+  u∙[v∙w]]∙x]≈[u∙v]∙[w∙x] : u ∙ ((v ∙ w) ∙ x) ≈ (u ∙ v) ∙ (w ∙ x)
+  u∙[v∙w]]∙x]≈[u∙v]∙[w∙x] = begin
+    u ∙ ((v ∙ w) ∙ x) ≈⟨ ∙-congˡ (assoc v w x) ⟩
+    u ∙ (v ∙ (w ∙ x)) ≈⟨ assoc u v (w ∙ x) ⟨
+    (u ∙ v) ∙ (w ∙ x) ∎
+
+  u∙[v∙[w∙x]]≈[[u∙v]∙w]∙x : u ∙ (v ∙ (w ∙ x)) ≈ ((u ∙ v) ∙ w) ∙ x
+  u∙[v∙[w∙x]]≈[[u∙v]∙w]∙x = sym (trans (assoc (u ∙ v) w x) (assoc u v (w ∙ x)))
+
+  u∙[v∙[w∙x]]≈[u∙[v∙w]]∙x : u ∙ (v ∙ (w ∙ x)) ≈ (u ∙ (v ∙ w)) ∙ x
+  u∙[v∙[w∙x]]≈[u∙[v∙w]]∙x = sym (trans (assoc u (v ∙ w) x) (∙-congˡ (assoc v w x)))
+
+open Assoc4 public
+
+module Pulls (uv≡w : u ∙ v ≈ w) where
+    pullʳ : ∀ {x} → (x ∙ u) ∙ v ≈ x ∙ w
+    pullʳ {x = x} = begin
+        (x ∙ u) ∙ v ≈⟨ assoc x u v ⟩
+        x ∙ (u ∙ v) ≈⟨ ∙-congˡ uv≡w ⟩
+        x ∙ w       ∎
+
+    pullˡ : ∀ {x} → u ∙ (v ∙ x) ≈ w ∙ x
+    pullˡ {x = x} = begin
+        u ∙ (v ∙ x) ≈⟨ assoc u v x ⟨
+        (u ∙ v) ∙ x ≈⟨ ∙-congʳ uv≡w ⟩
+        w ∙ x       ∎
+
+    pull-first : ∀ {x y} → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ (x ∙ y)
+    pull-first {x = x} {y = y} = begin
+      u ∙ ((v ∙ x) ∙ y) ≈⟨ ∙-congˡ (assoc v x y) ⟩
+      u ∙ (v ∙ (x ∙ y)) ≈⟨ pullˡ ⟩
+      w ∙ (x ∙ y)       ∎
+
+    pull-center : ∀ {x y} → x ∙ (u ∙ (v ∙ y)) ≈ x ∙ (w ∙ y)
+    pull-center {x = x} {y = y} = ∙-congˡ (pullˡ)
+
+    -- could be called pull₃ʳ
+    pull-last : ∀ {x y} → (x ∙ (y ∙ u)) ∙ v ≈ x ∙ (y ∙ w)
+    pull-last {x = x} {y = y} = begin
+      (x ∙ (y ∙ u)) ∙ v ≈⟨ assoc x (y ∙ u) v ⟩
+      x ∙ ((y ∙ u) ∙ v) ≈⟨ ∙-congˡ (pullʳ {x = y}) ⟩
+      x ∙ (y ∙ w)       ∎
+
+open Pulls public
+
+module Pushes (uv≡w : u ∙ v ≈ w) where
+    pushʳ : x ∙ w ≈ (x ∙ u) ∙ v
+    pushʳ {x = x} = begin
+        x ∙ w       ≈⟨ ∙-congˡ uv≡w ⟨
+        x ∙ (u ∙ v) ≈⟨ assoc x u v ⟨
+        (x ∙ u) ∙ v ∎
+
+    pushˡ : w ∙ x ≈ u ∙ (v ∙ x)
+    pushˡ {x = x} = begin
+        w ∙ x       ≈⟨ ∙-congʳ uv≡w ⟨
+        (u ∙ v) ∙ x ≈⟨ assoc u v x ⟩
+        u ∙ (v ∙ x) ∎
+open Pushes public
+
+module Center (eq : u ∙ v ≈ w) where
+  center : (x ∙ u) ∙ (v ∙ y) ≈ x ∙ (w ∙ y)
+  center = pullʳ (pullˡ eq)
+
+  center⁻¹ : x ∙ y ≈ z →  u ∙ ((v ∙ x) ∙ y) ≈ w ∙ z
+  center⁻¹ {x = x} {y = y} {z = z} xy≈z = begin
+    u ∙ ((v ∙ x) ∙ y) ≈⟨ ∙-congˡ (pullʳ xy≈z) ⟩
+    u ∙ (v ∙ z)       ≈⟨ pullˡ eq ⟩
+    w ∙ z             ∎
+
+  push-center : x ∙ (w ∙ y) ≈ x ∙ (u ∙ (v ∙ y))
+  push-center = sym (pull-center eq)
+
+open Center public
+
+module Extends {u v w x : Carrier} (s : u ∙ v ≈ w ∙ x) where
+  extendˡ : (y ∙ u) ∙ v ≈ (y ∙ w) ∙ x
+  extendˡ {y = y} = begin
+    (y ∙ u) ∙ v ≈⟨ pullʳ s ⟩
+    y ∙ (w ∙ x) ≈⟨ assoc y w x ⟨
+    (y ∙ w) ∙ x ∎
+
+  extendʳ : u ∙ (v ∙ y) ≈ w ∙ (x ∙ y)
+  extendʳ {y = y} = begin
+    u ∙ (v ∙ y) ≈⟨ pullˡ s ⟩
+    (w ∙ x) ∙ y ≈⟨ assoc w x y ⟩
+    w ∙ (x ∙ y) ∎
+
+  extend² : ∀ y z → (y ∙ u) ∙ (v ∙ z) ≈ (y ∙ w) ∙ (x ∙ z)
+  extend² y z = begin
+    (y ∙ u) ∙ (v ∙ z) ≈⟨ pullʳ (extendʳ {y = z}) ⟩
+    y ∙ (w ∙ (x ∙ z)) ≈⟨ assoc y w (x ∙ z) ⟨
+    (y ∙ w) ∙ (x ∙ z) ∎
+
+open Extends public
+
diff --git a/src/Algebra/Reasoning/Semigroup.agda b/src/Algebra/Reasoning/Semigroup.agda
deleted file mode 100644
index e2290fc84d..0000000000
--- a/src/Algebra/Reasoning/Semigroup.agda
+++ /dev/null
@@ -1,157 +0,0 @@
-------------------------------------------------------------------------
--- The Agda standard library
---
--- Equational reasoning for semigroups
--- (Utilities for associativity reasoning, pulling and pushing operations)
-------------------------------------------------------------------------
-
-{-# OPTIONS --cubical-compatible --safe #-}
-
-open import Algebra using (Semigroup)
-
-module Algebra.Reasoning.Semigroup {o ℓ} (S : Semigroup o ℓ) where
-
-open Semigroup S
-    using (Carrier; _∙_; _≈_; setoid; trans ; refl; sym; assoc; ∙-cong)
-open import Relation.Binary.Reasoning.Setoid setoid
-
-private
- variable
-    a b c d e x y z : Carrier
-
-module Assoc4  {a b c d : Carrier} where
-    {-
-  Explanation of naming scheme:
-
-  Each successive association is given a Greek letter, from 'α' associated all
-  the way to the left, to 'ε' associated all the way to the right. Then,
-  'assoc²XY' is the proof that X is equal to Y. Explicitly:
-
-  α = ((a ∙ b) ∙ c) ∙ d
-  β = (a ∙ (b ∙ c)) ∙ d
-  γ = (a ∙ b) ∙ (c ∙ d)
-  δ = a ∙ ((b ∙ c) ∙ d)
-  ε = a ∙ (b ∙ (c ∙ d))
-
-  Only reassociations that need two assoc steps are defined here.
-  -}
-  assoc²αδ : ((a ∙ b) ∙ c) ∙ d ≈ a ∙ ((b ∙ c) ∙ d)
-  assoc²αδ = trans (∙-cong (assoc a b c) refl) (assoc a (b ∙ c) d)
-
-  assoc²αε : ((a ∙ b) ∙ c) ∙ d ≈ a ∙ (b ∙ (c ∙ d))
-  assoc²αε = trans (assoc (a ∙ b) c d) (assoc a b (c ∙ d))
-
-  assoc²βγ : (a ∙ (b ∙ c)) ∙ d ≈ (a ∙ b) ∙ (c ∙ d)
-  assoc²βγ = trans (sym (∙-cong (assoc a b c) refl)) (assoc (a ∙ b) c d)
-
-  assoc²βε : (a ∙ (b ∙ c)) ∙ d ≈ a ∙ (b ∙ (c ∙ d))
-  assoc²βε = trans (assoc a (b ∙ c) d) (∙-cong refl (assoc b c d))
-
-  assoc²γβ : (a ∙ b) ∙ (c ∙ d) ≈ (a ∙ (b ∙ c)) ∙ d
-  assoc²γβ = trans (sym (assoc (a ∙ b) c d)) (∙-cong (assoc a b c) refl)
-
-  assoc²γδ : (a ∙ b) ∙ (c ∙ d) ≈ a ∙ ((b ∙ c) ∙ d)
-  assoc²γδ = begin
-    (a ∙ b) ∙ (c ∙ d) ≈⟨ assoc a b (c ∙ d) ⟩
-    a ∙ (b ∙ (c ∙ d)) ≈⟨ ∙-cong refl (sym (assoc b c d)) ⟩
-    a ∙ ((b ∙ c) ∙ d) ∎
-
-  assoc²δα : a ∙ ((b ∙ c) ∙ d) ≈ ((a ∙ b) ∙ c) ∙ d
-  assoc²δα = sym (trans (∙-cong (assoc a b c) refl) (assoc a (b ∙ c) d))
-
-  assoc²δγ : a ∙ ((b ∙ c) ∙ d) ≈ (a ∙ b) ∙ (c ∙ d)
-  assoc²δγ = begin
-    a ∙ ((b ∙ c) ∙ d) ≈⟨ ∙-cong refl (assoc b c d) ⟩
-    a ∙ (b ∙ (c ∙ d)) ≈⟨ sym (assoc a b (c ∙ d)) ⟩
-    (a ∙ b) ∙ (c ∙ d) ∎
-
-  assoc²εα : a ∙ (b ∙ (c ∙ d)) ≈ ((a ∙ b) ∙ c) ∙ d
-  assoc²εα = sym (trans (assoc (a ∙ b) c d) (assoc a b (c ∙ d)))
-
-  assoc²εβ : a ∙ (b ∙ (c ∙ d)) ≈ (a ∙ (b ∙ c)) ∙ d
-  assoc²εβ = sym (trans (assoc a (b ∙ c) d) (∙-cong refl (assoc b c d)))
-
-open Assoc4 public
-
-module Pulls (ab≡c : a ∙ b ≈ c) where
-    pullʳ : ∀ {x} → (x ∙ a) ∙ b ≈ x ∙ c
-    pullʳ {x = x} = begin
-        (x ∙ a) ∙ b ≈⟨ assoc x a b ⟩
-        x ∙ (a ∙ b) ≈⟨ ∙-cong refl ab≡c ⟩
-        x ∙ c       ∎
-
-    pullˡ : ∀ {x} → a ∙ (b ∙ x) ≈ c ∙ x
-    pullˡ {x = x} = begin
-        a ∙ (b ∙ x) ≈⟨ sym (assoc a b x) ⟩
-        (a ∙ b) ∙ x ≈⟨ ∙-cong ab≡c refl ⟩
-        c ∙ x       ∎
-
-    pull-first : ∀ {x y} → a ∙ ((b ∙ x) ∙ y) ≈ c ∙ (x ∙ y)
-    pull-first {x = x} {y = y} = begin
-      a ∙ ((b ∙ x) ∙ y) ≈⟨ ∙-cong refl (assoc b x y) ⟩
-      a ∙ (b ∙ (x ∙ y)) ≈⟨ pullˡ ⟩
-      c ∙ (x ∙ y)       ∎
-
-    pull-center : ∀ {x y} → x ∙ (a ∙ (b ∙ y)) ≈ x ∙ (c ∙ y)
-    pull-center {x = x} {y = y} = ∙-cong refl (pullˡ)
-
-    -- could be called pull₃ʳ
-    pull-last : ∀ {x y} → (x ∙ (y ∙ a)) ∙ b ≈ x ∙ (y ∙ c)
-    pull-last {x = x} {y = y} = begin
-      (x ∙ (y ∙ a)) ∙ b ≈⟨ assoc x (y ∙ a) b ⟩
-      x ∙ ((y ∙ a) ∙ b) ≈⟨ ∙-cong refl (pullʳ {x = y}) ⟩
-      x ∙ (y ∙ c)       ∎
-
-open Pulls public
-
-module Pushes (ab≡c : a ∙ b ≈ c) where
-    pushʳ : x ∙ c ≈ (x ∙ a) ∙ b
-    pushʳ {x = x} = begin
-        x ∙ c       ≈⟨ sym (∙-cong refl ab≡c) ⟩
-        x ∙ (a ∙ b) ≈⟨ sym (assoc x a b) ⟩
-        (x ∙ a) ∙ b ∎
-
-    pushˡ : c ∙ x ≈ a ∙ (b ∙ x)
-    pushˡ {x = x} = begin
-        c ∙ x       ≈⟨ sym (∙-cong ab≡c refl) ⟩
-        (a ∙ b) ∙ x ≈⟨ assoc a b x ⟩
-        a ∙ (b ∙ x) ∎
-open Pushes public
-
--- operate in the 'center' instead (like pull/push)
-center : a ∙ b ≈ c → (d ∙ a) ∙ (b ∙ e) ≈ d ∙ (c ∙ e)
-center eq = pullʳ (pullˡ eq)
-
--- operate on the left part, then the right part
-center⁻¹ : a ∙ b ≈ c → x ∙ y ≈ z →  a ∙ ((b ∙ x) ∙ y) ≈ c ∙ z
-center⁻¹ {a = a} {b = b} {c = c} {x = x} {y = y} {z = z} eq eq′ = begin
-  a ∙ ((b ∙ x) ∙ y) ≈⟨ ∙-cong refl (pullʳ eq′) ⟩
-  a ∙ (b ∙ z)       ≈⟨ pullˡ eq ⟩
-  c ∙ z             ∎
-
-push-center : a ∙ b ≈ c → x ∙ (c ∙ y) ≈ x ∙ (a ∙ (b ∙ y))
-push-center eq = sym (pull-center eq)
-
-module Extends {a b c d : Carrier} (s : a ∙ b ≈ c ∙ d) where
-  -- rewrite (x ∙ a) ∙ b to (x ∙ c) ∙ d
-  extendˡ : (x ∙ a) ∙ b ≈ (x ∙ c) ∙ d
-  extendˡ {x = x} = begin
-    (x ∙ a) ∙ b ≈⟨ pullʳ s ⟩
-    x ∙ (c ∙ d) ≈⟨ sym (assoc x c d) ⟩
-    (x ∙ c) ∙ d ∎
-
-  -- rewrite a ∙ (b ∙ x) to c ∙ (d ∙ x)
-  extendʳ : a ∙ (b ∙ x) ≈ c ∙ (d ∙ x)
-  extendʳ {x = x} = begin
-    a ∙ (b ∙ x) ≈⟨ pullˡ s ⟩
-    (c ∙ d) ∙ x ≈⟨ assoc c d x ⟩
-    c ∙ (d ∙ x) ∎
-
-  -- rewrite (x ∙ a) ∙ (b ∙ y) to (x ∙ c) ∙ (d ∙ y)
-  extend² : ∀ x y → (x ∙ a) ∙ (b ∙ y) ≈ (x ∙ c) ∙ (d ∙ y)
-  extend² x y = begin
-    (x ∙ a) ∙ (b ∙ y) ≈⟨ pullʳ (extendʳ {x = y}) ⟩
-    x ∙ (c ∙ (d ∙ y)) ≈⟨ sym (assoc x c (d ∙ y)) ⟩
-    (x ∙ c) ∙ (d ∙ y) ∎
-
-open Extends public

From 2361b4085ceef57c69fc5232fcbee804333a6a8e Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Thu, 3 Apr 2025 19:44:26 -0400
Subject: [PATCH 11/31] improve syntx

---
 src/Algebra/Properties/Semigroup/Reasoning.agda | 12 ++++--------
 1 file changed, 4 insertions(+), 8 deletions(-)

diff --git a/src/Algebra/Properties/Semigroup/Reasoning.agda b/src/Algebra/Properties/Semigroup/Reasoning.agda
index 58c35f6699..81ac2135b7 100644
--- a/src/Algebra/Properties/Semigroup/Reasoning.agda
+++ b/src/Algebra/Properties/Semigroup/Reasoning.agda
@@ -94,16 +94,11 @@ open Pulls public
 
 module Pushes (uv≡w : u ∙ v ≈ w) where
     pushʳ : x ∙ w ≈ (x ∙ u) ∙ v
-    pushʳ {x = x} = begin
-        x ∙ w       ≈⟨ ∙-congˡ uv≡w ⟨
-        x ∙ (u ∙ v) ≈⟨ assoc x u v ⟨
-        (x ∙ u) ∙ v ∎
+    pushʳ = sym (pullʳ uv≡w)
 
     pushˡ : w ∙ x ≈ u ∙ (v ∙ x)
-    pushˡ {x = x} = begin
-        w ∙ x       ≈⟨ ∙-congʳ uv≡w ⟨
-        (u ∙ v) ∙ x ≈⟨ assoc u v x ⟩
-        u ∙ (v ∙ x) ∎
+    pushˡ = sym (pullˡ uv≡w)
+
 open Pushes public
 
 module Center (eq : u ∙ v ≈ w) where
@@ -142,3 +137,4 @@ module Extends {u v w x : Carrier} (s : u ∙ v ≈ w ∙ x) where
 
 open Extends public
 
+ 
\ No newline at end of file

From 503c693ac6dffd67a4fb4d0873ad7fff86fc9922 Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Thu, 3 Apr 2025 19:45:05 -0400
Subject: [PATCH 12/31] fix-whitespace

---
 src/Algebra/Properties/Semigroup/Reasoning.agda | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/Algebra/Properties/Semigroup/Reasoning.agda b/src/Algebra/Properties/Semigroup/Reasoning.agda
index 81ac2135b7..3c2fdd38f9 100644
--- a/src/Algebra/Properties/Semigroup/Reasoning.agda
+++ b/src/Algebra/Properties/Semigroup/Reasoning.agda
@@ -137,4 +137,3 @@ module Extends {u v w x : Carrier} (s : u ∙ v ≈ w ∙ x) where
 
 open Extends public
 
- 
\ No newline at end of file

From 0d5c9ed1181ffe2af14b963423adc9047f3cd913 Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Mon, 7 Apr 2025 13:56:23 -0400
Subject: [PATCH 13/31] Name changes

---
 .../Properties/Semigroup/Reasoning.agda       | 129 +++++++-----------
 1 file changed, 50 insertions(+), 79 deletions(-)

diff --git a/src/Algebra/Properties/Semigroup/Reasoning.agda b/src/Algebra/Properties/Semigroup/Reasoning.agda
index 3c2fdd38f9..c97e42be45 100644
--- a/src/Algebra/Properties/Semigroup/Reasoning.agda
+++ b/src/Algebra/Properties/Semigroup/Reasoning.agda
@@ -14,126 +14,97 @@ module Algebra.Properties.Semigroup.Reasoning {o ℓ} (S : Semigroup o ℓ) wher
 open import Algebra.Structures using (IsMagma)
 
 open Semigroup S
-    using (Carrier; _∙_; _≈_; setoid; trans; refl; sym; assoc; ∙-cong; isMagma)
+  using (Carrier; _∙_; _≈_; setoid; trans; refl; sym; assoc; ∙-cong; isMagma
+  ; ∙-congˡ; ∙-congʳ)
 open import Relation.Binary.Reasoning.Setoid setoid
-open IsMagma isMagma using (∙-congˡ; ∙-congʳ)
 
 private
  variable
     u v w x y z : Carrier
 
+
 module Assoc4  {u v w x : Carrier} where
-  [[u∙v]∙w]∙x≈u∙[[v∙w]∙x] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ ((v ∙ w) ∙ x)
-  [[u∙v]∙w]∙x≈u∙[[v∙w]∙x] = trans (∙-congʳ (assoc u v w)) (assoc u (v ∙ w) x)
+  [uv∙w]x≈u[vw∙x] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ ((v ∙ w) ∙ x)
+  [uv∙w]x≈u[vw∙x] = trans (∙-congʳ (assoc u v w)) (assoc u (v ∙ w) x)
 
-  [[u∙v]∙w]∙x≈u∙[v∙[w∙x]] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ (v ∙ (w ∙ x))
-  [[u∙v]∙w]∙x≈u∙[v∙[w∙x]] = trans (assoc (u ∙ v) w x) (assoc u v (w ∙ x))
+  [uv∙w]x≈u[v∙wx] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ (v ∙ (w ∙ x))
+  [uv∙w]x≈u[v∙wx] = trans (assoc (u ∙ v) w x) (assoc u v (w ∙ x))
 
-  [u∙[v∙w]]∙x≈[u∙v]∙[w∙x] : (u ∙ (v ∙ w)) ∙ x ≈ (u ∙ v) ∙ (w ∙ x)
-  [u∙[v∙w]]∙x≈[u∙v]∙[w∙x] = trans (sym (∙-congʳ (assoc u v w))) (assoc (u ∙ v) w x)
+  [u∙vw]x≈uv∙wx : (u ∙ (v ∙ w)) ∙ x ≈ (u ∙ v) ∙ (w ∙ x)
+  [u∙vw]x≈uv∙wx = trans (sym (∙-congʳ (assoc u v w))) (assoc (u ∙ v) w x)
 
-  [u∙[v∙w]]∙x≈u∙[v∙[w∙x]] : (u ∙ (v ∙ w)) ∙ x ≈ u ∙ (v ∙ (w ∙ x))
-  [u∙[v∙w]]∙x≈u∙[v∙[w∙x]] = trans (assoc u (v ∙ w) x) (∙-congˡ (assoc v w x))
+  [u∙vw]x≈u[v∙wx] : (u ∙ (v ∙ w)) ∙ x ≈ u ∙ (v ∙ (w ∙ x))
+  [u∙vw]x≈u[v∙wx] = trans (assoc u (v ∙ w) x) (∙-congˡ (assoc v w x))
 
-  [u∙v]∙[w∙x]≈[u∙[v∙w]]∙x : (u ∙ v) ∙ (w ∙ x) ≈ (u ∙ (v ∙ w)) ∙ x
-  [u∙v]∙[w∙x]≈[u∙[v∙w]]∙x = trans (sym (assoc (u ∙ v) w x)) (∙-congʳ (assoc u v w))
+  uv∙wx≈[u∙vw]x : (u ∙ v) ∙ (w ∙ x) ≈ (u ∙ (v ∙ w)) ∙ x
+  uv∙wx≈[u∙vw]x = trans (sym (assoc (u ∙ v) w x)) (∙-congʳ (assoc u v w))
 
-  [u∙v]∙[w∙x]≈u∙[[v∙w]]∙x] : (u ∙ v) ∙ (w ∙ x) ≈ u ∙ ((v ∙ w) ∙ x)
-  [u∙v]∙[w∙x]≈u∙[[v∙w]]∙x] = begin
-    (u ∙ v) ∙ (w ∙ x) ≈⟨ assoc u v (w ∙ x) ⟩
-    u ∙ (v ∙ (w ∙ x)) ≈⟨ ∙-congˡ (sym (assoc v w x)) ⟩
-    u ∙ ((v ∙ w) ∙ x) ∎
+  uv∙wx≈u[vw∙x] : (u ∙ v) ∙ (w ∙ x) ≈ u ∙ ((v ∙ w) ∙ x)
+  uv∙wx≈u[vw∙x] = trans (assoc u v (w ∙ x)) (∙-congˡ (sym (assoc v w x)))
 
-  u∙[[v∙w]∙x]≈[[u∙v]∙w]∙x : u ∙ ((v ∙ w) ∙ x) ≈ ((u ∙ v) ∙ w) ∙ x
-  u∙[[v∙w]∙x]≈[[u∙v]∙w]∙x = sym (trans (∙-congʳ (assoc u v w)) (assoc u (v ∙ w) x))
+  u[vw∙x]≈[uv∙w]x : u ∙ ((v ∙ w) ∙ x) ≈ ((u ∙ v) ∙ w) ∙ x
+  u[vw∙x]≈[uv∙w]x = sym (trans (∙-congʳ (assoc u v w)) (assoc u (v ∙ w) x))
 
-  u∙[v∙w]]∙x]≈[u∙v]∙[w∙x] : u ∙ ((v ∙ w) ∙ x) ≈ (u ∙ v) ∙ (w ∙ x)
-  u∙[v∙w]]∙x]≈[u∙v]∙[w∙x] = begin
-    u ∙ ((v ∙ w) ∙ x) ≈⟨ ∙-congˡ (assoc v w x) ⟩
-    u ∙ (v ∙ (w ∙ x)) ≈⟨ assoc u v (w ∙ x) ⟨
-    (u ∙ v) ∙ (w ∙ x) ∎
+  u[vw∙x]≈uv∙wx : u ∙ ((v ∙ w) ∙ x) ≈ (u ∙ v) ∙ (w ∙ x)
+  u[vw∙x]≈uv∙wx = trans (∙-congˡ (assoc v w x)) (sym (assoc u v (w ∙ x)))
 
-  u∙[v∙[w∙x]]≈[[u∙v]∙w]∙x : u ∙ (v ∙ (w ∙ x)) ≈ ((u ∙ v) ∙ w) ∙ x
-  u∙[v∙[w∙x]]≈[[u∙v]∙w]∙x = sym (trans (assoc (u ∙ v) w x) (assoc u v (w ∙ x)))
+  u[v∙wx]≈[uv∙w]x : u ∙ (v ∙ (w ∙ x)) ≈ ((u ∙ v) ∙ w) ∙ x
+  u[v∙wx]≈[uv∙w]x = sym (trans (assoc (u ∙ v) w x) (assoc u v (w ∙ x)))
 
-  u∙[v∙[w∙x]]≈[u∙[v∙w]]∙x : u ∙ (v ∙ (w ∙ x)) ≈ (u ∙ (v ∙ w)) ∙ x
-  u∙[v∙[w∙x]]≈[u∙[v∙w]]∙x = sym (trans (assoc u (v ∙ w) x) (∙-congˡ (assoc v w x)))
+  u[v∙wx]≈[u∙vw]x : u ∙ (v ∙ (w ∙ x)) ≈ (u ∙ (v ∙ w)) ∙ x
+  u[v∙wx]≈[u∙vw]x  = sym (trans (assoc u (v ∙ w) x) (∙-congˡ (assoc v w x)))
 
 open Assoc4 public
 
 module Pulls (uv≡w : u ∙ v ≈ w) where
-    pullʳ : ∀ {x} → (x ∙ u) ∙ v ≈ x ∙ w
-    pullʳ {x = x} = begin
-        (x ∙ u) ∙ v ≈⟨ assoc x u v ⟩
-        x ∙ (u ∙ v) ≈⟨ ∙-congˡ uv≡w ⟩
-        x ∙ w       ∎
-
-    pullˡ : ∀ {x} → u ∙ (v ∙ x) ≈ w ∙ x
-    pullˡ {x = x} = begin
-        u ∙ (v ∙ x) ≈⟨ assoc u v x ⟨
-        (u ∙ v) ∙ x ≈⟨ ∙-congʳ uv≡w ⟩
-        w ∙ x       ∎
-
-    pull-first : ∀ {x y} → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ (x ∙ y)
-    pull-first {x = x} {y = y} = begin
-      u ∙ ((v ∙ x) ∙ y) ≈⟨ ∙-congˡ (assoc v x y) ⟩
-      u ∙ (v ∙ (x ∙ y)) ≈⟨ pullˡ ⟩
-      w ∙ (x ∙ y)       ∎
-
-    pull-center : ∀ {x y} → x ∙ (u ∙ (v ∙ y)) ≈ x ∙ (w ∙ y)
-    pull-center {x = x} {y = y} = ∙-congˡ (pullˡ)
+    uv≡w⇒xu∙v≈xw : ∀ {x} → (x ∙ u) ∙ v ≈ x ∙ w
+    uv≡w⇒xu∙v≈xw {x = x} =  trans (assoc x u v) (∙-congˡ uv≡w)
+
+    uv≡w⇒u∙vx≈wx : ∀ {x} → u ∙ (v ∙ x) ≈ w ∙ x
+    uv≡w⇒u∙vx≈wx {x = x} = trans (sym (assoc u v x)) (∙-congʳ uv≡w)
+
+    uv≡w⇒u[vx∙y]≈w∙xy : ∀ {x y} → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ (x ∙ y)
+    uv≡w⇒u[vx∙y]≈w∙xy {x = x} {y = y} = trans (∙-congˡ (assoc v x y)) uv≡w⇒u∙vx≈wx
+
+    uv≡w⇒x[uv∙y]≈x∙wy : ∀ {x y} → x ∙ (u ∙ (v ∙ y)) ≈ x ∙ (w ∙ y)
+    uv≡w⇒x[uv∙y]≈x∙wy {x = x} {y = y} = ∙-congˡ (uv≡w⇒u∙vx≈wx)
 
     -- could be called pull₃ʳ
-    pull-last : ∀ {x y} → (x ∙ (y ∙ u)) ∙ v ≈ x ∙ (y ∙ w)
-    pull-last {x = x} {y = y} = begin
-      (x ∙ (y ∙ u)) ∙ v ≈⟨ assoc x (y ∙ u) v ⟩
-      x ∙ ((y ∙ u) ∙ v) ≈⟨ ∙-congˡ (pullʳ {x = y}) ⟩
-      x ∙ (y ∙ w)       ∎
+    uv≡w⇒[x∙yu]v≈x∙yw : ∀ {x y} → (x ∙ (y ∙ u)) ∙ v ≈ x ∙ (y ∙ w)
+    uv≡w⇒[x∙yu]v≈x∙yw  {x = x} {y = y} = trans (assoc x (y ∙ u) v) (∙-congˡ (uv≡w⇒xu∙v≈xw {x = y}))
 
 open Pulls public
 
 module Pushes (uv≡w : u ∙ v ≈ w) where
     pushʳ : x ∙ w ≈ (x ∙ u) ∙ v
-    pushʳ = sym (pullʳ uv≡w)
+    pushʳ = sym (uv≡w⇒xu∙v≈xw uv≡w)
 
     pushˡ : w ∙ x ≈ u ∙ (v ∙ x)
-    pushˡ = sym (pullˡ uv≡w)
+    pushˡ = sym (uv≡w⇒u∙vx≈wx uv≡w)
 
 open Pushes public
 
 module Center (eq : u ∙ v ≈ w) where
   center : (x ∙ u) ∙ (v ∙ y) ≈ x ∙ (w ∙ y)
-  center = pullʳ (pullˡ eq)
+  center = uv≡w⇒xu∙v≈xw(uv≡w⇒u∙vx≈wx eq)
 
-  center⁻¹ : x ∙ y ≈ z →  u ∙ ((v ∙ x) ∙ y) ≈ w ∙ z
-  center⁻¹ {x = x} {y = y} {z = z} xy≈z = begin
-    u ∙ ((v ∙ x) ∙ y) ≈⟨ ∙-congˡ (pullʳ xy≈z) ⟩
-    u ∙ (v ∙ z)       ≈⟨ pullˡ eq ⟩
-    w ∙ z             ∎
+  center⁻¹ : ∀ z → x ∙ y ≈ z → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ z
+  center⁻¹ z xy≈z = trans (∙-congˡ (uv≡w⇒xu∙v≈xw xy≈z)) (uv≡w⇒u∙vx≈wx eq)
 
   push-center : x ∙ (w ∙ y) ≈ x ∙ (u ∙ (v ∙ y))
-  push-center = sym (pull-center eq)
+  push-center = sym (uv≡w⇒x[uv∙y]≈x∙wy eq)
 
 open Center public
 
 module Extends {u v w x : Carrier} (s : u ∙ v ≈ w ∙ x) where
-  extendˡ : (y ∙ u) ∙ v ≈ (y ∙ w) ∙ x
-  extendˡ {y = y} = begin
-    (y ∙ u) ∙ v ≈⟨ pullʳ s ⟩
-    y ∙ (w ∙ x) ≈⟨ assoc y w x ⟨
-    (y ∙ w) ∙ x ∎
-
-  extendʳ : u ∙ (v ∙ y) ≈ w ∙ (x ∙ y)
-  extendʳ {y = y} = begin
-    u ∙ (v ∙ y) ≈⟨ pullˡ s ⟩
-    (w ∙ x) ∙ y ≈⟨ assoc w x y ⟩
-    w ∙ (x ∙ y) ∎
-
-  extend² : ∀ y z → (y ∙ u) ∙ (v ∙ z) ≈ (y ∙ w) ∙ (x ∙ z)
-  extend² y z = begin
-    (y ∙ u) ∙ (v ∙ z) ≈⟨ pullʳ (extendʳ {y = z}) ⟩
-    y ∙ (w ∙ (x ∙ z)) ≈⟨ assoc y w (x ∙ z) ⟨
-    (y ∙ w) ∙ (x ∙ z) ∎
+  uv≈wx⇒yu∙v≈yw∙x : (y ∙ u) ∙ v ≈ (y ∙ w) ∙ x
+  uv≈wx⇒yu∙v≈yw∙x  {y = y} = trans (uv≡w⇒xu∙v≈xw s) (sym (assoc y w x))
+
+  uv≈wx⇒u∙vy≈w∙xy : ∀ y → u ∙ (v ∙ y) ≈ w ∙ (x ∙ y)
+  uv≈wx⇒u∙vy≈w∙xy y = trans (uv≡w⇒u∙vx≈wx s) (assoc w x y)
+
+  uv≈wx⇒yu∙vz≈yw∙xz : ∀ y z → (y ∙ u) ∙ (v ∙ z) ≈ (y ∙ w) ∙ (x ∙ z)
+  uv≈wx⇒yu∙vz≈yw∙xz y z = trans (uv≡w⇒xu∙v≈xw (uv≈wx⇒u∙vy≈w∙xy z))(sym (assoc y w (x ∙ z)))
 
 open Extends public
 

From 1a67eb953abf0a5df7d7385efc30b2a20118291b Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Mon, 7 Apr 2025 14:16:58 -0400
Subject: [PATCH 14/31] Names change

---
 .../Properties/Semigroup/Reasoning.agda       | 20 +++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/Algebra/Properties/Semigroup/Reasoning.agda b/src/Algebra/Properties/Semigroup/Reasoning.agda
index c97e42be45..9fc179dcee 100644
--- a/src/Algebra/Properties/Semigroup/Reasoning.agda
+++ b/src/Algebra/Properties/Semigroup/Reasoning.agda
@@ -76,23 +76,23 @@ module Pulls (uv≡w : u ∙ v ≈ w) where
 open Pulls public
 
 module Pushes (uv≡w : u ∙ v ≈ w) where
-    pushʳ : x ∙ w ≈ (x ∙ u) ∙ v
-    pushʳ = sym (uv≡w⇒xu∙v≈xw uv≡w)
+    uv≡w⇒xw≈xu∙v : x ∙ w ≈ (x ∙ u) ∙ v
+    uv≡w⇒xw≈xu∙v = sym (uv≡w⇒xu∙v≈xw uv≡w)
 
-    pushˡ : w ∙ x ≈ u ∙ (v ∙ x)
-    pushˡ = sym (uv≡w⇒u∙vx≈wx uv≡w)
+    uv≡w⇒wx≈u∙vx : w ∙ x ≈ u ∙ (v ∙ x)
+    uv≡w⇒wx≈u∙vx = sym (uv≡w⇒u∙vx≈wx uv≡w)
 
 open Pushes public
 
 module Center (eq : u ∙ v ≈ w) where
-  center : (x ∙ u) ∙ (v ∙ y) ≈ x ∙ (w ∙ y)
-  center = uv≡w⇒xu∙v≈xw(uv≡w⇒u∙vx≈wx eq)
+  uv≡w⇒xu∙vy≈x∙wy : (x ∙ u) ∙ (v ∙ y) ≈ x ∙ (w ∙ y)
+  uv≡w⇒xu∙vy≈x∙wy = uv≡w⇒xu∙v≈xw(uv≡w⇒u∙vx≈wx eq)
 
-  center⁻¹ : ∀ z → x ∙ y ≈ z → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ z
-  center⁻¹ z xy≈z = trans (∙-congˡ (uv≡w⇒xu∙v≈xw xy≈z)) (uv≡w⇒u∙vx≈wx eq)
+  uv≡w⇒xy≡z⇒u[vx∙y]≈wz : ∀ z → x ∙ y ≈ z → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ z
+  uv≡w⇒xy≡z⇒u[vx∙y]≈wz z xy≈z = trans (∙-congˡ (uv≡w⇒xu∙v≈xw xy≈z)) (uv≡w⇒u∙vx≈wx eq)
 
-  push-center : x ∙ (w ∙ y) ≈ x ∙ (u ∙ (v ∙ y))
-  push-center = sym (uv≡w⇒x[uv∙y]≈x∙wy eq)
+  uv≡w⇒x∙wy≈x∙[u∙vy] : x ∙ (w ∙ y) ≈ x ∙ (u ∙ (v ∙ y))
+  uv≡w⇒x∙wy≈x∙[u∙vy] = sym (uv≡w⇒x[uv∙y]≈x∙wy eq)
 
 open Center public
 

From 002cfad876d24ebd61df7caf9dc0474bfb6d9965 Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Mon, 7 Apr 2025 14:20:18 -0400
Subject: [PATCH 15/31] Space

---
 src/Algebra/Properties/Semigroup/Reasoning.agda | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/Algebra/Properties/Semigroup/Reasoning.agda b/src/Algebra/Properties/Semigroup/Reasoning.agda
index 9fc179dcee..06993f442c 100644
--- a/src/Algebra/Properties/Semigroup/Reasoning.agda
+++ b/src/Algebra/Properties/Semigroup/Reasoning.agda
@@ -22,7 +22,6 @@ private
  variable
     u v w x y z : Carrier
 
-
 module Assoc4  {u v w x : Carrier} where
   [uv∙w]x≈u[vw∙x] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ ((v ∙ w) ∙ x)
   [uv∙w]x≈u[vw∙x] = trans (∙-congʳ (assoc u v w)) (assoc u (v ∙ w) x)
@@ -69,7 +68,6 @@ module Pulls (uv≡w : u ∙ v ≈ w) where
     uv≡w⇒x[uv∙y]≈x∙wy : ∀ {x y} → x ∙ (u ∙ (v ∙ y)) ≈ x ∙ (w ∙ y)
     uv≡w⇒x[uv∙y]≈x∙wy {x = x} {y = y} = ∙-congˡ (uv≡w⇒u∙vx≈wx)
 
-    -- could be called pull₃ʳ
     uv≡w⇒[x∙yu]v≈x∙yw : ∀ {x y} → (x ∙ (y ∙ u)) ∙ v ≈ x ∙ (y ∙ w)
     uv≡w⇒[x∙yu]v≈x∙yw  {x = x} {y = y} = trans (assoc x (y ∙ u) v) (∙-congˡ (uv≡w⇒xu∙v≈xw {x = y}))
 

From a47bcc51fb003f4109d884abb8dad82731bf65f0 Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Tue, 8 Apr 2025 18:20:31 -0400
Subject: [PATCH 16/31] Proof of assoc with PUshes and Pulles

---
 .../Properties/Semigroup/Reasoning.agda       | 122 ++++++++++--------
 1 file changed, 68 insertions(+), 54 deletions(-)

diff --git a/src/Algebra/Properties/Semigroup/Reasoning.agda b/src/Algebra/Properties/Semigroup/Reasoning.agda
index 06993f442c..fa9ceae53d 100644
--- a/src/Algebra/Properties/Semigroup/Reasoning.agda
+++ b/src/Algebra/Properties/Semigroup/Reasoning.agda
@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Equational reasoning for semigroups
+-- uv≈wuational reasoning for semigroups
 -- (Utilities for associativity reasoning, pulling and pushing operations)
 ------------------------------------------------------------------------
 
@@ -11,8 +11,6 @@ open import Algebra.Bundles using (Semigroup)
 
 module Algebra.Properties.Semigroup.Reasoning {o ℓ} (S : Semigroup o ℓ) where
 
-open import Algebra.Structures using (IsMagma)
-
 open Semigroup S
   using (Carrier; _∙_; _≈_; setoid; trans; refl; sym; assoc; ∙-cong; isMagma
   ; ∙-congˡ; ∙-congʳ)
@@ -22,87 +20,103 @@ private
  variable
     u v w x y z : Carrier
 
-module Assoc4  {u v w x : Carrier} where
-  [uv∙w]x≈u[vw∙x] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ ((v ∙ w) ∙ x)
-  [uv∙w]x≈u[vw∙x] = trans (∙-congʳ (assoc u v w)) (assoc u (v ∙ w) x)
+module Pulls (uv≈w : u ∙ v ≈ w) where
+    uv≈w⇒xu∙v≈xw : ∀ {x} → (x ∙ u) ∙ v ≈ x ∙ w
+    uv≈w⇒xu∙v≈xw {x = x} =  trans (assoc x u v) (∙-congˡ uv≈w)
 
-  [uv∙w]x≈u[v∙wx] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ (v ∙ (w ∙ x))
-  [uv∙w]x≈u[v∙wx] = trans (assoc (u ∙ v) w x) (assoc u v (w ∙ x))
+    uv≈w⇒u∙vx≈wx : ∀ {x} → u ∙ (v ∙ x) ≈ w ∙ x
+    uv≈w⇒u∙vx≈wx {x = x} = trans (sym (assoc u v x)) (∙-congʳ uv≈w)
 
-  [u∙vw]x≈uv∙wx : (u ∙ (v ∙ w)) ∙ x ≈ (u ∙ v) ∙ (w ∙ x)
-  [u∙vw]x≈uv∙wx = trans (sym (∙-congʳ (assoc u v w))) (assoc (u ∙ v) w x)
+    uv≈w⇒u[vx∙y]≈w∙xy : ∀ {x y} → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ (x ∙ y)
+    uv≈w⇒u[vx∙y]≈w∙xy {x = x} {y = y} = trans (∙-congˡ (assoc v x y)) uv≈w⇒u∙vx≈wx
 
-  [u∙vw]x≈u[v∙wx] : (u ∙ (v ∙ w)) ∙ x ≈ u ∙ (v ∙ (w ∙ x))
-  [u∙vw]x≈u[v∙wx] = trans (assoc u (v ∙ w) x) (∙-congˡ (assoc v w x))
+    uv≈w⇒x[uv∙y]≈x∙wy : ∀ {x y} → x ∙ (u ∙ (v ∙ y)) ≈ x ∙ (w ∙ y)
+    uv≈w⇒x[uv∙y]≈x∙wy = ∙-congˡ uv≈w⇒u∙vx≈wx
 
-  uv∙wx≈[u∙vw]x : (u ∙ v) ∙ (w ∙ x) ≈ (u ∙ (v ∙ w)) ∙ x
-  uv∙wx≈[u∙vw]x = trans (sym (assoc (u ∙ v) w x)) (∙-congʳ (assoc u v w))
+    uv≈w⇒[x∙yu]v≈x∙yw : ∀ {x y} → (x ∙ (y ∙ u)) ∙ v ≈ x ∙ (y ∙ w)
+    uv≈w⇒[x∙yu]v≈x∙yw  {x = x} {y = y} = trans (assoc x (y ∙ u) v) (∙-congˡ (uv≈w⇒xu∙v≈xw {x = y}))
 
-  uv∙wx≈u[vw∙x] : (u ∙ v) ∙ (w ∙ x) ≈ u ∙ ((v ∙ w) ∙ x)
-  uv∙wx≈u[vw∙x] = trans (assoc u v (w ∙ x)) (∙-congˡ (sym (assoc v w x)))
+    uv≈w⇒[xu∙v]y≈x∙wy : ∀ {x y} → ((x ∙ u) ∙ v) ∙ y ≈ x ∙ (w ∙ y)
+    uv≈w⇒[xu∙v]y≈x∙wy = trans (∙-congʳ uv≈w⇒xu∙v≈xw ) (assoc _ _ _)
+    
+    uv≈w⇒[xy∙u]v≈x∙yw : ∀ {x y} → ((x ∙ y) ∙ u) ∙ v ≈ x ∙ (y ∙ w)
+    uv≈w⇒[xy∙u]v≈x∙yw {x = x} {y = y} = trans (∙-congʳ (assoc x y u)) uv≈w⇒[x∙yu]v≈x∙yw
 
-  u[vw∙x]≈[uv∙w]x : u ∙ ((v ∙ w) ∙ x) ≈ ((u ∙ v) ∙ w) ∙ x
-  u[vw∙x]≈[uv∙w]x = sym (trans (∙-congʳ (assoc u v w)) (assoc u (v ∙ w) x))
+open Pulls public
 
-  u[vw∙x]≈uv∙wx : u ∙ ((v ∙ w) ∙ x) ≈ (u ∙ v) ∙ (w ∙ x)
-  u[vw∙x]≈uv∙wx = trans (∙-congˡ (assoc v w x)) (sym (assoc u v (w ∙ x)))
+module Pushes (uv≈w : u ∙ v ≈ w) where
+    uv≈w⇒xw≈xu∙v : x ∙ w ≈ (x ∙ u) ∙ v
+    uv≈w⇒xw≈xu∙v = sym (uv≈w⇒xu∙v≈xw uv≈w)
 
-  u[v∙wx]≈[uv∙w]x : u ∙ (v ∙ (w ∙ x)) ≈ ((u ∙ v) ∙ w) ∙ x
-  u[v∙wx]≈[uv∙w]x = sym (trans (assoc (u ∙ v) w x) (assoc u v (w ∙ x)))
+    uv≈w⇒wx≈u∙vx : w ∙ x ≈ u ∙ (v ∙ x)
+    uv≈w⇒wx≈u∙vx = sym (uv≈w⇒u∙vx≈wx uv≈w)
 
-  u[v∙wx]≈[u∙vw]x : u ∙ (v ∙ (w ∙ x)) ≈ (u ∙ (v ∙ w)) ∙ x
-  u[v∙wx]≈[u∙vw]x  = sym (trans (assoc u (v ∙ w) x) (∙-congˡ (assoc v w x)))
+    uv≈w⇒w∙xy≈u[vx∙y] : ∀ {x y} → w ∙ (x ∙ y) ≈ u ∙ ((v ∙ x) ∙ y)
+    uv≈w⇒w∙xy≈u[vx∙y] {x = x} {y = y} = sym (uv≈w⇒u[vx∙y]≈w∙xy uv≈w)
 
-open Assoc4 public
+    uv≈w⇒x∙wy≈x[u∙vy] : ∀ {x y} → x ∙ (w ∙ y) ≈ x ∙ (u ∙ (v ∙ y))
+    uv≈w⇒x∙wy≈x[u∙vy] {x = x} {y = y} = sym (uv≈w⇒x[uv∙y]≈x∙wy uv≈w)
 
-module Pulls (uv≡w : u ∙ v ≈ w) where
-    uv≡w⇒xu∙v≈xw : ∀ {x} → (x ∙ u) ∙ v ≈ x ∙ w
-    uv≡w⇒xu∙v≈xw {x = x} =  trans (assoc x u v) (∙-congˡ uv≡w)
+    uv≈w⇒x∙yw≈[x∙yu]v : ∀ {x y} → x ∙ (y ∙ w) ≈ (x ∙ (y ∙ u)) ∙ v
+    uv≈w⇒x∙yw≈[x∙yu]v {x = x} {y = y} = sym (uv≈w⇒[x∙yu]v≈x∙yw uv≈w)
 
-    uv≡w⇒u∙vx≈wx : ∀ {x} → u ∙ (v ∙ x) ≈ w ∙ x
-    uv≡w⇒u∙vx≈wx {x = x} = trans (sym (assoc u v x)) (∙-congʳ uv≡w)
+open Pushes public
 
-    uv≡w⇒u[vx∙y]≈w∙xy : ∀ {x y} → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ (x ∙ y)
-    uv≡w⇒u[vx∙y]≈w∙xy {x = x} {y = y} = trans (∙-congˡ (assoc v x y)) uv≡w⇒u∙vx≈wx
+module Center (uv≈w : u ∙ v ≈ w) where
+  uv≈w⇒xu∙vy≈x∙wy : (x ∙ u) ∙ (v ∙ y) ≈ x ∙ (w ∙ y)
+  uv≈w⇒xu∙vy≈x∙wy = uv≈w⇒xu∙v≈xw (uv≈w⇒u∙vx≈wx uv≈w)
 
-    uv≡w⇒x[uv∙y]≈x∙wy : ∀ {x y} → x ∙ (u ∙ (v ∙ y)) ≈ x ∙ (w ∙ y)
-    uv≡w⇒x[uv∙y]≈x∙wy {x = x} {y = y} = ∙-congˡ (uv≡w⇒u∙vx≈wx)
+  uv≈w⇒xy≈z⇒u[vx∙y]≈wz : ∀ z → x ∙ y ≈ z → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ z
+  uv≈w⇒xy≈z⇒u[vx∙y]≈wz z xy≈z = trans (∙-congˡ (uv≈w⇒xu∙v≈xw xy≈z)) (uv≈w⇒u∙vx≈wx uv≈w)
 
-    uv≡w⇒[x∙yu]v≈x∙yw : ∀ {x y} → (x ∙ (y ∙ u)) ∙ v ≈ x ∙ (y ∙ w)
-    uv≡w⇒[x∙yu]v≈x∙yw  {x = x} {y = y} = trans (assoc x (y ∙ u) v) (∙-congˡ (uv≡w⇒xu∙v≈xw {x = y}))
+  uv≈w⇒x∙wy≈x∙[u∙vy] : x ∙ (w ∙ y) ≈ x ∙ (u ∙ (v ∙ y))
+  uv≈w⇒x∙wy≈x∙[u∙vy] = sym (uv≈w⇒x[uv∙y]≈x∙wy uv≈w)
 
-open Pulls public
+open Center public
 
-module Pushes (uv≡w : u ∙ v ≈ w) where
-    uv≡w⇒xw≈xu∙v : x ∙ w ≈ (x ∙ u) ∙ v
-    uv≡w⇒xw≈xu∙v = sym (uv≡w⇒xu∙v≈xw uv≡w)
+module Assoc4  {u v w x : Carrier} where
+  [uv∙w]x≈u[vw∙x] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ ((v ∙ w) ∙ x)
+  [uv∙w]x≈u[vw∙x] = uv≈w⇒[xu∙v]y≈x∙wy refl
 
-    uv≡w⇒wx≈u∙vx : w ∙ x ≈ u ∙ (v ∙ x)
-    uv≡w⇒wx≈u∙vx = sym (uv≡w⇒u∙vx≈wx uv≡w)
+  [uv∙w]x≈u[v∙wx] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ (v ∙ (w ∙ x))
+  [uv∙w]x≈u[v∙wx] = uv≈w⇒[xy∙u]v≈x∙yw refl
 
-open Pushes public
+  [u∙vw]x≈uv∙wx : (u ∙ (v ∙ w)) ∙ x ≈ (u ∙ v) ∙ (w ∙ x)
+  [u∙vw]x≈uv∙wx = trans (sym (∙-congʳ (assoc u v w))) (assoc (u ∙ v) w x)
 
-module Center (eq : u ∙ v ≈ w) where
-  uv≡w⇒xu∙vy≈x∙wy : (x ∙ u) ∙ (v ∙ y) ≈ x ∙ (w ∙ y)
-  uv≡w⇒xu∙vy≈x∙wy = uv≡w⇒xu∙v≈xw(uv≡w⇒u∙vx≈wx eq)
+  [u∙vw]x≈u[v∙wx] : (u ∙ (v ∙ w)) ∙ x ≈ u ∙ (v ∙ (w ∙ x))
+  [u∙vw]x≈u[v∙wx] = uv≈w⇒[x∙yu]v≈x∙yw refl
+  
+  uv∙wx≈u[vw∙x] : (u ∙ v) ∙ (w ∙ x) ≈ u ∙ ((v ∙ w) ∙ x)
+  uv∙wx≈u[vw∙x] = uv≈w⇒xu∙vy≈x∙wy refl
+  
+  uv∙wx≈[u∙vw]x : (u ∙ v) ∙ (w ∙ x) ≈ (u ∙ (v ∙ w)) ∙ x
+  uv∙wx≈[u∙vw]x = sym [u∙vw]x≈uv∙wx
 
-  uv≡w⇒xy≡z⇒u[vx∙y]≈wz : ∀ z → x ∙ y ≈ z → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ z
-  uv≡w⇒xy≡z⇒u[vx∙y]≈wz z xy≈z = trans (∙-congˡ (uv≡w⇒xu∙v≈xw xy≈z)) (uv≡w⇒u∙vx≈wx eq)
+  u[vw∙x]≈[uv∙w]x : u ∙ ((v ∙ w) ∙ x) ≈ ((u ∙ v) ∙ w) ∙ x
+  u[vw∙x]≈[uv∙w]x = sym [uv∙w]x≈u[vw∙x]
 
-  uv≡w⇒x∙wy≈x∙[u∙vy] : x ∙ (w ∙ y) ≈ x ∙ (u ∙ (v ∙ y))
-  uv≡w⇒x∙wy≈x∙[u∙vy] = sym (uv≡w⇒x[uv∙y]≈x∙wy eq)
+  u[vw∙x]≈uv∙wx : u ∙ ((v ∙ w) ∙ x) ≈ (u ∙ v) ∙ (w ∙ x)
+  u[vw∙x]≈uv∙wx = sym uv∙wx≈u[vw∙x]
 
-open Center public
+  u[v∙wx]≈[uv∙w]x : u ∙ (v ∙ (w ∙ x)) ≈ ((u ∙ v) ∙ w) ∙ x
+  u[v∙wx]≈[uv∙w]x = sym [uv∙w]x≈u[v∙wx]
+
+  u[v∙wx]≈[u∙vw]x : u ∙ (v ∙ (w ∙ x)) ≈ (u ∙ (v ∙ w)) ∙ x
+  u[v∙wx]≈[u∙vw]x  = sym [u∙vw]x≈u[v∙wx]
+
+open Assoc4 public
 
 module Extends {u v w x : Carrier} (s : u ∙ v ≈ w ∙ x) where
   uv≈wx⇒yu∙v≈yw∙x : (y ∙ u) ∙ v ≈ (y ∙ w) ∙ x
-  uv≈wx⇒yu∙v≈yw∙x  {y = y} = trans (uv≡w⇒xu∙v≈xw s) (sym (assoc y w x))
+  uv≈wx⇒yu∙v≈yw∙x  {y = y} = trans (uv≈w⇒xu∙v≈xw s) (sym (assoc y w x))
 
   uv≈wx⇒u∙vy≈w∙xy : ∀ y → u ∙ (v ∙ y) ≈ w ∙ (x ∙ y)
-  uv≈wx⇒u∙vy≈w∙xy y = trans (uv≡w⇒u∙vx≈wx s) (assoc w x y)
+  uv≈wx⇒u∙vy≈w∙xy y = trans (uv≈w⇒u∙vx≈wx s) (assoc w x y)
 
   uv≈wx⇒yu∙vz≈yw∙xz : ∀ y z → (y ∙ u) ∙ (v ∙ z) ≈ (y ∙ w) ∙ (x ∙ z)
-  uv≈wx⇒yu∙vz≈yw∙xz y z = trans (uv≡w⇒xu∙v≈xw (uv≈wx⇒u∙vy≈w∙xy z))(sym (assoc y w (x ∙ z)))
+  uv≈wx⇒yu∙vz≈yw∙xz y z = trans (uv≈w⇒xu∙v≈xw (uv≈wx⇒u∙vy≈w∙xy z))(sym (assoc y w (x ∙ z)))
 
 open Extends public
 
+  
\ No newline at end of file

From ca9f5766f434e9973f338dee7bef5eae01f6e173 Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Tue, 8 Apr 2025 18:20:55 -0400
Subject: [PATCH 17/31] Proof of assoc with PUshes and Pulles

---
 src/Algebra/Properties/Semigroup/Reasoning.agda | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/Algebra/Properties/Semigroup/Reasoning.agda b/src/Algebra/Properties/Semigroup/Reasoning.agda
index fa9ceae53d..34b23994f7 100644
--- a/src/Algebra/Properties/Semigroup/Reasoning.agda
+++ b/src/Algebra/Properties/Semigroup/Reasoning.agda
@@ -38,7 +38,7 @@ module Pulls (uv≈w : u ∙ v ≈ w) where
 
     uv≈w⇒[xu∙v]y≈x∙wy : ∀ {x y} → ((x ∙ u) ∙ v) ∙ y ≈ x ∙ (w ∙ y)
     uv≈w⇒[xu∙v]y≈x∙wy = trans (∙-congʳ uv≈w⇒xu∙v≈xw ) (assoc _ _ _)
-    
+
     uv≈w⇒[xy∙u]v≈x∙yw : ∀ {x y} → ((x ∙ y) ∙ u) ∙ v ≈ x ∙ (y ∙ w)
     uv≈w⇒[xy∙u]v≈x∙yw {x = x} {y = y} = trans (∙-congʳ (assoc x y u)) uv≈w⇒[x∙yu]v≈x∙yw
 
@@ -86,10 +86,10 @@ module Assoc4  {u v w x : Carrier} where
 
   [u∙vw]x≈u[v∙wx] : (u ∙ (v ∙ w)) ∙ x ≈ u ∙ (v ∙ (w ∙ x))
   [u∙vw]x≈u[v∙wx] = uv≈w⇒[x∙yu]v≈x∙yw refl
-  
+
   uv∙wx≈u[vw∙x] : (u ∙ v) ∙ (w ∙ x) ≈ u ∙ ((v ∙ w) ∙ x)
   uv∙wx≈u[vw∙x] = uv≈w⇒xu∙vy≈x∙wy refl
-  
+
   uv∙wx≈[u∙vw]x : (u ∙ v) ∙ (w ∙ x) ≈ (u ∙ (v ∙ w)) ∙ x
   uv∙wx≈[u∙vw]x = sym [u∙vw]x≈uv∙wx
 
@@ -119,4 +119,3 @@ module Extends {u v w x : Carrier} (s : u ∙ v ≈ w ∙ x) where
 
 open Extends public
 
-  
\ No newline at end of file

From e07f81b08dd549dc502867af9303afe59b881981 Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Wed, 9 Apr 2025 17:03:32 -0400
Subject: [PATCH 18/31] white space

---
 src/Algebra/Properties/Semigroup/Reasoning.agda | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Algebra/Properties/Semigroup/Reasoning.agda b/src/Algebra/Properties/Semigroup/Reasoning.agda
index 34b23994f7..30dc1ded75 100644
--- a/src/Algebra/Properties/Semigroup/Reasoning.agda
+++ b/src/Algebra/Properties/Semigroup/Reasoning.agda
@@ -74,7 +74,7 @@ module Center (uv≈w : u ∙ v ≈ w) where
 
 open Center public
 
-module Assoc4  {u v w x : Carrier} where
+module Assoc4 {u v w x : Carrier} where
   [uv∙w]x≈u[vw∙x] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ ((v ∙ w) ∙ x)
   [uv∙w]x≈u[vw∙x] = uv≈w⇒[xu∙v]y≈x∙wy refl
 
@@ -103,13 +103,13 @@ module Assoc4  {u v w x : Carrier} where
   u[v∙wx]≈[uv∙w]x = sym [uv∙w]x≈u[v∙wx]
 
   u[v∙wx]≈[u∙vw]x : u ∙ (v ∙ (w ∙ x)) ≈ (u ∙ (v ∙ w)) ∙ x
-  u[v∙wx]≈[u∙vw]x  = sym [u∙vw]x≈u[v∙wx]
+  u[v∙wx]≈[u∙vw]x = sym [u∙vw]x≈u[v∙wx]
 
 open Assoc4 public
 
 module Extends {u v w x : Carrier} (s : u ∙ v ≈ w ∙ x) where
-  uv≈wx⇒yu∙v≈yw∙x : (y ∙ u) ∙ v ≈ (y ∙ w) ∙ x
-  uv≈wx⇒yu∙v≈yw∙x  {y = y} = trans (uv≈w⇒xu∙v≈xw s) (sym (assoc y w x))
+  uv≈wx⇒yu∙v≈yw∙x : ∀ {y} → (y ∙ u) ∙ v ≈ (y ∙ w) ∙ x
+  uv≈wx⇒yu∙v≈yw∙x {y = y} = trans (uv≈w⇒xu∙v≈xw s) (sym (assoc y w x))
 
   uv≈wx⇒u∙vy≈w∙xy : ∀ y → u ∙ (v ∙ y) ≈ w ∙ (x ∙ y)
   uv≈wx⇒u∙vy≈w∙xy y = trans (uv≈w⇒u∙vx≈wx s) (assoc w x y)

From 86b06e047cb106e7335bc7e964e5cd9f1451a582 Mon Sep 17 00:00:00 2001
From: Jacques <149587529+jmougeot@users.noreply.github.com>
Date: Thu, 10 Apr 2025 14:59:42 -0400
Subject: [PATCH 19/31] Update src/Algebra/Properties/Semigroup/Reasoning.agda

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
---
 src/Algebra/Properties/Semigroup/Reasoning.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Algebra/Properties/Semigroup/Reasoning.agda b/src/Algebra/Properties/Semigroup/Reasoning.agda
index 30dc1ded75..6d16faf24f 100644
--- a/src/Algebra/Properties/Semigroup/Reasoning.agda
+++ b/src/Algebra/Properties/Semigroup/Reasoning.agda
@@ -21,8 +21,8 @@ private
     u v w x y z : Carrier
 
 module Pulls (uv≈w : u ∙ v ≈ w) where
-    uv≈w⇒xu∙v≈xw : ∀ {x} → (x ∙ u) ∙ v ≈ x ∙ w
-    uv≈w⇒xu∙v≈xw {x = x} =  trans (assoc x u v) (∙-congˡ uv≈w)
+    uv≈w⇒xu∙v≈xw : ∀ x → (x ∙ u) ∙ v ≈ x ∙ w
+    uv≈w⇒xu∙v≈xw x =  trans (assoc x u v) (∙-congˡ uv≈w)
 
     uv≈w⇒u∙vx≈wx : ∀ {x} → u ∙ (v ∙ x) ≈ w ∙ x
     uv≈w⇒u∙vx≈wx {x = x} = trans (sym (assoc u v x)) (∙-congʳ uv≈w)

From 7b72ff23b2ee99703edceead6e4a5d21b06aa104 Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Fri, 11 Apr 2025 11:23:24 -0400
Subject: [PATCH 20/31] Reasoning to Semigroup and explicit variables

---
 CHANGELOG.md                                  |   4 +-
 src/Algebra/Properties/Semigroup.agda         |  96 +++++++++++++-
 .../Properties/Semigroup/Reasoning.agda       | 121 ------------------
 3 files changed, 96 insertions(+), 125 deletions(-)
 delete mode 100644 src/Algebra/Properties/Semigroup/Reasoning.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 03e4631c65..e4d4c4b72f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -123,9 +123,7 @@ New modules
 
 * `Data.Sign.Show` to show a sign
 
-* `AlgebraPropreties.Semigroup.Reasoning` adding reasoning combinators for semigroups
-
-Additions to existing modules
+* `Algebra.Properties.Semigroup` adding consequences for associtvity for semigroups
 -----------------------------
 
 * In `Algebra.Construct.Pointwise`:
diff --git a/src/Algebra/Properties/Semigroup.agda b/src/Algebra/Properties/Semigroup.agda
index 22aab4e66e..52e8c76188 100644
--- a/src/Algebra/Properties/Semigroup.agda
+++ b/src/Algebra/Properties/Semigroup.agda
@@ -10,9 +10,15 @@ open import Algebra using (Semigroup)
 
 module Algebra.Properties.Semigroup {a ℓ} (S : Semigroup a ℓ) where
 
+open import Data.Product.Base using (_,_)
+
 open Semigroup S
 open import Algebra.Definitions _≈_
-open import Data.Product.Base using (_,_)
+open import Relation.Binary.Reasoning.Setoid setoid
+
+private
+ variable
+    u v w x y z : Carrier
 
 x∙yz≈xy∙z : ∀ x y z → x ∙ (y ∙ z) ≈ (x ∙ y) ∙ z
 x∙yz≈xy∙z x y z = sym (assoc x y z)
@@ -28,3 +34,91 @@ alternative = alternativeˡ , alternativeʳ
 
 flexible : Flexible _∙_
 flexible x y = assoc x y x
+
+module _ (uv≈w : u ∙ v ≈ w) where
+    uv≈w⇒xu∙v≈xw : ∀ x → (x ∙ u) ∙ v ≈ x ∙ w
+    uv≈w⇒xu∙v≈xw x =  trans (assoc x u v) (∙-congˡ uv≈w)
+
+    uv≈w⇒u∙vx≈wx : ∀ x → u ∙ (v ∙ x) ≈ w ∙ x
+    uv≈w⇒u∙vx≈wx x = trans (sym (assoc u v x)) (∙-congʳ uv≈w)
+
+    uv≈w⇒u[vx∙y]≈w∙xy : ∀ x y → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ (x ∙ y)
+    uv≈w⇒u[vx∙y]≈w∙xy x y  = trans (∙-congˡ (assoc v x y)) (uv≈w⇒u∙vx≈wx (x ∙ y))
+
+    uv≈w⇒x[uv∙y]≈x∙wy : ∀ x y → x ∙ (u ∙ (v ∙ y)) ≈ x ∙ (w ∙ y)
+    uv≈w⇒x[uv∙y]≈x∙wy x y = ∙-congˡ (uv≈w⇒u∙vx≈wx y)
+
+    uv≈w⇒[x∙yu]v≈x∙yw : ∀ x y → (x ∙ (y ∙ u)) ∙ v ≈ x ∙ (y ∙ w)
+    uv≈w⇒[x∙yu]v≈x∙yw  x y = trans (assoc x (y ∙ u) v) (∙-congˡ (uv≈w⇒xu∙v≈xw y))
+
+    uv≈w⇒[xu∙v]y≈x∙wy : ∀ x y → ((x ∙ u) ∙ v) ∙ y ≈ x ∙ (w ∙ y)
+    uv≈w⇒[xu∙v]y≈x∙wy x y = trans (∙-congʳ (uv≈w⇒xu∙v≈xw x)) (assoc _ _ _)
+
+    uv≈w⇒[xy∙u]v≈x∙yw : ∀ x y → ((x ∙ y) ∙ u) ∙ v ≈ x ∙ (y ∙ w)
+    uv≈w⇒[xy∙u]v≈x∙yw x y = trans (∙-congʳ (assoc x y u)) (uv≈w⇒[x∙yu]v≈x∙yw x  y )
+
+module _ (uv≈w : u ∙ v ≈ w) where
+    uv≈w⇒xw≈xu∙v : x ∙ w ≈ (x ∙ u) ∙ v
+    uv≈w⇒xw≈xu∙v = sym (uv≈w⇒xu∙v≈xw uv≈w _)
+
+    uv≈w⇒wx≈u∙vx : w ∙ x ≈ u ∙ (v ∙ x)
+    uv≈w⇒wx≈u∙vx = sym (uv≈w⇒u∙vx≈wx uv≈w _)
+
+    uv≈w⇒w∙xy≈u[vx∙y] : ∀ x y → w ∙ (x ∙ y) ≈ u ∙ ((v ∙ x) ∙ y)
+    uv≈w⇒w∙xy≈u[vx∙y] x y = sym (uv≈w⇒u[vx∙y]≈w∙xy uv≈w x y)
+
+    uv≈w⇒x∙wy≈x[u∙vy] : ∀ x y → x ∙ (w ∙ y) ≈ x ∙ (u ∙ (v ∙ y))
+    uv≈w⇒x∙wy≈x[u∙vy] x y = sym (uv≈w⇒x[uv∙y]≈x∙wy uv≈w x y)
+
+    uv≈w⇒x∙yw≈[x∙yu]v : ∀ x y  → x ∙ (y ∙ w) ≈ (x ∙ (y ∙ u)) ∙ v
+    uv≈w⇒x∙yw≈[x∙yu]v x y  = sym (uv≈w⇒[x∙yu]v≈x∙yw uv≈w x y)
+
+    uv≈w⇒xu∙vy≈x∙wy : (x ∙ u) ∙ (v ∙ y) ≈ x ∙ (w ∙ y)
+    uv≈w⇒xu∙vy≈x∙wy = uv≈w⇒xu∙v≈xw (uv≈w⇒u∙vx≈wx uv≈w _) _
+
+    uv≈w⇒xy≈z⇒u[vx∙y]≈wz : ∀ z → x ∙ y ≈ z → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ z
+    uv≈w⇒xy≈z⇒u[vx∙y]≈wz z xy≈z = trans (∙-congˡ (uv≈w⇒xu∙v≈xw xy≈z v)) (uv≈w⇒u∙vx≈wx uv≈w z)
+
+    uv≈w⇒x∙wy≈x∙[u∙vy] : x ∙ (w ∙ y) ≈ x ∙ (u ∙ (v ∙ y))
+    uv≈w⇒x∙wy≈x∙[u∙vy] = sym (uv≈w⇒x[uv∙y]≈x∙wy uv≈w _ _)
+
+module _ {u v w x : Carrier} where
+  [uv∙w]x≈u[vw∙x] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ ((v ∙ w) ∙ x)
+  [uv∙w]x≈u[vw∙x] = uv≈w⇒[xu∙v]y≈x∙wy refl u x
+
+  [uv∙w]x≈u[v∙wx] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ (v ∙ (w ∙ x))
+  [uv∙w]x≈u[v∙wx] = uv≈w⇒[xy∙u]v≈x∙yw refl u v
+
+  [u∙vw]x≈uv∙wx : (u ∙ (v ∙ w)) ∙ x ≈ (u ∙ v) ∙ (w ∙ x)
+  [u∙vw]x≈uv∙wx = trans (sym (∙-congʳ (assoc u v w))) (assoc (u ∙ v) w x)
+
+  [u∙vw]x≈u[v∙wx] : (u ∙ (v ∙ w)) ∙ x ≈ u ∙ (v ∙ (w ∙ x))
+  [u∙vw]x≈u[v∙wx] = uv≈w⇒[x∙yu]v≈x∙yw refl u v
+
+  uv∙wx≈u[vw∙x] : (u ∙ v) ∙ (w ∙ x) ≈ u ∙ ((v ∙ w) ∙ x)
+  uv∙wx≈u[vw∙x] = uv≈w⇒xu∙vy≈x∙wy refl
+
+  uv∙wx≈[u∙vw]x : (u ∙ v) ∙ (w ∙ x) ≈ (u ∙ (v ∙ w)) ∙ x
+  uv∙wx≈[u∙vw]x = sym [u∙vw]x≈uv∙wx
+
+  u[vw∙x]≈[uv∙w]x : u ∙ ((v ∙ w) ∙ x) ≈ ((u ∙ v) ∙ w) ∙ x
+  u[vw∙x]≈[uv∙w]x = sym [uv∙w]x≈u[vw∙x]
+
+  u[vw∙x]≈uv∙wx : u ∙ ((v ∙ w) ∙ x) ≈ (u ∙ v) ∙ (w ∙ x)
+  u[vw∙x]≈uv∙wx = sym uv∙wx≈u[vw∙x]
+
+  u[v∙wx]≈[uv∙w]x : u ∙ (v ∙ (w ∙ x)) ≈ ((u ∙ v) ∙ w) ∙ x
+  u[v∙wx]≈[uv∙w]x = sym [uv∙w]x≈u[v∙wx]
+
+  u[v∙wx]≈[u∙vw]x : u ∙ (v ∙ (w ∙ x)) ≈ (u ∙ (v ∙ w)) ∙ x
+  u[v∙wx]≈[u∙vw]x = sym [u∙vw]x≈u[v∙wx]
+
+module _ {u v w x : Carrier} (uv≈wx : u ∙ v ≈ w ∙ x) where
+  uv≈wx⇒yu∙v≈yw∙x : ∀ y → (y ∙ u) ∙ v ≈ (y ∙ w) ∙ x
+  uv≈wx⇒yu∙v≈yw∙x y = trans (uv≈w⇒xu∙v≈xw uv≈wx y) (sym (assoc y w x))
+
+  uv≈wx⇒u∙vy≈w∙xy : ∀ y → u ∙ (v ∙ y) ≈ w ∙ (x ∙ y)
+  uv≈wx⇒u∙vy≈w∙xy y = trans (uv≈w⇒u∙vx≈wx uv≈wx y) (assoc w x y)
+
+  uv≈wx⇒yu∙vz≈yw∙xz : ∀ y z → (y ∙ u) ∙ (v ∙ z) ≈ (y ∙ w) ∙ (x ∙ z)
+  uv≈wx⇒yu∙vz≈yw∙xz y z = trans (uv≈w⇒xu∙v≈xw (uv≈wx⇒u∙vy≈w∙xy z) y)(sym (assoc y w (x ∙ z)))
diff --git a/src/Algebra/Properties/Semigroup/Reasoning.agda b/src/Algebra/Properties/Semigroup/Reasoning.agda
deleted file mode 100644
index 6d16faf24f..0000000000
--- a/src/Algebra/Properties/Semigroup/Reasoning.agda
+++ /dev/null
@@ -1,121 +0,0 @@
-------------------------------------------------------------------------
--- The Agda standard library
---
--- uv≈wuational reasoning for semigroups
--- (Utilities for associativity reasoning, pulling and pushing operations)
-------------------------------------------------------------------------
-
-{-# OPTIONS --cubical-compatible --safe #-}
-
-open import Algebra.Bundles using (Semigroup)
-
-module Algebra.Properties.Semigroup.Reasoning {o ℓ} (S : Semigroup o ℓ) where
-
-open Semigroup S
-  using (Carrier; _∙_; _≈_; setoid; trans; refl; sym; assoc; ∙-cong; isMagma
-  ; ∙-congˡ; ∙-congʳ)
-open import Relation.Binary.Reasoning.Setoid setoid
-
-private
- variable
-    u v w x y z : Carrier
-
-module Pulls (uv≈w : u ∙ v ≈ w) where
-    uv≈w⇒xu∙v≈xw : ∀ x → (x ∙ u) ∙ v ≈ x ∙ w
-    uv≈w⇒xu∙v≈xw x =  trans (assoc x u v) (∙-congˡ uv≈w)
-
-    uv≈w⇒u∙vx≈wx : ∀ {x} → u ∙ (v ∙ x) ≈ w ∙ x
-    uv≈w⇒u∙vx≈wx {x = x} = trans (sym (assoc u v x)) (∙-congʳ uv≈w)
-
-    uv≈w⇒u[vx∙y]≈w∙xy : ∀ {x y} → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ (x ∙ y)
-    uv≈w⇒u[vx∙y]≈w∙xy {x = x} {y = y} = trans (∙-congˡ (assoc v x y)) uv≈w⇒u∙vx≈wx
-
-    uv≈w⇒x[uv∙y]≈x∙wy : ∀ {x y} → x ∙ (u ∙ (v ∙ y)) ≈ x ∙ (w ∙ y)
-    uv≈w⇒x[uv∙y]≈x∙wy = ∙-congˡ uv≈w⇒u∙vx≈wx
-
-    uv≈w⇒[x∙yu]v≈x∙yw : ∀ {x y} → (x ∙ (y ∙ u)) ∙ v ≈ x ∙ (y ∙ w)
-    uv≈w⇒[x∙yu]v≈x∙yw  {x = x} {y = y} = trans (assoc x (y ∙ u) v) (∙-congˡ (uv≈w⇒xu∙v≈xw {x = y}))
-
-    uv≈w⇒[xu∙v]y≈x∙wy : ∀ {x y} → ((x ∙ u) ∙ v) ∙ y ≈ x ∙ (w ∙ y)
-    uv≈w⇒[xu∙v]y≈x∙wy = trans (∙-congʳ uv≈w⇒xu∙v≈xw ) (assoc _ _ _)
-
-    uv≈w⇒[xy∙u]v≈x∙yw : ∀ {x y} → ((x ∙ y) ∙ u) ∙ v ≈ x ∙ (y ∙ w)
-    uv≈w⇒[xy∙u]v≈x∙yw {x = x} {y = y} = trans (∙-congʳ (assoc x y u)) uv≈w⇒[x∙yu]v≈x∙yw
-
-open Pulls public
-
-module Pushes (uv≈w : u ∙ v ≈ w) where
-    uv≈w⇒xw≈xu∙v : x ∙ w ≈ (x ∙ u) ∙ v
-    uv≈w⇒xw≈xu∙v = sym (uv≈w⇒xu∙v≈xw uv≈w)
-
-    uv≈w⇒wx≈u∙vx : w ∙ x ≈ u ∙ (v ∙ x)
-    uv≈w⇒wx≈u∙vx = sym (uv≈w⇒u∙vx≈wx uv≈w)
-
-    uv≈w⇒w∙xy≈u[vx∙y] : ∀ {x y} → w ∙ (x ∙ y) ≈ u ∙ ((v ∙ x) ∙ y)
-    uv≈w⇒w∙xy≈u[vx∙y] {x = x} {y = y} = sym (uv≈w⇒u[vx∙y]≈w∙xy uv≈w)
-
-    uv≈w⇒x∙wy≈x[u∙vy] : ∀ {x y} → x ∙ (w ∙ y) ≈ x ∙ (u ∙ (v ∙ y))
-    uv≈w⇒x∙wy≈x[u∙vy] {x = x} {y = y} = sym (uv≈w⇒x[uv∙y]≈x∙wy uv≈w)
-
-    uv≈w⇒x∙yw≈[x∙yu]v : ∀ {x y} → x ∙ (y ∙ w) ≈ (x ∙ (y ∙ u)) ∙ v
-    uv≈w⇒x∙yw≈[x∙yu]v {x = x} {y = y} = sym (uv≈w⇒[x∙yu]v≈x∙yw uv≈w)
-
-open Pushes public
-
-module Center (uv≈w : u ∙ v ≈ w) where
-  uv≈w⇒xu∙vy≈x∙wy : (x ∙ u) ∙ (v ∙ y) ≈ x ∙ (w ∙ y)
-  uv≈w⇒xu∙vy≈x∙wy = uv≈w⇒xu∙v≈xw (uv≈w⇒u∙vx≈wx uv≈w)
-
-  uv≈w⇒xy≈z⇒u[vx∙y]≈wz : ∀ z → x ∙ y ≈ z → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ z
-  uv≈w⇒xy≈z⇒u[vx∙y]≈wz z xy≈z = trans (∙-congˡ (uv≈w⇒xu∙v≈xw xy≈z)) (uv≈w⇒u∙vx≈wx uv≈w)
-
-  uv≈w⇒x∙wy≈x∙[u∙vy] : x ∙ (w ∙ y) ≈ x ∙ (u ∙ (v ∙ y))
-  uv≈w⇒x∙wy≈x∙[u∙vy] = sym (uv≈w⇒x[uv∙y]≈x∙wy uv≈w)
-
-open Center public
-
-module Assoc4 {u v w x : Carrier} where
-  [uv∙w]x≈u[vw∙x] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ ((v ∙ w) ∙ x)
-  [uv∙w]x≈u[vw∙x] = uv≈w⇒[xu∙v]y≈x∙wy refl
-
-  [uv∙w]x≈u[v∙wx] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ (v ∙ (w ∙ x))
-  [uv∙w]x≈u[v∙wx] = uv≈w⇒[xy∙u]v≈x∙yw refl
-
-  [u∙vw]x≈uv∙wx : (u ∙ (v ∙ w)) ∙ x ≈ (u ∙ v) ∙ (w ∙ x)
-  [u∙vw]x≈uv∙wx = trans (sym (∙-congʳ (assoc u v w))) (assoc (u ∙ v) w x)
-
-  [u∙vw]x≈u[v∙wx] : (u ∙ (v ∙ w)) ∙ x ≈ u ∙ (v ∙ (w ∙ x))
-  [u∙vw]x≈u[v∙wx] = uv≈w⇒[x∙yu]v≈x∙yw refl
-
-  uv∙wx≈u[vw∙x] : (u ∙ v) ∙ (w ∙ x) ≈ u ∙ ((v ∙ w) ∙ x)
-  uv∙wx≈u[vw∙x] = uv≈w⇒xu∙vy≈x∙wy refl
-
-  uv∙wx≈[u∙vw]x : (u ∙ v) ∙ (w ∙ x) ≈ (u ∙ (v ∙ w)) ∙ x
-  uv∙wx≈[u∙vw]x = sym [u∙vw]x≈uv∙wx
-
-  u[vw∙x]≈[uv∙w]x : u ∙ ((v ∙ w) ∙ x) ≈ ((u ∙ v) ∙ w) ∙ x
-  u[vw∙x]≈[uv∙w]x = sym [uv∙w]x≈u[vw∙x]
-
-  u[vw∙x]≈uv∙wx : u ∙ ((v ∙ w) ∙ x) ≈ (u ∙ v) ∙ (w ∙ x)
-  u[vw∙x]≈uv∙wx = sym uv∙wx≈u[vw∙x]
-
-  u[v∙wx]≈[uv∙w]x : u ∙ (v ∙ (w ∙ x)) ≈ ((u ∙ v) ∙ w) ∙ x
-  u[v∙wx]≈[uv∙w]x = sym [uv∙w]x≈u[v∙wx]
-
-  u[v∙wx]≈[u∙vw]x : u ∙ (v ∙ (w ∙ x)) ≈ (u ∙ (v ∙ w)) ∙ x
-  u[v∙wx]≈[u∙vw]x = sym [u∙vw]x≈u[v∙wx]
-
-open Assoc4 public
-
-module Extends {u v w x : Carrier} (s : u ∙ v ≈ w ∙ x) where
-  uv≈wx⇒yu∙v≈yw∙x : ∀ {y} → (y ∙ u) ∙ v ≈ (y ∙ w) ∙ x
-  uv≈wx⇒yu∙v≈yw∙x {y = y} = trans (uv≈w⇒xu∙v≈xw s) (sym (assoc y w x))
-
-  uv≈wx⇒u∙vy≈w∙xy : ∀ y → u ∙ (v ∙ y) ≈ w ∙ (x ∙ y)
-  uv≈wx⇒u∙vy≈w∙xy y = trans (uv≈w⇒u∙vx≈wx s) (assoc w x y)
-
-  uv≈wx⇒yu∙vz≈yw∙xz : ∀ y z → (y ∙ u) ∙ (v ∙ z) ≈ (y ∙ w) ∙ (x ∙ z)
-  uv≈wx⇒yu∙vz≈yw∙xz y z = trans (uv≈w⇒xu∙v≈xw (uv≈wx⇒u∙vy≈w∙xy z))(sym (assoc y w (x ∙ z)))
-
-open Extends public
-

From 13b5f0e1c4e7ae2e068244892a123ee37913e342 Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Fri, 11 Apr 2025 11:29:13 -0400
Subject: [PATCH 21/31] fix bug

---
 src/Algebra/Properties/Semigroup.agda | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Algebra/Properties/Semigroup.agda b/src/Algebra/Properties/Semigroup.agda
index 52e8c76188..0607c24ebc 100644
--- a/src/Algebra/Properties/Semigroup.agda
+++ b/src/Algebra/Properties/Semigroup.agda
@@ -122,3 +122,4 @@ module _ {u v w x : Carrier} (uv≈wx : u ∙ v ≈ w ∙ x) where
 
   uv≈wx⇒yu∙vz≈yw∙xz : ∀ y z → (y ∙ u) ∙ (v ∙ z) ≈ (y ∙ w) ∙ (x ∙ z)
   uv≈wx⇒yu∙vz≈yw∙xz y z = trans (uv≈w⇒xu∙v≈xw (uv≈wx⇒u∙vy≈w∙xy z) y)(sym (assoc y w (x ∙ z)))
+

From f58aceb786908de58fd56ccd9e49e701253a7fd2 Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Fri, 11 Apr 2025 11:30:01 -0400
Subject: [PATCH 22/31] space

---
 src/Algebra/Properties/Semigroup.agda | 53 +++++++++++++--------------
 1 file changed, 26 insertions(+), 27 deletions(-)

diff --git a/src/Algebra/Properties/Semigroup.agda b/src/Algebra/Properties/Semigroup.agda
index 0607c24ebc..0fbd24d86f 100644
--- a/src/Algebra/Properties/Semigroup.agda
+++ b/src/Algebra/Properties/Semigroup.agda
@@ -83,43 +83,42 @@ module _ (uv≈w : u ∙ v ≈ w) where
     uv≈w⇒x∙wy≈x∙[u∙vy] = sym (uv≈w⇒x[uv∙y]≈x∙wy uv≈w _ _)
 
 module _ {u v w x : Carrier} where
-  [uv∙w]x≈u[vw∙x] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ ((v ∙ w) ∙ x)
-  [uv∙w]x≈u[vw∙x] = uv≈w⇒[xu∙v]y≈x∙wy refl u x
+    [uv∙w]x≈u[vw∙x] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ ((v ∙ w) ∙ x)
+    [uv∙w]x≈u[vw∙x] = uv≈w⇒[xu∙v]y≈x∙wy refl u x
 
-  [uv∙w]x≈u[v∙wx] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ (v ∙ (w ∙ x))
-  [uv∙w]x≈u[v∙wx] = uv≈w⇒[xy∙u]v≈x∙yw refl u v
+    [uv∙w]x≈u[v∙wx] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ (v ∙ (w ∙ x))
+    [uv∙w]x≈u[v∙wx] = uv≈w⇒[xy∙u]v≈x∙yw refl u v
 
-  [u∙vw]x≈uv∙wx : (u ∙ (v ∙ w)) ∙ x ≈ (u ∙ v) ∙ (w ∙ x)
-  [u∙vw]x≈uv∙wx = trans (sym (∙-congʳ (assoc u v w))) (assoc (u ∙ v) w x)
+    [u∙vw]x≈uv∙wx : (u ∙ (v ∙ w)) ∙ x ≈ (u ∙ v) ∙ (w ∙ x)
+    [u∙vw]x≈uv∙wx = trans (sym (∙-congʳ (assoc u v w))) (assoc (u ∙ v) w x)
 
-  [u∙vw]x≈u[v∙wx] : (u ∙ (v ∙ w)) ∙ x ≈ u ∙ (v ∙ (w ∙ x))
-  [u∙vw]x≈u[v∙wx] = uv≈w⇒[x∙yu]v≈x∙yw refl u v
+    [u∙vw]x≈u[v∙wx] : (u ∙ (v ∙ w)) ∙ x ≈ u ∙ (v ∙ (w ∙ x))
+    [u∙vw]x≈u[v∙wx] = uv≈w⇒[x∙yu]v≈x∙yw refl u v
 
-  uv∙wx≈u[vw∙x] : (u ∙ v) ∙ (w ∙ x) ≈ u ∙ ((v ∙ w) ∙ x)
-  uv∙wx≈u[vw∙x] = uv≈w⇒xu∙vy≈x∙wy refl
+    uv∙wx≈u[vw∙x] : (u ∙ v) ∙ (w ∙ x) ≈ u ∙ ((v ∙ w) ∙ x)
+    uv∙wx≈u[vw∙x] = uv≈w⇒xu∙vy≈x∙wy refl
 
-  uv∙wx≈[u∙vw]x : (u ∙ v) ∙ (w ∙ x) ≈ (u ∙ (v ∙ w)) ∙ x
-  uv∙wx≈[u∙vw]x = sym [u∙vw]x≈uv∙wx
+    uv∙wx≈[u∙vw]x : (u ∙ v) ∙ (w ∙ x) ≈ (u ∙ (v ∙ w)) ∙ x
+    uv∙wx≈[u∙vw]x = sym [u∙vw]x≈uv∙wx
 
-  u[vw∙x]≈[uv∙w]x : u ∙ ((v ∙ w) ∙ x) ≈ ((u ∙ v) ∙ w) ∙ x
-  u[vw∙x]≈[uv∙w]x = sym [uv∙w]x≈u[vw∙x]
+    u[vw∙x]≈[uv∙w]x : u ∙ ((v ∙ w) ∙ x) ≈ ((u ∙ v) ∙ w) ∙ x
+    u[vw∙x]≈[uv∙w]x = sym [uv∙w]x≈u[vw∙x]
 
-  u[vw∙x]≈uv∙wx : u ∙ ((v ∙ w) ∙ x) ≈ (u ∙ v) ∙ (w ∙ x)
-  u[vw∙x]≈uv∙wx = sym uv∙wx≈u[vw∙x]
+    u[vw∙x]≈uv∙wx : u ∙ ((v ∙ w) ∙ x) ≈ (u ∙ v) ∙ (w ∙ x)
+    u[vw∙x]≈uv∙wx = sym uv∙wx≈u[vw∙x]
 
-  u[v∙wx]≈[uv∙w]x : u ∙ (v ∙ (w ∙ x)) ≈ ((u ∙ v) ∙ w) ∙ x
-  u[v∙wx]≈[uv∙w]x = sym [uv∙w]x≈u[v∙wx]
+    u[v∙wx]≈[uv∙w]x : u ∙ (v ∙ (w ∙ x)) ≈ ((u ∙ v) ∙ w) ∙ x
+    u[v∙wx]≈[uv∙w]x = sym [uv∙w]x≈u[v∙wx]
 
-  u[v∙wx]≈[u∙vw]x : u ∙ (v ∙ (w ∙ x)) ≈ (u ∙ (v ∙ w)) ∙ x
-  u[v∙wx]≈[u∙vw]x = sym [u∙vw]x≈u[v∙wx]
+    u[v∙wx]≈[u∙vw]x : u ∙ (v ∙ (w ∙ x)) ≈ (u ∙ (v ∙ w)) ∙ x
+    u[v∙wx]≈[u∙vw]x = sym [u∙vw]x≈u[v∙wx]
 
 module _ {u v w x : Carrier} (uv≈wx : u ∙ v ≈ w ∙ x) where
-  uv≈wx⇒yu∙v≈yw∙x : ∀ y → (y ∙ u) ∙ v ≈ (y ∙ w) ∙ x
-  uv≈wx⇒yu∙v≈yw∙x y = trans (uv≈w⇒xu∙v≈xw uv≈wx y) (sym (assoc y w x))
+    uv≈wx⇒yu∙v≈yw∙x : ∀ y → (y ∙ u) ∙ v ≈ (y ∙ w) ∙ x
+    uv≈wx⇒yu∙v≈yw∙x y = trans (uv≈w⇒xu∙v≈xw uv≈wx y) (sym (assoc y w x))
 
-  uv≈wx⇒u∙vy≈w∙xy : ∀ y → u ∙ (v ∙ y) ≈ w ∙ (x ∙ y)
-  uv≈wx⇒u∙vy≈w∙xy y = trans (uv≈w⇒u∙vx≈wx uv≈wx y) (assoc w x y)
-
-  uv≈wx⇒yu∙vz≈yw∙xz : ∀ y z → (y ∙ u) ∙ (v ∙ z) ≈ (y ∙ w) ∙ (x ∙ z)
-  uv≈wx⇒yu∙vz≈yw∙xz y z = trans (uv≈w⇒xu∙v≈xw (uv≈wx⇒u∙vy≈w∙xy z) y)(sym (assoc y w (x ∙ z)))
+    uv≈wx⇒u∙vy≈w∙xy : ∀ y → u ∙ (v ∙ y) ≈ w ∙ (x ∙ y)
+    uv≈wx⇒u∙vy≈w∙xy y = trans (uv≈w⇒u∙vx≈wx uv≈wx y) (assoc w x y)
 
+    uv≈wx⇒yu∙vz≈yw∙xz : ∀ y z → (y ∙ u) ∙ (v ∙ z) ≈ (y ∙ w) ∙ (x ∙ z)
+    uv≈wx⇒yu∙vz≈yw∙xz y z = trans (uv≈w⇒xu∙v≈xw (uv≈wx⇒u∙vy≈w∙xy z) y)(sym (assoc y w (x ∙ z)))

From 74607d506360e2c6b962c79ac5b7cfe280039c12 Mon Sep 17 00:00:00 2001
From: Jacques <149587529+jmougeot@users.noreply.github.com>
Date: Mon, 14 Apr 2025 14:36:07 -0400
Subject: [PATCH 23/31] Update src/Algebra/Properties/Semigroup.agda

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
---
 src/Algebra/Properties/Semigroup.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Algebra/Properties/Semigroup.agda b/src/Algebra/Properties/Semigroup.agda
index 0fbd24d86f..42157783fb 100644
--- a/src/Algebra/Properties/Semigroup.agda
+++ b/src/Algebra/Properties/Semigroup.agda
@@ -113,7 +113,7 @@ module _ {u v w x : Carrier} where
     u[v∙wx]≈[u∙vw]x : u ∙ (v ∙ (w ∙ x)) ≈ (u ∙ (v ∙ w)) ∙ x
     u[v∙wx]≈[u∙vw]x = sym [u∙vw]x≈u[v∙wx]
 
-module _ {u v w x : Carrier} (uv≈wx : u ∙ v ≈ w ∙ x) where
+module _ (uv≈wx : u ∙ v ≈ w ∙ x) where
     uv≈wx⇒yu∙v≈yw∙x : ∀ y → (y ∙ u) ∙ v ≈ (y ∙ w) ∙ x
     uv≈wx⇒yu∙v≈yw∙x y = trans (uv≈w⇒xu∙v≈xw uv≈wx y) (sym (assoc y w x))
 

From e3b25505797347f75badd2dcb3fcad11cf57b5b2 Mon Sep 17 00:00:00 2001
From: Jacques <149587529+jmougeot@users.noreply.github.com>
Date: Mon, 14 Apr 2025 14:36:54 -0400
Subject: [PATCH 24/31] Update CHANGELOG.md

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
---
 CHANGELOG.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index e4d4c4b72f..365607a11d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -123,7 +123,7 @@ New modules
 
 * `Data.Sign.Show` to show a sign
 
-* `Algebra.Properties.Semigroup` adding consequences for associtvity for semigroups
+* `Algebra.Properties.Semigroup` adding consequences for associativity for semigroups
 -----------------------------
 
 * In `Algebra.Construct.Pointwise`:

From e63afbd17cd9ece96f84745c8315a7b6b3b5c8fd Mon Sep 17 00:00:00 2001
From: Jacques <149587529+jmougeot@users.noreply.github.com>
Date: Mon, 14 Apr 2025 14:37:47 -0400
Subject: [PATCH 25/31] Update src/Algebra/Properties/Semigroup.agda

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
---
 src/Algebra/Properties/Semigroup.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Algebra/Properties/Semigroup.agda b/src/Algebra/Properties/Semigroup.agda
index 42157783fb..2b124f4c25 100644
--- a/src/Algebra/Properties/Semigroup.agda
+++ b/src/Algebra/Properties/Semigroup.agda
@@ -55,7 +55,7 @@ module _ (uv≈w : u ∙ v ≈ w) where
     uv≈w⇒[xu∙v]y≈x∙wy x y = trans (∙-congʳ (uv≈w⇒xu∙v≈xw x)) (assoc _ _ _)
 
     uv≈w⇒[xy∙u]v≈x∙yw : ∀ x y → ((x ∙ y) ∙ u) ∙ v ≈ x ∙ (y ∙ w)
-    uv≈w⇒[xy∙u]v≈x∙yw x y = trans (∙-congʳ (assoc x y u)) (uv≈w⇒[x∙yu]v≈x∙yw x  y )
+    uv≈w⇒[xy∙u]v≈x∙yw x y = trans (∙-congʳ (assoc x y u)) (uv≈w⇒[x∙yu]v≈x∙yw x y)
 
 module _ (uv≈w : u ∙ v ≈ w) where
     uv≈w⇒xw≈xu∙v : x ∙ w ≈ (x ∙ u) ∙ v

From b2bfa03ced5c9630b8b5517e806fd91e0be6d587 Mon Sep 17 00:00:00 2001
From: Jacques <149587529+jmougeot@users.noreply.github.com>
Date: Mon, 14 Apr 2025 14:38:20 -0400
Subject: [PATCH 26/31] Update src/Algebra/Properties/Semigroup.agda

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
---
 src/Algebra/Properties/Semigroup.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Algebra/Properties/Semigroup.agda b/src/Algebra/Properties/Semigroup.agda
index 2b124f4c25..8ae914f4ea 100644
--- a/src/Algebra/Properties/Semigroup.agda
+++ b/src/Algebra/Properties/Semigroup.agda
@@ -73,8 +73,8 @@ module _ (uv≈w : u ∙ v ≈ w) where
     uv≈w⇒x∙yw≈[x∙yu]v : ∀ x y  → x ∙ (y ∙ w) ≈ (x ∙ (y ∙ u)) ∙ v
     uv≈w⇒x∙yw≈[x∙yu]v x y  = sym (uv≈w⇒[x∙yu]v≈x∙yw uv≈w x y)
 
-    uv≈w⇒xu∙vy≈x∙wy : (x ∙ u) ∙ (v ∙ y) ≈ x ∙ (w ∙ y)
-    uv≈w⇒xu∙vy≈x∙wy = uv≈w⇒xu∙v≈xw (uv≈w⇒u∙vx≈wx uv≈w _) _
+    uv≈w⇒xu∙vy≈x∙wy : ∀ x y → (x ∙ u) ∙ (v ∙ y) ≈ x ∙ (w ∙ y)
+    uv≈w⇒xu∙vy≈x∙wy x y = uv≈w⇒xu∙v≈xw (uv≈w⇒u∙vx≈wx uv≈w x) y
 
     uv≈w⇒xy≈z⇒u[vx∙y]≈wz : ∀ z → x ∙ y ≈ z → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ z
     uv≈w⇒xy≈z⇒u[vx∙y]≈wz z xy≈z = trans (∙-congˡ (uv≈w⇒xu∙v≈xw xy≈z v)) (uv≈w⇒u∙vx≈wx uv≈w z)

From 14224b950ce28332c6968665414f596ed839cd01 Mon Sep 17 00:00:00 2001
From: Jacques <149587529+jmougeot@users.noreply.github.com>
Date: Mon, 14 Apr 2025 14:38:48 -0400
Subject: [PATCH 27/31] Update src/Algebra/Properties/Semigroup.agda

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
---
 src/Algebra/Properties/Semigroup.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Algebra/Properties/Semigroup.agda b/src/Algebra/Properties/Semigroup.agda
index 8ae914f4ea..e506c1a6f1 100644
--- a/src/Algebra/Properties/Semigroup.agda
+++ b/src/Algebra/Properties/Semigroup.agda
@@ -76,8 +76,8 @@ module _ (uv≈w : u ∙ v ≈ w) where
     uv≈w⇒xu∙vy≈x∙wy : ∀ x y → (x ∙ u) ∙ (v ∙ y) ≈ x ∙ (w ∙ y)
     uv≈w⇒xu∙vy≈x∙wy x y = uv≈w⇒xu∙v≈xw (uv≈w⇒u∙vx≈wx uv≈w x) y
 
-    uv≈w⇒xy≈z⇒u[vx∙y]≈wz : ∀ z → x ∙ y ≈ z → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ z
-    uv≈w⇒xy≈z⇒u[vx∙y]≈wz z xy≈z = trans (∙-congˡ (uv≈w⇒xu∙v≈xw xy≈z v)) (uv≈w⇒u∙vx≈wx uv≈w z)
+    uv≈w⇒xy≈z⇒u[vx∙y]≈wz : ∀ x y → x ∙ y ≈ z → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ z
+    uv≈w⇒xy≈z⇒u[vx∙y]≈wz x y xy≈z = trans (∙-congˡ (uv≈w⇒xu∙v≈xw xy≈z v)) (uv≈w⇒u∙vx≈wx uv≈w _)
 
     uv≈w⇒x∙wy≈x∙[u∙vy] : x ∙ (w ∙ y) ≈ x ∙ (u ∙ (v ∙ y))
     uv≈w⇒x∙wy≈x∙[u∙vy] = sym (uv≈w⇒x[uv∙y]≈x∙wy uv≈w _ _)

From 76b6637689273c4914c8fb2ccf4ce91a78ab66c5 Mon Sep 17 00:00:00 2001
From: Jacques <149587529+jmougeot@users.noreply.github.com>
Date: Mon, 14 Apr 2025 14:39:06 -0400
Subject: [PATCH 28/31] Update src/Algebra/Properties/Semigroup.agda

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
---
 src/Algebra/Properties/Semigroup.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Algebra/Properties/Semigroup.agda b/src/Algebra/Properties/Semigroup.agda
index e506c1a6f1..689045431a 100644
--- a/src/Algebra/Properties/Semigroup.agda
+++ b/src/Algebra/Properties/Semigroup.agda
@@ -82,7 +82,7 @@ module _ (uv≈w : u ∙ v ≈ w) where
     uv≈w⇒x∙wy≈x∙[u∙vy] : x ∙ (w ∙ y) ≈ x ∙ (u ∙ (v ∙ y))
     uv≈w⇒x∙wy≈x∙[u∙vy] = sym (uv≈w⇒x[uv∙y]≈x∙wy uv≈w _ _)
 
-module _ {u v w x : Carrier} where
+module _ u v w x where
     [uv∙w]x≈u[vw∙x] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ ((v ∙ w) ∙ x)
     [uv∙w]x≈u[vw∙x] = uv≈w⇒[xu∙v]y≈x∙wy refl u x
 

From 06af3274ab0f0e0843b95eb00b95f78f9243c51e Mon Sep 17 00:00:00 2001
From: Jacques <149587529+jmougeot@users.noreply.github.com>
Date: Mon, 14 Apr 2025 14:39:22 -0400
Subject: [PATCH 29/31] Update src/Algebra/Properties/Semigroup.agda

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
---
 src/Algebra/Properties/Semigroup.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Algebra/Properties/Semigroup.agda b/src/Algebra/Properties/Semigroup.agda
index 689045431a..8ea3b38b0a 100644
--- a/src/Algebra/Properties/Semigroup.agda
+++ b/src/Algebra/Properties/Semigroup.agda
@@ -79,8 +79,8 @@ module _ (uv≈w : u ∙ v ≈ w) where
     uv≈w⇒xy≈z⇒u[vx∙y]≈wz : ∀ x y → x ∙ y ≈ z → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ z
     uv≈w⇒xy≈z⇒u[vx∙y]≈wz x y xy≈z = trans (∙-congˡ (uv≈w⇒xu∙v≈xw xy≈z v)) (uv≈w⇒u∙vx≈wx uv≈w _)
 
-    uv≈w⇒x∙wy≈x∙[u∙vy] : x ∙ (w ∙ y) ≈ x ∙ (u ∙ (v ∙ y))
-    uv≈w⇒x∙wy≈x∙[u∙vy] = sym (uv≈w⇒x[uv∙y]≈x∙wy uv≈w _ _)
+    uv≈w⇒x∙wy≈x∙[u∙vy] : ∀ x y → x ∙ (w ∙ y) ≈ x ∙ (u ∙ (v ∙ y))
+    uv≈w⇒x∙wy≈x∙[u∙vy] x y = sym (uv≈w⇒x[uv∙y]≈x∙wy uv≈w x y)
 
 module _ u v w x where
     [uv∙w]x≈u[vw∙x] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ ((v ∙ w) ∙ x)

From a22f97db20bb42a1a806085fe49879ff6454f43e Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Mon, 14 Apr 2025 15:40:18 -0400
Subject: [PATCH 30/31]  variables

---
 src/Algebra/Properties/Semigroup.agda | 36 +++++++++++++--------------
 1 file changed, 18 insertions(+), 18 deletions(-)

diff --git a/src/Algebra/Properties/Semigroup.agda b/src/Algebra/Properties/Semigroup.agda
index 8ea3b38b0a..cbf96208ec 100644
--- a/src/Algebra/Properties/Semigroup.agda
+++ b/src/Algebra/Properties/Semigroup.agda
@@ -37,32 +37,32 @@ flexible x y = assoc x y x
 
 module _ (uv≈w : u ∙ v ≈ w) where
     uv≈w⇒xu∙v≈xw : ∀ x → (x ∙ u) ∙ v ≈ x ∙ w
-    uv≈w⇒xu∙v≈xw x =  trans (assoc x u v) (∙-congˡ uv≈w)
+    uv≈w⇒xu∙v≈xw x = trans (assoc x u v) (∙-congˡ uv≈w)
 
     uv≈w⇒u∙vx≈wx : ∀ x → u ∙ (v ∙ x) ≈ w ∙ x
     uv≈w⇒u∙vx≈wx x = trans (sym (assoc u v x)) (∙-congʳ uv≈w)
 
     uv≈w⇒u[vx∙y]≈w∙xy : ∀ x y → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ (x ∙ y)
-    uv≈w⇒u[vx∙y]≈w∙xy x y  = trans (∙-congˡ (assoc v x y)) (uv≈w⇒u∙vx≈wx (x ∙ y))
+    uv≈w⇒u[vx∙y]≈w∙xy x y = trans (∙-congˡ (assoc v x y)) (uv≈w⇒u∙vx≈wx (x ∙ y))
 
     uv≈w⇒x[uv∙y]≈x∙wy : ∀ x y → x ∙ (u ∙ (v ∙ y)) ≈ x ∙ (w ∙ y)
     uv≈w⇒x[uv∙y]≈x∙wy x y = ∙-congˡ (uv≈w⇒u∙vx≈wx y)
 
     uv≈w⇒[x∙yu]v≈x∙yw : ∀ x y → (x ∙ (y ∙ u)) ∙ v ≈ x ∙ (y ∙ w)
-    uv≈w⇒[x∙yu]v≈x∙yw  x y = trans (assoc x (y ∙ u) v) (∙-congˡ (uv≈w⇒xu∙v≈xw y))
+    uv≈w⇒[x∙yu]v≈x∙yw x y = trans (assoc x (y ∙ u) v) (∙-congˡ (uv≈w⇒xu∙v≈xw y))
 
     uv≈w⇒[xu∙v]y≈x∙wy : ∀ x y → ((x ∙ u) ∙ v) ∙ y ≈ x ∙ (w ∙ y)
-    uv≈w⇒[xu∙v]y≈x∙wy x y = trans (∙-congʳ (uv≈w⇒xu∙v≈xw x)) (assoc _ _ _)
+    uv≈w⇒[xu∙v]y≈x∙wy x y = trans (∙-congʳ (uv≈w⇒xu∙v≈xw x)) (assoc x w y)
 
     uv≈w⇒[xy∙u]v≈x∙yw : ∀ x y → ((x ∙ y) ∙ u) ∙ v ≈ x ∙ (y ∙ w)
-    uv≈w⇒[xy∙u]v≈x∙yw x y = trans (∙-congʳ (assoc x y u)) (uv≈w⇒[x∙yu]v≈x∙yw x y)
+    uv≈w⇒[xy∙u]v≈x∙yw x y = trans (∙-congʳ (assoc x y u)) (uv≈w⇒[x∙yu]v≈x∙yw x  y )
 
 module _ (uv≈w : u ∙ v ≈ w) where
-    uv≈w⇒xw≈xu∙v : x ∙ w ≈ (x ∙ u) ∙ v
-    uv≈w⇒xw≈xu∙v = sym (uv≈w⇒xu∙v≈xw uv≈w _)
+    uv≈w⇒xw≈xu∙v : ∀ x → x ∙ w ≈ (x ∙ u) ∙ v
+    uv≈w⇒xw≈xu∙v x = sym (uv≈w⇒xu∙v≈xw uv≈w x)
 
-    uv≈w⇒wx≈u∙vx : w ∙ x ≈ u ∙ (v ∙ x)
-    uv≈w⇒wx≈u∙vx = sym (uv≈w⇒u∙vx≈wx uv≈w _)
+    uv≈w⇒wx≈u∙vx : ∀ x → w ∙ x ≈ u ∙ (v ∙ x)
+    uv≈w⇒wx≈u∙vx x = sym (uv≈w⇒u∙vx≈wx uv≈w x)
 
     uv≈w⇒w∙xy≈u[vx∙y] : ∀ x y → w ∙ (x ∙ y) ≈ u ∙ ((v ∙ x) ∙ y)
     uv≈w⇒w∙xy≈u[vx∙y] x y = sym (uv≈w⇒u[vx∙y]≈w∙xy uv≈w x y)
@@ -74,15 +74,15 @@ module _ (uv≈w : u ∙ v ≈ w) where
     uv≈w⇒x∙yw≈[x∙yu]v x y  = sym (uv≈w⇒[x∙yu]v≈x∙yw uv≈w x y)
 
     uv≈w⇒xu∙vy≈x∙wy : ∀ x y → (x ∙ u) ∙ (v ∙ y) ≈ x ∙ (w ∙ y)
-    uv≈w⇒xu∙vy≈x∙wy x y = uv≈w⇒xu∙v≈xw (uv≈w⇒u∙vx≈wx uv≈w x) y
+    uv≈w⇒xu∙vy≈x∙wy x y = uv≈w⇒xu∙v≈xw (uv≈w⇒u∙vx≈wx uv≈w y) x
 
-    uv≈w⇒xy≈z⇒u[vx∙y]≈wz : ∀ x y → x ∙ y ≈ z → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ z
-    uv≈w⇒xy≈z⇒u[vx∙y]≈wz x y xy≈z = trans (∙-congˡ (uv≈w⇒xu∙v≈xw xy≈z v)) (uv≈w⇒u∙vx≈wx uv≈w _)
+    uv≈w⇒xy≈z⇒u[vx∙y]≈wz : ∀ z → x ∙ y ≈ z → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ z
+    uv≈w⇒xy≈z⇒u[vx∙y]≈wz z xy≈z = trans (∙-congˡ (uv≈w⇒xu∙v≈xw xy≈z v)) (uv≈w⇒u∙vx≈wx uv≈w z)
 
-    uv≈w⇒x∙wy≈x∙[u∙vy] : ∀ x y → x ∙ (w ∙ y) ≈ x ∙ (u ∙ (v ∙ y))
-    uv≈w⇒x∙wy≈x∙[u∙vy] x y = sym (uv≈w⇒x[uv∙y]≈x∙wy uv≈w x y)
+    uv≈w⇒x∙wy≈x∙[u∙vy] : x ∙ (w ∙ y) ≈ x ∙ (u ∙ (v ∙ y))
+    uv≈w⇒x∙wy≈x∙[u∙vy] = sym (uv≈w⇒x[uv∙y]≈x∙wy uv≈w _ _)
 
-module _ u v w x where
+module _ {u v w x : Carrier} where
     [uv∙w]x≈u[vw∙x] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ ((v ∙ w) ∙ x)
     [uv∙w]x≈u[vw∙x] = uv≈w⇒[xu∙v]y≈x∙wy refl u x
 
@@ -96,7 +96,7 @@ module _ u v w x where
     [u∙vw]x≈u[v∙wx] = uv≈w⇒[x∙yu]v≈x∙yw refl u v
 
     uv∙wx≈u[vw∙x] : (u ∙ v) ∙ (w ∙ x) ≈ u ∙ ((v ∙ w) ∙ x)
-    uv∙wx≈u[vw∙x] = uv≈w⇒xu∙vy≈x∙wy refl
+    uv∙wx≈u[vw∙x] = uv≈w⇒xu∙vy≈x∙wy refl u x
 
     uv∙wx≈[u∙vw]x : (u ∙ v) ∙ (w ∙ x) ≈ (u ∙ (v ∙ w)) ∙ x
     uv∙wx≈[u∙vw]x = sym [u∙vw]x≈uv∙wx
@@ -113,7 +113,7 @@ module _ u v w x where
     u[v∙wx]≈[u∙vw]x : u ∙ (v ∙ (w ∙ x)) ≈ (u ∙ (v ∙ w)) ∙ x
     u[v∙wx]≈[u∙vw]x = sym [u∙vw]x≈u[v∙wx]
 
-module _ (uv≈wx : u ∙ v ≈ w ∙ x) where
+module _ {u v w x : Carrier} (uv≈wx : u ∙ v ≈ w ∙ x) where
     uv≈wx⇒yu∙v≈yw∙x : ∀ y → (y ∙ u) ∙ v ≈ (y ∙ w) ∙ x
     uv≈wx⇒yu∙v≈yw∙x y = trans (uv≈w⇒xu∙v≈xw uv≈wx y) (sym (assoc y w x))
 
@@ -121,4 +121,4 @@ module _ (uv≈wx : u ∙ v ≈ w ∙ x) where
     uv≈wx⇒u∙vy≈w∙xy y = trans (uv≈w⇒u∙vx≈wx uv≈wx y) (assoc w x y)
 
     uv≈wx⇒yu∙vz≈yw∙xz : ∀ y z → (y ∙ u) ∙ (v ∙ z) ≈ (y ∙ w) ∙ (x ∙ z)
-    uv≈wx⇒yu∙vz≈yw∙xz y z = trans (uv≈w⇒xu∙v≈xw (uv≈wx⇒u∙vy≈w∙xy z) y)(sym (assoc y w (x ∙ z)))
+    uv≈wx⇒yu∙vz≈yw∙xz y z = trans (uv≈w⇒xu∙v≈xw (uv≈wx⇒u∙vy≈w∙xy z) y) (sym (assoc y w (x ∙ z)))

From 1283b57f3cc883c440a7c7975577c53b0a9dc0d0 Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Wed, 16 Apr 2025 12:13:15 -0400
Subject: [PATCH 31/31] update CHANGELOG

---
 CHANGELOG.md | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 365607a11d..1e6392c378 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -123,9 +123,11 @@ New modules
 
 * `Data.Sign.Show` to show a sign
 
-* `Algebra.Properties.Semigroup` adding consequences for associativity for semigroups
+Additions to existing modules
 -----------------------------
 
+* In `Algebra.Properties.Semigroup` adding consequences for associativity for semigroups
+
 * In `Algebra.Construct.Pointwise`:
   ```agda
   isNearSemiring                  : IsNearSemiring _≈_ _+_ _*_ 0# →