diff options
Diffstat (limited to 'Adjoint')
| -rw-r--r-- | Adjoint/Instance/List.agda | 107 | ||||
| -rw-r--r-- | Adjoint/Instance/Multiset.agda | 112 |
2 files changed, 219 insertions, 0 deletions
diff --git a/Adjoint/Instance/List.agda b/Adjoint/Instance/List.agda new file mode 100644 index 0000000..1b65985 --- /dev/null +++ b/Adjoint/Instance/List.agda @@ -0,0 +1,107 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level; _⊔_; suc) + +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-×) + +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; 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.Product using (_,_; uncurry) +open import Data.Setoid using (∣_∣) +open import Function using (_⟶ₛ_; _⟨$⟩_) +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⇒ + +open import Categories.Category using (Category) + +Mon[S] : Category (suc ℓ) ℓ ℓ +Mon[S] = Monoids S.monoidal + +Free : Functor S.U Mon[S] +Free = Free′ + +Forget : Functor Mon[S] S.U +Forget = Forget′ S.monoidal + +opaque + unfolding [-]ₛ mapₘ + map-[-]ₛ + : {X Y : Setoid ℓ ℓ} + (f : X ⟶ₛ Y) + {x : ∣ X ∣} + → (open Setoid (Listₛ Y)) + → [-]ₛ ⟨$⟩ (f ⟨$⟩ x) + ≈ arr (mapₘ f) ⟨$⟩ ([-]ₛ ⟨$⟩ x) + map-[-]ₛ {X} {Y} f {x} = Setoid.refl (Listₛ Y) + +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ₛ)) + → 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} + +opaque + unfolding foldₘ fold + zag : (M : Monoid) + {x : ∣ Carrier M ∣} + → (open Setoid (Carrier M)) + → arr (foldₘ M) ⟨$⟩ ([-]ₛ ⟨$⟩ x) ≈ x + zag M {x} = Setoid.sym (Carrier M) (identityʳ M {x , _}) + +List⊣ : Free ⊣ Forget +List⊣ = record + { unit = unit + ; counit = counit + ; zig = λ {X} → zig X + ; zag = λ {M} → zag M + } diff --git a/Adjoint/Instance/Multiset.agda b/Adjoint/Instance/Multiset.agda new file mode 100644 index 0000000..c51baa9 --- /dev/null +++ b/Adjoint/Instance/Multiset.agda @@ -0,0 +1,112 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level; _⊔_; suc; 0ℓ) + +module Adjoint.Instance.Multiset {ℓ : Level} where + +open import Category.Instance.Setoids.SymmetricMonoidal {ℓ} {ℓ} using (Setoids-×) + +private + module S = Setoids-× + +import Categories.Object.Monoid S.monoidal as MonoidObject +import Data.List as L +import Data.List.Relation.Binary.Permutation.Setoid as ↭ +import Functor.Forgetful.Instance.CMonoid S.symmetric as CMonoid +import Functor.Forgetful.Instance.Monoid S.monoidal as Monoid +import Object.Monoid.Commutative S.symmetric as CMonoidObject + +open import Categories.Adjoint using (_⊣_) +open import Categories.Category using (Category) +open import Categories.Functor using (Functor; id; _∘F_) +open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) +open import Category.Construction.CMonoids using (CMonoids) +open import Data.CMonoid using (toCMonoid; toCMonoid⇒) +open import Data.Monoid using (toMonoid; toMonoid⇒) +open import Data.Opaque.Multiset using ([-]ₛ; Multisetₛ; foldₛ; ++ₛ-homo; []ₛ-homo; fold-mapₛ; fold) +open import Data.Product using (_,_; uncurry) +open import Data.Setoid using (∣_∣) +open import Function using (_⟶ₛ_; _⟨$⟩_) +open import Functor.Free.Instance.CMonoid {ℓ} {ℓ} using (Multisetₘ; mapₘ; MultisetCMonoid) renaming (Free to Free′) +open import Relation.Binary using (Setoid) + +open CMonoidObject using (CommutativeMonoid; CommutativeMonoid⇒) +open CommutativeMonoid using (Carrier; monoid; identityʳ) +open CommutativeMonoid⇒ using (arr; monoid⇒) +open MonoidObject using (Monoid; Monoid⇒) +open Monoid⇒ using (preserves-μ; preserves-η) + +CMon[S] : Category (suc ℓ) ℓ ℓ +CMon[S] = CMonoids S.symmetric + +Free : Functor S.U CMon[S] +Free = Free′ + +Forget : Functor CMon[S] S.U +Forget = Monoid.Forget ∘F CMonoid.Forget + +opaque + unfolding [-]ₛ + map-[-]ₛ + : {X Y : Setoid ℓ ℓ} + (f : X ⟶ₛ Y) + {x : ∣ X ∣} + → (open Setoid (Multisetₛ Y)) + → [-]ₛ ⟨$⟩ (f ⟨$⟩ x) + ≈ arr (mapₘ f) ⟨$⟩ ([-]ₛ ⟨$⟩ x) + map-[-]ₛ {X} {Y} f {x} = Setoid.refl (Multisetₛ Y) + +unit : NaturalTransformation id (Forget ∘F Free) +unit = ntHelper record + { η = λ X → [-]ₛ {ℓ} {ℓ} {X} + ; commute = map-[-]ₛ + } + +opaque + unfolding toMonoid MultisetCMonoid + foldₘ : (X : CommutativeMonoid) → CommutativeMonoid⇒ (Multisetₘ (Carrier X)) X + foldₘ X .monoid⇒ .Monoid⇒.arr = foldₛ (toCMonoid X) + foldₘ X .monoid⇒ .preserves-μ {xs , ys} = ++ₛ-homo (toCMonoid X) xs ys + foldₘ X .monoid⇒ .preserves-η {_} = []ₛ-homo (toCMonoid X) + +opaque + unfolding foldₘ toMonoid⇒ + fold-mapₘ + : {X Y : CommutativeMonoid} + (f : CommutativeMonoid⇒ X Y) + {x : ∣ Multisetₛ (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ₛ (toCMonoid X) (toCMonoid Y)) (toCMonoid⇒ X Y f) + +counit : NaturalTransformation (Free ∘F Forget) id +counit = ntHelper record + { η = foldₘ + ; commute = fold-mapₘ + } + +opaque + unfolding foldₘ fold Multisetₛ + zig : (Aₛ : Setoid ℓ ℓ) + {xs : ∣ Multisetₛ Aₛ ∣} + → (open Setoid (Multisetₛ Aₛ)) + → arr (foldₘ (Multisetₘ Aₛ)) ⟨$⟩ (arr (mapₘ [-]ₛ) ⟨$⟩ xs) ≈ xs + zig Aₛ {L.[]} = ↭.↭-refl Aₛ + zig Aₛ {x L.∷ xs} = ↭.prep (Setoid.refl Aₛ) (zig Aₛ) + +opaque + unfolding foldₘ fold + zag : (M : CommutativeMonoid) + {x : ∣ Carrier M ∣} + → (open Setoid (Carrier M)) + → arr (foldₘ M) ⟨$⟩ ([-]ₛ ⟨$⟩ x) ≈ x + zag M {x} = Setoid.sym (Carrier M) (identityʳ M {x , _}) + +Multiset⊣ : Free ⊣ Forget +Multiset⊣ = record + { unit = unit + ; counit = counit + ; zig = λ {X} → zig X + ; zag = λ {M} → zag M + } |