From ecde03dadc013b853c3dab70a5185a96087a6ab5 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Mon, 11 Sep 2023 15:57:14 +0200 Subject: [PATCH] Added iota to delay --- .gitignore | 3 +- Makefile | 2 +- src/Monad/Instance/Delay.lagda.md | 191 +++++++++++++++++++----------- 3 files changed, 126 insertions(+), 70 deletions(-) diff --git a/.gitignore b/.gitignore index dd633f2..4065994 100644 --- a/.gitignore +++ b/.gitignore @@ -1,4 +1,5 @@ *.agdai *.pdf *.log -Everything.agda \ No newline at end of file +Everything.agda +public/ \ No newline at end of file diff --git a/Makefile b/Makefile index 9908195..867e6a5 100644 --- a/Makefile +++ b/Makefile @@ -20,7 +20,7 @@ open: push: all mv public/Everything.html public/index.html - scp -r public hy84coky@cip2a7.cip.cs.fau.de:.www/public + scp -r public hy84coky@cip2a7.cip.cs.fau.de:.www/bsc-thesis Everything.agda: diff --git a/src/Monad/Instance/Delay.lagda.md b/src/Monad/Instance/Delay.lagda.md index 4044ba6..fe9283e 100644 --- a/src/Monad/Instance/Delay.lagda.md +++ b/src/Monad/Instance/Delay.lagda.md @@ -10,10 +10,12 @@ open import Categories.Category.Extensive open import Categories.Category.BinaryProducts open import Categories.Category.Cocartesian open import Categories.Category.Cartesian -open import Categories.Category.Cartesian +open import Categories.Category.Cartesian.Bundle open import Categories.Object.Terminal +open import Categories.Object.Initial open import Categories.Object.Coproduct open import Categories.Category.Construction.F-Coalgebras +open import Categories.Category.Construction.F-Algebras open import Categories.Functor.Coalgebra open import Categories.Functor open import Categories.Functor.Algebra @@ -41,11 +43,18 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ open Cartesian (ExtensiveDistributiveCategory.cartesian ED) open BinaryProducts products + CC : CartesianCategory o ℓ e + CC = record { U = C ; cartesian = (ExtensiveDistributiveCategory.cartesian ED) } + + open import Categories.Object.NaturalNumbers.Parametrized CC + open import Categories.Object.NaturalNumbers.Properties.F-Algebras using (PNNO⇒Initial₂; PNNO-Algebra) + open M C open MR C open Equiv open HomReasoning open CoLambek + open F-Coalgebra-Morphism ``` ### *Proposition 1*: Characterization of the delay monad ***D*** @@ -66,7 +75,7 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ module D A = Functor (delayF A) module _ (X : Obj) where - open Terminal (algebras X) using (⊤; !) + open Terminal (algebras X) using (⊤; !; !-unique) open F-Coalgebra ⊤ renaming (A to DX) D₀ = DX @@ -93,6 +102,17 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ coit-commutes : ∀ (f : Y ⇒ X + Y) → out ∘ (coit f) ≈ (idC +₁ coit f) ∘ f coit-commutes f = F-Coalgebra-Morphism.commutes (! {A = record { A = Y ; α = f }}) + + module _ (ℕ : ParametrizedNNO) where + open ParametrizedNNO ℕ + + iso : X × N ≅ X + X × N + iso = Lambek.lambek (record { ⊥ = PNNO-Algebra CC coproducts X N z s ; ⊥-is-initial = PNNO⇒Initial₂ CC coproducts ℕ X }) + + ι : X × N ⇒ DX + ι = f (! {A = record { A = X × N ; α = _≅_.from iso }}) + + monad : Monad C monad = Kleisli⇒Monad C (record { F₀ = D₀ @@ -117,8 +137,75 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ [ i₁ ∘ idC , i₂ ∘ (extend (now X)) ] ∘ out X ≈˘⟨ []∘+₁ ⟩∘⟨refl ⟩ ([ i₁ , i₂ ] ∘ (idC +₁ extend (now X))) ∘ out X ≈⟨ (elimˡ +-η) ⟩∘⟨refl ⟩ (idC +₁ extend (now X)) ∘ out X ∎ }) - ; assoc = {! !} - ; sym-assoc = {! !} + ; assoc = λ {X} {Y} {Z} {g} {h} → {! !} + + -- begin + -- extend (extend h ∘ g) ≈⟨ insertˡ (_≅_.isoˡ (out-≅ Z)) ⟩ + -- out⁻¹ Z ∘ out Z ∘ extend (extend h ∘ g) ≈⟨ refl⟩∘⟨ (pullˡ (commutes (! (algebras Z)))) ⟩ + -- out⁻¹ Z ∘ ((idC +₁ (f (! (algebras Z)))) ∘ F-Coalgebra.α (alg (extend h ∘ g))) ∘ i₁ ≈⟨ refl⟩∘⟨ (pullʳ inject₁) ⟩ + -- out⁻¹ Z ∘ (idC +₁ (f (! (algebras Z)))) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Z ∘ extend h ∘ g , i₂ ∘ i₁ ] ∘ out X ≈⟨ refl⟩∘⟨ pullˡ ∘[] ⟩ + -- out⁻¹ Z ∘ [ (idC +₁ (f (! (algebras Z)))) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ out Z ∘ extend h ∘ g , (idC +₁ (f (! (algebras Z)))) ∘ i₂ ∘ i₁ ] ∘ out X ≈⟨ refl⟩∘⟨ (([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl) ⟩ + -- out⁻¹ Z ∘ [ [ (idC +₁ (f (! (algebras Z)))) ∘ i₁ , (idC +₁ (f (! (algebras Z)))) ∘ i₂ ∘ i₂ ] ∘ out Z ∘ extend h ∘ g , (i₂ ∘ (f (! (algebras Z)))) ∘ i₁ ] ∘ out X ≈⟨ refl⟩∘⟨ (([]-cong₂ (([]-cong₂ (+₁∘i₁ ○ identityʳ) (pullˡ +₁∘i₂)) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩ + -- out⁻¹ Z ∘ [ [ i₁ , (i₂ ∘ (f (! (algebras Z)))) ∘ i₂ ] ∘ out Z ∘ extend h ∘ g + -- , (i₂ ∘ (f (! (algebras Z)))) ∘ i₁ + -- ] ∘ out X ≈⟨ refl⟩∘⟨ (([]-cong₂ (refl⟩∘⟨ (pullˡ (pullˡ (commutes (! (algebras Z)))))) refl) ⟩∘⟨refl) ⟩ + -- out⁻¹ Z ∘ [ [ i₁ , (i₂ ∘ (f (! (algebras Z)))) ∘ i₂ ] ∘ (((idC +₁ f (! (algebras Z))) ∘ F-Coalgebra.α (alg h)) ∘ i₁) ∘ g , (i₂ ∘ (f (! (algebras Z)))) ∘ i₁ ] ∘ out X ≈⟨ refl⟩∘⟨ (([]-cong₂ (refl⟩∘⟨ ((pullʳ inject₁) ⟩∘⟨refl)) refl) ⟩∘⟨refl) ⟩ + -- out⁻¹ Z ∘ [ [ i₁ , (i₂ ∘ (f (! (algebras Z)))) ∘ i₂ ] ∘ ((idC +₁ f (! (algebras Z))) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Z ∘ h , i₂ ∘ i₁ ] ∘ out Y) ∘ g , (i₂ ∘ (f (! (algebras Z)))) ∘ i₁ ] ∘ out X ≈⟨ refl⟩∘⟨ (([]-cong₂ (pullˡ (pullˡ []∘+₁)) refl) ⟩∘⟨refl) ⟩ + -- out⁻¹ Z ∘ [ ([ i₁ ∘ idC , ((i₂ ∘ (f (! (algebras Z)))) ∘ i₂) ∘ f (! (algebras Z)) ] ∘ ([ [ i₁ , i₂ ∘ i₂ ] ∘ out Z ∘ h , i₂ ∘ i₁ ] ∘ out Y)) ∘ g , (i₂ ∘ (f (! (algebras Z)))) ∘ i₁ ] ∘ out X ≈⟨ refl⟩∘⟨ (([]-cong₂ ((pullˡ ∘[]) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩ + -- out⁻¹ Z ∘ [ ([ [ i₁ ∘ idC , ((i₂ ∘ (f (! (algebras Z)))) ∘ i₂) ∘ f (! (algebras Z)) ] ∘ [ i₁ , i₂ ∘ i₂ ] ∘ out Z ∘ h , [ i₁ ∘ idC , ((i₂ ∘ (f (! (algebras Z)))) ∘ i₂) ∘ f (! (algebras Z)) ] ∘ i₂ ∘ i₁ ] ∘ out Y) ∘ g , (i₂ ∘ (f (! (algebras Z)))) ∘ i₁ ] ∘ out X ≈⟨ refl⟩∘⟨ (([]-cong₂ ((([]-cong₂ (pullˡ ∘[]) (pullˡ inject₂)) ⟩∘⟨refl) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩ + -- out⁻¹ Z ∘ [ ([ [ [ i₁ ∘ idC , ((i₂ ∘ (f (! (algebras Z)))) ∘ i₂) ∘ f (! (algebras Z)) ] ∘ i₁ , [ i₁ ∘ idC , ((i₂ ∘ (f (! (algebras Z)))) ∘ i₂) ∘ f (! (algebras Z)) ] ∘ i₂ ∘ i₂ ] ∘ out Z ∘ h , (((i₂ ∘ (f (! (algebras Z)))) ∘ i₂) ∘ f (! (algebras Z))) ∘ i₁ ] ∘ out Y) ∘ g , (i₂ ∘ (f (! (algebras Z)))) ∘ i₁ ] ∘ out X ≈⟨ refl⟩∘⟨ (([]-cong₂ ((([]-cong₂ (([]-cong₂ inject₁ (pullˡ inject₂)) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩ + -- out⁻¹ Z ∘ [ ([ [ i₁ ∘ idC , (((i₂ ∘ (f (! (algebras Z)))) ∘ i₂) ∘ f (! (algebras Z))) ∘ i₂ ] ∘ out Z ∘ h , (((i₂ ∘ (f (! (algebras Z)))) ∘ i₂) ∘ f (! (algebras Z))) ∘ i₁ ] ∘ out Y) ∘ g + -- , (i₂ ∘ (f (! (algebras Z)))) ∘ i₁ + -- ] ∘ out X ≈⟨ {! !} ⟩ + -- {! !} ≈⟨ {! !} ⟩ + -- {! !} ≈˘⟨ {! _○_ !} ⟩ + -- {! !} ≈˘⟨ {! !} ⟩ + -- {! !} ≈˘⟨ {! !} ⟩ + -- out⁻¹ Z ∘ [ [ [ i₁ , (i₂ ∘ f (! (algebras Z))) ∘ i₂ ] ∘ out Z ∘ h , (((i₂ ∘ f (! (algebras Z))) ∘ i₁) ∘ f (! (algebras Y))) ∘ i₂ ] ∘ out Y ∘ g + -- , (((i₂ ∘ f (! (algebras Z))) ∘ i₁) ∘ f (! (algebras Y))) ∘ i₁ + -- ] ∘ out X ≈˘⟨ refl⟩∘⟨ (([]-cong₂ (([]-cong₂ inject₁ (pullˡ inject₂)) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩ + -- out⁻¹ Z ∘ [ [ [ [ i₁ , (i₂ ∘ f (! (algebras Z))) ∘ i₂ ] ∘ out Z ∘ h , ((i₂ ∘ f (! (algebras Z))) ∘ i₁) ∘ f (! (algebras Y)) ] ∘ i₁ , [ [ i₁ , (i₂ ∘ f (! (algebras Z))) ∘ i₂ ] ∘ out Z ∘ h , ((i₂ ∘ f (! (algebras Z))) ∘ i₁) ∘ f (! (algebras Y)) ] ∘ i₂ ∘ i₂ ] ∘ out Y ∘ g + -- , (((i₂ ∘ f (! (algebras Z))) ∘ i₁) ∘ f (! (algebras Y))) ∘ i₁ ] ∘ out X ≈˘⟨ refl⟩∘⟨ (([]-cong₂ (pullˡ ∘[]) (pullˡ inject₂)) ⟩∘⟨refl) ⟩ + -- out⁻¹ Z ∘ [ [ [ i₁ , (i₂ ∘ f (! (algebras Z))) ∘ i₂ ] ∘ out Z ∘ h , ((i₂ ∘ f (! (algebras Z))) ∘ i₁) ∘ f (! (algebras Y)) ] ∘ [ i₁ , i₂ ∘ i₂ ] ∘ out Y ∘ g + -- , [ [ i₁ , (i₂ ∘ f (! (algebras Z))) ∘ i₂ ] ∘ out Z ∘ h , ((i₂ ∘ f (! (algebras Z))) ∘ i₁) ∘ f (! (algebras Y)) ] ∘ i₂ ∘ i₁ ] ∘ out X ≈˘⟨ refl⟩∘⟨ (pullˡ ∘[]) ⟩ + -- out⁻¹ Z ∘ [ [ i₁ , (i₂ ∘ f (! (algebras Z))) ∘ i₂ ] ∘ out Z ∘ h , ((i₂ ∘ f (! (algebras Z))) ∘ i₁) ∘ f (! (algebras Y)) ] ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Y ∘ g , i₂ ∘ i₁ ] ∘ out X ≈˘⟨ refl⟩∘⟨ (([]-cong₂ (([]-cong₂ (+₁∘i₁ ○ identityʳ) (pullˡ +₁∘i₂)) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩ + -- out⁻¹ Z ∘ [ [ (idC +₁ f (! (algebras Z))) ∘ i₁ , (idC +₁ f (! (algebras Z))) ∘ i₂ ∘ i₂ ] ∘ out Z ∘ h , ((i₂ ∘ f (! (algebras Z))) ∘ i₁) ∘ f (! (algebras Y)) ] ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Y ∘ g , i₂ ∘ i₁ ] ∘ out X ≈˘⟨ refl⟩∘⟨ (([]-cong₂ ((refl⟩∘⟨ identityʳ) ○ (pullˡ ∘[])) (pullˡ (pullˡ +₁∘i₂))) ⟩∘⟨refl) ⟩ + -- out⁻¹ Z ∘ [ (idC +₁ f (! (algebras Z))) ∘ ([ i₁ , i₂ ∘ i₂ ] ∘ out Z ∘ h) ∘ idC , (idC +₁ f (! (algebras Z))) ∘ (i₂ ∘ i₁) ∘ f (! (algebras Y)) ] ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Y ∘ g , i₂ ∘ i₁ ] ∘ out X ≈˘⟨ refl⟩∘⟨ (pullˡ ∘[]) ⟩ + -- out⁻¹ Z ∘ (idC +₁ f (! (algebras Z))) ∘ [ ([ i₁ , i₂ ∘ i₂ ] ∘ out Z ∘ h) ∘ idC , (i₂ ∘ i₁) ∘ f (! (algebras Y)) ] ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Y ∘ g , i₂ ∘ i₁ ] ∘ out X ≈˘⟨ refl⟩∘⟨ (refl⟩∘⟨ (pullˡ []∘+₁)) ⟩ + -- out⁻¹ Z ∘ (idC +₁ f (! (algebras Z))) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Z ∘ h , i₂ ∘ i₁ ] + -- ∘ (idC +₁ f (! (algebras Y))) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Y ∘ g , i₂ ∘ i₁ ] ∘ out X ≈˘⟨ refl⟩∘⟨ (refl⟩∘⟨ (refl⟩∘⟨ identityˡ)) ⟩ + -- out⁻¹ Z ∘ (idC +₁ f (! (algebras Z))) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Z ∘ h , i₂ ∘ i₁ ] ∘ idC + -- ∘ (idC +₁ f (! (algebras Y))) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Y ∘ g , i₂ ∘ i₁ ] ∘ out X ≈˘⟨ pullʳ (pullʳ (pullʳ (pullˡ (_≅_.isoʳ (out-≅ Y))))) ⟩ + -- (out⁻¹ Z ∘ (idC +₁ f (! (algebras Z))) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Z ∘ h , i₂ ∘ i₁ ] ∘ out Y) + -- ∘ (out⁻¹ Y ∘ (idC +₁ f (! (algebras Y))) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Y ∘ g , i₂ ∘ i₁ ] ∘ out X) ≈˘⟨ (refl⟩∘⟨ (pullʳ inject₁)) ⟩∘⟨ (refl⟩∘⟨ (pullʳ inject₁)) ⟩ + -- (out⁻¹ Z ∘ ((idC +₁ (f (! (algebras Z)))) ∘ F-Coalgebra.α (alg h)) ∘ i₁) ∘ (out⁻¹ Y ∘ ((idC +₁ (f (! (algebras Y)))) ∘ F-Coalgebra.α (alg g)) ∘ i₁) ≈˘⟨ (refl⟩∘⟨ (pullˡ (commutes (! (algebras Z))))) ⟩∘⟨ refl⟩∘⟨ (pullˡ (commutes (! (algebras Y)))) ⟩ + -- (out⁻¹ Z ∘ out Z ∘ extend h) ∘ (out⁻¹ Y ∘ out Y ∘ extend g) ≈˘⟨ ((insertˡ (_≅_.isoˡ (out-≅ Z)))) ⟩∘⟨ ((insertˡ (_≅_.isoˡ (out-≅ Y)))) ⟩ + -- extend h ∘ extend g ∎ + + + -- begin + -- extend (extend h ∘ g) ≈⟨ (insertˡ (_≅_.isoˡ (out-≅ Z))) ⟩ + -- out⁻¹ Z ∘ out Z ∘ extend (extend h ∘ g) ≈⟨ refl⟩∘⟨ extendlaw (extend h ∘ g) ⟩ + -- out⁻¹ Z ∘ [ out Z ∘ extend h ∘ g , i₂ ∘ extend (extend h ∘ g) ] ∘ out X ≈⟨ {! !} ⟩ + -- {! !} ≈⟨ {! !} ⟩ + -- {! !} ≈⟨ {! !} ⟩ + -- {! !} ≈⟨ {! !} ⟩ + -- {! !} ≈˘⟨ {! !} ⟩ + -- {! !} ≈˘⟨ {! !} ⟩ + -- out⁻¹ Z ∘ [ [ out Z ∘ h , i₂ ∘ extend h ] ∘ out Y ∘ g , (i₂ ∘ extend h) ∘ extend g ] ∘ out X ≈˘⟨ refl⟩∘⟨ (([]-cong₂ refl (pullˡ inject₂)) ⟩∘⟨refl) ⟩ + -- out⁻¹ Z ∘ [ [ out Z ∘ h , i₂ ∘ extend h ] ∘ out Y ∘ g , [ out Z ∘ h , i₂ ∘ extend h ] ∘ i₂ ∘ extend g ] ∘ out X ≈˘⟨ refl⟩∘⟨ (pullˡ ∘[]) ⟩ + -- out⁻¹ Z ∘ [ out Z ∘ h , i₂ ∘ extend h ] ∘ [ out Y ∘ g , i₂ ∘ extend g ] ∘ out X ≈˘⟨ refl⟩∘⟨ (refl⟩∘⟨ identityˡ) ⟩ + -- out⁻¹ Z ∘ [ out Z ∘ h , i₂ ∘ extend h ] ∘ idC ∘ [ out Y ∘ g , i₂ ∘ extend g ] ∘ out X ≈˘⟨ pullʳ (pullʳ (pullˡ (_≅_.isoʳ (out-≅ Y)))) ⟩ + -- (out⁻¹ Z ∘ [ out Z ∘ h , i₂ ∘ extend h ] ∘ out Y) ∘ out⁻¹ Y ∘ [ out Y ∘ g , i₂ ∘ extend g ] ∘ out X ≈˘⟨ (refl⟩∘⟨ extendlaw h) ⟩∘⟨ (refl⟩∘⟨ extendlaw g) ⟩ + -- (out⁻¹ Z ∘ out Z ∘ extend h) ∘ (out⁻¹ Y ∘ out Y ∘ extend g) ≈˘⟨ ((insertˡ (_≅_.isoˡ (out-≅ Z)))) ⟩∘⟨ ((insertˡ (_≅_.isoˡ (out-≅ Y)))) ⟩ + -- extend h ∘ extend g ∎ + + + --begin + -- f (! (algebras Z) {A = alg (extend h ∘ g)}) ∘ i₁ {A = D₀ X} {B = D₀ Z} ≈⟨ (!-unique (algebras Z) (record { f = {! (f (! (algebras Z) {A = alg h}) ∘ i₁) ∘ f (! (algebras Y) {A = alg g}) !} ; commutes = {! !} })) ⟩∘⟨refl ⟩ + -- {! !} ∘ i₁ ≈⟨ {! !} ⟩ + -- (f (! (algebras Z) {A = alg h}) ∘ i₁) ∘ f (! (algebras Y) {A = alg g}) ∘ i₁ ∎ + ; sym-assoc = λ {X} {Y} {Z} {g} {h} → {! !} ; extend-≈ = λ {X} {Y} {f} {g} eq → begin F-Coalgebra-Morphism.f (Terminal.! (algebras Y) {A = alg f }) ∘ i₁ {B = D₀ Y} ≈⟨ (Terminal.!-unique (algebras Y) (record { f = (F-Coalgebra-Morphism.f (Terminal.! (algebras Y) {A = alg g }) ∘ idC) ; commutes = begin F-Coalgebra.α (Terminal.⊤ (algebras Y)) ∘ F-Coalgebra-Morphism.f (Terminal.! (algebras Y)) ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩ @@ -129,29 +216,47 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ extend g ∎ }) where + open Terminal alg' : ∀ {X Y} → F-Coalgebra (delayF Y) alg' {X} {Y} = record { A = D₀ X ; α = i₂ } module _ {X Y : Obj} (f : X ⇒ D₀ Y) where - open Terminal (algebras Y) using (!; ⊤-id) + -- open Terminal (algebras Y) using (!; ⊤-id) alg : F-Coalgebra (delayF Y) alg = record { A = D₀ X + D₀ Y ; α = [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ i₂) ∘ out Y ] } -- (idC +₁ (idC +₁ [ idC , idC ]) ∘ _≅_.to +-assoc ∘ _≅_.to +-comm) extend : D₀ X ⇒ D₀ Y - extend = F-Coalgebra-Morphism.f (! {A = alg}) ∘ i₁ {B = D₀ Y} - !∘i₂ : F-Coalgebra-Morphism.f (! {A = alg}) ∘ i₂ ≈ idC - !∘i₂ = ⊤-id (F-Coalgebras (delayF Y) [ ! ∘ record { f = i₂ ; commutes = inject₂ } ] ) + extend = F-Coalgebra-Morphism.f (! (algebras Y) {A = alg}) ∘ i₁ {B = D₀ Y} + !∘i₂ : F-Coalgebra-Morphism.f (! (algebras Y) {A = alg}) ∘ i₂ ≈ idC + !∘i₂ = ⊤-id (algebras Y) (F-Coalgebras (delayF Y) [ ! (algebras Y) ∘ record { f = i₂ ; commutes = inject₂ } ] ) extendlaw : out Y ∘ extend ≈ [ out Y ∘ f , i₂ ∘ extend ] ∘ out X extendlaw = begin - out Y ∘ extend ≈⟨ pullˡ (F-Coalgebra-Morphism.commutes (! {A = alg})) ⟩ - ((idC +₁ (F-Coalgebra-Morphism.f !)) ∘ F-Coalgebra.α alg) ∘ coproduct.i₁ ≈⟨ pullʳ inject₁ ⟩ - (idC +₁ (F-Coalgebra-Morphism.f !)) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X ≈⟨ pullˡ ∘[] ⟩ - [ (idC +₁ (F-Coalgebra-Morphism.f !)) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) - , (idC +₁ (F-Coalgebra-Morphism.f !)) ∘ i₂ ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl ⟩ - [ [ (idC +₁ (F-Coalgebra-Morphism.f !)) ∘ i₁ - , (idC +₁ (F-Coalgebra-Morphism.f !)) ∘ i₂ ∘ i₂ ] ∘ (out Y ∘ f) - , (i₂ ∘ (F-Coalgebra-Morphism.f !)) ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ (([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl) refl) ⟩∘⟨refl ⟩ - [ [ i₁ ∘ idC , (i₂ ∘ (F-Coalgebra-Morphism.f !)) ∘ i₂ ] ∘ (out Y ∘ f) - , (i₂ ∘ (F-Coalgebra-Morphism.f !)) ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ (elimˡ (([]-cong₂ identityʳ (cancelʳ !∘i₂)) ○ +-η)) assoc) ⟩∘⟨refl ⟩ + out Y ∘ extend ≈⟨ pullˡ (F-Coalgebra-Morphism.commutes (! (algebras Y) {A = alg})) ⟩ + ((idC +₁ (F-Coalgebra-Morphism.f (! (algebras Y)))) ∘ F-Coalgebra.α alg) ∘ coproduct.i₁ ≈⟨ pullʳ inject₁ ⟩ + (idC +₁ (F-Coalgebra-Morphism.f (! (algebras Y)))) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X ≈⟨ pullˡ ∘[] ⟩ + [ (idC +₁ (F-Coalgebra-Morphism.f (! (algebras Y)))) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) + , (idC +₁ (F-Coalgebra-Morphism.f (! (algebras Y)))) ∘ i₂ ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl ⟩ + [ [ (idC +₁ (F-Coalgebra-Morphism.f (! (algebras Y)))) ∘ i₁ + , (idC +₁ (F-Coalgebra-Morphism.f (! (algebras Y)))) ∘ i₂ ∘ i₂ ] ∘ (out Y ∘ f) + , (i₂ ∘ (F-Coalgebra-Morphism.f (! (algebras Y)))) ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ (([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl) refl) ⟩∘⟨refl ⟩ + [ [ i₁ ∘ idC , (i₂ ∘ (F-Coalgebra-Morphism.f (! (algebras Y)))) ∘ i₂ ] ∘ (out Y ∘ f) + , (i₂ ∘ (F-Coalgebra-Morphism.f (! (algebras Y)))) ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ (elimˡ (([]-cong₂ identityʳ (cancelʳ !∘i₂)) ○ +-η)) assoc) ⟩∘⟨refl ⟩ [ out Y ∘ f , i₂ ∘ extend ] ∘ out X ∎ + extend-unique : (g : D₀ X ⇒ D₀ Y) → extend ≈ g + extend-unique g = {! !} + -- begin + -- F-Coalgebra-Morphism.f (! (algebras Y) {A = alg}) ∘ i₁ {B = D₀ Y} ≈⟨ (!-unique (algebras Y) (record { f = [ g , idC ] ; commutes = begin + -- out Y ∘ [ g , idC ] ≈⟨ ∘[] ⟩ + -- [ out Y ∘ g , out Y ∘ idC ] ≈⟨ []-cong₂ {! !} identityʳ ⟩ + -- {! !} ≈˘⟨ {! !} ⟩ + -- [ ([ out Y , i₂ ] ∘ (f +₁ g)) ∘ out X , out Y ] ≈˘⟨ []-cong₂ (sym []∘+₁ ⟩∘⟨refl) refl ⟩ + -- [ [ out Y ∘ f , i₂ ∘ g ] ∘ out X , out Y ] ≈˘⟨ {! !} ⟩ + -- [ [ [ i₁ , i₂ ∘ idC ] ∘ (out Y ∘ f) , i₂ ∘ g ] ∘ out X , out Y ] ≈˘⟨ []-cong₂ (([]-cong₂ (([]-cong₂ identityʳ (pullʳ inject₂)) ⟩∘⟨refl) refl) ⟩∘⟨refl) refl ⟩ + -- [ [ [ i₁ ∘ idC , (i₂ ∘ [ g , idC ]) ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ g ] ∘ out X , out Y ] ≈˘⟨ []-cong₂ (([]-cong₂ (([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl) (pullʳ inject₁)) ⟩∘⟨refl) (elimˡ (Functor.identity (delayF Y))) ⟩ + -- [ [ [ (idC +₁ [ g , idC ]) ∘ i₁ , (idC +₁ [ g , idC ]) ∘ i₂ ∘ i₂ ] ∘ (out Y ∘ f) , (i₂ ∘ [ g , idC ]) ∘ i₁ ] ∘ out X , (idC +₁ idC) ∘ out Y ] ≈˘⟨ []-cong₂ (([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl) ((+₁-cong₂ identity² inject₂) ⟩∘⟨refl) ⟩ + -- [ [ (idC +₁ [ g , idC ]) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , (idC +₁ [ g , idC ]) ∘ i₂ ∘ i₁ ] ∘ out X , (idC ∘ idC +₁ [ g , idC ] ∘ i₂) ∘ out Y ] ≈˘⟨ []-cong₂ (pullˡ ∘[]) (pullˡ +₁∘+₁) ⟩ + -- [ (idC +₁ [ g , idC ]) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ [ g , idC ]) ∘ (idC +₁ i₂) ∘ out Y ] ≈˘⟨ ∘[] ⟩ + -- (idC +₁ [ g , idC ]) ∘ F-Coalgebra.α alg ∎ })) ⟩∘⟨refl ⟩ + -- [ g , idC ] ∘ i₁ ≈⟨ inject₁ ⟩ + -- g ∎ αf≈αg : ∀ {X Y} {f g : X ⇒ D₀ Y} → f ≈ g → F-Coalgebra.α (alg f) ≈ F-Coalgebra.α (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) @@ -173,56 +278,6 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ } ``` -### Old definitions: - -```agda - record DelayMonad : Set (o ⊔ ℓ ⊔ e) where - field - D₀ : Obj → Obj - - field - now : ∀ {X} → X ⇒ D₀ X - later : ∀ {X} → D₀ X ⇒ D₀ X - isIso : ∀ {X} → IsIso ([ now {X} , later {X} ]) - - out : ∀ {X} → D₀ X ⇒ X + D₀ X - out {X} = IsIso.inv (isIso {X}) - - field - coit : ∀ {X Y} → Y ⇒ X + Y → Y ⇒ D₀ X - coit-law : ∀ {X Y} {f : Y ⇒ X + Y} → out ∘ (coit f) ≈ (idC +₁ (coit f)) ∘ f - - field - _* : ∀ {X Y} → X ⇒ D₀ Y → D₀ X ⇒ D₀ Y - *-law : ∀ {X Y} {f : X ⇒ D₀ Y} → out ∘ (f *) ≈ [ out ∘ f , i₂ ∘ (f *) ] ∘ out - *-unique : ∀ {X Y} (f : X ⇒ D₀ Y) (h : D₀ X ⇒ D₀ Y) → h ≈ f * - *-resp-≈ : ∀ {X Y} {f h : X ⇒ D₀ Y} → f ≈ h → f * ≈ h * - - unitLaw : ∀ {X} → out {X} ∘ now {X} ≈ i₁ - unitLaw = begin - out ∘ now ≈⟨ refl⟩∘⟨ sym inject₁ ⟩ - out ∘ [ now , later ] ∘ i₁ ≈⟨ cancelˡ (IsIso.isoˡ isIso) ⟩ - i₁ ∎ - - toMonad : KleisliTriple C - toMonad = record - { F₀ = D₀ - ; unit = now - ; extend = _* - ; identityʳ = λ {X} {Y} {k} → begin - k * ∘ now ≈⟨ introˡ (IsIso.isoʳ isIso) ⟩∘⟨refl ⟩ - (([ now , later ] ∘ out) ∘ k *) ∘ now ≈⟨ pullʳ *-law ⟩∘⟨refl ⟩ - ([ now , later ] ∘ [ out ∘ k , i₂ ∘ (k *) ] ∘ out) ∘ now ≈⟨ pullʳ (pullʳ unitLaw) ⟩ - [ now , later ] ∘ [ out ∘ k , i₂ ∘ (k *) ] ∘ i₁ ≈⟨ refl⟩∘⟨ inject₁ ⟩ - [ now , later ] ∘ out ∘ k ≈⟨ cancelˡ (IsIso.isoʳ isIso) ⟩ - k ∎ - ; identityˡ = λ {X} → sym (*-unique now idC) - ; assoc = λ {X} {Y} {Z} {f} {g} → sym (*-unique ((g *) ∘ f) ((g *) ∘ (f *))) - ; sym-assoc = λ {X} {Y} {Z} {f} {g} → *-unique ((g *) ∘ f) ((g *) ∘ (f *)) - ; extend-≈ = *-resp-≈ - } -``` - ### Definition 30: Search-Algebras TODO