This file introduces (guarded) elgot algebras
module ElgotAlgebra where diff --git a/public/ElgotAlgebras.html b/public/ElgotAlgebras.html index ad65c42..e602a6c 100644 --- a/public/ElgotAlgebras.html +++ b/public/ElgotAlgebras.html @@ -11,8 +11,11 @@ div.columns{display: flex; gap: min(4vw, 1.5em);} div.column{flex: auto; overflow-x: auto;} div.hanging-indent{margin-left: 1.5em; text-indent: -1.5em;} - ul.task-list{list-style: none;} + /* The extra [class] is a hack that increases specificity enough to + override a similar rule in reveal.js */ + ul.task-list[class]{list-style: none;} ul.task-list li input[type="checkbox"] { + font-size: inherit; width: 0.8em; margin: 0 0.8em 0.2em -1.6em; vertical-align: middle; @@ -48,12 +51,12 @@This file introduces the category of unguarded elgot algebras
module ElgotAlgebras where diff --git a/public/Monad.ElgotMonad.html b/public/Monad.ElgotMonad.html index 4df0531..628c103 100644 --- a/public/Monad.ElgotMonad.html +++ b/public/Monad.ElgotMonad.html @@ -11,8 +11,11 @@ div.columns{display: flex; gap: min(4vw, 1.5em);} div.column{flex: auto; overflow-x: auto;} div.hanging-indent{margin-left: 1.5em; text-indent: -1.5em;} - ul.task-list{list-style: none;} + /* The extra [class] is a hack that increases specificity enough to + override a similar rule in reveal.js */ + ul.task-list[class]{list-style: none;} ul.task-list li input[type="checkbox"] { + font-size: inherit; width: 0.8em; margin: 0 0.8em 0.2em -1.6em; vertical-align: middle; @@ -44,16 +47,16 @@Summary
This file introduces Elgot Monads.
module Monad.ElgotMonad {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) where diff --git a/public/Monad.Instance.Delay.html b/public/Monad.Instance.Delay.html index 21d3ca7..3765c49 100644 --- a/public/Monad.Instance.Delay.html +++ b/public/Monad.Instance.Delay.html @@ -11,8 +11,11 @@ div.columns{display: flex; gap: min(4vw, 1.5em);} div.column{flex: auto; overflow-x: auto;} div.hanging-indent{margin-left: 1.5em; text-indent: -1.5em;} - ul.task-list{list-style: none;} + /* The extra [class] is a hack that increases specificity enough to + override a similar rule in reveal.js */ + ul.task-list[class]{list-style: none;} ul.task-list li input[type="checkbox"] { + font-size: inherit; width: 0.8em; margin: 0 0.8em 0.2em -1.6em; vertical-align: middle; @@ -26,136 +29,230 @@Summary
This file introduces the delay monad D
module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) where - open ExtensiveDistributiveCategory ED renaming (U to C; id to idC) - open Cocartesian (Extensive.cocartesian extensive) - open Cartesian (ExtensiveDistributiveCategory.cartesian ED) - open BinaryProducts products +module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) where + open ExtensiveDistributiveCategory ED renaming (U to C; id to idC) + open Cocartesian (Extensive.cocartesian extensive) + open Cartesian (ExtensiveDistributiveCategory.cartesian ED) + open BinaryProducts products - open M C - open MR C - open Equiv - open HomReasoning - open CoLambek + open M C + open MR C + open Equiv + open HomReasoning + open CoLambekProposition 1: Characterization of the delay monad D
-First I postulate the Functor D, maybe I should derive it… -TODO: - how to define using final coalgebra(s)? - DX -can be defined as retract of infinite streams, how? - how to express -Theorem 8 in agda?
-record DelayFunctor : Set (o ⊔ ℓ ⊔ e) where - field - D : Endofunctor C +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 + } - open Functor D public renaming (F₀ to D₀; F₁ to D₁) + record DelayM : Set (o ⊔ ℓ ⊔ e) where + field + algebras : ∀ (A : Obj) → Terminal (F-Coalgebras (delayF A)) + + module D A = Functor (delayF A) - field - now : ∀ {X} → X ⇒ D₀ X - later : ∀ {X} → D₀ X ⇒ D₀ X - isIso : ∀ {X} → IsIso [ now {X} , later {X} ] + module _ (X : Obj) where + open Terminal (algebras X) using (⊤; !) + open F-Coalgebra ⊤ renaming (A to DX) - out : ∀ {X} → D₀ X ⇒ X + D₀ X - out {X} = IsIso.inv (isIso {X}) + D₀ = DX - 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 + out-≅ : DX ≅ X + DX + out-≅ = colambek {F = delayF X} (algebras X) + + -- note: out-≅.from ≡ ⊤.α + open _≅_ out-≅ using () renaming (to to out⁻¹; from to out) public + + now : X ⇒ DX + now = out⁻¹ ∘ i₁ + + later : DX ⇒ DX + later = out⁻¹ ∘ i₂ + + -- TODO inline + unitlaw : out ∘ now ≈ i₁ + unitlaw = cancelˡ (_≅_.isoʳ out-≅) + + module _ {Y : Obj} where + coit : Y ⇒ X + Y → Y ⇒ DX + coit f = F-Coalgebra-Morphism.f (! {A = record { A = Y ; α = f }}) + + 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 }}) + + monad : Monad C + monad = Kleisli⇒Monad C (record + { F₀ = D₀ + ; unit = λ {X} → now X + ; extend = extend + ; identityʳ = λ {X} {Y} {f} → begin + extend f ∘ now X ≈⟨ (insertˡ (_≅_.isoˡ (out-≅ Y))) ⟩∘⟨refl ⟩ + (out⁻¹ Y ∘ out Y ∘ extend f) ∘ now X ≈⟨ (refl⟩∘⟨ (extendlaw f)) ⟩∘⟨refl ⟩ + (out⁻¹ Y ∘ [ out Y ∘ f , i₂ ∘ extend f ] ∘ out X) ∘ now X ≈⟨ pullʳ (pullʳ (unitlaw X)) ⟩ + out⁻¹ Y ∘ [ out Y ∘ f , i₂ ∘ extend f ] ∘ i₁ ≈⟨ refl⟩∘⟨ inject₁ ⟩ + out⁻¹ Y ∘ out Y ∘ f ≈⟨ cancelˡ (_≅_.isoˡ (out-≅ Y)) ⟩ + f ∎ + ; identityˡ = λ {X} → Terminal.⊤-id (algebras X) (record { f = extend (now X) ; commutes = begin + out X ∘ extend (now X) ≈⟨ pullˡ ((F-Coalgebra-Morphism.commutes (Terminal.! (algebras X) {A = alg (now X)}))) ⟩ + ((idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras X) {A = alg (now X)}))) ∘ F-Coalgebra.α (alg (now X))) ∘ i₁ ≈⟨ pullʳ inject₁ ⟩ + (idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras X) {A = alg (now X)}))) + ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out X ∘ (now X)) , i₂ ∘ i₁ ] ∘ out X ≈⟨ refl⟩∘⟨ []-cong₂ ((refl⟩∘⟨ (unitlaw X)) ○ inject₁) refl ⟩∘⟨refl ⟩ + (idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras X) {A = alg (now X)}))) ∘ [ i₁ , i₂ ∘ i₁ ] ∘ out X ≈⟨ pullˡ ∘[] ⟩ + [ (idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras X) {A = alg (now X)}))) ∘ i₁ + , (idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras X) {A = alg (now X)}))) ∘ i₂ ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl ⟩ + [ i₁ ∘ idC , (i₂ ∘ (F-Coalgebra-Morphism.f (Terminal.! (algebras X) {A = alg (now X)}))) ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ refl assoc) ⟩∘⟨refl ⟩ + [ 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 = {! !} + ; extend-≈ = λ {X} {Y} {f} {g} eq → {! !} + + -- begin + -- extend f ≈⟨ sym (Terminal.!-unique (algebras Y) (record { f = extend f ; commutes = F-Coalgebra-Morphism.commutes {! !} })) ⟩ + -- F-Coalgebra-Morphism.f ((Terminal.! (algebras Y) {A = alg' {X} {Y}})) ≈˘⟨ sym (Terminal.!-unique (algebras Y) (record { f = extend g ; commutes = {! !} })) ⟩ + -- extend g ∎ + + -- let + -- h : F-Coalgebra-Morphism (alg f) (alg g) + -- h = record { f = idC ; commutes = begin + -- F-Coalgebra.α (alg g) ∘ idC ≈⟨ id-comm ⟩ + -- idC ∘ F-Coalgebra.α (alg g) ≈⟨ refl⟩∘⟨ []-cong₂ (([]-cong₂ (refl⟩∘⟨ (refl⟩∘⟨ (sym eq))) refl) ⟩∘⟨refl) refl ⟩ + -- idC ∘ F-Coalgebra.α (alg f) ≈˘⟨ ([]-cong₂ identityʳ identityʳ ○ +-η) ⟩∘⟨refl ⟩ + -- (idC +₁ idC) ∘ F-Coalgebra.α (alg f) ∎ } + -- x : F-Coalgebra-Morphism (alg f) (Terminal.⊤ (algebras Y)) + -- x = (F-Coalgebras (delayF Y)) [ Terminal.! (algebras Y) ∘ h ] + -- in Terminal.!-unique₂ (algebras Y) {f = Terminal.! (algebras Y)} {g = {! !} } ⟩∘⟨refl + + -- extend f ≈⟨ insertˡ (_≅_.isoˡ (out-≅ Y)) ⟩ + -- out⁻¹ Y ∘ out Y ∘ extend f ≈⟨ refl⟩∘⟨ pullˡ (F-Coalgebra-Morphism.commutes (Terminal.! (algebras Y) {A = alg f})) ⟩ + -- out⁻¹ Y ∘ ((idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras Y)))) ∘ [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ i₂) ∘ out Y ]) ∘ i₁ ≈⟨ refl⟩∘⟨ ((+₁-cong₂ refl (Terminal.!-unique₂ (algebras Y) {f = Terminal.! (algebras Y) {A = alg f}} {g = Terminal.! (algebras Y) {A = alg f}}) ⟩∘⟨ ([]-cong₂ (([]-cong₂ (refl⟩∘⟨ (refl⟩∘⟨ eq)) refl) ⟩∘⟨refl) refl)) ⟩∘⟨refl) ⟩ + -- out⁻¹ Y ∘ ((idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras Y)))) ∘ [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ g) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ i₂) ∘ out Y ]) ∘ i₁ ≈⟨ refl⟩∘⟨ (((+₁-cong₂ refl (Terminal.!-unique₂ (algebras Y) {f = Terminal.! (algebras Y)} {g = record { f = F-Coalgebra-Morphism.f (Terminal.! (algebras Y)) ; commutes = {! !} }})) ⟩∘⟨refl) ⟩∘⟨refl) ⟩ + -- out⁻¹ Y ∘ ((idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras Y)))) ∘ [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ g) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ i₂) ∘ out Y ]) ∘ i₁ ≈˘⟨ refl⟩∘⟨ pullˡ (F-Coalgebra-Morphism.commutes (Terminal.! (algebras Y) {A = alg g})) ⟩ + -- out⁻¹ Y ∘ out Y ∘ extend g ≈˘⟨ insertˡ (_≅_.isoˡ (out-≅ Y)) ⟩ + -- extend g ∎ + }) + where + 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) + 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₂ } ] ) + 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 ∘ f , i₂ ∘ extend ] ∘ out X ∎-Now let’s define the monad:
-record DelayMonad : Set (o ⊔ ℓ ⊔ e) where - field - D : DelayFunctor - open DelayFunctor D +Old definitions:
+record DelayMonad : Set (o ⊔ ℓ ⊔ e) where + field + D₀ : Obj → Obj - 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 * + field + now : ∀ {X} → X ⇒ D₀ X + later : ∀ {X} → D₀ X ⇒ D₀ X + isIso : ∀ {X} → IsIso ([ now {X} , later {X} ]) - unitLaw : ∀ {X} → out {X} ∘ now {X} ≈ i₁ - unitLaw = begin - out ∘ now ≈⟨ refl⟩∘⟨ sym inject₁ ⟩ - out ∘ [ now , later ] ∘ i₁ ≈⟨ cancelˡ (IsIso.isoˡ isIso) ⟩ - i₁ ∎ + out : ∀ {X} → D₀ X ⇒ X + D₀ X + out {X} = IsIso.inv (isIso {X}) - 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-≈ - } + 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
-record SearchAlgebra (DF : DelayFunctor) : Set (o ⊔ ℓ ⊔ e) where - open DelayFunctor DF - - field - FA : F-Algebra D - - open F-Algebra FA - - field - now-id : α ∘ now ≈ idC - later-same : α ∘ later ≈ α -+TODO
Proposition 31 : the category of uniform-iteration algebras coincides with the category of search-algebras
-TODOs:
-
record SearchAlgebras (DF : DelayFunctor) : Set (o ⊔ ℓ ⊔ e) where - open DelayFunctor DF -+
TODO