------------------------------------------------------------------------
-- 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 using (++-assoc; ++-identityʳ)
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 }
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4