Add the Setoid-based Monoid on (List, [], _++_) (#2393)

* refactored from #2350

* enriched the `module` contents in response to review comments

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

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 }