diff options
| -rw-r--r-- | Functor/Instance/FreeMonoid.agda | 64 | ||||
| -rw-r--r-- | Functor/Instance/List.agda | 14 |
2 files changed, 73 insertions, 5 deletions
diff --git a/Functor/Instance/FreeMonoid.agda b/Functor/Instance/FreeMonoid.agda new file mode 100644 index 0000000..bb26fd4 --- /dev/null +++ b/Functor/Instance/FreeMonoid.agda @@ -0,0 +1,64 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level; _⊔_) + +module Functor.Instance.FreeMonoid {c ℓ : Level} where + +import Categories.Object.Monoid as MonoidObject + +open import Categories.Category.Construction.Monoids using (Monoids) +open import Categories.Category.Instance.Setoids using (Setoids) +open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) +open import Categories.Functor using (Functor) +open import Categories.NaturalTransformation using (NaturalTransformation) +open import Category.Instance.Setoids.SymmetricMonoidal {c} {c ⊔ ℓ} using (Setoids-×) +open import Data.List.Properties using (++-assoc; ++-identityˡ; ++-identityʳ) +open import Data.Product using (_,_) +open import Function using (_⟶ₛ_) +open import Functor.Instance.List {c} {ℓ} using (List) +open import NaturalTransformation.Instance.EmptyList {c} {ℓ} using (⊤⇒[]) +open import NaturalTransformation.Instance.ListAppend {c} {ℓ} using (++) +open import Relation.Binary using (Setoid) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) + +module List = Functor List +module Setoids-× = SymmetricMonoidalCategory Setoids-× +module ++ = NaturalTransformation ++ +module ⊤⇒[] = NaturalTransformation ⊤⇒[] + +open Functor +open MonoidObject Setoids-×.monoidal using (Monoid; IsMonoid; Monoid⇒) +open IsMonoid + +module _ (X : Setoid c ℓ) where + + private + module X = Setoid X + module ListX = Setoid (List.₀ X) + + ListMonoid : IsMonoid (List.₀ X) + ListMonoid .μ = ++.η X + ListMonoid .η = ⊤⇒[].η X + ListMonoid .assoc {(x , y) , z} = ListX.reflexive (++-assoc x y z) + ListMonoid .identityˡ {_ , x} = ListX.reflexive (++-identityˡ x) + ListMonoid .identityʳ {x , _} = ListX.reflexive (≡.sym (++-identityʳ x)) + +FreeMonoid₀ : (X : Setoid c ℓ) → Monoid +FreeMonoid₀ X = record { isMonoid = ListMonoid X } + +FreeMonoid₁ + : {A B : Setoid c ℓ} + (f : A ⟶ₛ B) + → Monoid⇒ (FreeMonoid₀ A) (FreeMonoid₀ B) +FreeMonoid₁ f = record + { arr = List.₁ f + ; preserves-μ = λ {x,y} → ++.sym-commute f {x,y} + ; preserves-η = ⊤⇒[].commute f + } + +FreeMonoid : Functor (Setoids c ℓ) (Monoids Setoids-×.monoidal) +FreeMonoid .F₀ = FreeMonoid₀ +FreeMonoid .F₁ = FreeMonoid₁ +FreeMonoid .identity {X} = List.identity {X} +FreeMonoid .homomorphism {X} {Y} {Z} {f} {g} = List.homomorphism {X} {Y} {Z} {f} {g} +FreeMonoid .F-resp-≈ {A} {B} {f} {g} = List.F-resp-≈ {A} {B} {f} {g} diff --git a/Functor/Instance/List.agda b/Functor/Instance/List.agda index 05db349..b40670d 100644 --- a/Functor/Instance/List.agda +++ b/Functor/Instance/List.agda @@ -16,7 +16,7 @@ open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_) open import Relation.Binary using (Setoid) open Functor -open Setoid +open Setoid using (reflexive) open Func private @@ -36,15 +36,19 @@ mapₛ : A ⟶ₛ B → Listₛ A ⟶ₛ Listₛ B mapₛ f .to = List.map (to f) mapₛ f .cong = PW.map⁺ (to f) (to f) ∘ PW.map (cong f) -map-id : (xs : ∣ Listₛ A ∣) → PW.Pointwise (_≈_ A) (List.map id xs) xs -map-id {A} = PW.map (reflexive A) ∘ PW.≡⇒Pointwise-≡ ∘ ListProps.map-id +map-id + : (xs : ∣ Listₛ A ∣) + → (open Setoid (Listₛ A)) + → List.map id xs ≈ xs +map-id {A} = reflexive (Listₛ A) ∘ ListProps.map-id List-homo : (f : A ⟶ₛ B) (g : B ⟶ₛ C) → (xs : ∣ Listₛ A ∣) - → PW.Pointwise (_≈_ C) (List.map (to g ∘ to f) xs) (List.map (to g) (List.map (to f) xs)) -List-homo {C = C} f g = PW.map (reflexive C) ∘ PW.≡⇒Pointwise-≡ ∘ ListProps.map-∘ + → (open Setoid (Listₛ C)) + → List.map (to g ∘ to f) xs ≈ List.map (to g) (List.map (to f) xs) +List-homo {C = C} f g = reflexive (Listₛ C) ∘ ListProps.map-∘ List : Functor (Setoids c ℓ) (Setoids c (c ⊔ ℓ)) List .F₀ = Listₛ |