From b9845ceac359e477880376b5e2078f057850f973 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 2 Apr 2024 07:26:23 +0100
Subject: [PATCH 01/39] beginnings

---
 src/Algebra/Construct/WreathProduct.agda | 74 ++++++++++++++++++++++++
 1 file changed, 74 insertions(+)
 create mode 100644 src/Algebra/Construct/WreathProduct.agda

diff --git a/src/Algebra/Construct/WreathProduct.agda b/src/Algebra/Construct/WreathProduct.agda
new file mode 100644
index 0000000000..299176ba60
--- /dev/null
+++ b/src/Algebra/Construct/WreathProduct.agda
@@ -0,0 +1,74 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Monoid Actions and Wreath Products of a Monoid with a Monoid Action
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Algebra.Construct.WreathProduct where
+
+open import Algebra.Bundles.Raw using (RawMonoid)
+open import Algebra.Bundles using (Monoid)
+open import Algebra.Structures using (IsMonoid)
+
+open import Data.Product.Base using (_,_; _×_)
+
+open import Function.Base using (flip)
+
+open import Level using (Level; suc; _⊔_)
+
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Structures using (IsEquivalence)
+open import Relation.Binary.Definitions
+
+private
+  variable
+    a c r ℓ : Level
+
+
+module MonoidAction (𝓜 : Monoid c ℓ) (𝓐 : Setoid a r) where
+
+  private
+
+    open module M = Monoid 𝓜 using () renaming (Carrier to M)
+    open module A = Setoid 𝓐 using (_≈_) renaming (Carrier to A)
+
+    variable
+      x y z : A
+      m n p q : M
+
+  record RawMonoidAction : Set (a ⊔ r ⊔ c ⊔ ℓ)  where
+    --constructor mkRawAct
+
+    infixr 5 _∙_
+
+    field
+      _∙_ : M → A → A
+
+  record MonoidAction (rawMonoidAction : RawMonoidAction) : Set (a ⊔ r ⊔ c ⊔ ℓ)  where
+    --constructor mkAct
+
+    open RawMonoidAction rawMonoidAction
+
+    field
+      ∙-cong : m M.≈ n → x ≈ y → m ∙ x ≈ n ∙ y
+      ∙-act  : ∀ m n x → m M.∙ n ∙ x ≈ m ∙ n ∙ x
+      ε-act  : ∀ x → M.ε ∙ x ≈ x
+
+module LeftRegular (𝓜 : Monoid c ℓ) where
+  private
+
+    open module M = Monoid 𝓜 using (setoid)
+    open MonoidAction 𝓜 setoid
+
+  rawMonoidAction : RawMonoidAction
+  rawMonoidAction = record { _∙_ = M._∙_ }
+
+  monoidAction : MonoidAction rawMonoidAction
+  monoidAction = record
+    { ∙-cong = M.∙-cong
+    ; ∙-act = M.assoc
+    ; ε-act = M.identityˡ
+    }
+

From 43c9fdb5e31ac47e883cb6cd7e1c3f022e33c713 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Tue, 9 Apr 2024 14:52:38 +0100
Subject: [PATCH 02/39] factored out `MonoidAction`

---
 src/Algebra/Construct/MonoidAction.agda | 227 ++++++++++++++++++++++++
 1 file changed, 227 insertions(+)
 create mode 100644 src/Algebra/Construct/MonoidAction.agda

diff --git a/src/Algebra/Construct/MonoidAction.agda b/src/Algebra/Construct/MonoidAction.agda
new file mode 100644
index 0000000000..074c4988b3
--- /dev/null
+++ b/src/Algebra/Construct/MonoidAction.agda
@@ -0,0 +1,227 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Monoid Actions and the free Monoid Action on a Setoid
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Algebra.Construct.MonoidAction where
+
+open import Algebra.Bundles using (Monoid)
+open import Algebra.Structures using (IsMonoid)
+
+open import Data.List.Base
+  using (List; []; _∷_; _++_; foldl; foldr)
+import Data.List.Properties as List
+open import Data.List.Relation.Binary.Pointwise as Pointwise
+  using (Pointwise; []; _∷_)
+import Data.List.Relation.Binary.Equality.Setoid as ≋
+open import Data.Product.Base using (_,_)
+
+open import Function.Base using (id; _∘_; flip)
+
+open import Level using (Level; suc; _⊔_)
+
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Structures using (IsEquivalence)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Definitions
+
+private
+  variable
+    a c r ℓ : Level
+    A : Set a
+    M : Set c
+
+
+------------------------------------------------------------------------
+-- Basic definitions: fix notation for underlying 'raw' actions
+
+module _ {c a ℓ r} {M : Set c} {A : Set a}
+         (_≈ᴹ_ : Rel M ℓ) (_≈_ : Rel A r)
+  where
+
+  private
+    variable
+      x y z : A
+      m n p q : M
+      ms ns ps qs : List M
+
+  record RawLeftAction : Set (a ⊔ r ⊔ c ⊔ ℓ)  where
+    infixr 5 _ᴹ∙ᴬ_ _ᴹ⋆ᴬ_
+
+    field
+      _ᴹ∙ᴬ_ : M → A → A
+      ∙-cong : m ≈ᴹ n → x ≈ y → (m ᴹ∙ᴬ x) ≈ (n ᴹ∙ᴬ y)
+
+-- derived form: iterated action, satisfying congruence
+
+    _ᴹ⋆ᴬ_ : List M → A → A
+    ms ᴹ⋆ᴬ a = foldr _ᴹ∙ᴬ_ a ms
+
+    ⋆-cong : Pointwise _≈ᴹ_ ms ns → x ≈ y → (ms ᴹ⋆ᴬ x) ≈ (ns ᴹ⋆ᴬ y)
+    ⋆-cong []            x≈y = x≈y
+    ⋆-cong (m≈n ∷ ms≋ns) x≈y = ∙-cong m≈n (⋆-cong ms≋ns x≈y)
+
+    ⋆-act-cong : Reflexive _≈ᴹ_ →
+                 ∀ ms ns → x ≈ y → ((ms ++ ns) ᴹ⋆ᴬ x) ≈ (ms ᴹ⋆ᴬ ns ᴹ⋆ᴬ y)
+    ⋆-act-cong refl []       ns x≈y = ⋆-cong {ns = ns} (Pointwise.refl refl) x≈y
+    ⋆-act-cong refl (m ∷ ms) ns x≈y = ∙-cong refl (⋆-act-cong refl ms ns x≈y)
+
+    []-act-cong : x ≈ y → ([] ᴹ⋆ᴬ x) ≈ y
+    []-act-cong = id
+
+  record RawRightAction : Set (a ⊔ r ⊔ c ⊔ ℓ)  where
+    infixl 5 _ᴬ∙ᴹ_ _ᴬ⋆ᴹ_
+
+    field
+      _ᴬ∙ᴹ_ : A → M → A
+      ∙-cong : x ≈ y → m ≈ᴹ n → (x ᴬ∙ᴹ m) ≈ (y ᴬ∙ᴹ n)
+    
+-- derived form: iterated action, satisfying congruence
+
+    _ᴬ⋆ᴹ_ : A → List M → A
+    a ᴬ⋆ᴹ ms = foldl _ᴬ∙ᴹ_ a ms
+
+    ⋆-cong : x ≈ y → Pointwise _≈ᴹ_ ms ns → (x ᴬ⋆ᴹ ms) ≈ (y ᴬ⋆ᴹ ns)
+    ⋆-cong x≈y []            = x≈y
+    ⋆-cong x≈y (m≈n ∷ ms≋ns) = ⋆-cong (∙-cong x≈y m≈n) ms≋ns
+
+    ⋆-act-cong : Reflexive _≈ᴹ_ →
+                 x ≈ y → ∀ ms ns → (x ᴬ⋆ᴹ (ms ++ ns)) ≈ (y ᴬ⋆ᴹ ms ᴬ⋆ᴹ ns)
+    ⋆-act-cong refl x≈y []       ns = ⋆-cong {ns = ns} x≈y (Pointwise.refl refl)
+    ⋆-act-cong refl x≈y (m ∷ ms) ns = ⋆-act-cong refl (∙-cong x≈y refl) ms ns
+
+    []-act-cong : x ≈ y → (x ᴬ⋆ᴹ []) ≈ y
+    []-act-cong = id
+
+
+------------------------------------------------------------------------
+-- Definition: indexed over an underlying raw action
+
+module _ (M : Monoid c ℓ) (A : Setoid a r) where
+
+  private
+
+    open module M = Monoid M using () renaming (Carrier to M)
+    open module A = Setoid A using (_≈_) renaming (Carrier to A)
+    open ≋ M.setoid using (_≋_; [] ; _∷_)
+
+    variable
+      x y z : A.Carrier
+      m n p q : M.Carrier
+      ms ns ps qs : List M.Carrier
+
+  record LeftAction (rawLeftAction : RawLeftAction M._≈_ _≈_) : Set (a ⊔ r ⊔ c ⊔ ℓ)
+    where
+
+    open RawLeftAction rawLeftAction public
+      renaming (_ᴹ∙ᴬ_ to _∙_; _ᴹ⋆ᴬ_ to _⋆_)
+
+    field
+      ∙-act  : ∀ m n x → m M.∙ n ∙ x ≈ m ∙ n ∙ x
+      ε-act  : ∀ x → M.ε ∙ x ≈ x
+
+    ∙-congˡ : x ≈ y → m ∙ x ≈ m ∙ y
+    ∙-congˡ x≈y = ∙-cong M.refl x≈y
+
+    ∙-congʳ : m M.≈ n → m ∙ x ≈ n ∙ x
+    ∙-congʳ m≈n = ∙-cong m≈n A.refl
+
+    ⋆-act : ∀ ms ns x → (ms ++ ns) ⋆ x ≈ ms ⋆ ns ⋆ x
+    ⋆-act ms ns x = ⋆-act-cong M.refl ms ns A.refl
+
+    []-act : ∀ x → [] ⋆ x ≈ x
+    []-act _ = []-act-cong A.refl
+
+  record RightAction (rawRightAction : RawRightAction M._≈_ _≈_) : Set (a ⊔ r ⊔ c ⊔ ℓ)
+    where
+
+    open RawRightAction rawRightAction public
+      renaming (_ᴬ∙ᴹ_ to _∙_; _ᴬ⋆ᴹ_ to _⋆_)
+
+    field
+      ∙-act  : ∀ x m n → x ∙ m M.∙ n ≈ x ∙ m ∙ n
+      ε-act  : ∀ x → x ∙ M.ε ≈ x
+
+    ∙-congˡ : x ≈ y → x ∙ m ≈ y ∙ m
+    ∙-congˡ x≈y = ∙-cong x≈y M.refl
+
+    ∙-congʳ : m M.≈ n → x ∙ m ≈ x ∙ n
+    ∙-congʳ m≈n = ∙-cong A.refl m≈n
+
+    ⋆-act : ∀ x ms ns → x ⋆ (ms ++ ns) ≈ x ⋆ ms ⋆ ns
+    ⋆-act _ = ⋆-act-cong M.refl A.refl
+
+    []-act : ∀ x → x ⋆ [] ≈ x
+    []-act x = []-act-cong A.refl
+
+------------------------------------------------------------------------
+-- Distinguished actions: of a module over itself
+
+module Regular (M : Monoid c ℓ) where
+
+  open Monoid M
+
+  private
+    rawLeftAction : RawLeftAction _≈_ _≈_
+    rawLeftAction = record { _ᴹ∙ᴬ_ = _∙_ ; ∙-cong = ∙-cong }
+
+    rawRightAction : RawRightAction _≈_ _≈_
+    rawRightAction = record { _ᴬ∙ᴹ_ = _∙_ ; ∙-cong = ∙-cong }
+
+  leftAction : LeftAction M setoid rawLeftAction
+  leftAction = record
+    { ∙-act = assoc
+    ; ε-act = identityˡ
+    }
+
+  rightAction : RightAction M setoid rawRightAction
+  rightAction = record
+    { ∙-act = λ x m n → sym (assoc x m n)
+    ; ε-act = identityʳ
+    }
+
+------------------------------------------------------------------------
+-- Distinguished *free* action: lifting a raw action to a List action
+
+module Free (M : Setoid c ℓ) (S : Setoid a r) where
+
+  private
+
+    open ≋ M using (_≋_; ≋-refl; ≋-reflexive; ≋-isEquivalence; ++⁺)
+    open module M = Setoid M using () renaming (Carrier to M)
+    open module A = Setoid S using (_≈_) renaming (Carrier to A)
+
+    isMonoid : IsMonoid _≋_ _++_ []
+    isMonoid = record
+      { isSemigroup = record
+        { isMagma = record
+          { isEquivalence = ≋-isEquivalence
+          ; ∙-cong = ++⁺
+          }
+        ; assoc = λ xs ys zs → ≋-reflexive (List.++-assoc xs ys zs)
+        }
+      ; identity = (λ _ → ≋-refl) , ≋-reflexive ∘ List.++-identityʳ }
+
+    monoid : Monoid _ _
+    monoid = record { isMonoid = isMonoid }
+
+  leftAction : (rawLeftAction : RawLeftAction M._≈_ _≈_) →
+               (open RawLeftAction rawLeftAction) →
+               LeftAction monoid S (record { _ᴹ∙ᴬ_ = _ᴹ⋆ᴬ_  ; ∙-cong = ⋆-cong })
+  leftAction rawLeftAction = record
+    { ∙-act = λ ms ns x → ⋆-act-cong M.refl ms ns A.refl
+    ; ε-act = λ _ → []-act-cong A.refl
+    }
+    where open RawLeftAction rawLeftAction
+
+  rightAction : (rawRightAction : RawRightAction M._≈_ _≈_) →
+                (open RawRightAction rawRightAction) →
+                RightAction monoid S (record { _ᴬ∙ᴹ_ = _ᴬ⋆ᴹ_  ; ∙-cong = ⋆-cong })
+  rightAction rawRightAction = record
+    { ∙-act = λ _ → ⋆-act-cong M.refl A.refl
+    ; ε-act = λ _ → []-act-cong A.refl
+    }
+    where open RawRightAction rawRightAction

From a5031566f4c31cc35938914ee0d963325c6e71d6 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Tue, 9 Apr 2024 15:23:47 +0100
Subject: [PATCH 03/39] second beginning

---
 src/Algebra/Construct/WreathProduct.agda | 70 +++++++-----------------
 1 file changed, 21 insertions(+), 49 deletions(-)

diff --git a/src/Algebra/Construct/WreathProduct.agda b/src/Algebra/Construct/WreathProduct.agda
index 299176ba60..5b0cfedb41 100644
--- a/src/Algebra/Construct/WreathProduct.agda
+++ b/src/Algebra/Construct/WreathProduct.agda
@@ -1,15 +1,22 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Monoid Actions and Wreath Products of a Monoid with a Monoid Action
+-- The Wreath Product of a Monoid N with a Monoid Action of M on A
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-module Algebra.Construct.WreathProduct where
+open import Algebra.Bundles using (Monoid)
+open import Algebra.Construct.MonoidAction using (RawLeftAction; LeftAction)
+open import Relation.Binary.Bundles using (Setoid)
+
+module Algebra.Construct.WreathProduct
+  {b c ℓb ℓc a r} {M : Monoid b ℓb} {A : Setoid a r}
+  {rawLeftAction : RawLeftAction (Monoid._≈_ M) (Setoid._≈_ A)}
+  (M∙A : LeftAction M A rawLeftAction) (N : Monoid c ℓc)
+  where
 
 open import Algebra.Bundles.Raw using (RawMonoid)
-open import Algebra.Bundles using (Monoid)
 open import Algebra.Structures using (IsMonoid)
 
 open import Data.Product.Base using (_,_; _×_)
@@ -18,57 +25,22 @@ open import Function.Base using (flip)
 
 open import Level using (Level; suc; _⊔_)
 
-open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Structures using (IsEquivalence)
 open import Relation.Binary.Definitions
 
+open module M = Monoid M using () renaming (Carrier to M)
+open module N = Monoid N using () renaming (Carrier to N)
+open module A = Setoid A using (_≈_) renaming (Carrier to A)
+
 private
   variable
-    a c r ℓ : Level
-
-
-module MonoidAction (𝓜 : Monoid c ℓ) (𝓐 : Setoid a r) where
-
-  private
-
-    open module M = Monoid 𝓜 using () renaming (Carrier to M)
-    open module A = Setoid 𝓐 using (_≈_) renaming (Carrier to A)
+    x y z : A.Carrier
+    m m′ m″ : M.Carrier
+    n n′ n″ : N.Carrier
 
-    variable
-      x y z : A
-      m n p q : M
 
-  record RawMonoidAction : Set (a ⊔ r ⊔ c ⊔ ℓ)  where
-    --constructor mkRawAct
-
-    infixr 5 _∙_
-
-    field
-      _∙_ : M → A → A
-
-  record MonoidAction (rawMonoidAction : RawMonoidAction) : Set (a ⊔ r ⊔ c ⊔ ℓ)  where
-    --constructor mkAct
-
-    open RawMonoidAction rawMonoidAction
-
-    field
-      ∙-cong : m M.≈ n → x ≈ y → m ∙ x ≈ n ∙ y
-      ∙-act  : ∀ m n x → m M.∙ n ∙ x ≈ m ∙ n ∙ x
-      ε-act  : ∀ x → M.ε ∙ x ≈ x
-
-module LeftRegular (𝓜 : Monoid c ℓ) where
-  private
-
-    open module M = Monoid 𝓜 using (setoid)
-    open MonoidAction 𝓜 setoid
-
-  rawMonoidAction : RawMonoidAction
-  rawMonoidAction = record { _∙_ = M._∙_ }
-
-  monoidAction : MonoidAction rawMonoidAction
-  monoidAction = record
-    { ∙-cong = M.∙-cong
-    ; ∙-act = M.assoc
-    ; ε-act = M.identityˡ
-    }
+------------------------------------------------------------------------
+-- Infix notation for when opening the module unparameterised
 
+infixl 4 _⋊_
+_⋊_ = {!monoidᵂ!}

From e2a981554c6c3f9e091f2548f9d253c96b6bb11b Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Tue, 9 Apr 2024 15:25:58 +0100
Subject: [PATCH 04/39] start small(er)

---
 src/Algebra/Construct/WreathProduct.agda | 46 ------------------------
 1 file changed, 46 deletions(-)
 delete mode 100644 src/Algebra/Construct/WreathProduct.agda

