diff options
| -rw-r--r-- | Functor/Forgetful/Instance/Monoid.agda | 10 | ||||
| -rw-r--r-- | Functor/Free/Instance/Monoid.agda | 73 |
2 files changed, 59 insertions, 24 deletions
diff --git a/Functor/Forgetful/Instance/Monoid.agda b/Functor/Forgetful/Instance/Monoid.agda index 2c786ef..2f9e4d8 100644 --- a/Functor/Forgetful/Instance/Monoid.agda +++ b/Functor/Forgetful/Instance/Monoid.agda @@ -1,23 +1,25 @@ {-# OPTIONS --without-K --safe #-} -open import Categories.Category.Monoidal using (MonoidalCategory) +open import Categories.Category using (Category) +open import Categories.Category.Monoidal using (Monoidal) open import Level using (Level) -module Functor.Forgetful.Instance.Monoid {o ℓ e : Level} (S : MonoidalCategory o ℓ e) where +module Functor.Forgetful.Instance.Monoid {o ℓ e : Level} {S : Category o ℓ e} (monoidal : Monoidal S) where open import Categories.Category.Construction.Monoids using (Monoids) open import Categories.Functor using (Functor) open import Categories.Object.Monoid using (Monoid; Monoid⇒) open import Function using (id) -module S = MonoidalCategory S +private + module S = Category S open Monoid open Monoid⇒ open S.Equiv using (refl) open Functor -Forget : Functor (Monoids S.monoidal) S.U +Forget : Functor (Monoids monoidal) S Forget .F₀ = Carrier Forget .F₁ = arr Forget .identity = refl diff --git a/Functor/Free/Instance/Monoid.agda b/Functor/Free/Instance/Monoid.agda index 34fa2dd..e08e42d 100644 --- a/Functor/Free/Instance/Monoid.agda +++ b/Functor/Free/Instance/Monoid.agda @@ -1,17 +1,18 @@ {-# OPTIONS --without-K --safe #-} -open import Level using (Level; _⊔_) +open import Level using (Level; _⊔_; suc) module Functor.Free.Instance.Monoid {c ℓ : Level} where import Categories.Object.Monoid as MonoidObject +open import Categories.Category using (Category) 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 Category.Instance.Setoids.SymmetricMonoidal {c} {c ⊔ ℓ} using (Setoids-×; ×-monoidal′) open import Data.List.Properties using (++-assoc; ++-identityˡ; ++-identityʳ) open import Data.Opaque.List using ([]ₛ; Listₛ; ++ₛ; mapₛ) open import Data.Product using (_,_) @@ -24,11 +25,13 @@ open import Relation.Binary using (Setoid) open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) module Setoids-× = SymmetricMonoidalCategory Setoids-× + module ++ = NaturalTransformation ++ module ⊤⇒[] = NaturalTransformation ⊤⇒[] open Functor open MonoidObject Setoids-×.monoidal using (Monoid; IsMonoid; Monoid⇒) + open IsMonoid -- the functor sending a setoid A to the monoid List A @@ -57,29 +60,59 @@ module _ (X : Setoid c ℓ) where → x ≈ ++ₛ ⟨$⟩ (x , []ₛ ⟨$⟩ _) ++ₛ-identityʳ x = sym (reflexive (++-identityʳ x)) - ListMonoid : IsMonoid (List.₀ X) - ListMonoid .μ = ++.η X - ListMonoid .η = ⊤⇒[].η X - ListMonoid .assoc {(x , y) , z} = ++ₛ-assoc x y z - ListMonoid .identityˡ {bro , x} = ++ₛ-identityˡ x - ListMonoid .identityʳ {x , _} = ++ₛ-identityʳ x + opaque + + unfolding ×-monoidal′ + + ListMonoid : IsMonoid (List.₀ X) + ListMonoid = record + { μ = ++.η X + ; η = ⊤⇒[].η X + ; assoc = λ { {(x , y) , z} → ++ₛ-assoc x y z } + ; identityˡ = λ { {_ , x} → ++ₛ-identityˡ x } + ; identityʳ = λ { {x , _} → ++ₛ-identityʳ x } + } Listₘ : Setoid c ℓ → Monoid Listₘ X = record { isMonoid = ListMonoid X } -mapₘ - : {Aₛ Bₛ : Setoid c ℓ} - (f : Aₛ ⟶ₛ Bₛ) - → Monoid⇒ (Listₘ Aₛ) (Listₘ Bₛ) -mapₘ f = record - { arr = List.₁ f - ; preserves-μ = λ {x,y} → ++.sym-commute f {x,y} - ; preserves-η = ⊤⇒[].sym-commute f - } +opaque + + unfolding ListMonoid + + mapₘ + : {Aₛ Bₛ : Setoid c ℓ} + (f : Aₛ ⟶ₛ Bₛ) + → Monoid⇒ (Listₘ Aₛ) (Listₘ Bₛ) + mapₘ f = record + { arr = List.₁ f + ; preserves-μ = λ {x,y} → ++.sym-commute f {x,y} + ; preserves-η = ⊤⇒[].sym-commute f + } + +module U = Category Setoids-×.U +open Monoid⇒ using (arr) +open import Function.Construct.Identity using () renaming (function to Id) +open import Function.Construct.Composition using () renaming (function to compose) +opaque + unfolding mapₘ + Free-identity : {X : Setoid c ℓ} → arr (mapₘ (Id X)) U.≈ U.id + Free-identity = List.identity + + Free-homomorphism : {X Y Z : Setoid c ℓ} {f : X ⟶ₛ Y} {g : Y ⟶ₛ Z} → arr (mapₘ (compose f g)) U.≈ arr (mapₘ g) U.∘ arr (mapₘ f) + Free-homomorphism = List.homomorphism + + Free-resp-≈ + : {X Y : Setoid c ℓ} + {f g : X ⟶ₛ Y} + (let module Y = Setoid Y) + → (∀ {x} → f ⟨$⟩ x Y.≈ g ⟨$⟩ x) + → arr (mapₘ f) U.≈ arr (mapₘ g) + Free-resp-≈ = List.F-resp-≈ Free : Functor (Setoids c ℓ) (Monoids Setoids-×.monoidal) Free .F₀ = Listₘ Free .F₁ = mapₘ -Free .identity {X} = List.identity {X} -Free .homomorphism {X} {Y} {Z} {f} {g} = List.homomorphism {X} {Y} {Z} {f} {g} -Free .F-resp-≈ {A} {B} {f} {g} = List.F-resp-≈ {A} {B} {f} {g} +Free .identity = Free-identity +Free .homomorphism = Free-homomorphism +Free .F-resp-≈ = Free-resp-≈ |