From be62e95b68c9e5c6eb10e5eb2aad741988cc5d0d Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Tue, 21 May 2024 09:48:45 +0100
Subject: [PATCH 1/2] refactored from #2350

---
 CHANGELOG.md                                  |  5 ++
 .../Binary/Equality/Setoid/Properties.agda    | 46 +++++++++++++++++++
 2 files changed, 51 insertions(+)
 create mode 100644 src/Data/List/Relation/Binary/Equality/Setoid/Properties.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 30dc56b3d0..922fa12e5c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -89,6 +89,11 @@ New modules
   Algebra.Module.Bundles.Raw
   ```
 
+* Properties of `List` modulo `Setoid` equality (currently only the ([],++) monoid):
+  ```
+  Data.List.Relation.Binary.Equality.Setoid.Properties
+  ```
+
 * Prime factorisation of natural numbers.
   ```
   Data.Nat.Primality.Factorisation
diff --git a/src/Data/List/Relation/Binary/Equality/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Equality/Setoid/Properties.agda
new file mode 100644
index 0000000000..50783fee89
--- /dev/null
+++ b/src/Data/List/Relation/Binary/Equality/Setoid/Properties.agda
@@ -0,0 +1,46 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of List modulo ≋
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Bundles using (Setoid)
+
+module Data.List.Relation.Binary.Equality.Setoid.Properties
+  {c ℓ} (S : Setoid c ℓ)
+  where
+
+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 (_⊔_)
+
+open ≋ S using (_≋_; ≋-refl; ≋-reflexive; ≋-isEquivalence; ++⁺)
+
+------------------------------------------------------------------------
+-- The []-++-Monoid
+
+-- Structure
+
+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ʳ
+  }
+
+-- Bundle
+
+monoid : Monoid c (c ⊔ ℓ)
+monoid = record { isMonoid = isMonoid }

From b0216723b94d9c5e0953fe6a7858837a2058542a Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 24 May 2024 16:07:53 +0100
Subject: [PATCH 2/2] enriched the `module` contents in response to review
 comments

---
 .../Binary/Equality/Setoid/Properties.agda    | 37 +++++++++++++------
 1 file changed, 25 insertions(+), 12 deletions(-)

diff --git a/src/Data/List/Relation/Binary/Equality/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Equality/Setoid/Properties.agda
index 50783fee89..fea2638f66 100644
--- a/src/Data/List/Relation/Binary/Equality/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Equality/Setoid/Properties.agda
@@ -12,8 +12,8 @@ module Data.List.Relation.Binary.Equality.Setoid.Properties
   {c ℓ} (S : Setoid c ℓ)
   where
 
-open import Algebra.Bundles using (Monoid)
-open import Algebra.Structures using (IsMonoid)
+open import Algebra.Bundles using (Magma; Semigroup; Monoid)
+import Algebra.Structures as Structures
 open import Data.List.Base using (List; []; _++_)
 import Data.List.Properties as List
 import Data.List.Relation.Binary.Equality.Setoid as ≋
@@ -22,25 +22,38 @@ open import Function.Base using (_∘_)
 open import Level using (_⊔_)
 
 open ≋ S using (_≋_; ≋-refl; ≋-reflexive; ≋-isEquivalence; ++⁺)
+open Structures _≋_ using (IsMagma; IsSemigroup; IsMonoid)
 
 ------------------------------------------------------------------------
 -- The []-++-Monoid
 
--- Structure
+-- Structures
 
-isMonoid : IsMonoid _≋_ _++_ []
+isMagma : IsMagma _++_
+isMagma = record
+  { isEquivalence = ≋-isEquivalence
+  ; ∙-cong = ++⁺
+  }
+
+isSemigroup : IsSemigroup _++_
+isSemigroup = record
+  { isMagma = isMagma
+  ; assoc = λ xs ys zs → ≋-reflexive (List.++-assoc xs ys zs)
+  }
+
+isMonoid : IsMonoid _++_ []
 isMonoid = record
-  { isSemigroup = record
-    { isMagma = record
-      { isEquivalence = ≋-isEquivalence
-      ; ∙-cong = ++⁺
-      }
-    ; assoc = λ xs ys zs → ≋-reflexive (List.++-assoc xs ys zs)
-    }
+  { isSemigroup = isSemigroup
   ; identity = (λ _ → ≋-refl) , ≋-reflexive ∘ List.++-identityʳ
   }
 
--- Bundle
+-- Bundles
+
+magma : Magma c (c ⊔ ℓ)
+magma = record { isMagma = isMagma }
+
+semigroup : Semigroup c (c ⊔ ℓ)
+semigroup = record { isSemigroup = isSemigroup }
 
 monoid : Monoid c (c ⊔ ℓ)
 monoid = record { isMonoid = isMonoid }