diff --git a/src/Algebra/Construct/WreathProduct.agda b/src/Algebra/Construct/WreathProduct.agda
deleted file mode 100644
index 5b0cfedb41..0000000000
--- a/src/Algebra/Construct/WreathProduct.agda
+++ /dev/null
@@ -1,46 +0,0 @@
-------------------------------------------------------------------------
--- The Agda standard library
---
--- The Wreath Product of a Monoid N with a Monoid Action of M on A
-------------------------------------------------------------------------
-
-{-# OPTIONS --cubical-compatible --safe #-}
-
-open import Algebra.Bundles using (Monoid)
-open import Algebra.Construct.MonoidAction using (RawLeftAction; LeftAction)
-open import Relation.Binary.Bundles using (Setoid)
-
-module Algebra.Construct.WreathProduct
-  {b c ℓb ℓc a r} {M : Monoid b ℓb} {A : Setoid a r}
-  {rawLeftAction : RawLeftAction (Monoid._≈_ M) (Setoid._≈_ A)}
-  (M∙A : LeftAction M A rawLeftAction) (N : Monoid c ℓc)
-  where
-
-open import Algebra.Bundles.Raw using (RawMonoid)
-open import Algebra.Structures using (IsMonoid)
-
-open import Data.Product.Base using (_,_; _×_)
-
-open import Function.Base using (flip)
-
-open import Level using (Level; suc; _⊔_)
-
-open import Relation.Binary.Structures using (IsEquivalence)
-open import Relation.Binary.Definitions
-
-open module M = Monoid M using () renaming (Carrier to M)
-open module N = Monoid N using () renaming (Carrier to N)
-open module A = Setoid A using (_≈_) renaming (Carrier to A)
-
-private
-  variable
-    x y z : A.Carrier
-    m m′ m″ : M.Carrier
-    n n′ n″ : N.Carrier
-
-
-------------------------------------------------------------------------
--- Infix notation for when opening the module unparameterised
-
-infixl 4 _⋊_
-_⋊_ = {!monoidᵂ!}

From d9e6bc0b184515039e72a14e9099457555861ad9 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Tue, 9 Apr 2024 15:43:04 +0100
Subject: [PATCH 05/39] `fix-whitespace`

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

diff --git a/src/Algebra/Construct/MonoidAction.agda b/src/Algebra/Construct/MonoidAction.agda
index 074c4988b3..ac591de525 100644
--- a/src/Algebra/Construct/MonoidAction.agda
+++ b/src/Algebra/Construct/MonoidAction.agda
@@ -78,7 +78,7 @@ module _ {c a ℓ r} {M : Set c} {A : Set a}
     field
       _ᴬ∙ᴹ_ : A → M → A
       ∙-cong : x ≈ y → m ≈ᴹ n → (x ᴬ∙ᴹ m) ≈ (y ᴬ∙ᴹ n)
-    
+
 -- derived form: iterated action, satisfying congruence
 
     _ᴬ⋆ᴹ_ : A → List M → A

From d7a4ceb9e4927cf28520e1351fffcf06287d3fc7 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 11 Apr 2024 10:07:35 +0100
Subject: [PATCH 06/39] refactor in favour of `Pointwise` congruence

---
 src/Algebra/Construct/MonoidAction.agda | 26 ++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

diff --git a/src/Algebra/Construct/MonoidAction.agda b/src/Algebra/Construct/MonoidAction.agda
index ac591de525..851b677fe0 100644
--- a/src/Algebra/Construct/MonoidAction.agda
+++ b/src/Algebra/Construct/MonoidAction.agda
@@ -64,10 +64,10 @@ module _ {c a ℓ r} {M : Set c} {A : Set a}
     ⋆-cong []            x≈y = x≈y
     ⋆-cong (m≈n ∷ ms≋ns) x≈y = ∙-cong m≈n (⋆-cong ms≋ns x≈y)
 
-    ⋆-act-cong : Reflexive _≈ᴹ_ →
-                 ∀ ms ns → x ≈ y → ((ms ++ ns) ᴹ⋆ᴬ x) ≈ (ms ᴹ⋆ᴬ ns ᴹ⋆ᴬ y)
-    ⋆-act-cong refl []       ns x≈y = ⋆-cong {ns = ns} (Pointwise.refl refl) x≈y
-    ⋆-act-cong refl (m ∷ ms) ns x≈y = ∙-cong refl (⋆-act-cong refl ms ns x≈y)
+    ⋆-act-cong : ∀ ms → Pointwise _≈ᴹ_ ps (ms ++ ns) →
+                 x ≈ y → (ps ᴹ⋆ᴬ x) ≈ (ms ᴹ⋆ᴬ ns ᴹ⋆ᴬ y)
+    ⋆-act-cong []       ps≋ns             x≈y = ⋆-cong ps≋ns x≈y
+    ⋆-act-cong (m ∷ ms) (p≈m ∷ ps≋ms++ns) x≈y = ∙-cong p≈m (⋆-act-cong ms ps≋ms++ns x≈y)
 
     []-act-cong : x ≈ y → ([] ᴹ⋆ᴬ x) ≈ y
     []-act-cong = id
@@ -88,10 +88,10 @@ module _ {c a ℓ r} {M : Set c} {A : Set a}
     ⋆-cong x≈y []            = x≈y
     ⋆-cong x≈y (m≈n ∷ ms≋ns) = ⋆-cong (∙-cong x≈y m≈n) ms≋ns
 
-    ⋆-act-cong : Reflexive _≈ᴹ_ →
-                 x ≈ y → ∀ ms ns → (x ᴬ⋆ᴹ (ms ++ ns)) ≈ (y ᴬ⋆ᴹ ms ᴬ⋆ᴹ ns)
-    ⋆-act-cong refl x≈y []       ns = ⋆-cong {ns = ns} x≈y (Pointwise.refl refl)
-    ⋆-act-cong refl x≈y (m ∷ ms) ns = ⋆-act-cong refl (∙-cong x≈y refl) ms ns
+    ⋆-act-cong : x ≈ y → ∀ ms → Pointwise _≈ᴹ_ ps (ms ++ ns) →
+                 (x ᴬ⋆ᴹ ps) ≈ (y ᴬ⋆ᴹ ms ᴬ⋆ᴹ ns)
+    ⋆-act-cong x≈y []       ps≋ns             = ⋆-cong x≈y ps≋ns
+    ⋆-act-cong x≈y (m ∷ ms) (p≈m ∷ ps≋ms++ns) = ⋆-act-cong (∙-cong x≈y p≈m) ms ps≋ms++ns
 
     []-act-cong : x ≈ y → (x ᴬ⋆ᴹ []) ≈ y
     []-act-cong = id
@@ -106,7 +106,7 @@ module _ (M : Monoid c ℓ) (A : Setoid a r) where
 
     open module M = Monoid M using () renaming (Carrier to M)
     open module A = Setoid A using (_≈_) renaming (Carrier to A)
-    open ≋ M.setoid using (_≋_; [] ; _∷_)
+    open ≋ M.setoid using (_≋_; [] ; _∷_; ≋-refl)
 
     variable
       x y z : A.Carrier
@@ -130,7 +130,7 @@ module _ (M : Monoid c ℓ) (A : Setoid a r) where
     ∙-congʳ m≈n = ∙-cong m≈n A.refl
 
     ⋆-act : ∀ ms ns x → (ms ++ ns) ⋆ x ≈ ms ⋆ ns ⋆ x
-    ⋆-act ms ns x = ⋆-act-cong M.refl ms ns A.refl
+    ⋆-act ms ns x = ⋆-act-cong ms ≋-refl A.refl
 
     []-act : ∀ x → [] ⋆ x ≈ x
     []-act _ = []-act-cong A.refl
@@ -152,7 +152,7 @@ module _ (M : Monoid c ℓ) (A : Setoid a r) where
     ∙-congʳ m≈n = ∙-cong A.refl m≈n
 
     ⋆-act : ∀ x ms ns → x ⋆ (ms ++ ns) ≈ x ⋆ ms ⋆ ns
-    ⋆-act _ = ⋆-act-cong M.refl A.refl
+    ⋆-act x ms ns = ⋆-act-cong A.refl ms ≋-refl
 
     []-act : ∀ x → x ⋆ [] ≈ x
     []-act x = []-act-cong A.refl
@@ -212,7 +212,7 @@ module Free (M : Setoid c ℓ) (S : Setoid a r) where
                (open RawLeftAction rawLeftAction) →
                LeftAction monoid S (record { _ᴹ∙ᴬ_ = _ᴹ⋆ᴬ_  ; ∙-cong = ⋆-cong })
   leftAction rawLeftAction = record
-    { ∙-act = λ ms ns x → ⋆-act-cong M.refl ms ns A.refl
+    { ∙-act = λ ms ns x → ⋆-act-cong ms ≋-refl A.refl
     ; ε-act = λ _ → []-act-cong A.refl
     }
     where open RawLeftAction rawLeftAction
@@ -221,7 +221,7 @@ module Free (M : Setoid c ℓ) (S : Setoid a r) where
                 (open RawRightAction rawRightAction) →
                 RightAction monoid S (record { _ᴬ∙ᴹ_ = _ᴬ⋆ᴹ_  ; ∙-cong = ⋆-cong })
   rightAction rawRightAction = record
-    { ∙-act = λ _ → ⋆-act-cong M.refl A.refl
+    { ∙-act = λ x ms ns → ⋆-act-cong A.refl ms ≋-refl
     ; ε-act = λ _ → []-act-cong A.refl
     }
     where open RawRightAction rawRightAction

From aa6788edb37dc17d6e6a5b70a391e8b587daf21a Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 11 Apr 2024 10:26:53 +0100
Subject: [PATCH 07/39] begin refactoring

---
 src/Algebra/Action/Structures/Raw.agda | 77 ++++++++++++++++++++++++++
 1 file changed, 77 insertions(+)
 create mode 100644 src/Algebra/Action/Structures/Raw.agda

diff --git a/src/Algebra/Action/Structures/Raw.agda b/src/Algebra/Action/Structures/Raw.agda
new file mode 100644
index 0000000000..c1882265ea
--- /dev/null
+++ b/src/Algebra/Action/Structures/Raw.agda
@@ -0,0 +1,77 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Raw Actions of one (pre-)Setoid on another
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Core using (Rel)
+
+module Algebra.Action.Structures.Raw
+  {c a ℓ r} {M : Set c} {A : Set a} (_≈ᴹ_ : Rel M ℓ) (_≈_ : Rel A r)
+  where
+
+open import Data.List.Base
+  using (List; []; _∷_; _++_; foldl; foldr)
+open import Data.List.Relation.Binary.Pointwise as Pointwise
+  using (Pointwise; []; _∷_)
+open import Function.Base using (id)
+open import Level using (Level; _⊔_)
+
+private
+  variable
+    x y z : A
+    m n p : M
+    ms ns ps : List M
+
+------------------------------------------------------------------------
+-- Basic definitions: fix notation
+
+record IsRawLeftAction : Set (a ⊔ r ⊔ c ⊔ ℓ) where
+  infixr 5 _ᴹ∙ᴬ_ _ᴹ⋆ᴬ_
+
+  field
+    _ᴹ∙ᴬ_  : M → A → A
+    ∙-cong : m ≈ᴹ n → x ≈ y → (m ᴹ∙ᴬ x) ≈ (n ᴹ∙ᴬ y)
+
+-- derived form: iterated action, satisfying congruence
+
+  _ᴹ⋆ᴬ_ : List M → A → A
+  ms ᴹ⋆ᴬ a = foldr _ᴹ∙ᴬ_ a ms
+
+  ⋆-cong : Pointwise _≈ᴹ_ ms ns → x ≈ y → (ms ᴹ⋆ᴬ x) ≈ (ns ᴹ⋆ᴬ y)
+  ⋆-cong []            x≈y = x≈y
+  ⋆-cong (m≈n ∷ ms≋ns) x≈y = ∙-cong m≈n (⋆-cong ms≋ns x≈y)
+
+  ⋆-act-cong : ∀ ms → Pointwise _≈ᴹ_ ps (ms ++ ns) →
+               x ≈ y → (ps ᴹ⋆ᴬ x) ≈ (ms ᴹ⋆ᴬ ns ᴹ⋆ᴬ y)
+  ⋆-act-cong []       ps≋ns             x≈y = ⋆-cong ps≋ns x≈y
+  ⋆-act-cong (m ∷ ms) (p≈m ∷ ps≋ms++ns) x≈y = ∙-cong p≈m (⋆-act-cong ms ps≋ms++ns x≈y)
+
+  []-act-cong : x ≈ y → ([] ᴹ⋆ᴬ x) ≈ y
+  []-act-cong = id
+
+record IsRawRightAction : Set (a ⊔ r ⊔ c ⊔ ℓ) where
+  infixl 5 _ᴬ∙ᴹ_ _ᴬ⋆ᴹ_
+
+  field
+    _ᴬ∙ᴹ_  : A → M → A
+    ∙-cong : x ≈ y → m ≈ᴹ n → (x ᴬ∙ᴹ m) ≈ (y ᴬ∙ᴹ n)
+
+-- derived form: iterated action, satisfying congruence
+
+  _ᴬ⋆ᴹ_ : A → List M → A
+  a ᴬ⋆ᴹ ms = foldl _ᴬ∙ᴹ_ a ms
+
+  ⋆-cong : x ≈ y → Pointwise _≈ᴹ_ ms ns → (x ᴬ⋆ᴹ ms) ≈ (y ᴬ⋆ᴹ ns)
+  ⋆-cong x≈y []            = x≈y
+  ⋆-cong x≈y (m≈n ∷ ms≋ns) = ⋆-cong (∙-cong x≈y m≈n) ms≋ns
+
+  ⋆-act-cong : x ≈ y → ∀ ms → Pointwise _≈ᴹ_ ps (ms ++ ns) →
+               (x ᴬ⋆ᴹ ps) ≈ (y ᴬ⋆ᴹ ms ᴬ⋆ᴹ ns)
+  ⋆-act-cong x≈y []       ps≋ns             = ⋆-cong x≈y ps≋ns
+  ⋆-act-cong x≈y (m ∷ ms) (p≈m ∷ ps≋ms++ns) = ⋆-act-cong (∙-cong x≈y p≈m) ms ps≋ms++ns
+
+  []-act-cong : x ≈ y → (x ᴬ⋆ᴹ []) ≈ y
+  []-act-cong = id

From 48a79e5cc1faf19b7884ef33ee8c815e5e0bc987 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 11 Apr 2024 12:32:04 +0100
Subject: [PATCH 08/39] more refactoring

---
 src/Algebra/Action/Bundles.agda | 113 ++++++++++++++++++++++++++++++++
 1 file changed, 113 insertions(+)
 create mode 100644 src/Algebra/Action/Bundles.agda

diff --git a/src/Algebra/Action/Bundles.agda b/src/Algebra/Action/Bundles.agda
new file mode 100644
index 0000000000..5c29a80bd6
--- /dev/null
+++ b/src/Algebra/Action/Bundles.agda
@@ -0,0 +1,113 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Monoid Actions and the free Monoid Action on a Setoid
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Algebra.Action.Bundles where
+
+open import Algebra.Action.Structures.Raw using (IsRawLeftAction; IsRawRightAction)
+open import Algebra.Bundles using (Monoid)
+
+open import Data.List.Base using ([]; _++_)
+import Data.List.Relation.Binary.Equality.Setoid as ≋
+open import Data.Product.Base using (curry)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
+
+open import Function.Bundles using (Func)
+
+open import Level using (Level; _⊔_)
+
+open import Relation.Binary.Bundles using (Setoid)
+
+private
+  variable
+    a c r ℓ : Level
+
+
+------------------------------------------------------------------------
+-- Basic definition: a Setoid action yields underlying raw action
+
+module SetoidAction (M : Setoid c ℓ) (A : Setoid a r) where
+
+  private
+
+    open module M = Setoid M using ()
+    open module A = Setoid A using (_≈_)
+
+  record Left : Set (a ⊔ r ⊔ c ⊔ ℓ) where
+
+    field
+      act : Func (M ×ₛ A) A
+
+    isRawLeftAction : IsRawLeftAction M._≈_ _≈_
+    isRawLeftAction = record { _ᴹ∙ᴬ_ = curry to ; ∙-cong = curry cong }
+      where open Func act
+
+  record Right : Set (a ⊔ r ⊔ c ⊔ ℓ) where
+
+    field
+      act : Func (A ×ₛ M) A
+
+    isRawRightAction : IsRawRightAction M._≈_ _≈_
+    isRawRightAction = record { _ᴬ∙ᴹ_ = curry to ; ∙-cong = curry cong }
+      where open Func act
+
+
+------------------------------------------------------------------------
+-- Definition: indexed over an underlying raw action
+
+module MonoidAction (M : Monoid c ℓ) (A : Setoid a r) where
+
+  private
+
+    open module M = Monoid M using ()
+    open module A = Setoid A using (_≈_)
+    open ≋ M.setoid using (≋-refl)
+
+  record Left (isRawLeftAction : IsRawLeftAction M._≈_ _≈_) : Set (a ⊔ r ⊔ c ⊔ ℓ)
+    where
+
+    open IsRawLeftAction isRawLeftAction public
+      renaming (_ᴹ∙ᴬ_ to _∙_; _ᴹ⋆ᴬ_ to _⋆_)
+
+    field
+      ∙-act  : ∀ m n x → m M.∙ n ∙ x ≈ m ∙ n ∙ x
+      ε-act  : ∀ x → M.ε ∙ x ≈ x
+
+    ∙-congˡ : ∀ {m x y} → x ≈ y → m ∙ x ≈ m ∙ y
+    ∙-congˡ x≈y = ∙-cong M.refl x≈y
+
+    ∙-congʳ : ∀ {m n x} → m M.≈ n → m ∙ x ≈ n ∙ x
+    ∙-congʳ m≈n = ∙-cong m≈n A.refl
+
+    ⋆-act : ∀ ms ns x → (ms ++ ns) ⋆ x ≈ ms ⋆ ns ⋆ x
+    ⋆-act ms ns x = ⋆-act-cong ms ≋-refl A.refl
+
+    []-act : ∀ x → [] ⋆ x ≈ x
+    []-act _ = []-act-cong A.refl
+
+  record Right (isRawRightAction : IsRawRightAction M._≈_ _≈_) : Set (a ⊔ r ⊔ c ⊔ ℓ)
+    where
+
+    open IsRawRightAction isRawRightAction public
+      renaming (_ᴬ∙ᴹ_ to _∙_; _ᴬ⋆ᴹ_ to _⋆_)
+
+    field
+      ∙-act  : ∀ x m n → x ∙ m M.∙ n ≈ x ∙ m ∙ n
+      ε-act  : ∀ x → x ∙ M.ε ≈ x
+
+    ∙-congˡ : ∀ {x y m} → x ≈ y → x ∙ m ≈ y ∙ m
+    ∙-congˡ x≈y = ∙-cong x≈y M.refl
+
+    ∙-congʳ : ∀ {m n x} → m M.≈ n → x ∙ m ≈ x ∙ n
+    ∙-congʳ m≈n = ∙-cong A.refl m≈n
+
+    ⋆-act : ∀ x ms ns → x ⋆ (ms ++ ns) ≈ x ⋆ ms ⋆ ns
+    ⋆-act x ms ns = ⋆-act-cong A.refl ms ≋-refl
+
+    []-act : ∀ x → x ⋆ [] ≈ x
+    []-act x = []-act-cong A.refl
+

From 56d99025cc66abf5d784b9fbba5845980019a4e4 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 11 Apr 2024 12:40:44 +0100
Subject: [PATCH 09/39] more refactoring

---
 src/Algebra/Action/Bundles.agda | 36 ++++++++++++++++++---------------
 1 file changed, 20 insertions(+), 16 deletions(-)

diff --git a/src/Algebra/Action/Bundles.agda b/src/Algebra/Action/Bundles.agda
index 5c29a80bd6..92aae675b5 100644
--- a/src/Algebra/Action/Bundles.agda
+++ b/src/Algebra/Action/Bundles.agda
@@ -63,51 +63,55 @@ module MonoidAction (M : Monoid c ℓ) (A : Setoid a r) where
 
   private
 
-    open module M = Monoid M using ()
-    open module A = Setoid A using (_≈_)
+    module M = Monoid M
+    module A = Setoid A
     open ≋ M.setoid using (≋-refl)
 
-  record Left (isRawLeftAction : IsRawLeftAction M._≈_ _≈_) : Set (a ⊔ r ⊔ c ⊔ ℓ)
+  record Left (leftAction : SetoidAction.Left M.setoid A) : Set (a ⊔ r ⊔ c ⊔ ℓ)
     where
 
+    open SetoidAction.Left leftAction public
+      using (isRawLeftAction)
     open IsRawLeftAction isRawLeftAction public
       renaming (_ᴹ∙ᴬ_ to _∙_; _ᴹ⋆ᴬ_ to _⋆_)
 
     field
-      ∙-act  : ∀ m n x → m M.∙ n ∙ x ≈ m ∙ n ∙ x
-      ε-act  : ∀ x → M.ε ∙ x ≈ x
+      ∙-act  : ∀ m n x → m M.∙ n ∙ x A.≈ m ∙ n ∙ x
+      ε-act  : ∀ x → M.ε ∙ x A.≈ x
 
-    ∙-congˡ : ∀ {m x y} → x ≈ y → m ∙ x ≈ m ∙ y
+    ∙-congˡ : ∀ {m x y} → x A.≈ y → m ∙ x A.≈ m ∙ y
     ∙-congˡ x≈y = ∙-cong M.refl x≈y
 
-    ∙-congʳ : ∀ {m n x} → m M.≈ n → m ∙ x ≈ n ∙ x
+    ∙-congʳ : ∀ {m n x} → m M.≈ n → m ∙ x A.≈ n ∙ x
     ∙-congʳ m≈n = ∙-cong m≈n A.refl
 
-    ⋆-act : ∀ ms ns x → (ms ++ ns) ⋆ x ≈ ms ⋆ ns ⋆ x
+    ⋆-act : ∀ ms ns x → (ms ++ ns) ⋆ x A.≈ ms ⋆ ns ⋆ x
     ⋆-act ms ns x = ⋆-act-cong ms ≋-refl A.refl
 
-    []-act : ∀ x → [] ⋆ x ≈ x
+    []-act : ∀ x → [] ⋆ x A.≈ x
     []-act _ = []-act-cong A.refl
 
-  record Right (isRawRightAction : IsRawRightAction M._≈_ _≈_) : Set (a ⊔ r ⊔ c ⊔ ℓ)
+  record Right (rightAction : SetoidAction.Right M.setoid A) : Set (a ⊔ r ⊔ c ⊔ ℓ)
     where
 
+    open SetoidAction.Right rightAction public
+      using (isRawRightAction)
     open IsRawRightAction isRawRightAction public
       renaming (_ᴬ∙ᴹ_ to _∙_; _ᴬ⋆ᴹ_ to _⋆_)
 
     field
-      ∙-act  : ∀ x m n → x ∙ m M.∙ n ≈ x ∙ m ∙ n
-      ε-act  : ∀ x → x ∙ M.ε ≈ x
+      ∙-act  : ∀ x m n → x ∙ m M.∙ n A.≈ x ∙ m ∙ n
+      ε-act  : ∀ x → x ∙ M.ε A.≈ x
 
-    ∙-congˡ : ∀ {x y m} → x ≈ y → x ∙ m ≈ y ∙ m
+    ∙-congˡ : ∀ {x y m} → x A.≈ y → x ∙ m A.≈ y ∙ m
     ∙-congˡ x≈y = ∙-cong x≈y M.refl
 
-    ∙-congʳ : ∀ {m n x} → m M.≈ n → x ∙ m ≈ x ∙ n
+    ∙-congʳ : ∀ {m n x} → m M.≈ n → x ∙ m A.≈ x ∙ n
     ∙-congʳ m≈n = ∙-cong A.refl m≈n
 
-    ⋆-act : ∀ x ms ns → x ⋆ (ms ++ ns) ≈ x ⋆ ms ⋆ ns
+    ⋆-act : ∀ x ms ns → x ⋆ (ms ++ ns) A.≈ x ⋆ ms ⋆ ns
     ⋆-act x ms ns = ⋆-act-cong A.refl ms ≋-refl
 
-    []-act : ∀ x → x ⋆ [] ≈ x
+    []-act : ∀ x → x ⋆ [] A.≈ x
     []-act x = []-act-cong A.refl
 

From ace7e4dc333105ce4c3cae67035d29e884c1e81f Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 11 Apr 2024 13:12:38 +0100
Subject: [PATCH 10/39] factored out regular and free monoid actions

---
 src/Algebra/Action/Construct/Free.agda | 72 ++++++++++++++++++++++++++
 src/Algebra/Action/Construct/Self.agda | 37 +++++++++++++
 2 files changed, 109 insertions(+)
 create mode 100644 src/Algebra/Action/Construct/Free.agda
 create mode 100644 src/Algebra/Action/Construct/Self.agda

diff --git a/src/Algebra/Action/Construct/Free.agda b/src/Algebra/Action/Construct/Free.agda
new file mode 100644
index 0000000000..d41d9e6d55
--- /dev/null
+++ b/src/Algebra/Action/Construct/Free.agda
@@ -0,0 +1,72 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Monoid Actions and the free Monoid Action on a Setoid
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Bundles using (Setoid)
+
+module Algebra.Action.Construct.Free
+  {a c r ℓ} (M : Setoid c ℓ) (S : Setoid a r)
+  where
+
+open import Algebra.Action.Bundles
+open import Algebra.Action.Structures.Raw using (IsRawLeftAction; IsRawRightAction)
+open import Algebra.Bundles using (Monoid)
+open import Algebra.Structures using (IsMonoid)
+
+open import Data.List.Base using (List; []; _++_)
+import Data.List.Properties as List
+import Data.List.Relation.Binary.Equality.Setoid as ≋
+open import Data.Product.Base using (_,_)
+
+open import Function.Base using (_∘_)
+
+open import Level using (Level; _⊔_)
+
+
+------------------------------------------------------------------------
+-- Distinguished *free* action: lifting a raw action to a List action
+
+module Free where
+
+  open ≋ M using (_≋_; ≋-refl; ≋-reflexive; ≋-isEquivalence; ++⁺)
+  open MonoidAction
+
+  private
+
+    module M = Setoid M
+    module A = Setoid S
+
+    isMonoid : IsMonoid _≋_ _++_ []
+    isMonoid = record
+      { isSemigroup = record
+        { isMagma = record
+          { isEquivalence = ≋-isEquivalence
+          ; ∙-cong = ++⁺
+          }
+        ; assoc = λ xs ys zs → ≋-reflexive (List.++-assoc xs ys zs)
+        }
+      ; identity = (λ _ → ≋-refl) , ≋-reflexive ∘ List.++-identityʳ }
+
+    monoid : Monoid c (c ⊔ ℓ)
+    monoid = record { isMonoid = isMonoid }
+
+
+  leftAction : (leftAction : SetoidAction.Left M S) →
+               Left monoid S {!leftAction!}
+  leftAction leftAction = record
+    { ∙-act = λ ms ns x → ⋆-act-cong ms ≋-refl A.refl
+    ; ε-act = λ _ → []-act-cong A.refl
+    }
+    where open SetoidAction.Left leftAction; open IsRawLeftAction isRawLeftAction
+
+  rightAction : (rightAction : SetoidAction.Right M S) →
+                Right monoid S {!rightAction!}
+  rightAction rightAction = record
+    { ∙-act = λ x ms ns → ⋆-act-cong A.refl ms ≋-refl
+    ; ε-act = λ _ → []-act-cong A.refl
+    }
+    where open SetoidAction.Right rightAction; open IsRawRightAction isRawRightAction
diff --git a/src/Algebra/Action/Construct/Self.agda b/src/Algebra/Action/Construct/Self.agda
new file mode 100644
index 0000000000..39990e6dc9
--- /dev/null
+++ b/src/Algebra/Action/Construct/Self.agda
@@ -0,0 +1,37 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The left- and right- regular actions: of a Monoid over itself
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Algebra.Bundles using (Monoid)
+
+module Algebra.Action.Construct.Self {c ℓ} (M : Monoid c ℓ) where
+
+open import Algebra.Action.Bundles using (module MonoidAction)
+open import Algebra.Action.Structures.Raw using (IsRawLeftAction; IsRawRightAction)
+
+open Monoid M
+open MonoidAction M setoid
+
+private
+  isRawLeftAction : IsRawLeftAction _≈_ _≈_
+  isRawLeftAction = record { _ᴹ∙ᴬ_ = _∙_ ; ∙-cong = ∙-cong }
+
+  isRawRightAction : IsRawRightAction _≈_ _≈_
+  isRawRightAction = record { _ᴬ∙ᴹ_ = _∙_ ; ∙-cong = ∙-cong }
+
+leftAction : Left {!isRawLeftAction!}
+leftAction = record
+  { ∙-act = assoc
+  ; ε-act = identityˡ
+  }
+
+rightAction : Right {!isRawRightAction!}
+rightAction = record
+  { ∙-act = λ x m n → sym (assoc x m n)
+  ; ε-act = identityʳ
+  }
+

From d579e3172176f82a34703ab14f24b62d5d298549 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 11 Apr 2024 13:16:21 +0100
Subject: [PATCH 11/39] nearly there

---
 CHANGELOG.md | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2b9d357511..d17614fb39 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -57,6 +57,26 @@ Deprecated names
 New modules
 -----------
 
+* Bundles for left- and right- actions:
+  ```
+  Algebra.Action.Bundles
+  ```
+
+* The free `List` actions over a `SetoidAction`:
+  ```
+  Algebra.Action.Construct.Free
+  ```
+
+* The left- and right- regular actions (of a `Monoid`) over itself:
+  ```
+  Algebra.Action.Construct.Self
+  ```
+
+* Raw structures for left- and right- actions:
+  ```
+  Algebra.Action.Structures.Raw
+  ```
+
 * Raw bundles for module-like algebraic structures:
   ```
   Algebra.Module.Bundles.Raw

From 361ac2488689e0cc393c43d591c76e8f01d26c51 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 11 Apr 2024 13:24:57 +0100
Subject: [PATCH 12/39] little by little...

---
 src/Algebra/Action/Construct/Free.agda | 76 +++++++++++++-------------
 1 file changed, 38 insertions(+), 38 deletions(-)

diff --git a/src/Algebra/Action/Construct/Free.agda b/src/Algebra/Action/Construct/Free.agda
index d41d9e6d55..d276adb50a 100644
--- a/src/Algebra/Action/Construct/Free.agda
+++ b/src/Algebra/Action/Construct/Free.agda
@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Monoid Actions and the free Monoid Action on a Setoid
+-- The free MonoidAction on a SetoidAction
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
@@ -26,47 +26,47 @@ open import Function.Base using (_∘_)
 
 open import Level using (Level; _⊔_)
 
+open ≋ M using (_≋_; ≋-refl; ≋-reflexive; ≋-isEquivalence; ++⁺)
+open MonoidAction
 
 ------------------------------------------------------------------------
--- Distinguished *free* action: lifting a raw action to a List action
+-- First: define the Monoid structure on List M.Carrier
 
-module Free where
+private
 
-  open ≋ M using (_≋_; ≋-refl; ≋-reflexive; ≋-isEquivalence; ++⁺)
-  open MonoidAction
+  module M = Setoid M
+  module A = Setoid S
 
-  private
+  isMonoid : IsMonoid _≋_ _++_ []
+  isMonoid = record
+    { isSemigroup = record
+      { isMagma = record
+        { isEquivalence = ≋-isEquivalence
+        ; ∙-cong = ++⁺
+        }
+      ; assoc = λ xs ys zs → ≋-reflexive (List.++-assoc xs ys zs)
+      }
+    ; identity = (λ _ → ≋-refl) , ≋-reflexive ∘ List.++-identityʳ }
 
-    module M = Setoid M
-    module A = Setoid S
+  monoid : Monoid c (c ⊔ ℓ)
+  monoid = record { isMonoid = isMonoid }
 
-    isMonoid : IsMonoid _≋_ _++_ []
-    isMonoid = record
-      { isSemigroup = record
-        { isMagma = record
-          { isEquivalence = ≋-isEquivalence
-          ; ∙-cong = ++⁺
-          }
-        ; assoc = λ xs ys zs → ≋-reflexive (List.++-assoc xs ys zs)
-        }
-      ; identity = (λ _ → ≋-refl) , ≋-reflexive ∘ List.++-identityʳ }
-
-    monoid : Monoid c (c ⊔ ℓ)
-    monoid = record { isMonoid = isMonoid }
-
-
-  leftAction : (leftAction : SetoidAction.Left M S) →
-               Left monoid S {!leftAction!}
-  leftAction leftAction = record
-    { ∙-act = λ ms ns x → ⋆-act-cong ms ≋-refl A.refl
-    ; ε-act = λ _ → []-act-cong A.refl
-    }
-    where open SetoidAction.Left leftAction; open IsRawLeftAction isRawLeftAction
-
-  rightAction : (rightAction : SetoidAction.Right M S) →
-                Right monoid S {!rightAction!}
-  rightAction rightAction = record
-    { ∙-act = λ x ms ns → ⋆-act-cong A.refl ms ≋-refl
-    ; ε-act = λ _ → []-act-cong A.refl
-    }
-    where open SetoidAction.Right rightAction; open IsRawRightAction isRawRightAction
+
+------------------------------------------------------------------------
+-- Second: define the actions of that Monoid
+
+leftAction : (leftAction : SetoidAction.Left M S) →
+             Left monoid S {!leftAction!}
+leftAction leftAction = record
+  { ∙-act = λ ms ns x → ⋆-act-cong ms ≋-refl A.refl
+  ; ε-act = λ _ → []-act-cong A.refl
+  }
+  where open SetoidAction.Left leftAction; open IsRawLeftAction isRawLeftAction
+
+rightAction : (rightAction : SetoidAction.Right M S) →
+              Right monoid S {!rightAction!}
+rightAction rightAction = record
+  { ∙-act = λ x ms ns → ⋆-act-cong A.refl ms ≋-refl
+  ; ε-act = λ _ → []-act-cong A.refl
+  }
+  where open SetoidAction.Right rightAction; open IsRawRightAction isRawRightAction

From 160837f73d38cb152d630a3883263464f3999407 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 11 Apr 2024 13:34:45 +0100
Subject: [PATCH 13/39] `Self` just needs tidying up: `Biased` smart
 constructor

---
 src/Algebra/Action/Construct/Self.agda | 23 ++++++++++++++++++++---
 1 file changed, 20 insertions(+), 3 deletions(-)

diff --git a/src/Algebra/Action/Construct/Self.agda b/src/Algebra/Action/Construct/Self.agda
index 39990e6dc9..697bd07803 100644
--- a/src/Algebra/Action/Construct/Self.agda
+++ b/src/Algebra/Action/Construct/Self.agda
@@ -10,8 +10,9 @@ open import Algebra.Bundles using (Monoid)
 
 module Algebra.Action.Construct.Self {c ℓ} (M : Monoid c ℓ) where
 
-open import Algebra.Action.Bundles using (module MonoidAction)
+open import Algebra.Action.Bundles
 open import Algebra.Action.Structures.Raw using (IsRawLeftAction; IsRawRightAction)
+open import Data.Product.Base using (uncurry)
 
 open Monoid M
 open MonoidAction M setoid
@@ -23,13 +24,29 @@ private
   isRawRightAction : IsRawRightAction _≈_ _≈_
   isRawRightAction = record { _ᴬ∙ᴹ_ = _∙_ ; ∙-cong = ∙-cong }
 
-leftAction : Left {!isRawLeftAction!}
+  leftSetoidAction : SetoidAction.Left setoid setoid
+  leftSetoidAction = record
+    { act = record
+      { to = uncurry _∙_
+      ; cong = uncurry ∙-cong
+      }
+    }
+
+  rightSetoidAction : SetoidAction.Right setoid setoid
+  rightSetoidAction = record
+    { act = record
+      { to = uncurry _∙_
+      ; cong = uncurry ∙-cong
+      }
+    }
+
+leftAction : Left leftSetoidAction
 leftAction = record
   { ∙-act = assoc
   ; ε-act = identityˡ
   }
 
-rightAction : Right {!isRawRightAction!}
+rightAction : Right rightSetoidAction
 rightAction = record
   { ∙-act = λ x m n → sym (assoc x m n)
   ; ε-act = identityʳ

From 8d0ed2200f3aae0ac8d4664b8e9faddc52f6c821 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 11 Apr 2024 14:02:52 +0100
Subject: [PATCH 14/39] temp commit

---
 src/Algebra/Action/Bundles.agda        | 20 ++++++++++--
 src/Algebra/Action/Construct/Free.agda | 43 ++++++++++++++++----------
 2 files changed, 45 insertions(+), 18 deletions(-)

diff --git a/src/Algebra/Action/Bundles.agda b/src/Algebra/Action/Bundles.agda
index 92aae675b5..7a16b0f28b 100644
--- a/src/Algebra/Action/Bundles.agda
+++ b/src/Algebra/Action/Bundles.agda
@@ -4,8 +4,8 @@
 -- Monoid Actions and the free Monoid Action on a Setoid
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible --safe #-}
-
+{-# OPTIONS --cubical-compatible #-}
+{-# OPTIONS --allow-unsolved-metas #-}
 module Algebra.Action.Bundles where
 
 open import Algebra.Action.Structures.Raw using (IsRawLeftAction; IsRawRightAction)
@@ -55,6 +55,22 @@ module SetoidAction (M : Setoid c ℓ) (A : Setoid a r) where
     isRawRightAction = record { _ᴬ∙ᴹ_ = curry to ; ∙-cong = curry cong }
       where open Func act
 
+  
+------------------------------------------------------------------------
+-- A Setoid action yields an iterated List action
+
+module _ {M : Setoid c ℓ} {A : Setoid a r} where
+
+  open SetoidAction
+
+  open ≋ M using (≋-setoid)
+
+  leftListAction : (leftAction : Left M A) → Left ≋-setoid A
+  leftListAction leftAction = {!!}
+
+  rightListAction : (rightAction : Right M A) → Right ≋-setoid A
+  rightListAction rightAction = {!!}
+  
 
 ------------------------------------------------------------------------
 -- Definition: indexed over an underlying raw action
diff --git a/src/Algebra/Action/Construct/Free.agda b/src/Algebra/Action/Construct/Free.agda
index d276adb50a..81222a07eb 100644
--- a/src/Algebra/Action/Construct/Free.agda
+++ b/src/Algebra/Action/Construct/Free.agda
@@ -4,7 +4,7 @@
 -- The free MonoidAction on a SetoidAction
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --cubical-compatible #-}
 
 open import Relation.Binary.Bundles using (Setoid)
 
@@ -55,18 +55,29 @@ private
 ------------------------------------------------------------------------
 -- Second: define the actions of that Monoid
 
-leftAction : (leftAction : SetoidAction.Left M S) →
-             Left monoid S {!leftAction!}
-leftAction leftAction = record
-  { ∙-act = λ ms ns x → ⋆-act-cong ms ≋-refl A.refl
-  ; ε-act = λ _ → []-act-cong A.refl
-  }
-  where open SetoidAction.Left leftAction; open IsRawLeftAction isRawLeftAction
-
-rightAction : (rightAction : SetoidAction.Right M S) →
-              Right monoid S {!rightAction!}
-rightAction rightAction = record
-  { ∙-act = λ x ms ns → ⋆-act-cong A.refl ms ≋-refl
-  ; ε-act = λ _ → []-act-cong A.refl
-  }
-  where open SetoidAction.Right rightAction; open IsRawRightAction isRawRightAction
+module _ (left : SetoidAction.Left M S) where
+
+  private listAction = leftListAction left
+
+  open SetoidAction.Left listAction
+  open IsRawLeftAction isRawLeftAction
+
+  leftAction : Left monoid S listAction
+  leftAction = record
+    { ∙-act = λ ms ns x → ∙-cong ≋-refl A.refl
+    ; ε-act = λ _ → []-act-cong A.refl
+    }
+
+module _ (right : SetoidAction.Right M S) where
+
+  private listAction = rightListAction right
+
+  open SetoidAction.Right listAction
+  open IsRawRightAction isRawRightAction
+
+  rightAction : Right monoid S listAction
+  rightAction = record
+    { ∙-act = λ x ms ns → ⋆-act-cong A.refl ms ≋-refl
+    ; ε-act = λ _ → []-act-cong A.refl
+    }
+

From a5995f3cfcf64d7a2c19bb635bd8c4253eebf697 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 11 Apr 2024 15:35:38 +0100
Subject: [PATCH 15/39] fixed `Free`

---
 src/Algebra/Action/Bundles.agda        | 20 ++++++++++++++------
 src/Algebra/Action/Construct/Free.agda | 12 ++++++------
 2 files changed, 20 insertions(+), 12 deletions(-)

diff --git a/src/Algebra/Action/Bundles.agda b/src/Algebra/Action/Bundles.agda
index 7a16b0f28b..c6b4b4e267 100644
--- a/src/Algebra/Action/Bundles.agda
+++ b/src/Algebra/Action/Bundles.agda
@@ -1,11 +1,11 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Monoid Actions and the free Monoid Action on a Setoid
+-- Setoid Actions and Monoid Actions
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible #-}
-{-# OPTIONS --allow-unsolved-metas #-}
+{-# OPTIONS --cubical-compatible --safe #-}
+
 module Algebra.Action.Bundles where
 
 open import Algebra.Action.Structures.Raw using (IsRawLeftAction; IsRawRightAction)
@@ -13,7 +13,7 @@ open import Algebra.Bundles using (Monoid)
 
 open import Data.List.Base using ([]; _++_)
 import Data.List.Relation.Binary.Equality.Setoid as ≋
-open import Data.Product.Base using (curry)
+open import Data.Product.Base using (curry; uncurry)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
 
 open import Function.Bundles using (Func)
@@ -66,10 +66,18 @@ module _ {M : Setoid c ℓ} {A : Setoid a r} where
   open ≋ M using (≋-setoid)
 
   leftListAction : (leftAction : Left M A) → Left ≋-setoid A
-  leftListAction leftAction = {!!}
+  leftListAction leftAction = record
+    { act = record
+      { to = uncurry _ᴹ⋆ᴬ_ ; cong = uncurry ⋆-cong }
+    }
+    where open Left leftAction; open IsRawLeftAction isRawLeftAction
 
   rightListAction : (rightAction : Right M A) → Right ≋-setoid A
-  rightListAction rightAction = {!!}
+  rightListAction rightAction = record
+    { act = record
+      { to = uncurry _ᴬ⋆ᴹ_ ; cong = uncurry ⋆-cong }
+    }
+    where open Right rightAction; open IsRawRightAction isRawRightAction
   
 
 ------------------------------------------------------------------------
diff --git a/src/Algebra/Action/Construct/Free.agda b/src/Algebra/Action/Construct/Free.agda
index 81222a07eb..d07225eea4 100644
--- a/src/Algebra/Action/Construct/Free.agda
+++ b/src/Algebra/Action/Construct/Free.agda
@@ -4,7 +4,7 @@
 -- The free MonoidAction on a SetoidAction
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible #-}
+{-# OPTIONS --cubical-compatible --safe #-}
 
 open import Relation.Binary.Bundles using (Setoid)
 
@@ -59,25 +59,25 @@ module _ (left : SetoidAction.Left M S) where
 
   private listAction = leftListAction left
 
-  open SetoidAction.Left listAction
+  open SetoidAction.Left left
   open IsRawLeftAction isRawLeftAction
 
   leftAction : Left monoid S listAction
   leftAction = record
-    { ∙-act = λ ms ns x → ∙-cong ≋-refl A.refl
-    ; ε-act = λ _ → []-act-cong A.refl
+    { ∙-act = λ ms ns x → ⋆-act-cong ms ≋-refl A.refl
+    ; ε-act = λ _ → A.refl
     }
 
 module _ (right : SetoidAction.Right M S) where
 
   private listAction = rightListAction right
 
-  open SetoidAction.Right listAction
+  open SetoidAction.Right right
   open IsRawRightAction isRawRightAction
 
   rightAction : Right monoid S listAction
   rightAction = record
     { ∙-act = λ x ms ns → ⋆-act-cong A.refl ms ≋-refl
-    ; ε-act = λ _ → []-act-cong A.refl
+    ; ε-act = λ _ → A.refl
     }
 

From 0eebed16f880636bf801e7cd4ca584fbfeb00687 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 11 Apr 2024 15:37:36 +0100
Subject: [PATCH 16/39] refactored `Self`

---
 src/Algebra/Action/Construct/Self.agda | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/Algebra/Action/Construct/Self.agda b/src/Algebra/Action/Construct/Self.agda
index 697bd07803..a3bf4b4528 100644
--- a/src/Algebra/Action/Construct/Self.agda
+++ b/src/Algebra/Action/Construct/Self.agda
@@ -18,12 +18,6 @@ open Monoid M
 open MonoidAction M setoid
 
 private
-  isRawLeftAction : IsRawLeftAction _≈_ _≈_
-  isRawLeftAction = record { _ᴹ∙ᴬ_ = _∙_ ; ∙-cong = ∙-cong }
-
-  isRawRightAction : IsRawRightAction _≈_ _≈_
-  isRawRightAction = record { _ᴬ∙ᴹ_ = _∙_ ; ∙-cong = ∙-cong }
-
   leftSetoidAction : SetoidAction.Left setoid setoid
   leftSetoidAction = record
     { act = record
@@ -40,6 +34,12 @@ private
       }
     }
 
+isRawLeftAction : IsRawLeftAction _≈_ _≈_
+isRawLeftAction = record { _ᴹ∙ᴬ_ = _∙_ ; ∙-cong = ∙-cong }
+
+isRawRightAction : IsRawRightAction _≈_ _≈_
+isRawRightAction = record { _ᴬ∙ᴹ_ = _∙_ ; ∙-cong = ∙-cong }
+
 leftAction : Left leftSetoidAction
 leftAction = record
   { ∙-act = assoc

From 8be311db62ae72c347a5f5acbbf68b82a70bf27a Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 11 Apr 2024 15:38:35 +0100
Subject: [PATCH 17/39] `fix-whitespace`

---
 src/Algebra/Action/Bundles.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Algebra/Action/Bundles.agda b/src/Algebra/Action/Bundles.agda
index c6b4b4e267..00c6ac9455 100644
--- a/src/Algebra/Action/Bundles.agda
+++ b/src/Algebra/Action/Bundles.agda
@@ -55,7 +55,7 @@ module SetoidAction (M : Setoid c ℓ) (A : Setoid a r) where
     isRawRightAction = record { _ᴬ∙ᴹ_ = curry to ; ∙-cong = curry cong }
       where open Func act
 
-  
+
 ------------------------------------------------------------------------
 -- A Setoid action yields an iterated List action
 
@@ -78,7 +78,7 @@ module _ {M : Setoid c ℓ} {A : Setoid a r} where
       { to = uncurry _ᴬ⋆ᴹ_ ; cong = uncurry ⋆-cong }
     }
     where open Right rightAction; open IsRawRightAction isRawRightAction
-  
+
 
 ------------------------------------------------------------------------
 -- Definition: indexed over an underlying raw action

From 47a5e717587d87a0ca636c99b588226aed312512 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 11 Apr 2024 15:47:01 +0100
Subject: [PATCH 18/39] tidy up!

---
 src/Algebra/Construct/MonoidAction.agda | 227 ------------------------
 1 file changed, 227 deletions(-)
 delete mode 100644 src/Algebra/Construct/MonoidAction.agda

diff --git a/src/Algebra/Construct/MonoidAction.agda b/src/Algebra/Construct/MonoidAction.agda
deleted file mode 100644
index 851b677fe0..0000000000
--- a/src/Algebra/Construct/MonoidAction.agda
+++ /dev/null
@@ -1,227 +0,0 @@
-------------------------------------------------------------------------
--- The Agda standard library
---
--- Monoid Actions and the free Monoid Action on a Setoid
-------------------------------------------------------------------------
-
-{-# OPTIONS --cubical-compatible --safe #-}
-
-module Algebra.Construct.MonoidAction where
-
-open import Algebra.Bundles using (Monoid)
-open import Algebra.Structures using (IsMonoid)
-
-open import Data.List.Base
-  using (List; []; _∷_; _++_; foldl; foldr)
-import Data.List.Properties as List
-open import Data.List.Relation.Binary.Pointwise as Pointwise
-  using (Pointwise; []; _∷_)
-import Data.List.Relation.Binary.Equality.Setoid as ≋
-open import Data.Product.Base using (_,_)
-
-open import Function.Base using (id; _∘_; flip)
-
-open import Level using (Level; suc; _⊔_)
-
-open import Relation.Binary.Bundles using (Setoid)
-open import Relation.Binary.Structures using (IsEquivalence)
-open import Relation.Binary.Core using (Rel)
-open import Relation.Binary.Definitions
-
-private
-  variable
-    a c r ℓ : Level
-    A : Set a
-    M : Set c
-
-
-------------------------------------------------------------------------
--- Basic definitions: fix notation for underlying 'raw' actions
-
-module _ {c a ℓ r} {M : Set c} {A : Set a}
-         (_≈ᴹ_ : Rel M ℓ) (_≈_ : Rel A r)
-  where
-
-  private
-    variable
-      x y z : A
-      m n p q : M
-      ms ns ps qs : List M
-
-  record RawLeftAction : Set (a ⊔ r ⊔ c ⊔ ℓ)  where
-    infixr 5 _ᴹ∙ᴬ_ _ᴹ⋆ᴬ_
-
-    field
-      _ᴹ∙ᴬ_ : M → A → A
-      ∙-cong : m ≈ᴹ n → x ≈ y → (m ᴹ∙ᴬ x) ≈ (n ᴹ∙ᴬ y)
-
--- derived form: iterated action, satisfying congruence
-
-    _ᴹ⋆ᴬ_ : List M → A → A
-    ms ᴹ⋆ᴬ a = foldr _ᴹ∙ᴬ_ a ms
-
-    ⋆-cong : Pointwise _≈ᴹ_ ms ns → x ≈ y → (ms ᴹ⋆ᴬ x) ≈ (ns ᴹ⋆ᴬ y)
-    ⋆-cong []            x≈y = x≈y
-    ⋆-cong (m≈n ∷ ms≋ns) x≈y = ∙-cong m≈n (⋆-cong ms≋ns x≈y)
-
-    ⋆-act-cong : ∀ ms → Pointwise _≈ᴹ_ ps (ms ++ ns) →
-                 x ≈ y → (ps ᴹ⋆ᴬ x) ≈ (ms ᴹ⋆ᴬ ns ᴹ⋆ᴬ y)
-    ⋆-act-cong []       ps≋ns             x≈y = ⋆-cong ps≋ns x≈y
-    ⋆-act-cong (m ∷ ms) (p≈m ∷ ps≋ms++ns) x≈y = ∙-cong p≈m (⋆-act-cong ms ps≋ms++ns x≈y)
-
-    []-act-cong : x ≈ y → ([] ᴹ⋆ᴬ x) ≈ y
-    []-act-cong = id
-
-  record RawRightAction : Set (a ⊔ r ⊔ c ⊔ ℓ)  where
-    infixl 5 _ᴬ∙ᴹ_ _ᴬ⋆ᴹ_
-
-    field
-      _ᴬ∙ᴹ_ : A → M → A
-      ∙-cong : x ≈ y → m ≈ᴹ n → (x ᴬ∙ᴹ m) ≈ (y ᴬ∙ᴹ n)
-
--- derived form: iterated action, satisfying congruence
-
-    _ᴬ⋆ᴹ_ : A → List M → A
-    a ᴬ⋆ᴹ ms = foldl _ᴬ∙ᴹ_ a ms
-
-    ⋆-cong : x ≈ y → Pointwise _≈ᴹ_ ms ns → (x ᴬ⋆ᴹ ms) ≈ (y ᴬ⋆ᴹ ns)
-    ⋆-cong x≈y []            = x≈y
-    ⋆-cong x≈y (m≈n ∷ ms≋ns) = ⋆-cong (∙-cong x≈y m≈n) ms≋ns
-
-    ⋆-act-cong : x ≈ y → ∀ ms → Pointwise _≈ᴹ_ ps (ms ++ ns) →
-                 (x ᴬ⋆ᴹ ps) ≈ (y ᴬ⋆ᴹ ms ᴬ⋆ᴹ ns)
-    ⋆-act-cong x≈y []       ps≋ns             = ⋆-cong x≈y ps≋ns
-    ⋆-act-cong x≈y (m ∷ ms) (p≈m ∷ ps≋ms++ns) = ⋆-act-cong (∙-cong x≈y p≈m) ms ps≋ms++ns
-
-    []-act-cong : x ≈ y → (x ᴬ⋆ᴹ []) ≈ y
-    []-act-cong = id
-
-
-------------------------------------------------------------------------
--- Definition: indexed over an underlying raw action
-
-module _ (M : Monoid c ℓ) (A : Setoid a r) where
-
-  private
-
-    open module M = Monoid M using () renaming (Carrier to M)
-    open module A = Setoid A using (_≈_) renaming (Carrier to A)
-    open ≋ M.setoid using (_≋_; [] ; _∷_; ≋-refl)
-
-    variable
-      x y z : A.Carrier
-      m n p q : M.Carrier
-      ms ns ps qs : List M.Carrier
-
-  record LeftAction (rawLeftAction : RawLeftAction M._≈_ _≈_) : Set (a ⊔ r ⊔ c ⊔ ℓ)
-    where
-
-    open RawLeftAction rawLeftAction public
-      renaming (_ᴹ∙ᴬ_ to _∙_; _ᴹ⋆ᴬ_ to _⋆_)
-
-    field
-      ∙-act  : ∀ m n x → m M.∙ n ∙ x ≈ m ∙ n ∙ x
-      ε-act  : ∀ x → M.ε ∙ x ≈ x
-
-    ∙-congˡ : x ≈ y → m ∙ x ≈ m ∙ y
-    ∙-congˡ x≈y = ∙-cong M.refl x≈y
-
-    ∙-congʳ : m M.≈ n → m ∙ x ≈ n ∙ x
-    ∙-congʳ m≈n = ∙-cong m≈n A.refl
-
-    ⋆-act : ∀ ms ns x → (ms ++ ns) ⋆ x ≈ ms ⋆ ns ⋆ x
-    ⋆-act ms ns x = ⋆-act-cong ms ≋-refl A.refl
-
-    []-act : ∀ x → [] ⋆ x ≈ x
-    []-act _ = []-act-cong A.refl
-
-  record RightAction (rawRightAction : RawRightAction M._≈_ _≈_) : Set (a ⊔ r ⊔ c ⊔ ℓ)
-    where
-
-    open RawRightAction rawRightAction public
-      renaming (_ᴬ∙ᴹ_ to _∙_; _ᴬ⋆ᴹ_ to _⋆_)
-
-    field
-      ∙-act  : ∀ x m n → x ∙ m M.∙ n ≈ x ∙ m ∙ n
-      ε-act  : ∀ x → x ∙ M.ε ≈ x
-
-    ∙-congˡ : x ≈ y → x ∙ m ≈ y ∙ m
-    ∙-congˡ x≈y = ∙-cong x≈y M.refl
-
-    ∙-congʳ : m M.≈ n → x ∙ m ≈ x ∙ n
-    ∙-congʳ m≈n = ∙-cong A.refl m≈n
-
-    ⋆-act : ∀ x ms ns → x ⋆ (ms ++ ns) ≈ x ⋆ ms ⋆ ns
-    ⋆-act x ms ns = ⋆-act-cong A.refl ms ≋-refl
-
-    []-act : ∀ x → x ⋆ [] ≈ x
-    []-act x = []-act-cong A.refl
-
-------------------------------------------------------------------------
--- Distinguished actions: of a module over itself
-
-module Regular (M : Monoid c ℓ) where
-
-  open Monoid M
-
-  private
-    rawLeftAction : RawLeftAction _≈_ _≈_
-    rawLeftAction = record { _ᴹ∙ᴬ_ = _∙_ ; ∙-cong = ∙-cong }
-
-    rawRightAction : RawRightAction _≈_ _≈_
-    rawRightAction = record { _ᴬ∙ᴹ_ = _∙_ ; ∙-cong = ∙-cong }
-
-  leftAction : LeftAction M setoid rawLeftAction
-  leftAction = record
-    { ∙-act = assoc
-    ; ε-act = identityˡ
-    }
-
-  rightAction : RightAction M setoid rawRightAction
-  rightAction = record
-    { ∙-act = λ x m n → sym (assoc x m n)
-    ; ε-act = identityʳ
-    }
-
-------------------------------------------------------------------------
--- Distinguished *free* action: lifting a raw action to a List action
-
-module Free (M : Setoid c ℓ) (S : Setoid a r) where
-
-  private
-
-    open ≋ M using (_≋_; ≋-refl; ≋-reflexive; ≋-isEquivalence; ++⁺)
-    open module M = Setoid M using () renaming (Carrier to M)
-    open module A = Setoid S using (_≈_) renaming (Carrier to A)
-
-    isMonoid : IsMonoid _≋_ _++_ []
-    isMonoid = record
-      { isSemigroup = record
-        { isMagma = record
-          { isEquivalence = ≋-isEquivalence
-          ; ∙-cong = ++⁺
-          }
-        ; assoc = λ xs ys zs → ≋-reflexive (List.++-assoc xs ys zs)
-        }
-      ; identity = (λ _ → ≋-refl) , ≋-reflexive ∘ List.++-identityʳ }
-
-    monoid : Monoid _ _
-    monoid = record { isMonoid = isMonoid }
-
-  leftAction : (rawLeftAction : RawLeftAction M._≈_ _≈_) →
-               (open RawLeftAction rawLeftAction) →
-               LeftAction monoid S (record { _ᴹ∙ᴬ_ = _ᴹ⋆ᴬ_  ; ∙-cong = ⋆-cong })
-  leftAction rawLeftAction = record
-    { ∙-act = λ ms ns x → ⋆-act-cong ms ≋-refl A.refl
-    ; ε-act = λ _ → []-act-cong A.refl
-    }
-    where open RawLeftAction rawLeftAction
-
-  rightAction : (rawRightAction : RawRightAction M._≈_ _≈_) →
-                (open RawRightAction rawRightAction) →
-                RightAction monoid S (record { _ᴬ∙ᴹ_ = _ᴬ⋆ᴹ_  ; ∙-cong = ⋆-cong })
-  rightAction rawRightAction = record
-    { ∙-act = λ x ms ns → ⋆-act-cong A.refl ms ≋-refl
-    ; ε-act = λ _ → []-act-cong A.refl
-    }
-    where open RawRightAction rawRightAction

From 364925d2eddb84c15cc05efd0b36c1acecc9e666 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 12 Apr 2024 08:59:08 +0100
Subject: [PATCH 19/39] some response to review comments: give up on `Raw`
 structures; tweak notation; more modularisation for generality

---
 CHANGELOG.md                                  |  4 +-
 src/Algebra/Action/Bundles.agda               | 50 ++++++-------
 src/Algebra/Action/Construct/Free.agda        | 74 ++++++++++---------
 src/Algebra/Action/Construct/Self.agda        | 73 +++++++++---------
 .../{Structures/Raw.agda => Structures.agda}  |  6 +-
 5 files changed, 109 insertions(+), 98 deletions(-)
 rename src/Algebra/Action/{Structures/Raw.agda => Structures.agda} (94%)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d17614fb39..a569e62b61 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -72,9 +72,9 @@ New modules
   Algebra.Action.Construct.Self
   ```
 
-* Raw structures for left- and right- actions:
+* Structures for left- and right- actions:
   ```
-  Algebra.Action.Structures.Raw
+  Algebra.Action.Structures
   ```
 
 * Raw bundles for module-like algebraic structures:
diff --git a/src/Algebra/Action/Bundles.agda b/src/Algebra/Action/Bundles.agda
index 00c6ac9455..b56870460e 100644
--- a/src/Algebra/Action/Bundles.agda
+++ b/src/Algebra/Action/Bundles.agda
@@ -8,7 +8,7 @@
 
 module Algebra.Action.Bundles where
 
-open import Algebra.Action.Structures.Raw using (IsRawLeftAction; IsRawRightAction)
+open import Algebra.Action.Structures using (IsLeftAction; IsRightAction)
 open import Algebra.Bundles using (Monoid)
 
 open import Data.List.Base using ([]; _++_)
@@ -42,8 +42,8 @@ module SetoidAction (M : Setoid c ℓ) (A : Setoid a r) where
     field
       act : Func (M ×ₛ A) A
 
-    isRawLeftAction : IsRawLeftAction M._≈_ _≈_
-    isRawLeftAction = record { _ᴹ∙ᴬ_ = curry to ; ∙-cong = curry cong }
+    isLeftAction : IsLeftAction M._≈_ _≈_
+    isLeftAction = record { _ᴹ∙ᴬ_ = curry to ; ∙-cong = curry cong }
       where open Func act
 
   record Right : Set (a ⊔ r ⊔ c ⊔ ℓ) where
@@ -51,8 +51,8 @@ module SetoidAction (M : Setoid c ℓ) (A : Setoid a r) where
     field
       act : Func (A ×ₛ M) A
 
-    isRawRightAction : IsRawRightAction M._≈_ _≈_
-    isRawRightAction = record { _ᴬ∙ᴹ_ = curry to ; ∙-cong = curry cong }
+    isRightAction : IsRightAction M._≈_ _≈_
+    isRightAction = record { _ᴬ∙ᴹ_ = curry to ; ∙-cong = curry cong }
       where open Func act
 
 
@@ -70,14 +70,14 @@ module _ {M : Setoid c ℓ} {A : Setoid a r} where
     { act = record
       { to = uncurry _ᴹ⋆ᴬ_ ; cong = uncurry ⋆-cong }
     }
-    where open Left leftAction; open IsRawLeftAction isRawLeftAction
+    where open Left leftAction; open IsLeftAction isLeftAction
 
   rightListAction : (rightAction : Right M A) → Right ≋-setoid A
   rightListAction rightAction = record
     { act = record
       { to = uncurry _ᴬ⋆ᴹ_ ; cong = uncurry ⋆-cong }
     }
-    where open Right rightAction; open IsRawRightAction isRawRightAction
+    where open Right rightAction; open IsRightAction isRightAction
 
 
 ------------------------------------------------------------------------
@@ -87,55 +87,55 @@ module MonoidAction (M : Monoid c ℓ) (A : Setoid a r) where
 
   private
 
-    module M = Monoid M
-    module A = Setoid A
+    open module M = Monoid M using (ε) renaming (_∙_ to _∙ᴹ_)
+    open module A = Setoid A using (_≈_)
     open ≋ M.setoid using (≋-refl)
 
   record Left (leftAction : SetoidAction.Left M.setoid A) : Set (a ⊔ r ⊔ c ⊔ ℓ)
     where
 
     open SetoidAction.Left leftAction public
-      using (isRawLeftAction)
-    open IsRawLeftAction isRawLeftAction public
+      using (isLeftAction)
+    open IsLeftAction isLeftAction public
       renaming (_ᴹ∙ᴬ_ to _∙_; _ᴹ⋆ᴬ_ to _⋆_)
 
     field
-      ∙-act  : ∀ m n x → m M.∙ n ∙ x A.≈ m ∙ n ∙ x
-      ε-act  : ∀ x → M.ε ∙ x A.≈ x
+      ∙-act  : ∀ m n x → m ∙ᴹ n ∙ x ≈ m ∙ n ∙ x
+      ε-act  : ∀ x → ε ∙ x ≈ x
 
-    ∙-congˡ : ∀ {m x y} → x A.≈ y → m ∙ x A.≈ m ∙ y
+    ∙-congˡ : ∀ {m x y} → x ≈ y → m ∙ x ≈ m ∙ y
     ∙-congˡ x≈y = ∙-cong M.refl x≈y
 
-    ∙-congʳ : ∀ {m n x} → m M.≈ n → m ∙ x A.≈ n ∙ x
+    ∙-congʳ : ∀ {m n x} → m M.≈ n → m ∙ x ≈ n ∙ x
     ∙-congʳ m≈n = ∙-cong m≈n A.refl
 
-    ⋆-act : ∀ ms ns x → (ms ++ ns) ⋆ x A.≈ ms ⋆ ns ⋆ x
+    ⋆-act : ∀ ms ns x → (ms ++ ns) ⋆ x ≈ ms ⋆ ns ⋆ x
     ⋆-act ms ns x = ⋆-act-cong ms ≋-refl A.refl
 
-    []-act : ∀ x → [] ⋆ x A.≈ x
+    []-act : ∀ x → [] ⋆ x ≈ x
     []-act _ = []-act-cong A.refl
 
   record Right (rightAction : SetoidAction.Right M.setoid A) : Set (a ⊔ r ⊔ c ⊔ ℓ)
     where
 
     open SetoidAction.Right rightAction public
-      using (isRawRightAction)
-    open IsRawRightAction isRawRightAction public
+      using (isRightAction)
+    open IsRightAction isRightAction public
       renaming (_ᴬ∙ᴹ_ to _∙_; _ᴬ⋆ᴹ_ to _⋆_)
 
     field
-      ∙-act  : ∀ x m n → x ∙ m M.∙ n A.≈ x ∙ m ∙ n
-      ε-act  : ∀ x → x ∙ M.ε A.≈ x
+      ∙-act  : ∀ x m n → x ∙ m ∙ᴹ n ≈ x ∙ m ∙ n
+      ε-act  : ∀ x → x ∙ ε ≈ x
 
-    ∙-congˡ : ∀ {x y m} → x A.≈ y → x ∙ m A.≈ y ∙ m
+    ∙-congˡ : ∀ {x y m} → x ≈ y → x ∙ m ≈ y ∙ m
     ∙-congˡ x≈y = ∙-cong x≈y M.refl
 
-    ∙-congʳ : ∀ {m n x} → m M.≈ n → x ∙ m A.≈ x ∙ n
+    ∙-congʳ : ∀ {m n x} → m M.≈ n → x ∙ m ≈ x ∙ n
     ∙-congʳ m≈n = ∙-cong A.refl m≈n
 
-    ⋆-act : ∀ x ms ns → x ⋆ (ms ++ ns) A.≈ x ⋆ ms ⋆ ns
+    ⋆-act : ∀ x ms ns → x ⋆ (ms ++ ns) ≈ x ⋆ ms ⋆ ns
     ⋆-act x ms ns = ⋆-act-cong A.refl ms ≋-refl
 
-    []-act : ∀ x → x ⋆ [] A.≈ x
+    []-act : ∀ x → x ⋆ [] ≈ x
     []-act x = []-act-cong A.refl
 
diff --git a/src/Algebra/Action/Construct/Free.agda b/src/Algebra/Action/Construct/Free.agda
index d07225eea4..1082c6e76b 100644
--- a/src/Algebra/Action/Construct/Free.agda
+++ b/src/Algebra/Action/Construct/Free.agda
@@ -13,7 +13,7 @@ module Algebra.Action.Construct.Free
   where
 
 open import Algebra.Action.Bundles
-open import Algebra.Action.Structures.Raw using (IsRawLeftAction; IsRawRightAction)
+open import Algebra.Action.Structures using (IsLeftAction; IsRightAction)
 open import Algebra.Bundles using (Monoid)
 open import Algebra.Structures using (IsMonoid)
 
@@ -26,58 +26,64 @@ open import Function.Base using (_∘_)
 
 open import Level using (Level; _⊔_)
 
-open ≋ M using (_≋_; ≋-refl; ≋-reflexive; ≋-isEquivalence; ++⁺)
-open MonoidAction
+------------------------------------------------------------------------
+-- Monoid: the Free action arises from List
+
+module FreeMonoidAction where
+
+  open ≋ M using (_≋_; ≋-refl; ≋-reflexive; ≋-isEquivalence; ++⁺)
+  open MonoidAction
 
 ------------------------------------------------------------------------
 -- First: define the Monoid structure on List M.Carrier
 
-private
+  private
 
-  module M = Setoid M
-  module A = Setoid S
+    module M = Setoid M
+    module A = Setoid S
 
-  isMonoid : IsMonoid _≋_ _++_ []
-  isMonoid = record
-    { isSemigroup = record
-      { isMagma = record
-        { isEquivalence = ≋-isEquivalence
-        ; ∙-cong = ++⁺
+    isMonoid : IsMonoid _≋_ _++_ []
+    isMonoid = record
+      { isSemigroup = record
+        { isMagma = record
+          { isEquivalence = ≋-isEquivalence
+          ; ∙-cong = ++⁺
+          }
+        ; assoc = λ xs ys zs → ≋-reflexive (List.++-assoc xs ys zs)
         }
-      ; assoc = λ xs ys zs → ≋-reflexive (List.++-assoc xs ys zs)
+      ; identity = (λ _ → ≋-refl) , ≋-reflexive ∘ List.++-identityʳ
       }
-    ; identity = (λ _ → ≋-refl) , ≋-reflexive ∘ List.++-identityʳ }
 
-  monoid : Monoid c (c ⊔ ℓ)
-  monoid = record { isMonoid = isMonoid }
+    monoid : Monoid c (c ⊔ ℓ)
+    monoid = record { isMonoid = isMonoid }
 
 
 ------------------------------------------------------------------------
 -- Second: define the actions of that Monoid
 
-module _ (left : SetoidAction.Left M S) where
+  module _ (left : SetoidAction.Left M S) where
 
-  private listAction = leftListAction left
+    private listAction = leftListAction left
 
-  open SetoidAction.Left left
-  open IsRawLeftAction isRawLeftAction
+    open SetoidAction.Left left
+    open IsLeftAction isLeftAction
 
-  leftAction : Left monoid S listAction
-  leftAction = record
-    { ∙-act = λ ms ns x → ⋆-act-cong ms ≋-refl A.refl
-    ; ε-act = λ _ → A.refl
-    }
+    leftAction : Left monoid S listAction
+    leftAction = record
+      { ∙-act = λ ms ns x → ⋆-act-cong ms ≋-refl A.refl
+      ; ε-act = λ _ → A.refl
+      }
 
-module _ (right : SetoidAction.Right M S) where
+  module _ (right : SetoidAction.Right M S) where
 
-  private listAction = rightListAction right
+    private listAction = rightListAction right
 
-  open SetoidAction.Right right
-  open IsRawRightAction isRawRightAction
+    open SetoidAction.Right right
+    open IsRightAction isRightAction
 
-  rightAction : Right monoid S listAction
-  rightAction = record
-    { ∙-act = λ x ms ns → ⋆-act-cong A.refl ms ≋-refl
-    ; ε-act = λ _ → A.refl
-    }
+    rightAction : Right monoid S listAction
+    rightAction = record
+      { ∙-act = λ x ms ns → ⋆-act-cong A.refl ms ≋-refl
+      ; ε-act = λ _ → A.refl
+      }
 
diff --git a/src/Algebra/Action/Construct/Self.agda b/src/Algebra/Action/Construct/Self.agda
index a3bf4b4528..1f4098bd61 100644
--- a/src/Algebra/Action/Construct/Self.agda
+++ b/src/Algebra/Action/Construct/Self.agda
@@ -1,54 +1,59 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- The left- and right- regular actions: of a Monoid over itself
+-- Left- and right- regular actions
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra.Bundles using (Monoid)
-
-module Algebra.Action.Construct.Self {c ℓ} (M : Monoid c ℓ) where
+module Algebra.Action.Construct.Self where
 
 open import Algebra.Action.Bundles
-open import Algebra.Action.Structures.Raw using (IsRawLeftAction; IsRawRightAction)
+open import Algebra.Action.Structures using (IsLeftAction; IsRightAction)
+open import Algebra.Bundles using (Monoid)
+
 open import Data.Product.Base using (uncurry)
 
-open Monoid M
-open MonoidAction M setoid
+------------------------------------------------------------------------
+-- Action of a Monoid over itself
+
+module Regular {c ℓ} (M : Monoid c ℓ) where
 
-private
-  leftSetoidAction : SetoidAction.Left setoid setoid
-  leftSetoidAction = record
-    { act = record
-      { to = uncurry _∙_
-      ; cong = uncurry ∙-cong
+  open Monoid M
+  open MonoidAction M setoid
+
+  private
+    leftSetoidAction : SetoidAction.Left setoid setoid
+    leftSetoidAction = record
+      { act = record
+        { to = uncurry _∙_
+        ; cong = uncurry ∙-cong
+        }
       }
-    }
 
-  rightSetoidAction : SetoidAction.Right setoid setoid
-  rightSetoidAction = record
-    { act = record
-      { to = uncurry _∙_
-      ; cong = uncurry ∙-cong
+    rightSetoidAction : SetoidAction.Right setoid setoid
+    rightSetoidAction = record
+      { act = record
+        { to = uncurry _∙_
+        ; cong = uncurry ∙-cong
+        }
       }
-    }
 
-isRawLeftAction : IsRawLeftAction _≈_ _≈_
-isRawLeftAction = record { _ᴹ∙ᴬ_ = _∙_ ; ∙-cong = ∙-cong }
+  isLeftAction : IsLeftAction _≈_ _≈_
+  isLeftAction = record { _ᴹ∙ᴬ_ = _∙_ ; ∙-cong = ∙-cong }
 
-isRawRightAction : IsRawRightAction _≈_ _≈_
-isRawRightAction = record { _ᴬ∙ᴹ_ = _∙_ ; ∙-cong = ∙-cong }
+  isRightAction : IsRightAction _≈_ _≈_
+  isRightAction = record { _ᴬ∙ᴹ_ = _∙_ ; ∙-cong = ∙-cong }
 
-leftAction : Left leftSetoidAction
-leftAction = record
-  { ∙-act = assoc
-  ; ε-act = identityˡ
-  }
+  leftAction : Left leftSetoidAction
+  leftAction = record
+    { ∙-act = assoc
+    ; ε-act = identityˡ
+    }
 
-rightAction : Right rightSetoidAction
-rightAction = record
-  { ∙-act = λ x m n → sym (assoc x m n)
-  ; ε-act = identityʳ
-  }
+  rightAction : Right rightSetoidAction
+  rightAction = record
+    { ∙-act = λ x m n → sym (assoc x m n)
+    ; ε-act = identityʳ
+    }
 
diff --git a/src/Algebra/Action/Structures/Raw.agda b/src/Algebra/Action/Structures.agda
similarity index 94%
rename from src/Algebra/Action/Structures/Raw.agda
rename to src/Algebra/Action/Structures.agda
index c1882265ea..f764423b98 100644
--- a/src/Algebra/Action/Structures/Raw.agda
+++ b/src/Algebra/Action/Structures.agda
@@ -8,7 +8,7 @@
 
 open import Relation.Binary.Core using (Rel)
 
-module Algebra.Action.Structures.Raw
+module Algebra.Action.Structures
   {c a ℓ r} {M : Set c} {A : Set a} (_≈ᴹ_ : Rel M ℓ) (_≈_ : Rel A r)
   where
 
@@ -28,7 +28,7 @@ private
 ------------------------------------------------------------------------
 -- Basic definitions: fix notation
 
-record IsRawLeftAction : Set (a ⊔ r ⊔ c ⊔ ℓ) where
+record IsLeftAction : Set (a ⊔ r ⊔ c ⊔ ℓ) where
   infixr 5 _ᴹ∙ᴬ_ _ᴹ⋆ᴬ_
 
   field
@@ -52,7 +52,7 @@ record IsRawLeftAction : Set (a ⊔ r ⊔ c ⊔ ℓ) where
   []-act-cong : x ≈ y → ([] ᴹ⋆ᴬ x) ≈ y
   []-act-cong = id
 
-record IsRawRightAction : Set (a ⊔ r ⊔ c ⊔ ℓ) where
+record IsRightAction : Set (a ⊔ r ⊔ c ⊔ ℓ) where
   infixl 5 _ᴬ∙ᴹ_ _ᴬ⋆ᴹ_
 
   field

From 110d57699191c8879f782f1e0225d36d4b78a0ea Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 12 Apr 2024 09:04:39 +0100
Subject: [PATCH 20/39] fixed comment

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

diff --git a/src/Algebra/Action/Bundles.agda b/src/Algebra/Action/Bundles.agda
index b56870460e..6cd91f4840 100644
--- a/src/Algebra/Action/Bundles.agda
+++ b/src/Algebra/Action/Bundles.agda
@@ -81,7 +81,7 @@ module _ {M : Setoid c ℓ} {A : Setoid a r} where
 
 
 ------------------------------------------------------------------------
--- Definition: indexed over an underlying raw action
+-- Definition: indexed over an underlying SetoidAction
 
 module MonoidAction (M : Monoid c ℓ) (A : Setoid a r) where
 

From 63ef07ed4e67d03942e9c092afc27d5a4b7fcbeb Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 12 Apr 2024 09:05:57 +0100
Subject: [PATCH 21/39] removed more qualifications

---
 src/Algebra/Action/Bundles.agda | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Algebra/Action/Bundles.agda b/src/Algebra/Action/Bundles.agda
index 6cd91f4840..69a6cf7c58 100644
--- a/src/Algebra/Action/Bundles.agda
+++ b/src/Algebra/Action/Bundles.agda
@@ -87,11 +87,11 @@ module MonoidAction (M : Monoid c ℓ) (A : Setoid a r) where
 
   private
 
-    open module M = Monoid M using (ε) renaming (_∙_ to _∙ᴹ_)
+    open module M = Monoid M using (ε; setoid) renaming (_∙_ to _∙ᴹ_)
     open module A = Setoid A using (_≈_)
-    open ≋ M.setoid using (≋-refl)
+    open ≋ setoid using (≋-refl)
 
-  record Left (leftAction : SetoidAction.Left M.setoid A) : Set (a ⊔ r ⊔ c ⊔ ℓ)
+  record Left (leftAction : SetoidAction.Left setoid A) : Set (a ⊔ r ⊔ c ⊔ ℓ)
     where
 
     open SetoidAction.Left leftAction public
@@ -115,7 +115,7 @@ module MonoidAction (M : Monoid c ℓ) (A : Setoid a r) where
     []-act : ∀ x → [] ⋆ x ≈ x
     []-act _ = []-act-cong A.refl
 
-  record Right (rightAction : SetoidAction.Right M.setoid A) : Set (a ⊔ r ⊔ c ⊔ ℓ)
+  record Right (rightAction : SetoidAction.Right setoid A) : Set (a ⊔ r ⊔ c ⊔ ℓ)
     where
 
     open SetoidAction.Right rightAction public

From 2f2c9b91eef43bcfb5295b9077c1d2b53e101aea Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 12 Apr 2024 12:46:16 +0100
Subject: [PATCH 22/39] long opening comment on naming added

---
 src/Algebra/Action/Bundles.agda | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/src/Algebra/Action/Bundles.agda b/src/Algebra/Action/Bundles.agda
index 69a6cf7c58..34c24a0254 100644
--- a/src/Algebra/Action/Bundles.agda
+++ b/src/Algebra/Action/Bundles.agda
@@ -4,6 +4,16 @@
 -- Setoid Actions and Monoid Actions
 ------------------------------------------------------------------------
 
+------------------------------------------------------------------------
+-- Currently, this module (attempts to) systematically distinguish
+-- between left- and right- actions, but unfortunately, trying to avoid
+-- long names such as `Algebra.Action.Bundles.MonoidAction.LeftAction`
+-- leads to the possibly/probably suboptimal use of `Left` and `Right` as
+-- submodule names, when these are intended only to be used qualified by
+-- the type of Action to which they refer, eg. as MonoidAction.Left etc.
+------------------------------------------------------------------------
+
+
 {-# OPTIONS --cubical-compatible --safe #-}
 
 module Algebra.Action.Bundles where

From 8e6b1308388743e3b2d8d30cb13b245e6d495113 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 25 Apr 2024 11:06:05 +0100
Subject: [PATCH 23/39] notation

---
 src/Algebra/Action/Structures.agda | 69 +++++++++++++++++-------------
 1 file changed, 40 insertions(+), 29 deletions(-)

diff --git a/src/Algebra/Action/Structures.agda b/src/Algebra/Action/Structures.agda
index f764423b98..f9dc87c68d 100644
--- a/src/Algebra/Action/Structures.agda
+++ b/src/Algebra/Action/Structures.agda
@@ -14,6 +14,8 @@ module Algebra.Action.Structures
 
 open import Data.List.Base
   using (List; []; _∷_; _++_; foldl; foldr)
+open import Data.List.NonEmpty.Base
+  using (List⁺; _∷_)
 open import Data.List.Relation.Binary.Pointwise as Pointwise
   using (Pointwise; []; _∷_)
 open import Function.Base using (id)
@@ -29,49 +31,58 @@ private
 -- Basic definitions: fix notation
 
 record IsLeftAction : Set (a ⊔ r ⊔ c ⊔ ℓ) where
-  infixr 5 _ᴹ∙ᴬ_ _ᴹ⋆ᴬ_
+  infixr 5 _◁_ _◁⋆_ _◁⁺_
 
   field
-    _ᴹ∙ᴬ_  : M → A → A
-    ∙-cong : m ≈ᴹ n → x ≈ y → (m ᴹ∙ᴬ x) ≈ (n ᴹ∙ᴬ y)
+    _◁_  : M → A → A
+    ◁-cong : m ≈ᴹ n → x ≈ y → (m ◁ x) ≈ (n ◁ y)
 
 -- derived form: iterated action, satisfying congruence
 
-  _ᴹ⋆ᴬ_ : List M → A → A
-  ms ᴹ⋆ᴬ a = foldr _ᴹ∙ᴬ_ a ms
-
-  ⋆-cong : Pointwise _≈ᴹ_ ms ns → x ≈ y → (ms ᴹ⋆ᴬ x) ≈ (ns ᴹ⋆ᴬ y)
-  ⋆-cong []            x≈y = x≈y
-  ⋆-cong (m≈n ∷ ms≋ns) x≈y = ∙-cong m≈n (⋆-cong ms≋ns x≈y)
-
-  ⋆-act-cong : ∀ ms → Pointwise _≈ᴹ_ ps (ms ++ ns) →
-               x ≈ y → (ps ᴹ⋆ᴬ x) ≈ (ms ᴹ⋆ᴬ ns ᴹ⋆ᴬ y)
-  ⋆-act-cong []       ps≋ns             x≈y = ⋆-cong ps≋ns x≈y
-  ⋆-act-cong (m ∷ ms) (p≈m ∷ ps≋ms++ns) x≈y = ∙-cong p≈m (⋆-act-cong ms ps≋ms++ns x≈y)
-
-  []-act-cong : x ≈ y → ([] ᴹ⋆ᴬ x) ≈ y
+  _◁⋆_ : List M → A → A
+  ms ◁⋆ a = foldr _◁_ a ms
+
+  _◁⁺_ : List⁺ M → A → A
+  (m ∷ ms) ◁⁺ a = m ◁ ms ◁⋆ a
+
+  ◁⋆-cong : Pointwise _≈ᴹ_ ms ns → x ≈ y → (ms ◁⋆ x) ≈ (ns ◁⋆ y)
+  ◁⋆-cong []            x≈y = x≈y
+  ◁⋆-cong (m≈n ∷ ms≋ns) x≈y = ◁-cong m≈n (◁⋆-cong ms≋ns x≈y)
+{-
+  ◁⁺-cong : Pointwise _≈ᴹ_ ms ns → x ≈ y → (ms ◁⁺ x) ≈ (ns ◁⁺ y)
+  ◁⁺-cong (m≈n ∷ ms≋ns) x≈y = ◁-cong m≈n (◁⋆-cong ms≋ns x≈y)
+-}
+  ◁⋆-act-cong : ∀ ms → Pointwise _≈ᴹ_ ps (ms ++ ns) →
+                x ≈ y → (ps ◁⋆ x) ≈ (ms ◁⋆ ns ◁⋆ y)
+  ◁⋆-act-cong []       ps≋ns             x≈y = ◁⋆-cong ps≋ns x≈y
+  ◁⋆-act-cong (m ∷ ms) (p≈m ∷ ps≋ms++ns) x≈y = ◁-cong p≈m (◁⋆-act-cong ms ps≋ms++ns x≈y)
+
+  []-act-cong : x ≈ y → ([] ◁⋆ x) ≈ y
   []-act-cong = id
 
 record IsRightAction : Set (a ⊔ r ⊔ c ⊔ ℓ) where
-  infixl 5 _ᴬ∙ᴹ_ _ᴬ⋆ᴹ_
+  infixl 5 _▷_ _▷⋆_ _▷⁺_
 
   field
-    _ᴬ∙ᴹ_  : A → M → A
-    ∙-cong : x ≈ y → m ≈ᴹ n → (x ᴬ∙ᴹ m) ≈ (y ᴬ∙ᴹ n)
+    _▷_  : A → M → A
+    ▷-cong : x ≈ y → m ≈ᴹ n → (x ▷ m) ≈ (y ▷ n)
 
 -- derived form: iterated action, satisfying congruence
 
-  _ᴬ⋆ᴹ_ : A → List M → A
-  a ᴬ⋆ᴹ ms = foldl _ᴬ∙ᴹ_ a ms
+  _▷⋆_ : A → List M → A
+  a ▷⋆ ms = foldl _▷_ a ms
+
+  _▷⁺_ : A → List⁺ M → A
+  a ▷⁺ (m ∷ ms) = a ▷ m ▷⋆ ms
 
-  ⋆-cong : x ≈ y → Pointwise _≈ᴹ_ ms ns → (x ᴬ⋆ᴹ ms) ≈ (y ᴬ⋆ᴹ ns)
-  ⋆-cong x≈y []            = x≈y
-  ⋆-cong x≈y (m≈n ∷ ms≋ns) = ⋆-cong (∙-cong x≈y m≈n) ms≋ns
+  ▷⋆-cong : x ≈ y → Pointwise _≈ᴹ_ ms ns → (x ▷⋆ ms) ≈ (y ▷⋆ ns)
+  ▷⋆-cong x≈y []            = x≈y
+  ▷⋆-cong x≈y (m≈n ∷ ms≋ns) = ▷⋆-cong (▷-cong x≈y m≈n) ms≋ns
 
-  ⋆-act-cong : x ≈ y → ∀ ms → Pointwise _≈ᴹ_ ps (ms ++ ns) →
-               (x ᴬ⋆ᴹ ps) ≈ (y ᴬ⋆ᴹ ms ᴬ⋆ᴹ ns)
-  ⋆-act-cong x≈y []       ps≋ns             = ⋆-cong x≈y ps≋ns
-  ⋆-act-cong x≈y (m ∷ ms) (p≈m ∷ ps≋ms++ns) = ⋆-act-cong (∙-cong x≈y p≈m) ms ps≋ms++ns
+  ▷⋆-act-cong : x ≈ y → ∀ ms → Pointwise _≈ᴹ_ ps (ms ++ ns) →
+               (x ▷⋆ ps) ≈ (y ▷⋆ ms ▷⋆ ns)
+  ▷⋆-act-cong x≈y []       ps≋ns             = ▷⋆-cong x≈y ps≋ns
+  ▷⋆-act-cong x≈y (m ∷ ms) (p≈m ∷ ps≋ms++ns) = ▷⋆-act-cong (▷-cong x≈y p≈m) ms ps≋ms++ns
 
-  []-act-cong : x ≈ y → (x ᴬ⋆ᴹ []) ≈ y
+  []-act-cong : x ≈ y → (x ▷⋆ []) ≈ y
   []-act-cong = id

From c0aa8b66995880e7df833c9d497498bbfdfd968e Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 25 Apr 2024 11:28:17 +0100
Subject: [PATCH 24/39] flip notation; simplify `Bundles`

---
 src/Algebra/Action/Bundles.agda    | 89 +++++++++++++-----------------
 src/Algebra/Action/Structures.agda | 64 ++++++++++-----------
 2 files changed, 71 insertions(+), 82 deletions(-)

diff --git a/src/Algebra/Action/Bundles.agda b/src/Algebra/Action/Bundles.agda
index 34c24a0254..d045196806 100644
--- a/src/Algebra/Action/Bundles.agda
+++ b/src/Algebra/Action/Bundles.agda
@@ -23,11 +23,6 @@ open import Algebra.Bundles using (Monoid)
 
 open import Data.List.Base using ([]; _++_)
 import Data.List.Relation.Binary.Equality.Setoid as ≋
-open import Data.Product.Base using (curry; uncurry)
-open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
-
-open import Function.Bundles using (Func)
-
 open import Level using (Level; _⊔_)
 
 open import Relation.Binary.Bundles using (Setoid)
@@ -44,50 +39,46 @@ module SetoidAction (M : Setoid c ℓ) (A : Setoid a r) where
 
   private
 
-    open module M = Setoid M using ()
-    open module A = Setoid A using (_≈_)
+    module M = Setoid M
+    module A = Setoid A
 
   record Left : Set (a ⊔ r ⊔ c ⊔ ℓ) where
 
     field
-      act : Func (M ×ₛ A) A
-
-    isLeftAction : IsLeftAction M._≈_ _≈_
-    isLeftAction = record { _ᴹ∙ᴬ_ = curry to ; ∙-cong = curry cong }
-      where open Func act
+      isLeftAction : IsLeftAction M._≈_ A._≈_
 
   record Right : Set (a ⊔ r ⊔ c ⊔ ℓ) where
 
     field
-      act : Func (A ×ₛ M) A
-
-    isRightAction : IsRightAction M._≈_ _≈_
-    isRightAction = record { _ᴬ∙ᴹ_ = curry to ; ∙-cong = curry cong }
-      where open Func act
+      isRightAction : IsRightAction M._≈_ A._≈_
 
 
 ------------------------------------------------------------------------
 -- A Setoid action yields an iterated List action
 
-module _ {M : Setoid c ℓ} {A : Setoid a r} where
+module ListAction {M : Setoid c ℓ} {A : Setoid a r} where
 
   open SetoidAction
 
   open ≋ M using (≋-setoid)
 
-  leftListAction : (leftAction : Left M A) → Left ≋-setoid A
-  leftListAction leftAction = record
-    { act = record
-      { to = uncurry _ᴹ⋆ᴬ_ ; cong = uncurry ⋆-cong }
+  leftAction : (left : Left M A) → Left ≋-setoid A
+  leftAction left = record
+    { isLeftAction = record
+      { _▷_ = _▷⋆_
+      ; ▷-cong = ▷⋆-cong
+      }
     }
-    where open Left leftAction; open IsLeftAction isLeftAction
-
-  rightListAction : (rightAction : Right M A) → Right ≋-setoid A
-  rightListAction rightAction = record
-    { act = record
-      { to = uncurry _ᴬ⋆ᴹ_ ; cong = uncurry ⋆-cong }
+    where open Left left; open IsLeftAction isLeftAction
+
+  rightAction : (right : Right M A) → Right ≋-setoid A
+  rightAction right = record
+    { isRightAction = record
+      { _◁_ = _◁⋆_
+      ; ◁-cong = ◁⋆-cong
+      }
     }
-    where open Right rightAction; open IsRightAction isRightAction
+    where open Right right; open IsRightAction isRightAction
 
 
 ------------------------------------------------------------------------
@@ -97,7 +88,7 @@ module MonoidAction (M : Monoid c ℓ) (A : Setoid a r) where
 
   private
 
-    open module M = Monoid M using (ε; setoid) renaming (_∙_ to _∙ᴹ_)
+    open module M = Monoid M using (ε; _∙_; setoid)
     open module A = Setoid A using (_≈_)
     open ≋ setoid using (≋-refl)
 
@@ -107,22 +98,21 @@ module MonoidAction (M : Monoid c ℓ) (A : Setoid a r) where
     open SetoidAction.Left leftAction public
       using (isLeftAction)
     open IsLeftAction isLeftAction public
-      renaming (_ᴹ∙ᴬ_ to _∙_; _ᴹ⋆ᴬ_ to _⋆_)
 
     field
-      ∙-act  : ∀ m n x → m ∙ᴹ n ∙ x ≈ m ∙ n ∙ x
-      ε-act  : ∀ x → ε ∙ x ≈ x
+      ▷-act  : ∀ m n x → m ∙ n ▷ x ≈ m ▷ n ▷ x
+      ε-act  : ∀ x → ε ▷ x ≈ x
 
-    ∙-congˡ : ∀ {m x y} → x ≈ y → m ∙ x ≈ m ∙ y
-    ∙-congˡ x≈y = ∙-cong M.refl x≈y
+    ▷-congˡ : ∀ {m x y} → x ≈ y → m ▷ x ≈ m ▷ y
+    ▷-congˡ x≈y = ▷-cong M.refl x≈y
 
-    ∙-congʳ : ∀ {m n x} → m M.≈ n → m ∙ x ≈ n ∙ x
-    ∙-congʳ m≈n = ∙-cong m≈n A.refl
+    ▷-congʳ : ∀ {m n x} → m M.≈ n → m ▷ x ≈ n ▷ x
+    ▷-congʳ m≈n = ▷-cong m≈n A.refl
 
-    ⋆-act : ∀ ms ns x → (ms ++ ns) ⋆ x ≈ ms ⋆ ns ⋆ x
-    ⋆-act ms ns x = ⋆-act-cong ms ≋-refl A.refl
+    ▷⋆-act : ∀ ms ns x → (ms ++ ns) ▷⋆ x ≈ ms ▷⋆ ns ▷⋆ x
+    ▷⋆-act ms ns x = ▷⋆-act-cong ms ≋-refl A.refl
 
-    []-act : ∀ x → [] ⋆ x ≈ x
+    []-act : ∀ x → [] ▷⋆ x ≈ x
     []-act _ = []-act-cong A.refl
 
   record Right (rightAction : SetoidAction.Right setoid A) : Set (a ⊔ r ⊔ c ⊔ ℓ)
@@ -131,21 +121,20 @@ module MonoidAction (M : Monoid c ℓ) (A : Setoid a r) where
     open SetoidAction.Right rightAction public
       using (isRightAction)
     open IsRightAction isRightAction public
-      renaming (_ᴬ∙ᴹ_ to _∙_; _ᴬ⋆ᴹ_ to _⋆_)
 
     field
-      ∙-act  : ∀ x m n → x ∙ m ∙ᴹ n ≈ x ∙ m ∙ n
-      ε-act  : ∀ x → x ∙ ε ≈ x
+      ◁-act  : ∀ x m n → x ◁ m ∙ n ≈ x ◁ m ◁ n
+      ε-act  : ∀ x → x ◁ ε ≈ x
 
-    ∙-congˡ : ∀ {x y m} → x ≈ y → x ∙ m ≈ y ∙ m
-    ∙-congˡ x≈y = ∙-cong x≈y M.refl
+    ◁-congˡ : ∀ {x y m} → x ≈ y → x ◁ m ≈ y ◁ m
+    ◁-congˡ x≈y = ◁-cong x≈y M.refl
 
-    ∙-congʳ : ∀ {m n x} → m M.≈ n → x ∙ m ≈ x ∙ n
-    ∙-congʳ m≈n = ∙-cong A.refl m≈n
+    ◁-congʳ : ∀ {m n x} → m M.≈ n → x ◁ m ≈ x ◁ n
+    ◁-congʳ m≈n = ◁-cong A.refl m≈n
 
-    ⋆-act : ∀ x ms ns → x ⋆ (ms ++ ns) ≈ x ⋆ ms ⋆ ns
-    ⋆-act x ms ns = ⋆-act-cong A.refl ms ≋-refl
+    ◁⋆-act : ∀ x ms ns → x ◁⋆ (ms ++ ns) ≈ x ◁⋆ ms ◁⋆ ns
+    ◁⋆-act x ms ns = ◁⋆-act-cong A.refl ms ≋-refl
 
-    []-act : ∀ x → x ⋆ [] ≈ x
+    []-act : ∀ x → x ◁⋆ [] ≈ x
     []-act x = []-act-cong A.refl
 
diff --git a/src/Algebra/Action/Structures.agda b/src/Algebra/Action/Structures.agda
index f9dc87c68d..1d47a59f82 100644
--- a/src/Algebra/Action/Structures.agda
+++ b/src/Algebra/Action/Structures.agda
@@ -31,58 +31,58 @@ private
 -- Basic definitions: fix notation
 
 record IsLeftAction : Set (a ⊔ r ⊔ c ⊔ ℓ) where
-  infixr 5 _◁_ _◁⋆_ _◁⁺_
+  infixr 5 _▷_ _▷⋆_ _▷⁺_
 
   field
-    _◁_  : M → A → A
-    ◁-cong : m ≈ᴹ n → x ≈ y → (m ◁ x) ≈ (n ◁ y)
+    _▷_  : M → A → A
+    ▷-cong : m ≈ᴹ n → x ≈ y → (m ▷ x) ≈ (n ▷ y)
 
 -- derived form: iterated action, satisfying congruence
 
-  _◁⋆_ : List M → A → A
-  ms ◁⋆ a = foldr _◁_ a ms
+  _▷⋆_ : List M → A → A
+  ms ▷⋆ a = foldr _▷_ a ms
 
-  _◁⁺_ : List⁺ M → A → A
-  (m ∷ ms) ◁⁺ a = m ◁ ms ◁⋆ a
+  _▷⁺_ : List⁺ M → A → A
+  (m ∷ ms) ▷⁺ a = m ▷ ms ▷⋆ a
 
-  ◁⋆-cong : Pointwise _≈ᴹ_ ms ns → x ≈ y → (ms ◁⋆ x) ≈ (ns ◁⋆ y)
-  ◁⋆-cong []            x≈y = x≈y
-  ◁⋆-cong (m≈n ∷ ms≋ns) x≈y = ◁-cong m≈n (◁⋆-cong ms≋ns x≈y)
+  ▷⋆-cong : Pointwise _≈ᴹ_ ms ns → x ≈ y → (ms ▷⋆ x) ≈ (ns ▷⋆ y)
+  ▷⋆-cong []            x≈y = x≈y
+  ▷⋆-cong (m≈n ∷ ms≋ns) x≈y = ▷-cong m≈n (▷⋆-cong ms≋ns x≈y)
 {-
-  ◁⁺-cong : Pointwise _≈ᴹ_ ms ns → x ≈ y → (ms ◁⁺ x) ≈ (ns ◁⁺ y)
-  ◁⁺-cong (m≈n ∷ ms≋ns) x≈y = ◁-cong m≈n (◁⋆-cong ms≋ns x≈y)
+  ▷⁺-cong : Pointwise _≈ᴹ_ ms ns → x ≈ y → (ms ▷⁺ x) ≈ (ns ▷⁺ y)
+  ▷⁺-cong (m≈n ∷ ms≋ns) x≈y = ▷-cong m≈n (▷⋆-cong ms≋ns x≈y)
 -}
-  ◁⋆-act-cong : ∀ ms → Pointwise _≈ᴹ_ ps (ms ++ ns) →
-                x ≈ y → (ps ◁⋆ x) ≈ (ms ◁⋆ ns ◁⋆ y)
-  ◁⋆-act-cong []       ps≋ns             x≈y = ◁⋆-cong ps≋ns x≈y
-  ◁⋆-act-cong (m ∷ ms) (p≈m ∷ ps≋ms++ns) x≈y = ◁-cong p≈m (◁⋆-act-cong ms ps≋ms++ns x≈y)
+  ▷⋆-act-cong : ∀ ms → Pointwise _≈ᴹ_ ps (ms ++ ns) →
+                x ≈ y → (ps ▷⋆ x) ≈ (ms ▷⋆ ns ▷⋆ y)
+  ▷⋆-act-cong []       ps≋ns             x≈y = ▷⋆-cong ps≋ns x≈y
+  ▷⋆-act-cong (m ∷ ms) (p≈m ∷ ps≋ms++ns) x≈y = ▷-cong p≈m (▷⋆-act-cong ms ps≋ms++ns x≈y)
 
-  []-act-cong : x ≈ y → ([] ◁⋆ x) ≈ y
+  []-act-cong : x ≈ y → ([] ▷⋆ x) ≈ y
   []-act-cong = id
 
 record IsRightAction : Set (a ⊔ r ⊔ c ⊔ ℓ) where
-  infixl 5 _▷_ _▷⋆_ _▷⁺_
+  infixl 5 _◁_ _◁⋆_ _◁⁺_
 
   field
-    _▷_  : A → M → A
-    ▷-cong : x ≈ y → m ≈ᴹ n → (x ▷ m) ≈ (y ▷ n)
+    _◁_  : A → M → A
+    ◁-cong : x ≈ y → m ≈ᴹ n → (x ◁ m) ≈ (y ◁ n)
 
 -- derived form: iterated action, satisfying congruence
 
-  _▷⋆_ : A → List M → A
-  a ▷⋆ ms = foldl _▷_ a ms
+  _◁⋆_ : A → List M → A
+  a ◁⋆ ms = foldl _◁_ a ms
 
-  _▷⁺_ : A → List⁺ M → A
-  a ▷⁺ (m ∷ ms) = a ▷ m ▷⋆ ms
+  _◁⁺_ : A → List⁺ M → A
+  a ◁⁺ (m ∷ ms) = a ◁ m ◁⋆ ms
 
-  ▷⋆-cong : x ≈ y → Pointwise _≈ᴹ_ ms ns → (x ▷⋆ ms) ≈ (y ▷⋆ ns)
-  ▷⋆-cong x≈y []            = x≈y
-  ▷⋆-cong x≈y (m≈n ∷ ms≋ns) = ▷⋆-cong (▷-cong x≈y m≈n) ms≋ns
+  ◁⋆-cong : x ≈ y → Pointwise _≈ᴹ_ ms ns → (x ◁⋆ ms) ≈ (y ◁⋆ ns)
+  ◁⋆-cong x≈y []            = x≈y
+  ◁⋆-cong x≈y (m≈n ∷ ms≋ns) = ◁⋆-cong (◁-cong x≈y m≈n) ms≋ns
 
-  ▷⋆-act-cong : x ≈ y → ∀ ms → Pointwise _≈ᴹ_ ps (ms ++ ns) →
-               (x ▷⋆ ps) ≈ (y ▷⋆ ms ▷⋆ ns)
-  ▷⋆-act-cong x≈y []       ps≋ns             = ▷⋆-cong x≈y ps≋ns
-  ▷⋆-act-cong x≈y (m ∷ ms) (p≈m ∷ ps≋ms++ns) = ▷⋆-act-cong (▷-cong x≈y p≈m) ms ps≋ms++ns
+  ◁⋆-act-cong : x ≈ y → ∀ ms → Pointwise _≈ᴹ_ ps (ms ++ ns) →
+               (x ◁⋆ ps) ≈ (y ◁⋆ ms ◁⋆ ns)
+  ◁⋆-act-cong x≈y []       ps≋ns             = ◁⋆-cong x≈y ps≋ns
+  ◁⋆-act-cong x≈y (m ∷ ms) (p≈m ∷ ps≋ms++ns) = ◁⋆-act-cong (◁-cong x≈y p≈m) ms ps≋ms++ns
 
-  []-act-cong : x ≈ y → (x ▷⋆ []) ≈ y
+  []-act-cong : x ≈ y → (x ◁⋆ []) ≈ y
   []-act-cong = id

From 79728c5af3695b610818aab04ccc755e8c0d0a91 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 25 Apr 2024 11:37:25 +0100
Subject: [PATCH 25/39] =?UTF-8?q?congruence=20for=20`List=E2=81=BA`=20acti?=
 =?UTF-8?q?ons?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Algebra/Action/Structures.agda | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/src/Algebra/Action/Structures.agda b/src/Algebra/Action/Structures.agda
index 1d47a59f82..6e87c2168d 100644
--- a/src/Algebra/Action/Structures.agda
+++ b/src/Algebra/Action/Structures.agda
@@ -48,10 +48,10 @@ record IsLeftAction : Set (a ⊔ r ⊔ c ⊔ ℓ) where
   ▷⋆-cong : Pointwise _≈ᴹ_ ms ns → x ≈ y → (ms ▷⋆ x) ≈ (ns ▷⋆ y)
   ▷⋆-cong []            x≈y = x≈y
   ▷⋆-cong (m≈n ∷ ms≋ns) x≈y = ▷-cong m≈n (▷⋆-cong ms≋ns x≈y)
-{-
-  ▷⁺-cong : Pointwise _≈ᴹ_ ms ns → x ≈ y → (ms ▷⁺ x) ≈ (ns ▷⁺ y)
-  ▷⁺-cong (m≈n ∷ ms≋ns) x≈y = ▷-cong m≈n (▷⋆-cong ms≋ns x≈y)
--}
+
+  ▷⁺-cong : m ≈ᴹ n → Pointwise _≈ᴹ_ ms ns → x ≈ y → ((m ∷ ms) ▷⁺ x) ≈ ((n ∷ ns) ▷⁺ y)
+  ▷⁺-cong m≈n ms≋ns x≈y = ▷-cong m≈n (▷⋆-cong ms≋ns x≈y)
+
   ▷⋆-act-cong : ∀ ms → Pointwise _≈ᴹ_ ps (ms ++ ns) →
                 x ≈ y → (ps ▷⋆ x) ≈ (ms ▷⋆ ns ▷⋆ y)
   ▷⋆-act-cong []       ps≋ns             x≈y = ▷⋆-cong ps≋ns x≈y
@@ -79,6 +79,9 @@ record IsRightAction : Set (a ⊔ r ⊔ c ⊔ ℓ) where
   ◁⋆-cong x≈y []            = x≈y
   ◁⋆-cong x≈y (m≈n ∷ ms≋ns) = ◁⋆-cong (◁-cong x≈y m≈n) ms≋ns
 
+  ◁⁺-cong : x ≈ y → m ≈ᴹ n → Pointwise _≈ᴹ_ ms ns → (x ◁⁺ (m ∷ ms)) ≈ (y ◁⁺ (n ∷ ns))
+  ◁⁺-cong x≈y m≈n ms≋ns = ◁⋆-cong (◁-cong x≈y m≈n) (ms≋ns)
+
   ◁⋆-act-cong : x ≈ y → ∀ ms → Pointwise _≈ᴹ_ ps (ms ++ ns) →
                (x ◁⋆ ps) ≈ (y ◁⋆ ms ◁⋆ ns)
   ◁⋆-act-cong x≈y []       ps≋ns             = ◁⋆-cong x≈y ps≋ns

From 937823ddaf496c77d251b57b57b6b33cce993846 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 25 Apr 2024 11:47:05 +0100
Subject: [PATCH 26/39] simplify `Self` actions

---
 src/Algebra/Action/Construct/Self.agda | 33 ++++++--------------------
 1 file changed, 7 insertions(+), 26 deletions(-)

diff --git a/src/Algebra/Action/Construct/Self.agda b/src/Algebra/Action/Construct/Self.agda
index 1f4098bd61..4e19747cf2 100644
--- a/src/Algebra/Action/Construct/Self.agda
+++ b/src/Algebra/Action/Construct/Self.agda
@@ -12,48 +12,29 @@ open import Algebra.Action.Bundles
 open import Algebra.Action.Structures using (IsLeftAction; IsRightAction)
 open import Algebra.Bundles using (Monoid)
 
-open import Data.Product.Base using (uncurry)
-
 ------------------------------------------------------------------------
--- Action of a Monoid over itself
+-- Left- and Right- Actions of a Monoid over itself
 
 module Regular {c ℓ} (M : Monoid c ℓ) where
 
   open Monoid M
   open MonoidAction M setoid
 
-  private
-    leftSetoidAction : SetoidAction.Left setoid setoid
-    leftSetoidAction = record
-      { act = record
-        { to = uncurry _∙_
-        ; cong = uncurry ∙-cong
-        }
-      }
-
-    rightSetoidAction : SetoidAction.Right setoid setoid
-    rightSetoidAction = record
-      { act = record
-        { to = uncurry _∙_
-        ; cong = uncurry ∙-cong
-        }
-      }
-
   isLeftAction : IsLeftAction _≈_ _≈_
-  isLeftAction = record { _ᴹ∙ᴬ_ = _∙_ ; ∙-cong = ∙-cong }
+  isLeftAction = record { _▷_ = _∙_ ; ▷-cong = ∙-cong }
 
   isRightAction : IsRightAction _≈_ _≈_
-  isRightAction = record { _ᴬ∙ᴹ_ = _∙_ ; ∙-cong = ∙-cong }
+  isRightAction = record { _◁_ = _∙_ ; ◁-cong = ∙-cong }
 
-  leftAction : Left leftSetoidAction
+  leftAction : Left record { isLeftAction = isLeftAction }
   leftAction = record
-    { ∙-act = assoc
+    { ▷-act = assoc
     ; ε-act = identityˡ
     }
 
-  rightAction : Right rightSetoidAction
+  rightAction : Right record { isRightAction = isRightAction }
   rightAction = record
-    { ∙-act = λ x m n → sym (assoc x m n)
+    { ◁-act = λ x m n → sym (assoc x m n)
     ; ε-act = identityʳ
     }
 

From 654eda0f66ff623093787b57cba11d5e5f5eb06a Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 25 Apr 2024 11:56:51 +0100
Subject: [PATCH 27/39] renamed `Free` to `FreeMonoid`: needs simplifying!

---
 .../Action/Construct/{Free.agda => FreeMonoid.agda}    | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)
 rename src/Algebra/Action/Construct/{Free.agda => FreeMonoid.agda} (89%)

diff --git a/src/Algebra/Action/Construct/Free.agda b/src/Algebra/Action/Construct/FreeMonoid.agda
similarity index 89%
rename from src/Algebra/Action/Construct/Free.agda
rename to src/Algebra/Action/Construct/FreeMonoid.agda
index 1082c6e76b..9fd58e8e7c 100644
--- a/src/Algebra/Action/Construct/Free.agda
+++ b/src/Algebra/Action/Construct/FreeMonoid.agda
@@ -8,7 +8,7 @@
 
 open import Relation.Binary.Bundles using (Setoid)
 
-module Algebra.Action.Construct.Free
+module Algebra.Action.Construct.FreeMonoid
   {a c r ℓ} (M : Setoid c ℓ) (S : Setoid a r)
   where
 
@@ -63,27 +63,27 @@ module FreeMonoidAction where
 
   module _ (left : SetoidAction.Left M S) where
 
-    private listAction = leftListAction left
+    private listAction = ListAction.leftAction left
 
     open SetoidAction.Left left
     open IsLeftAction isLeftAction
 
     leftAction : Left monoid S listAction
     leftAction = record
-      { ∙-act = λ ms ns x → ⋆-act-cong ms ≋-refl A.refl
+      { ▷-act = λ ms _ _ → ▷⋆-act-cong ms ≋-refl A.refl
       ; ε-act = λ _ → A.refl
       }
 
   module _ (right : SetoidAction.Right M S) where
 
-    private listAction = rightListAction right
+    private listAction = ListAction.rightAction right
 
     open SetoidAction.Right right
     open IsRightAction isRightAction
 
     rightAction : Right monoid S listAction
     rightAction = record
-      { ∙-act = λ x ms ns → ⋆-act-cong A.refl ms ≋-refl
+      { ◁-act = λ _ ms _ → ◁⋆-act-cong A.refl ms ≋-refl
       ; ε-act = λ _ → A.refl
       }
 

From 04c535d52c1797cbb7200001069c338130738013 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 25 Apr 2024 11:58:06 +0100
Subject: [PATCH 28/39] fix-up

---
 CHANGELOG.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index a569e62b61..105fc3de96 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -62,9 +62,9 @@ New modules
   Algebra.Action.Bundles
   ```
 
-* The free `List` actions over a `SetoidAction`:
+* The free `Monoid` actions over a `SetoidAction`:
   ```
-  Algebra.Action.Construct.Free
+  Algebra.Action.Construct.FreeMonoid
   ```
 
 * The left- and right- regular actions (of a `Monoid`) over itself:

From 305173d8533731406c586b86c7e4e24c7902a185 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 29 Apr 2024 13:43:07 +0100
Subject: [PATCH 29/39] tidied up `FreeMonoid`

---
 src/Algebra/Action/Construct/FreeMonoid.agda | 75 ++++++++++----------
 1 file changed, 36 insertions(+), 39 deletions(-)

diff --git a/src/Algebra/Action/Construct/FreeMonoid.agda b/src/Algebra/Action/Construct/FreeMonoid.agda
index 9fd58e8e7c..99b60d9158 100644
--- a/src/Algebra/Action/Construct/FreeMonoid.agda
+++ b/src/Algebra/Action/Construct/FreeMonoid.agda
@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- The free MonoidAction on a SetoidAction
+-- The free MonoidAction on a SetoidAction, arising from ListAction
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
@@ -26,64 +26,61 @@ open import Function.Base using (_∘_)
 
 open import Level using (Level; _⊔_)
 
-------------------------------------------------------------------------
--- Monoid: the Free action arises from List
-
-module FreeMonoidAction where
+open ≋ M using (_≋_; ≋-refl; ≋-reflexive; ≋-isEquivalence; ++⁺)
 
-  open ≋ M using (_≋_; ≋-refl; ≋-reflexive; ≋-isEquivalence; ++⁺)
-  open MonoidAction
 
 ------------------------------------------------------------------------
 -- First: define the Monoid structure on List M.Carrier
 
-  private
+private
 
-    module M = Setoid M
-    module A = Setoid S
+  module M = Setoid M
+  module A = Setoid S
 
-    isMonoid : IsMonoid _≋_ _++_ []
-    isMonoid = record
-      { isSemigroup = record
-        { isMagma = record
-          { isEquivalence = ≋-isEquivalence
-          ; ∙-cong = ++⁺
-          }
-        ; assoc = λ xs ys zs → ≋-reflexive (List.++-assoc xs ys zs)
+  isMonoid : IsMonoid _≋_ _++_ []
+  isMonoid = record
+    { isSemigroup = record
+      { isMagma = record
+        { isEquivalence = ≋-isEquivalence
+        ; ∙-cong = ++⁺
         }
-      ; identity = (λ _ → ≋-refl) , ≋-reflexive ∘ List.++-identityʳ
+      ; assoc = λ xs ys zs → ≋-reflexive (List.++-assoc xs ys zs)
       }
+    ; identity = (λ _ → ≋-refl) , ≋-reflexive ∘ List.++-identityʳ
+    }
 
-    monoid : Monoid c (c ⊔ ℓ)
-    monoid = record { isMonoid = isMonoid }
+  monoid : Monoid c (c ⊔ ℓ)
+  monoid = record { isMonoid = isMonoid }
 
 
 ------------------------------------------------------------------------
 -- Second: define the actions of that Monoid
 
-  module _ (left : SetoidAction.Left M S) where
+open MonoidAction monoid S
 
-    private listAction = ListAction.leftAction left
+module _ (left : SetoidAction.Left M S) where
 
-    open SetoidAction.Left left
-    open IsLeftAction isLeftAction
+  private listAction = ListAction.leftAction left
 
-    leftAction : Left monoid S listAction
-    leftAction = record
-      { ▷-act = λ ms _ _ → ▷⋆-act-cong ms ≋-refl A.refl
-      ; ε-act = λ _ → A.refl
-      }
+  open SetoidAction.Left left
+  open IsLeftAction isLeftAction
 
-  module _ (right : SetoidAction.Right M S) where
+  leftAction : Left listAction
+  leftAction = record
+    { ▷-act = λ ms _ _ → ▷⋆-act-cong ms ≋-refl A.refl
+    ; ε-act = λ _ → A.refl
+    }
 
-    private listAction = ListAction.rightAction right
+module _ (right : SetoidAction.Right M S) where
 
-    open SetoidAction.Right right
-    open IsRightAction isRightAction
+  private listAction = ListAction.rightAction right
 
-    rightAction : Right monoid S listAction
-    rightAction = record
-      { ◁-act = λ _ ms _ → ◁⋆-act-cong A.refl ms ≋-refl
-      ; ε-act = λ _ → A.refl
-      }
+  open SetoidAction.Right right
+  open IsRightAction isRightAction
+
+  rightAction : Right listAction
+  rightAction = record
+    { ◁-act = λ _ ms _ → ◁⋆-act-cong A.refl ms ≋-refl
+    ; ε-act = λ _ → A.refl
+    }
 

From 5702c462c6e990a6227cb57ebd3f6da30bbfa464 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 29 Apr 2024 18:27:56 +0100
Subject: [PATCH 30/39] `open` API more eagerly

---
 src/Algebra/Action/Bundles.agda              | 32 ++++++++++----------
 src/Algebra/Action/Construct/FreeMonoid.agda |  2 --
 2 files changed, 16 insertions(+), 18 deletions(-)

diff --git a/src/Algebra/Action/Bundles.agda b/src/Algebra/Action/Bundles.agda
index d045196806..57b9875545 100644
--- a/src/Algebra/Action/Bundles.agda
+++ b/src/Algebra/Action/Bundles.agda
@@ -33,52 +33,56 @@ private
 
 
 ------------------------------------------------------------------------
--- Basic definition: a Setoid action yields underlying raw action
+-- Basic definition: a Setoid action yields underlying action structure
 
-module SetoidAction (M : Setoid c ℓ) (A : Setoid a r) where
+module SetoidAction (S : Setoid c ℓ) (A : Setoid a r) where
 
   private
 
-    module M = Setoid M
+    module S = Setoid S
     module A = Setoid A
 
   record Left : Set (a ⊔ r ⊔ c ⊔ ℓ) where
 
     field
-      isLeftAction : IsLeftAction M._≈_ A._≈_
+      isLeftAction : IsLeftAction S._≈_ A._≈_
+
+    open IsLeftAction isLeftAction public
 
   record Right : Set (a ⊔ r ⊔ c ⊔ ℓ) where
 
     field
-      isRightAction : IsRightAction M._≈_ A._≈_
+      isRightAction : IsRightAction S._≈_ A._≈_
+
+    open IsRightAction isRightAction public
 
 
 ------------------------------------------------------------------------
 -- A Setoid action yields an iterated List action
 
-module ListAction {M : Setoid c ℓ} {A : Setoid a r} where
+module ListAction {S : Setoid c ℓ} {A : Setoid a r} where
 
   open SetoidAction
 
-  open ≋ M using (≋-setoid)
+  open ≋ S using (≋-setoid)
 
-  leftAction : (left : Left M A) → Left ≋-setoid A
+  leftAction : (left : Left S A) → Left ≋-setoid A
   leftAction left = record
     { isLeftAction = record
       { _▷_ = _▷⋆_
       ; ▷-cong = ▷⋆-cong
       }
     }
-    where open Left left; open IsLeftAction isLeftAction
+    where open Left left
 
-  rightAction : (right : Right M A) → Right ≋-setoid A
+  rightAction : (right : Right S A) → Right ≋-setoid A
   rightAction right = record
     { isRightAction = record
       { _◁_ = _◁⋆_
       ; ◁-cong = ◁⋆-cong
       }
     }
-    where open Right right; open IsRightAction isRightAction
+    where open Right right
 
 
 ------------------------------------------------------------------------
@@ -96,8 +100,6 @@ module MonoidAction (M : Monoid c ℓ) (A : Setoid a r) where
     where
 
     open SetoidAction.Left leftAction public
-      using (isLeftAction)
-    open IsLeftAction isLeftAction public
 
     field
       ▷-act  : ∀ m n x → m ∙ n ▷ x ≈ m ▷ n ▷ x
@@ -119,9 +121,7 @@ module MonoidAction (M : Monoid c ℓ) (A : Setoid a r) where
     where
 
     open SetoidAction.Right rightAction public
-      using (isRightAction)
-    open IsRightAction isRightAction public
-
+ 
     field
       ◁-act  : ∀ x m n → x ◁ m ∙ n ≈ x ◁ m ◁ n
       ε-act  : ∀ x → x ◁ ε ≈ x
diff --git a/src/Algebra/Action/Construct/FreeMonoid.agda b/src/Algebra/Action/Construct/FreeMonoid.agda
index 99b60d9158..f148999b7b 100644
--- a/src/Algebra/Action/Construct/FreeMonoid.agda
+++ b/src/Algebra/Action/Construct/FreeMonoid.agda
@@ -63,7 +63,6 @@ module _ (left : SetoidAction.Left M S) where
   private listAction = ListAction.leftAction left
 
   open SetoidAction.Left left
-  open IsLeftAction isLeftAction
 
   leftAction : Left listAction
   leftAction = record
@@ -76,7 +75,6 @@ module _ (right : SetoidAction.Right M S) where
   private listAction = ListAction.rightAction right
 
   open SetoidAction.Right right
-  open IsRightAction isRightAction
 
   rightAction : Right listAction
   rightAction = record

From f1f73bf7154ad806b504168f09f41a809af40e0f Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 29 Apr 2024 18:32:01 +0100
Subject: [PATCH 31/39] `fix-whitespace`

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

diff --git a/src/Algebra/Action/Bundles.agda b/src/Algebra/Action/Bundles.agda
index 57b9875545..7c1422d553 100644
--- a/src/Algebra/Action/Bundles.agda
+++ b/src/Algebra/Action/Bundles.agda
@@ -121,7 +121,7 @@ module MonoidAction (M : Monoid c ℓ) (A : Setoid a r) where
     where
 
     open SetoidAction.Right rightAction public
- 
+
     field
       ◁-act  : ∀ x m n → x ◁ m ∙ n ≈ x ◁ m ◁ n
       ε-act  : ∀ x → x ◁ ε ≈ x

From 7df8e8cf9447e7fb1c870b314b164deb0f4a51c0 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Wed, 1 May 2024 13:49:48 +0100
Subject: [PATCH 32/39] things in their right places, now

---
 src/Algebra/Action/Bundles.agda | 52 ++++++++++++++++-----------------
 1 file changed, 26 insertions(+), 26 deletions(-)

diff --git a/src/Algebra/Action/Bundles.agda b/src/Algebra/Action/Bundles.agda
index 7c1422d553..9d749e4eca 100644
--- a/src/Algebra/Action/Bundles.agda
+++ b/src/Algebra/Action/Bundles.agda
@@ -42,6 +42,8 @@ module SetoidAction (S : Setoid c ℓ) (A : Setoid a r) where
     module S = Setoid S
     module A = Setoid A
 
+    open ≋ S using (≋-refl)
+
   record Left : Set (a ⊔ r ⊔ c ⊔ ℓ) where
 
     field
@@ -49,6 +51,18 @@ module SetoidAction (S : Setoid c ℓ) (A : Setoid a r) where
 
     open IsLeftAction isLeftAction public
 
+    ▷-congˡ : ∀ {m x y} → x A.≈ y → m ▷ x A.≈ m ▷ y
+    ▷-congˡ x≈y = ▷-cong S.refl x≈y
+
+    ▷-congʳ : ∀ {m n x} → m S.≈ n → m ▷ x A.≈ n ▷ x
+    ▷-congʳ m≈n = ▷-cong m≈n A.refl
+
+    []-act : ∀ x → [] ▷⋆ x A.≈ x
+    []-act _ = []-act-cong A.refl
+
+    ▷⋆-act : ∀ ms ns x → (ms ++ ns) ▷⋆ x A.≈ ms ▷⋆ ns ▷⋆ x
+    ▷⋆-act ms ns x = ▷⋆-act-cong ms ≋-refl A.refl
+
   record Right : Set (a ⊔ r ⊔ c ⊔ ℓ) where
 
     field
@@ -56,6 +70,18 @@ module SetoidAction (S : Setoid c ℓ) (A : Setoid a r) where
 
     open IsRightAction isRightAction public
 
+    ◁-congˡ : ∀ {x y m} → x A.≈ y → x ◁ m A.≈ y ◁ m
+    ◁-congˡ x≈y = ◁-cong x≈y S.refl
+
+    ◁-congʳ : ∀ {m n x} → m S.≈ n → x ◁ m A.≈ x ◁ n
+    ◁-congʳ m≈n = ◁-cong A.refl m≈n
+
+    ◁⋆-act : ∀ x ms ns → x ◁⋆ (ms ++ ns) A.≈ x ◁⋆ ms ◁⋆ ns
+    ◁⋆-act x ms ns = ◁⋆-act-cong A.refl ms ≋-refl
+
+    []-act : ∀ x → x ◁⋆ [] A.≈ x
+    []-act x = []-act-cong A.refl
+
 
 ------------------------------------------------------------------------
 -- A Setoid action yields an iterated List action
@@ -94,7 +120,6 @@ module MonoidAction (M : Monoid c ℓ) (A : Setoid a r) where
 
     open module M = Monoid M using (ε; _∙_; setoid)
     open module A = Setoid A using (_≈_)
-    open ≋ setoid using (≋-refl)
 
   record Left (leftAction : SetoidAction.Left setoid A) : Set (a ⊔ r ⊔ c ⊔ ℓ)
     where
@@ -105,18 +130,6 @@ module MonoidAction (M : Monoid c ℓ) (A : Setoid a r) where
       ▷-act  : ∀ m n x → m ∙ n ▷ x ≈ m ▷ n ▷ x
       ε-act  : ∀ x → ε ▷ x ≈ x
 
-    ▷-congˡ : ∀ {m x y} → x ≈ y → m ▷ x ≈ m ▷ y
-    ▷-congˡ x≈y = ▷-cong M.refl x≈y
-
-    ▷-congʳ : ∀ {m n x} → m M.≈ n → m ▷ x ≈ n ▷ x
-    ▷-congʳ m≈n = ▷-cong m≈n A.refl
-
-    ▷⋆-act : ∀ ms ns x → (ms ++ ns) ▷⋆ x ≈ ms ▷⋆ ns ▷⋆ x
-    ▷⋆-act ms ns x = ▷⋆-act-cong ms ≋-refl A.refl
-
-    []-act : ∀ x → [] ▷⋆ x ≈ x
-    []-act _ = []-act-cong A.refl
-
   record Right (rightAction : SetoidAction.Right setoid A) : Set (a ⊔ r ⊔ c ⊔ ℓ)
     where
 
@@ -125,16 +138,3 @@ module MonoidAction (M : Monoid c ℓ) (A : Setoid a r) where
     field
       ◁-act  : ∀ x m n → x ◁ m ∙ n ≈ x ◁ m ◁ n
       ε-act  : ∀ x → x ◁ ε ≈ x
-
-    ◁-congˡ : ∀ {x y m} → x ≈ y → x ◁ m ≈ y ◁ m
-    ◁-congˡ x≈y = ◁-cong x≈y M.refl
-
-    ◁-congʳ : ∀ {m n x} → m M.≈ n → x ◁ m ≈ x ◁ n
-    ◁-congʳ m≈n = ◁-cong A.refl m≈n
-
-    ◁⋆-act : ∀ x ms ns → x ◁⋆ (ms ++ ns) ≈ x ◁⋆ ms ◁⋆ ns
-    ◁⋆-act x ms ns = ◁⋆-act-cong A.refl ms ≋-refl
-
-    []-act : ∀ x → x ◁⋆ [] ≈ x
-    []-act x = []-act-cong A.refl
-

From 753e216f19e59474b0885fbb0ba0a3db42cd2c04 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Wed, 1 May 2024 14:11:50 +0100
Subject: [PATCH 33/39] rethink notation

---
 src/Algebra/Action/Bundles.agda              | 12 ++++++------
 src/Algebra/Action/Construct/FreeMonoid.agda |  8 ++++----
 src/Algebra/Action/Structures.agda           | 15 ++++++++-------
 3 files changed, 18 insertions(+), 17 deletions(-)

diff --git a/src/Algebra/Action/Bundles.agda b/src/Algebra/Action/Bundles.agda
index 9d749e4eca..74a36c55a2 100644
--- a/src/Algebra/Action/Bundles.agda
+++ b/src/Algebra/Action/Bundles.agda
@@ -60,8 +60,8 @@ module SetoidAction (S : Setoid c ℓ) (A : Setoid a r) where
     []-act : ∀ x → [] ▷⋆ x A.≈ x
     []-act _ = []-act-cong A.refl
 
-    ▷⋆-act : ∀ ms ns x → (ms ++ ns) ▷⋆ x A.≈ ms ▷⋆ ns ▷⋆ x
-    ▷⋆-act ms ns x = ▷⋆-act-cong ms ≋-refl A.refl
+    ++-act : ∀ ms ns x → (ms ++ ns) ▷⋆ x A.≈ ms ▷⋆ ns ▷⋆ x
+    ++-act ms ns x = ++-act-cong ms ≋-refl A.refl
 
   record Right : Set (a ⊔ r ⊔ c ⊔ ℓ) where
 
@@ -76,8 +76,8 @@ module SetoidAction (S : Setoid c ℓ) (A : Setoid a r) where
     ◁-congʳ : ∀ {m n x} → m S.≈ n → x ◁ m A.≈ x ◁ n
     ◁-congʳ m≈n = ◁-cong A.refl m≈n
 
-    ◁⋆-act : ∀ x ms ns → x ◁⋆ (ms ++ ns) A.≈ x ◁⋆ ms ◁⋆ ns
-    ◁⋆-act x ms ns = ◁⋆-act-cong A.refl ms ≋-refl
+    ++-act : ∀ x ms ns → x ◁⋆ (ms ++ ns) A.≈ x ◁⋆ ms ◁⋆ ns
+    ++-act x ms ns = ++-act-cong A.refl ms ≋-refl
 
     []-act : ∀ x → x ◁⋆ [] A.≈ x
     []-act x = []-act-cong A.refl
@@ -127,7 +127,7 @@ module MonoidAction (M : Monoid c ℓ) (A : Setoid a r) where
     open SetoidAction.Left leftAction public
 
     field
-      ▷-act  : ∀ m n x → m ∙ n ▷ x ≈ m ▷ n ▷ x
+      ∙-act  : ∀ m n x → m ∙ n ▷ x ≈ m ▷ n ▷ x
       ε-act  : ∀ x → ε ▷ x ≈ x
 
   record Right (rightAction : SetoidAction.Right setoid A) : Set (a ⊔ r ⊔ c ⊔ ℓ)
@@ -136,5 +136,5 @@ module MonoidAction (M : Monoid c ℓ) (A : Setoid a r) where
     open SetoidAction.Right rightAction public
 
     field
-      ◁-act  : ∀ x m n → x ◁ m ∙ n ≈ x ◁ m ◁ n
+      ∙-act  : ∀ x m n → x ◁ m ∙ n ≈ x ◁ m ◁ n
       ε-act  : ∀ x → x ◁ ε ≈ x
diff --git a/src/Algebra/Action/Construct/FreeMonoid.agda b/src/Algebra/Action/Construct/FreeMonoid.agda
index f148999b7b..245f7732fb 100644
--- a/src/Algebra/Action/Construct/FreeMonoid.agda
+++ b/src/Algebra/Action/Construct/FreeMonoid.agda
@@ -66,8 +66,8 @@ module _ (left : SetoidAction.Left M S) where
 
   leftAction : Left listAction
   leftAction = record
-    { ▷-act = λ ms _ _ → ▷⋆-act-cong ms ≋-refl A.refl
-    ; ε-act = λ _ → A.refl
+    { ∙-act = ++-act
+    ; ε-act = []-act
     }
 
 module _ (right : SetoidAction.Right M S) where
@@ -78,7 +78,7 @@ module _ (right : SetoidAction.Right M S) where
 
   rightAction : Right listAction
   rightAction = record
-    { ◁-act = λ _ ms _ → ◁⋆-act-cong A.refl ms ≋-refl
-    ; ε-act = λ _ → A.refl
+    { ∙-act = ++-act
+    ; ε-act = []-act
     }
 
diff --git a/src/Algebra/Action/Structures.agda b/src/Algebra/Action/Structures.agda
index 6e87c2168d..ad7a074ae6 100644
--- a/src/Algebra/Action/Structures.agda
+++ b/src/Algebra/Action/Structures.agda
@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Raw Actions of one (pre-)Setoid on another
+-- Structure of the Action of one (pre-)Setoid on another
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
@@ -27,6 +27,7 @@ private
     m n p : M
     ms ns ps : List M
 
+
 ------------------------------------------------------------------------
 -- Basic definitions: fix notation
 
@@ -52,10 +53,10 @@ record IsLeftAction : Set (a ⊔ r ⊔ c ⊔ ℓ) where
   ▷⁺-cong : m ≈ᴹ n → Pointwise _≈ᴹ_ ms ns → x ≈ y → ((m ∷ ms) ▷⁺ x) ≈ ((n ∷ ns) ▷⁺ y)
   ▷⁺-cong m≈n ms≋ns x≈y = ▷-cong m≈n (▷⋆-cong ms≋ns x≈y)
 
-  ▷⋆-act-cong : ∀ ms → Pointwise _≈ᴹ_ ps (ms ++ ns) →
+  ++-act-cong : ∀ ms → Pointwise _≈ᴹ_ ps (ms ++ ns) →
                 x ≈ y → (ps ▷⋆ x) ≈ (ms ▷⋆ ns ▷⋆ y)
-  ▷⋆-act-cong []       ps≋ns             x≈y = ▷⋆-cong ps≋ns x≈y
-  ▷⋆-act-cong (m ∷ ms) (p≈m ∷ ps≋ms++ns) x≈y = ▷-cong p≈m (▷⋆-act-cong ms ps≋ms++ns x≈y)
+  ++-act-cong []       ps≋ns             x≈y = ▷⋆-cong ps≋ns x≈y
+  ++-act-cong (m ∷ ms) (p≈m ∷ ps≋ms++ns) x≈y = ▷-cong p≈m (++-act-cong ms ps≋ms++ns x≈y)
 
   []-act-cong : x ≈ y → ([] ▷⋆ x) ≈ y
   []-act-cong = id
@@ -82,10 +83,10 @@ record IsRightAction : Set (a ⊔ r ⊔ c ⊔ ℓ) where
   ◁⁺-cong : x ≈ y → m ≈ᴹ n → Pointwise _≈ᴹ_ ms ns → (x ◁⁺ (m ∷ ms)) ≈ (y ◁⁺ (n ∷ ns))
   ◁⁺-cong x≈y m≈n ms≋ns = ◁⋆-cong (◁-cong x≈y m≈n) (ms≋ns)
 
-  ◁⋆-act-cong : x ≈ y → ∀ ms → Pointwise _≈ᴹ_ ps (ms ++ ns) →
+  ++-act-cong : x ≈ y → ∀ ms → Pointwise _≈ᴹ_ ps (ms ++ ns) →
                (x ◁⋆ ps) ≈ (y ◁⋆ ms ◁⋆ ns)
-  ◁⋆-act-cong x≈y []       ps≋ns             = ◁⋆-cong x≈y ps≋ns
-  ◁⋆-act-cong x≈y (m ∷ ms) (p≈m ∷ ps≋ms++ns) = ◁⋆-act-cong (◁-cong x≈y p≈m) ms ps≋ms++ns
+  ++-act-cong x≈y []       ps≋ns             = ◁⋆-cong x≈y ps≋ns
+  ++-act-cong x≈y (m ∷ ms) (p≈m ∷ ps≋ms++ns) = ++-act-cong (◁-cong x≈y p≈m) ms ps≋ms++ns
 
   []-act-cong : x ≈ y → (x ◁⋆ []) ≈ y
   []-act-cong = id

From 7570960c1cc92ba5e632048aca13439c94df4068 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Wed, 1 May 2024 14:16:50 +0100
Subject: [PATCH 34/39] knock-on

---
 src/Algebra/Action/Construct/Self.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Algebra/Action/Construct/Self.agda b/src/Algebra/Action/Construct/Self.agda
index 4e19747cf2..adecc31910 100644
--- a/src/Algebra/Action/Construct/Self.agda
+++ b/src/Algebra/Action/Construct/Self.agda
@@ -28,13 +28,13 @@ module Regular {c ℓ} (M : Monoid c ℓ) where
 
   leftAction : Left record { isLeftAction = isLeftAction }
   leftAction = record
-    { ▷-act = assoc
+    { ∙-act = assoc
     ; ε-act = identityˡ
     }
 
   rightAction : Right record { isRightAction = isRightAction }
   rightAction = record
-    { ◁-act = λ x m n → sym (assoc x m n)
+    { ∙-act = λ x m n → sym (assoc x m n)
     ; ε-act = identityʳ
     }
 

From 3981c4cf234b7d6fba806bd18c6076f2f6555e58 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Wed, 1 May 2024 15:41:01 +0100
Subject: [PATCH 35/39] tightened up dependencies

---
 src/Algebra/Action/Construct/FreeMonoid.agda | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/Algebra/Action/Construct/FreeMonoid.agda b/src/Algebra/Action/Construct/FreeMonoid.agda
index 245f7732fb..173cf18956 100644
--- a/src/Algebra/Action/Construct/FreeMonoid.agda
+++ b/src/Algebra/Action/Construct/FreeMonoid.agda
@@ -26,16 +26,14 @@ open import Function.Base using (_∘_)
 
 open import Level using (Level; _⊔_)
 
-open ≋ M using (_≋_; ≋-refl; ≋-reflexive; ≋-isEquivalence; ++⁺)
-
 
 ------------------------------------------------------------------------
 -- First: define the Monoid structure on List M.Carrier
+-- NB should be defined somewhere under `Data.List`!?
 
 private
 
-  module M = Setoid M
-  module A = Setoid S
+  open ≋ M using (_≋_; ≋-refl; ≋-reflexive; ≋-isEquivalence; ++⁺)
 
   isMonoid : IsMonoid _≋_ _++_ []
   isMonoid = record

From 2e292e77e66c3967206086d5a6c681a437039188 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 3 May 2024 07:15:28 +0100
Subject: [PATCH 36/39] inline uses of `ListAction`

---
 src/Algebra/Action/Construct/FreeMonoid.agda | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

diff --git a/src/Algebra/Action/Construct/FreeMonoid.agda b/src/Algebra/Action/Construct/FreeMonoid.agda
index 173cf18956..91e9fc3d7d 100644
--- a/src/Algebra/Action/Construct/FreeMonoid.agda
+++ b/src/Algebra/Action/Construct/FreeMonoid.agda
@@ -58,11 +58,9 @@ open MonoidAction monoid S
 
 module _ (left : SetoidAction.Left M S) where
 
-  private listAction = ListAction.leftAction left
-
   open SetoidAction.Left left
 
-  leftAction : Left listAction
+  leftAction : Left (ListAction.leftAction left)
   leftAction = record
     { ∙-act = ++-act
     ; ε-act = []-act
@@ -70,11 +68,9 @@ module _ (left : SetoidAction.Left M S) where
 
 module _ (right : SetoidAction.Right M S) where
 
-  private listAction = ListAction.rightAction right
-
   open SetoidAction.Right right
 
-  rightAction : Right listAction
+  rightAction : Right (ListAction.rightAction right)
   rightAction = record
     { ∙-act = ++-act
     ; ε-act = []-act

From 9b775da7a55464ba0079514c7b4a05f6f9ba6855 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Wed, 8 May 2024 12:31:44 +0100
Subject: [PATCH 37/39] refactored to streamline `FreeMonoid`'s use of iterated
 `List` actions

---
 src/Algebra/Action/Bundles.agda              | 32 +-----------
 src/Algebra/Action/Construct/FreeMonoid.agda | 54 ++++++++++++++------
 2 files changed, 40 insertions(+), 46 deletions(-)

diff --git a/src/Algebra/Action/Bundles.agda b/src/Algebra/Action/Bundles.agda
index 74a36c55a2..ca02f2e86d 100644
--- a/src/Algebra/Action/Bundles.agda
+++ b/src/Algebra/Action/Bundles.agda
@@ -20,11 +20,9 @@ module Algebra.Action.Bundles where
 
 open import Algebra.Action.Structures using (IsLeftAction; IsRightAction)
 open import Algebra.Bundles using (Monoid)
-
+open import Level using (Level; _⊔_)
 open import Data.List.Base using ([]; _++_)
 import Data.List.Relation.Binary.Equality.Setoid as ≋
-open import Level using (Level; _⊔_)
-
 open import Relation.Binary.Bundles using (Setoid)
 
 private
@@ -83,34 +81,6 @@ module SetoidAction (S : Setoid c ℓ) (A : Setoid a r) where
     []-act x = []-act-cong A.refl
 
 
-------------------------------------------------------------------------
--- A Setoid action yields an iterated List action
-
-module ListAction {S : Setoid c ℓ} {A : Setoid a r} where
-
-  open SetoidAction
-
-  open ≋ S using (≋-setoid)
-
-  leftAction : (left : Left S A) → Left ≋-setoid A
-  leftAction left = record
-    { isLeftAction = record
-      { _▷_ = _▷⋆_
-      ; ▷-cong = ▷⋆-cong
-      }
-    }
-    where open Left left
-
-  rightAction : (right : Right S A) → Right ≋-setoid A
-  rightAction right = record
-    { isRightAction = record
-      { _◁_ = _◁⋆_
-      ; ◁-cong = ◁⋆-cong
-      }
-    }
-    where open Right right
-
-
 ------------------------------------------------------------------------
 -- Definition: indexed over an underlying SetoidAction
 
diff --git a/src/Algebra/Action/Construct/FreeMonoid.agda b/src/Algebra/Action/Construct/FreeMonoid.agda
index 91e9fc3d7d..eb36f28e0b 100644
--- a/src/Algebra/Action/Construct/FreeMonoid.agda
+++ b/src/Algebra/Action/Construct/FreeMonoid.agda
@@ -9,7 +9,7 @@
 open import Relation.Binary.Bundles using (Setoid)
 
 module Algebra.Action.Construct.FreeMonoid
-  {a c r ℓ} (M : Setoid c ℓ) (S : Setoid a r)
+  {a c r ℓ} (S : Setoid c ℓ) (A : Setoid a r)
   where
 
 open import Algebra.Action.Bundles
@@ -28,12 +28,12 @@ open import Level using (Level; _⊔_)
 
 
 ------------------------------------------------------------------------
--- First: define the Monoid structure on List M.Carrier
+-- Temporary: define the Monoid structure on List S.Carrier
 -- NB should be defined somewhere under `Data.List`!?
 
 private
 
-  open ≋ M using (_≋_; ≋-refl; ≋-reflexive; ≋-isEquivalence; ++⁺)
+  open ≋ S using (_≋_; ≋-refl; ≋-reflexive; ≋-isEquivalence; ++⁺)
 
   isMonoid : IsMonoid _≋_ _++_ []
   isMonoid = record
@@ -52,27 +52,51 @@ private
 
 
 ------------------------------------------------------------------------
--- Second: define the actions of that Monoid
+-- A Setoid action yields an iterated ListS action, which is
+-- the underlying SetoidAction of the FreeMonoid construction
 
-open MonoidAction monoid S
+module SetoidActions where
 
-module _ (left : SetoidAction.Left M S) where
+  open SetoidAction
+  open ≋ S renaming (≋-setoid to ListS)
 
-  open SetoidAction.Left left
+  leftAction : (left : Left S A) → Left ListS A
+  leftAction left = record
+    { isLeftAction = record
+      { _▷_ = _▷⋆_
+      ; ▷-cong = ▷⋆-cong
+      }
+    }
+    where open Left left
 
-  leftAction : Left (ListAction.leftAction left)
-  leftAction = record
-    { ∙-act = ++-act
-    ; ε-act = []-act
+  rightAction : (right : Right S A) → Right ListS A
+  rightAction right = record
+    { isRightAction = record
+      { _◁_ = _◁⋆_
+      ; ◁-cong = ◁⋆-cong
+      }
     }
+    where open Right right
+
 
-module _ (right : SetoidAction.Right M S) where
+------------------------------------------------------------------------
+-- Now: define the MonoidActions of the (Monoid based on) ListS on A
+
+module MonoidActions where
+
+  open MonoidAction monoid A
 
-  open SetoidAction.Right right
+  leftAction : (left : SetoidAction.Left S A) → Left (SetoidActions.leftAction left)
+  leftAction left = record
+    { ∙-act = ++-act
+    ; ε-act = []-act
+    }
+    where open SetoidAction.Left left
 
-  rightAction : Right (ListAction.rightAction right)
-  rightAction = record
+  rightAction : (right : SetoidAction.Right S A) → Right (SetoidActions.rightAction right)
+  rightAction right = record
     { ∙-act = ++-act
     ; ε-act = []-act
     }
+    where open SetoidAction.Right right
 

From c599ae3e5359822f1a656e4598c4205277bae5c9 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 18 Jan 2025 09:33:44 +0000
Subject: [PATCH 38/39] `CHANGELOG`: reset

---
 CHANGELOG.md | 409 +--------------------------------------------------
 1 file changed, 4 insertions(+), 405 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 105fc3de96..edb7c3e57f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,7 +1,7 @@
-Version 2.1-dev
+Version 2.3-dev
 ===============
 
-The library has been tested using Agda 2.6.4, 2.6.4.1, and 2.6.4.3.
+The library has been tested using Agda 2.7.0 and 2.7.0.1.
 
 Highlights
 ----------
@@ -9,421 +9,20 @@ Highlights
 Bug-fixes
 ---------
 
-* Fix statement of `Data.Vec.Properties.toList-replicate`, where `replicate`
-  was mistakenly applied to the level of the type `A` instead of the
-  variable `x` of type `A`.
-
-* Module `Data.List.Relation.Ternary.Appending.Setoid.Properties` no longer
-  exports the `Setoid` module under the alias `S`.
-
 Non-backwards compatible changes
 --------------------------------
 
-* The modules and morphisms in `Algebra.Module.Morphism.Structures` are now
-  parametrized by _raw_ bundles rather than lawful bundles, in line with other
-  modules defining morphism structures.
-* The definitions in `Algebra.Module.Morphism.Construct.Composition` are now
-  parametrized by _raw_ bundles, and as such take a proof of transitivity.
-* The definitions in `Algebra.Module.Morphism.Construct.Identity` are now
-  parametrized by _raw_ bundles, and as such take a proof of reflexivity.
-
-Other major improvements
-------------------------
+Minor improvements
+------------------
 
 Deprecated modules
 ------------------
 
-* `Data.List.Relation.Binary.Sublist.Propositional.Disjoint` deprecated in favour of
-  `Data.List.Relation.Binary.Sublist.Propositional.Slice`.
-
 Deprecated names
 ----------------
 
-* In `Algebra.Properties.Semiring.Mult`:
-  ```agda
-  1×-identityʳ  ↦  ×-homo-1
-  ```
-
-* In `Algebra.Structures.IsGroup`:
-  ```agda
-  _-_  ↦  _//_
-  ```
-
-* In `Data.Nat.Divisibility.Core`:
-  ```agda
-  *-pres-∣  ↦  Data.Nat.Divisibility.*-pres-∣
-  ```
-
 New modules
 -----------
 
-* Bundles for left- and right- actions:
-  ```
-  Algebra.Action.Bundles
-  ```
-
-* The free `Monoid` actions over a `SetoidAction`:
-  ```
-  Algebra.Action.Construct.FreeMonoid
-  ```
-
-* The left- and right- regular actions (of a `Monoid`) over itself:
-  ```
-  Algebra.Action.Construct.Self
-  ```
-
-* Structures for left- and right- actions:
-  ```
-  Algebra.Action.Structures
-  ```
-
-* Raw bundles for module-like algebraic structures:
-  ```
-  Algebra.Module.Bundles.Raw
-  ```
-
-* Prime factorisation of natural numbers.
-  ```
-  Data.Nat.Primality.Factorisation
-  ```
-
-* Consequences of 'infinite descent' for (accessible elements of) well-founded relations:
-  ```agda
-  Induction.InfiniteDescent
-  ```
-
-* The unique morphism from the initial, resp. terminal, algebra:
-  ```agda
-  Algebra.Morphism.Construct.Initial
-  Algebra.Morphism.Construct.Terminal
-  ```
-
-* Nagata's construction of the "idealization of a module":
-  ```agda
-  Algebra.Module.Construct.Idealization
-  ```
-
-* `Data.List.Relation.Binary.Sublist.Propositional.Slice`
-  replacing `Data.List.Relation.Binary.Sublist.Propositional.Disjoint` (*)
-  and adding new functions:
-  - `⊆-upper-bound-is-cospan` generalising `⊆-disjoint-union-is-cospan` from (*)
-  - `⊆-upper-bound-cospan` generalising `⊆-disjoint-union-cospan` from (*)
-
-* `Data.Vec.Functional.Relation.Binary.Permutation`, defining:
-  ```agda
-  _↭_ : IRel (Vector A) _
-  ```
-
-* `Data.Vec.Functional.Relation.Binary.Permutation.Properties` of the above:
-  ```agda
-  ↭-refl      : Reflexive (Vector A) _↭_
-  ↭-reflexive : xs ≡ ys → xs ↭ ys
-  ↭-sym       : Symmetric (Vector A) _↭_
-  ↭-trans     : Transitive (Vector A) _↭_
-  isIndexedEquivalence : {A : Set a} → IsIndexedEquivalence (Vector A) _↭_
-  indexedSetoid        : {A : Set a} → IndexedSetoid ℕ a _
-  ```
-
-* `Function.Relation.Binary.Equality`
-  ```agda
-  setoid : Setoid a₁ a₂ → Setoid b₁ b₂ → Setoid _ _
-  ```
-  and a convenient infix version
-  ```agda
-  _⇨_ = setoid
-  ```
-
-* Symmetric interior of a binary relation
-  ```
-  Relation.Binary.Construct.Interior.Symmetric
-  ```
-
-* Pointwise and equality relations over indexed containers:
-  ```agda
-  Data.Container.Indexed.Relation.Binary.Pointwise
-  Data.Container.Indexed.Relation.Binary.Pointwise.Properties
-  Data.Container.Indexed.Relation.Binary.Equality.Setoid
-  ```
-
 Additions to existing modules
 -----------------------------
-
-* Exporting more `Raw` substructures from `Algebra.Bundles.Ring`:
-  ```agda
-  rawNearSemiring   : RawNearSemiring _ _
-  rawRingWithoutOne : RawRingWithoutOne _ _
-  +-rawGroup        : RawGroup _ _
-  ```
-
-* In `Algebra.Module.Bundles`, raw bundles are re-exported and the bundles expose their raw counterparts.
-
-* In `Algebra.Module.Construct.DirectProduct`:
-  ```agda
-  rawLeftSemimodule  : RawLeftSemimodule R m ℓm → RawLeftSemimodule m′ ℓm′ → RawLeftSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
-  rawLeftModule      : RawLeftModule R m ℓm → RawLeftModule m′ ℓm′ → RawLeftModule R (m ⊔ m′) (ℓm ⊔ ℓm′)
-  rawRightSemimodule : RawRightSemimodule R m ℓm → RawRightSemimodule m′ ℓm′ → RawRightSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
-  rawRightModule     : RawRightModule R m ℓm → RawRightModule m′ ℓm′ → RawRightModule R (m ⊔ m′) (ℓm ⊔ ℓm′)
-  rawBisemimodule    : RawBisemimodule R m ℓm → RawBisemimodule m′ ℓm′ → RawBisemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
-  rawBimodule        : RawBimodule R m ℓm → RawBimodule m′ ℓm′ → RawBimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
-  rawSemimodule      : RawSemimodule R m ℓm → RawSemimodule m′ ℓm′ → RawSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
-  rawModule          : RawModule R m ℓm → RawModule m′ ℓm′ → RawModule R (m ⊔ m′) (ℓm ⊔ ℓm′)
-  ```
-
-* In `Algebra.Module.Construct.TensorUnit`:
-  ```agda
-  rawLeftSemimodule  : RawLeftSemimodule _ c ℓ
-  rawLeftModule      : RawLeftModule _ c ℓ
-  rawRightSemimodule : RawRightSemimodule _ c ℓ
-  rawRightModule     : RawRightModule _ c ℓ
-  rawBisemimodule    : RawBisemimodule _ _ c ℓ
-  rawBimodule        : RawBimodule _ _ c ℓ
-  rawSemimodule      : RawSemimodule _ c ℓ
-  rawModule          : RawModule _ c ℓ
-  ```
-
-* In `Algebra.Module.Construct.Zero`:
-  ```agda
-  rawLeftSemimodule  : RawLeftSemimodule R c ℓ
-  rawLeftModule      : RawLeftModule R c ℓ
-  rawRightSemimodule : RawRightSemimodule R c ℓ
-  rawRightModule     : RawRightModule R c ℓ
-  rawBisemimodule    : RawBisemimodule R c ℓ
-  rawBimodule        : RawBimodule R c ℓ
-  rawSemimodule      : RawSemimodule R c ℓ
-  rawModule          : RawModule R c ℓ
-  ```
-
-* In `Algebra.Properties.Group`:
-  ```agda
-  isQuasigroup    : IsQuasigroup _∙_ _\\_ _//_
-  quasigroup      : Quasigroup _ _
-  isLoop          : IsLoop _∙_ _\\_ _//_ ε
-  loop            : Loop _ _
-
-  \\-leftDividesˡ  : LeftDividesˡ _∙_ _\\_
-  \\-leftDividesʳ  : LeftDividesʳ _∙_ _\\_
-  \\-leftDivides   : LeftDivides _∙_ _\\_
-  //-rightDividesˡ : RightDividesˡ _∙_ _//_
-  //-rightDividesʳ : RightDividesʳ _∙_ _//_
-  //-rightDivides  : RightDivides _∙_ _//_
-
-  ⁻¹-selfInverse  : SelfInverse _⁻¹
-  \\≗flip-//⇒comm : (∀ x y → x \\ y ≈ y // x) → Commutative _∙_
-  comm⇒\\≗flip-// : Commutative _∙_ → ∀ x y → x \\ y ≈ y // x
-  ```
-
-* In `Algebra.Properties.Loop`:
-  ```agda
-  identityˡ-unique : x ∙ y ≈ y → x ≈ ε
-  identityʳ-unique : x ∙ y ≈ x → y ≈ ε
-  identity-unique  : Identity x _∙_ → x ≈ ε
-  ```
-
-* In `Algebra.Construct.Terminal`:
-  ```agda
-  rawNearSemiring : RawNearSemiring c ℓ
-  nearSemiring    : NearSemiring c ℓ
-  ```
-
-* In `Algebra.Properties.Monoid.Mult`:
-  ```agda
-  ×-homo-0 : ∀ x → 0 × x ≈ 0#
-  ×-homo-1 : ∀ x → 1 × x ≈ x
-  ```
-
-* In `Algebra.Properties.Semiring.Mult`:
-  ```agda
-  ×-homo-0#     : ∀ x → 0 × x ≈ 0# * x
-  ×-homo-1#     : ∀ x → 1 × x ≈ 1# * x
-  idem-×-homo-* : (_*_ IdempotentOn x) → (m × x) * (n × x) ≈ (m ℕ.* n) × x
-  ```
-
-* In `Algebra.Structures.IsGroup`:
-  ```agda
-  infixl 6 _//_
-  _//_ : Op₂ A
-  x // y = x ∙ (y ⁻¹)
-  infixr 6 _\\_
-  _\\_ : Op₂ A
-  x \\ y = (x ⁻¹) ∙ y
-  ```
-
-* In `Data.Container.Indexed.Core`:
-  ```agda
-  Subtrees o c = (r : Response c) → X (next c r)
-  ```
-
-* In `Data.Fin.Properties`:
-  ```agda
-  nonZeroIndex : Fin n → ℕ.NonZero n
-  ```
-
-* In `Data.Integer.Divisibility`: introduce `divides` as an explicit pattern synonym
-  ```agda
-  pattern divides k eq = Data.Nat.Divisibility.divides k eq
-  ```
-
-* In `Data.Integer.Properties`:
-  ```agda
-  ◃-nonZero : .{{_ : ℕ.NonZero n}} → NonZero (s ◃ n)
-  sign-*    : .{{NonZero (i * j)}} → sign (i * j) ≡ sign i Sign.* sign j
-  i*j≢0     : .{{_ : NonZero i}} .{{_ : NonZero j}} → NonZero (i * j)
-  ```
-
-* In `Data.List.Properties`:
-  ```agda
-  applyUpTo-∷ʳ          : applyUpTo f n ∷ʳ f n ≡ applyUpTo f (suc n)
-  applyDownFrom-∷ʳ      : applyDownFrom (f ∘ suc) n ∷ʳ f 0 ≡ applyDownFrom f (suc n)
-  upTo-∷ʳ               : upTo n ∷ʳ n ≡ upTo (suc n)
-  downFrom-∷ʳ           : applyDownFrom suc n ∷ʳ 0 ≡ downFrom (suc n)
-  reverse-applyUpTo     : reverse (applyUpTo f n) ≡ applyDownFrom f n
-  reverse-upTo          : reverse (upTo n) ≡ downFrom n
-  reverse-applyDownFrom : reverse (applyDownFrom f n) ≡ applyUpTo f n
-  reverse-downFrom      : reverse (downFrom n) ≡ upTo n
-  ```
-
-* In `Data.List.Relation.Unary.All.Properties`:
-  ```agda
-  All-catMaybes⁺ : All (Maybe.All P) xs → All P (catMaybes xs)
-  Any-catMaybes⁺ : All (Maybe.Any P) xs → All P (catMaybes xs)
-  ```
-
-* In `Data.List.Relation.Unary.AllPairs.Properties`:
-  ```agda
-  catMaybes⁺ : AllPairs (Pointwise R) xs → AllPairs R (catMaybes xs)
-  tabulate⁺-< : (i < j → R (f i) (f j)) → AllPairs R (tabulate f)
-  ```
-
-* In `Data.List.Relation.Ternary.Appending.Setoid.Properties`:
-  ```agda
-  through→ : ∃[ xs ] Pointwise _≈_ as xs × Appending xs bs cs →
-             ∃[ ys ] Appending as bs ys × Pointwise _≈_ ys cs
-  through← : ∃[ ys ] Appending as bs ys × Pointwise _≈_ ys cs →
-             ∃[ xs ] Pointwise _≈_ as xs × Appending xs bs cs
-  assoc→   : ∃[ xs ] Appending as bs xs × Appending xs cs ds →
-             ∃[ ys ] Appending bs cs ys × Appending as ys ds
-  ```
-
-* In `Data.List.Relation.Ternary.Appending.Properties`:
-  ```agda
-  through→ : (R ⇒ (S ; T)) → ((U ; V) ⇒ (W ; T)) →
-                 ∃[ xs ] Pointwise U as xs × Appending V R xs bs cs →
-                         ∃[ ys ] Appending W S as bs ys × Pointwise T ys cs
-  through← : ((R ; S) ⇒ T) → ((U ; S) ⇒ (V ; W)) →
-                 ∃[ ys ] Appending U R as bs ys × Pointwise S ys cs →
-                         ∃[ xs ] Pointwise V as xs × Appending W T xs bs cs
-  assoc→ :   (R ⇒ (S ; T)) → ((U ; V) ⇒ (W ; T)) → ((Y ; V) ⇒ X) →
-                     ∃[ xs ] Appending Y U as bs xs × Appending V R xs cs ds →
-                         ∃[ ys ] Appending W S bs cs ys × Appending X T as ys ds
-  assoc← :   ((S ; T) ⇒ R) → ((W ; T) ⇒ (U ; V)) → (X ⇒ (Y ; V)) →
-             ∃[ ys ] Appending W S bs cs ys × Appending X T as ys ds →
-                         ∃[ xs ] Appending Y U as bs xs × Appending V R xs cs ds
-  ```
-
-* In `Data.List.Relation.Binary.Pointwise.Base`:
-  ```agda
-  unzip : Pointwise (R ; S) ⇒ (Pointwise R ; Pointwise S)
-  ```
-
-* In `Data.Maybe.Relation.Binary.Pointwise`:
-  ```agda
-  pointwise⊆any : Pointwise R (just x) ⊆ Any (R x)
-  ```
-
-* In `Data.List.Relation.Binary.Sublist.Setoid`:
-  ```agda
-  ⊆-upper-bound : ∀ {xs ys zs} (τ : xs ⊆ zs) (σ : ys ⊆ zs) → UpperBound τ σ
-  ```
-
-* In `Data.Nat.Divisibility`:
-  ```agda
-  quotient≢0       : m ∣ n → .{{NonZero n}} → NonZero quotient
-
-  m∣n⇒n≡quotient*m : m ∣ n → n ≡ quotient * m
-  m∣n⇒n≡m*quotient : m ∣ n → n ≡ m * quotient
-  quotient-∣       : m ∣ n → quotient ∣ n
-  quotient>1       : m ∣ n → m < n → 1 < quotient
-  quotient-<       : m ∣ n → .{{NonTrivial m}} → .{{NonZero n}} → quotient < n
-  n/m≡quotient     : m ∣ n → .{{_ : NonZero m}} → n / m ≡ quotient
-
-  m/n≡0⇒m<n    : .{{_ : NonZero n}} → m / n ≡ 0 → m < n
-  m/n≢0⇒n≤m    : .{{_ : NonZero n}} → m / n ≢ 0 → n ≤ m
-
-  nonZeroDivisor : DivMod dividend divisor → NonZero divisor
-  ```
-
-* Added new proofs in `Data.Nat.Properties`:
-  ```agda
-  m≤n+o⇒m∸n≤o : ∀ m n {o} → m ≤ n + o → m ∸ n ≤ o
-  m<n+o⇒m∸n<o : ∀ m n {o} → .{{NonZero o}} → m < n + o → m ∸ n < o
-  pred-cancel-≤ : pred m ≤ pred n → (m ≡ 1 × n ≡ 0) ⊎ m ≤ n
-  pred-cancel-< : pred m < pred n → m < n
-  pred-injective : .{{NonZero m}} → .{{NonZero n}} → pred m ≡ pred n → m ≡ n
-  pred-cancel-≡ : pred m ≡ pred n → ((m ≡ 0 × n ≡ 1) ⊎ (m ≡ 1 × n ≡ 0)) ⊎ m ≡ n
-  ```
-
-* Added new proofs to `Data.Nat.Primality`:
-  ```agda
-  rough∧square>⇒prime : .{{NonTrivial n}} → m Rough n → m * m > n → Prime n
-  productOfPrimes≢0 : All Prime as → NonZero (product as)
-  productOfPrimes≥1 : All Prime as → product as ≥ 1
-  ```
-
-* Added new proofs to `Data.List.Relation.Binary.Permutation.Propositional.Properties`:
-  ```agda
-  product-↭ : product Preserves _↭_ ⟶ _≡_
-  ```
-
-* Added new functions in `Data.String.Base`:
-  ```agda
-  map : (Char → Char) → String → String
-
-* Added new definition in `Relation.Binary.Construct.Closure.Transitive`
-  ```
-  transitive⁻ : Transitive _∼_ → TransClosure _∼_ ⇒ _∼_
-  ```
-
-* Added new definition in `Relation.Unary`
-  ```
-  Stable : Pred A ℓ → Set _
-  ```
-
-* In `Function.Bundles`, added `_⟶ₛ_` as a synonym for `Func` that can
-  be used infix.
-
-* Added new proofs in `Relation.Binary.Construct.Composition`:
-  ```agda
-  transitive⇒≈;≈⊆≈ : Transitive ≈ → (≈ ; ≈) ⇒ ≈
-  ```
-
-* Added new definitions in `Relation.Binary.Definitions`
-  ```
-  Stable _∼_ = ∀ x y → Nullary.Stable (x ∼ y)
-  Empty  _∼_ = ∀ {x y} → x ∼ y → ⊥
-  ```
-
-* Added new proofs in `Relation.Binary.Properties.Setoid`:
-  ```agda
-  ≈;≈⇒≈ : _≈_ ; _≈_ ⇒ _≈_
-  ≈⇒≈;≈ : _≈_ ⇒ _≈_ ; _≈_
-  ```
-
-* Added new definitions in `Relation.Nullary`
-  ```
-  Recomputable    : Set _
-  WeaklyDecidable : Set _
-  ```
-
-* Added new proof in `Relation.Nullary.Decidable`:
-  ```agda
-  ⌊⌋-map′ : (a? : Dec A) → ⌊ map′ t f a? ⌋ ≡ ⌊ a? ⌋
-  ```
-
-* Added new definitions in `Relation.Unary`
-  ```
-  Stable          : Pred A ℓ → Set _
-  WeaklyDecidable : Pred A ℓ → Set _
-  ```
-
-* `Tactic.Cong` now provides a marker function, `⌞_⌟`, for user-guided
-  anti-unification. See README.Tactic.Cong for details.

From 2534bd0109eea056e84be5824f71e01d42fdae03 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 18 Jan 2025 09:41:51 +0000
Subject: [PATCH 39/39] `CHANGELOG`: added fresh entries

---
 CHANGELOG.md | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index edb7c3e57f..5d1d8caad4 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -24,5 +24,25 @@ Deprecated names
 New modules
 -----------
 
+* Bundles for left- and right- actions:
+  ```
+  Algebra.Action.Bundles
+  ```
+
+* The free `Monoid` actions over a `SetoidAction`:
+  ```
+  Algebra.Action.Construct.FreeMonoid
+  ```
+
+* The left- and right- regular actions (of a `Monoid`) over itself:
+  ```
+  Algebra.Action.Construct.Self
+  ```
+
+* Structures for left- and right- actions:
+  ```
+  Algebra.Action.Structures
+  ```
+
 Additions to existing modules
 -----------------------------