diff options
| -rw-r--r-- | Adjoint/Instance/List.agda | 100 |
1 files changed, 60 insertions, 40 deletions
diff --git a/Adjoint/Instance/List.agda b/Adjoint/Instance/List.agda index f517f16..f3bf061 100644 --- a/Adjoint/Instance/List.agda +++ b/Adjoint/Instance/List.agda @@ -2,83 +2,103 @@ open import Level using (Level; _⊔_; suc; 0ℓ) -module Adjoint.Instance.List {c ℓ : Level} where +module Adjoint.Instance.List {ℓ : Level} where import Data.List as L import Data.List.Relation.Binary.Pointwise as PW open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory) -open import Category.Instance.Setoids.SymmetricMonoidal using (Setoids-×) +open import Category.Instance.Setoids.SymmetricMonoidal {ℓ} {ℓ} using (Setoids-×) -module S = SymmetricMonoidalCategory (Setoids-× {c ⊔ ℓ} {c ⊔ ℓ}) +module S = SymmetricMonoidalCategory Setoids-× open import Categories.Adjoint using (_⊣_) open import Categories.Category.Construction.Monoids using (Monoids) open import Categories.Functor using (Functor; id; _∘F_) open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) -open import Categories.Object.Monoid S.monoidal using (Monoid; Monoid⇒) +open import Categories.Object.Monoid S.monoidal using (Monoid; IsMonoid; Monoid⇒) open import Data.Monoid using (toMonoid; toMonoid⇒) -open import Data.Opaque.List using ([-]ₛ; Listₛ; mapₛ; foldₛ; ++ₛ; ++ₛ-homo; []ₛ-homo; fold-mapₛ; fold) +open import Data.Opaque.List using ([-]ₛ; Listₛ; mapₛ; foldₛ; ++ₛ-homo; []ₛ-homo; fold-mapₛ; fold) open import Data.Product using (_,_; uncurry) open import Data.Setoid using (∣_∣) open import Function using (_⟶ₛ_; _⟨$⟩_) -open import Functor.Forgetful.Instance.Monoid {suc (c ⊔ ℓ)} {c ⊔ ℓ} {c ⊔ ℓ} using (Forget) -open import Functor.Free.Instance.Monoid {c ⊔ ℓ} {c ⊔ ℓ} using (Free; Listₘ) +open import Functor.Forgetful.Instance.Monoid {suc ℓ} {ℓ} {ℓ} using () renaming (Forget to Forget′) +open import Functor.Free.Instance.Monoid {ℓ} {ℓ} using (Listₘ; mapₘ; ListMonoid) renaming (Free to Free′) open import Relation.Binary using (Setoid) open Monoid open Monoid⇒ -S-mc : MonoidalCategory (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ) -S-mc = record { monoidal = S.monoidal } +open import Categories.Category using (Category) -opaque +Mon[S] : Category (suc ℓ) ℓ ℓ +Mon[S] = Monoids S.monoidal + +Free : Functor S.U Mon[S] +Free = Free′ - unfolding [-]ₛ - unfolding fold +Forget : Functor Mon[S] S.U +Forget = Forget′ S.monoidal +opaque + unfolding [-]ₛ mapₘ map-[-]ₛ - : {X Y : Setoid (c ⊔ ℓ) (c ⊔ ℓ)} - → (f : X ⟶ₛ Y) + : {X Y : Setoid ℓ ℓ} + (f : X ⟶ₛ Y) + {x : ∣ X ∣} → (open Setoid (Listₛ Y)) - → {x : ∣ X ∣} → [-]ₛ ⟨$⟩ (f ⟨$⟩ x) - ≈ mapₛ f ⟨$⟩ ([-]ₛ ⟨$⟩ x) + ≈ arr (mapₘ f) ⟨$⟩ ([-]ₛ ⟨$⟩ x) map-[-]ₛ {X} {Y} f {x} = Setoid.refl (Listₛ Y) - zig - : (Aₛ : Setoid (c ⊔ ℓ) (c ⊔ ℓ)) +unit : NaturalTransformation id (Forget ∘F Free) +unit = ntHelper record + { η = λ X → [-]ₛ {ℓ} {ℓ} {X} + ; commute = map-[-]ₛ + } + +opaque + unfolding toMonoid ListMonoid + foldₘ : (X : Monoid) → Monoid⇒ (Listₘ (Carrier X)) X + foldₘ X .arr = foldₛ (toMonoid X) + foldₘ X .preserves-μ {xs , ys} = ++ₛ-homo (toMonoid X) xs ys + foldₘ X .preserves-η {_} = []ₛ-homo (toMonoid X) + +opaque + unfolding foldₘ toMonoid⇒ mapₘ + fold-mapₘ + : {X Y : Monoid} + (f : Monoid⇒ X Y) + {x : ∣ Listₛ (Carrier X) ∣} + → (open Setoid (Carrier Y)) + → arr (foldₘ Y) ⟨$⟩ (arr (mapₘ (arr f)) ⟨$⟩ x) + ≈ arr f ⟨$⟩ (arr (foldₘ X) ⟨$⟩ x) + fold-mapₘ {X} {Y} f = uncurry (fold-mapₛ (toMonoid X) (toMonoid Y)) (toMonoid⇒ X Y f) + +counit : NaturalTransformation (Free ∘F Forget) id +counit = ntHelper record + { η = foldₘ + ; commute = fold-mapₘ + } + +opaque + unfolding mapₘ foldₘ fold + zig : (Aₛ : Setoid ℓ ℓ) {xs : ∣ Listₛ Aₛ ∣} → (open Setoid (Listₛ Aₛ)) - → foldₛ (toMonoid (Listₘ Aₛ)) ⟨$⟩ (mapₛ [-]ₛ ⟨$⟩ xs) ≈ xs + → arr (foldₘ (Listₘ Aₛ)) ⟨$⟩ (arr (mapₘ [-]ₛ) ⟨$⟩ xs) ≈ xs zig Aₛ {xs = L.[]} = Setoid.refl (Listₛ Aₛ) zig Aₛ {xs = x L.∷ xs} = Setoid.refl Aₛ PW.∷ zig Aₛ {xs = xs} - zag - : (M : Monoid) +opaque + unfolding foldₘ fold + zag : (M : Monoid) {x : ∣ Carrier M ∣} → (open Setoid (Carrier M)) - → fold (toMonoid M) ([-]ₛ ⟨$⟩ x) ≈ x + → arr (foldₘ M) ⟨$⟩ ([-]ₛ ⟨$⟩ x) ≈ x zag M {x} = Setoid.sym (Carrier M) (identityʳ M {x , _}) -unit : NaturalTransformation id (Forget S-mc ∘F Free) -unit = ntHelper record - { η = λ X → [-]ₛ {c ⊔ ℓ} {c ⊔ ℓ} {X} - ; commute = map-[-]ₛ - } - -foldₘ : (X : Monoid) → Monoid⇒ (Listₘ (Carrier X)) X -foldₘ X .arr = foldₛ (toMonoid X) -foldₘ X .preserves-μ {xs , ys} = ++ₛ-homo (toMonoid X) xs ys -foldₘ X .preserves-η {_} = []ₛ-homo (toMonoid X) - -counit : NaturalTransformation (Free ∘F Forget S-mc) id -counit = ntHelper record - { η = foldₘ - ; commute = λ {X} {Y} f → uncurry (fold-mapₛ (toMonoid X) (toMonoid Y)) (toMonoid⇒ X Y f) - } - -List⊣ : Free ⊣ Forget S-mc +List⊣ : Free ⊣ Forget List⊣ = record { unit = unit ; counit = counit |