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] 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 }