From d992900179fb4c96787c0904dedc36610a19e32b Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Thu, 30 May 2024 15:39:18 +0100
Subject: [PATCH] Add the `Setoid`-based `Monoid` on `(List, [], _++_)` (#2393)

* refactored from #2350

* enriched the `module` contents in response to review comments
---
 CHANGELOG.md                                  |  5 ++
 .../Binary/Equality/Setoid/Properties.agda    | 59 +++++++++++++++++++
 2 files changed, 64 insertions(+)
 create mode 100644 src/Data/List/Relation/Binary/Equality/Setoid/Properties.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 88dbe3c075..567782c261 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -113,6 +113,11 @@ New modules
   Algebra.Module.Bundles.Raw
   ```
 
+* Properties of `List` modulo `Setoid` equality (currently only the ([],++) monoid):
+  ```
+  Data.List.Relation.Binary.Equality.Setoid.Properties
+  ```
+
 * Refactoring of `Data.List.Base.{scanr|scanl}` and their properties:
   ```
   Data.List.Scans.Base
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..fea2638f66
--- /dev/null
+++ b/src/Data/List/Relation/Binary/Equality/Setoid/Properties.agda
@@ -0,0 +1,59 @@
+------------------------------------------------------------------------
+-- 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 (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 ≋
+open import Data.Product.Base using (_,_)
+open import Function.Base using (_∘_)
+open import Level using (_⊔_)
+
+open ≋ S using (_≋_; ≋-refl; ≋-reflexive; ≋-isEquivalence; ++⁺)
+open Structures _≋_ using (IsMagma; IsSemigroup; IsMonoid)
+
+------------------------------------------------------------------------
+-- The []-++-Monoid
+
+-- Structures
+
+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 = isSemigroup
+  ; identity = (λ _ → ≋-refl) , ≋-reflexive ∘ List.++-identityʳ
+  }
+
+-- 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 }