From 230b34da49d39e09ee5b76c3c87ee38bfe2bebca Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Mon, 11 Sep 2023 21:06:23 +0200 Subject: [PATCH] use coproduct functor from library, minor changes --- src/Monad/Instance/Delay.lagda.md | 42 ++++++++++++------------------- 1 file changed, 16 insertions(+), 26 deletions(-) diff --git a/src/Monad/Instance/Delay.lagda.md b/src/Monad/Instance/Delay.lagda.md index deca1bd..d59f297 100644 --- a/src/Monad/Instance/Delay.lagda.md +++ b/src/Monad/Instance/Delay.lagda.md @@ -58,25 +58,13 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ ``` --> -The delay monad is described via existence of final (Y + \_)-coalgebras, so first we need to define the (Y + \_)-functor: - -```agda - delayF : Obj → Endofunctor C - delayF Y = record - { F₀ = Y +_ - ; F₁ = idC +₁_ - ; identity = CC.coproduct.unique id-comm-sym id-comm-sym - ; homomorphism = ⟺ (+₁∘+₁ ○ +₁-cong₂ identity² refl) - ; F-resp-≈ = +₁-cong₂ refl - } -``` - -Using this functor we can define the delay monad ***D***: +The Delay monad is usually described by existence of final coalgebras for the functor `(X + -)` where `X` is some arbitrary object. +This functor trivially sends objects `Y` to `X + Y` and functions `f` to `id + f`. ```agda record DelayM : Set (o ⊔ ℓ ⊔ e) where field - coalgebras : ∀ (A : Obj) → Terminal (F-Coalgebras (delayF A)) + coalgebras : ∀ (A : Obj) → Terminal (F-Coalgebras (A +-)) ``` These are all the fields this record needs! @@ -94,7 +82,7 @@ We can now define these functions by bisecting the isomorphism `out : DX ≅ X + D₀ = DX out-≅ : DX ≅ X + DX - out-≅ = colambek {F = delayF X} (coalgebras X) + out-≅ = colambek {F = X +- } (coalgebras X) -- note: out-≅.from ≡ ⊤.α open _≅_ out-≅ using () renaming (to to out⁻¹; from to out) public @@ -109,8 +97,10 @@ We can now define these functions by bisecting the isomorphism `out : DX ≅ X + unitlaw = cancelˡ (_≅_.isoʳ out-≅) ``` -Since `DX` is part of a final coalgebra, we can define a *coiteration operator* that sends every `Y ⇒ X + Y` to `Y ⇒ DX` for an arbitrary `Y` -TODO rephrase, add diagram +Since `Y ⇒ X + Y` is an algebra for the `(X + -)` functor, we can use our terminal coalgebras to get a *coiteration operator* `coit`: + +TODO add diagram + ```agda module _ {Y : Obj} where coit : Y ⇒ X + Y → Y ⇒ DX @@ -120,8 +110,8 @@ TODO rephrase, add diagram coit-commutes f = commutes (! {A = record { A = Y ; α = f }}) ``` -If we combine the interal algebra structure of Parametrized NNOs with Lambek's lemma, we get the isomorphism `X × N ≅ X + X × N`. -At the same time the morphism `X × N ⇒ X + X × N` is a coalgebra for the `delayF` defined above, this gives us another morphism `ι : X × N ⇒ DX` by using the final coalgebras. +If we combine the internal algebra structure of Parametrized NNOs with Lambek's lemma, we get the isomorphism `X × N ≅ X + X × N`. +At the same time the morphism `X × N ⇒ X + X × N` is a coalgebra for the `(Y + \_)`-functor defined above, this gives us another morphism `ι : X × N ⇒ DX` by using the final coalgebras. TODO add diagram ```agda @@ -157,14 +147,14 @@ TODO where open Terminal module _ {X Y : Obj} (f : X ⇒ D₀ Y) where - alg : F-Coalgebra (delayF Y) + alg : F-Coalgebra (Y +-) alg = record { A = D₀ X + D₀ Y ; α = [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ i₂) ∘ out Y ] } extend : D₀ X ⇒ D₀ Y extend = u (! (coalgebras Y) {A = alg}) ∘ i₁ {B = D₀ Y} !∘i₂ : u (! (coalgebras Y) {A = alg}) ∘ i₂ ≈ idC - !∘i₂ = ⊤-id (coalgebras Y) (F-Coalgebras (delayF Y) [ ! (coalgebras Y) ∘ record { f = i₂ ; commutes = inject₂ } ] ) + !∘i₂ = ⊤-id (coalgebras Y) (F-Coalgebras (Y +-) [ ! (coalgebras Y) ∘ record { f = i₂ ; commutes = inject₂ } ] ) extendlaw : out Y ∘ extend ≈ [ out Y ∘ f , i₂ ∘ extend ] ∘ out X extendlaw = begin @@ -213,7 +203,7 @@ TODO (([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl) (pullʳ inject₁)) ⟩∘⟨refl) - (elimˡ (Functor.identity (delayF Y))) + (elimˡ (Functor.identity (Y +-))) ⟩ [ [ [ (idC +₁ [ g , idC ]) ∘ i₁ , (idC +₁ [ g , idC ]) ∘ i₂ ∘ i₂ ] ∘ (out Y ∘ f) @@ -233,7 +223,7 @@ TODO αf≈αg : ∀ {X Y} {f g : X ⇒ D₀ Y} → f ≈ g → α (alg f) ≈ α (alg g) αf≈αg {X} {Y} {f} {g} eq = []-cong₂ ([]-cong₂ (refl⟩∘⟨ refl⟩∘⟨ eq) refl ⟩∘⟨refl) refl - alg-f≈alg-g : ∀ {X Y} {f g : X ⇒ D₀ Y} → f ≈ g → M._≅_ (F-Coalgebras (delayF Y)) (alg f) (alg g) + alg-f≈alg-g : ∀ {X Y} {f g : X ⇒ D₀ Y} → f ≈ g → M._≅_ (F-Coalgebras (Y +-)) (alg f) (alg g) alg-f≈alg-g {X} {Y} {f} {g} eq = record { from = record { f = idC ; commutes = begin α (alg g) ∘ idC ≈⟨ identityʳ ⟩ @@ -250,7 +240,7 @@ TODO ; isoʳ = identity² } } - where open Functor (delayF Y) using (identity) + where open Functor (Y +-) using (identity) identityʳ' : ∀ {X} {Y} {f} → extend f ∘ now X ≈ f identityʳ' {X} {Y} {f} = begin @@ -290,7 +280,7 @@ TODO u (! (coalgebras Y) {A = alg f }) ∘ i₁ {B = D₀ Y} ≈⟨ (!-unique (coalgebras Y) (record { f = (u (! (coalgebras Y) {A = alg g }) ∘ idC) ; commutes = begin α (⊤ (coalgebras Y)) ∘ u (! (coalgebras Y)) ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩ α (⊤ (coalgebras Y)) ∘ u (! (coalgebras Y)) ≈⟨ commutes (! (coalgebras Y)) ⟩ - (idC +₁ u (! (coalgebras Y))) ∘ α (alg g) ≈˘⟨ Functor.F-resp-≈ (delayF Y) identityʳ ⟩∘⟨ αf≈αg eq ⟩ + (idC +₁ u (! (coalgebras Y))) ∘ α (alg g) ≈˘⟨ Functor.F-resp-≈ (Y +-) identityʳ ⟩∘⟨ αf≈αg eq ⟩ (idC +₁ u (! (coalgebras Y)) ∘ idC) ∘ α (alg f) ∎ })) ⟩∘⟨refl ⟩ (u (! (coalgebras Y) {A = alg g }) ∘ idC) ∘ i₁ {B = D₀ Y} ≈⟨ identityʳ ⟩∘⟨refl ⟩