diff --git a/Makefile b/Makefile index 867e6a5..02aca67 100644 --- a/Makefile +++ b/Makefile @@ -20,7 +20,10 @@ open: push: all mv public/Everything.html public/index.html - scp -r public hy84coky@cip2a7.cip.cs.fau.de:.www/bsc-thesis + chmod +w public/Agda.css + mv public bsc-thesis + scp -r bsc-thesis hy84coky@cip2a7.cip.cs.fau.de:.www/ + mv bsc-thesis public Everything.agda: diff --git a/src/Monad/Instance/Delay.lagda.md b/src/Monad/Instance/Delay.lagda.md index 14ee386..deca1bd 100644 --- a/src/Monad/Instance/Delay.lagda.md +++ b/src/Monad/Instance/Delay.lagda.md @@ -1,6 +1,5 @@ + +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 @@ -68,21 +69,32 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ ; homomorphism = ⟺ (+₁∘+₁ ○ +₁-cong₂ identity² refl) ; F-resp-≈ = +₁-cong₂ refl } +``` +Using this functor we can define the delay monad ***D***: + +```agda record DelayM : Set (o ⊔ ℓ ⊔ e) where field - algebras : ∀ (A : Obj) → Terminal (F-Coalgebras (delayF A)) - - module D A = Functor (delayF A) + coalgebras : ∀ (A : Obj) → Terminal (F-Coalgebras (delayF A)) +``` + +These are all the fields this record needs! +Of course this doesn't tell us very much, so our goal will be to extract a monad from this definition. + +Conventionally the delay monad is described via functions `now` and `later` where the former lifts a value into a computation and the latter postpones a computation by one time unit. +We can now define these functions by bisecting the isomorphism `out : DX ≅ X + DX` which we get by Lambek's lemma. (Here `DX` is the element of the final coalgebra for `X`) + +```agda module _ (X : Obj) where - open Terminal (algebras X) using (⊤; !; !-unique) + open Terminal (coalgebras X) using (⊤; !; !-unique) open F-Coalgebra ⊤ renaming (A to DX) D₀ = DX out-≅ : DX ≅ X + DX - out-≅ = colambek {F = delayF X} (algebras X) + out-≅ = colambek {F = delayF X} (coalgebras X) -- note: out-≅.from ≡ ⊤.α open _≅_ out-≅ using () renaming (to to out⁻¹; from to out) public @@ -95,14 +107,24 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ unitlaw : out ∘ now ≈ i₁ 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 +```agda module _ {Y : Obj} where coit : Y ⇒ X + Y → Y ⇒ DX coit f = u (! {A = record { A = Y ; α = f }}) coit-commutes : ∀ (f : Y ⇒ X + Y) → out ∘ (coit f) ≈ (idC +₁ coit f) ∘ f 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. +TODO add diagram + +```agda module _ (ℕ : ParametrizedNNO) where open ParametrizedNNO ℕ @@ -111,7 +133,15 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ ι : X × N ⇒ DX ι = u (! {A = record { A = X × N ; α = _≅_.from iso }}) +``` +With these definitions at hand, we can now indeed construct a monad (in extension form) as the triple `(F₀, unit, extend)`. +`F₀` corresponds to `D₀` of course and `unit` is `now`, the tricky part is kleisli lifting aka. `extend`. + +TODO + + +```agda monad : Monad C monad = Kleisli⇒Monad C (record @@ -131,33 +161,33 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ 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 (! (algebras Y) {A = alg}) ∘ i₁ {B = D₀ Y} + extend = u (! (coalgebras Y) {A = alg}) ∘ i₁ {B = D₀ Y} - !∘i₂ : u (! (algebras Y) {A = alg}) ∘ i₂ ≈ idC - !∘i₂ = ⊤-id (algebras Y) (F-Coalgebras (delayF Y) [ ! (algebras Y) ∘ record { f = i₂ ; commutes = inject₂ } ] ) + !∘i₂ : u (! (coalgebras Y) {A = alg}) ∘ i₂ ≈ idC + !∘i₂ = ⊤-id (coalgebras Y) (F-Coalgebras (delayF Y) [ ! (coalgebras Y) ∘ record { f = i₂ ; commutes = inject₂ } ] ) extendlaw : out Y ∘ extend ≈ [ out Y ∘ f , i₂ ∘ extend ] ∘ out X extendlaw = begin - out Y ∘ extend ≈⟨ pullˡ (commutes (! (algebras Y) {A = alg})) ⟩ - ((idC +₁ (u (! (algebras Y)))) ∘ α alg) ∘ i₁ ≈⟨ pullʳ inject₁ ⟩ - (idC +₁ (u (! (algebras Y)))) ∘ [ [ i₁ , i₂ ∘ i₂ ] + out Y ∘ extend ≈⟨ pullˡ (commutes (! (coalgebras Y) {A = alg})) ⟩ + ((idC +₁ (u (! (coalgebras Y)))) ∘ α alg) ∘ i₁ ≈⟨ pullʳ inject₁ ⟩ + (idC +₁ (u (! (coalgebras Y)))) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X ≈⟨ pullˡ ∘[] ⟩ - [ (idC +₁ (u (! (algebras Y)))) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) - , (idC +₁ (u (! (algebras Y)))) ∘ i₂ ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl ⟩ - [ [ (idC +₁ (u (! (algebras Y)))) ∘ i₁ - , (idC +₁ (u (! (algebras Y)))) ∘ i₂ ∘ i₂ ] ∘ (out Y ∘ f) - , (i₂ ∘ (u (! (algebras Y)))) ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ + [ (idC +₁ (u (! (coalgebras Y)))) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) + , (idC +₁ (u (! (coalgebras Y)))) ∘ i₂ ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl ⟩ + [ [ (idC +₁ (u (! (coalgebras Y)))) ∘ i₁ + , (idC +₁ (u (! (coalgebras Y)))) ∘ i₂ ∘ i₂ ] ∘ (out Y ∘ f) + , (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ (([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl) refl) ⟩∘⟨refl ⟩ - [ [ i₁ ∘ idC , (i₂ ∘ (u (! (algebras Y)))) ∘ i₂ ] ∘ (out Y ∘ f) - , (i₂ ∘ (u (! (algebras Y)))) ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ + [ [ i₁ ∘ idC , (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₂ ] ∘ (out Y ∘ f) + , (i₂ ∘ (u (! (coalgebras 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) → (out Y ∘ g ≈ [ out Y ∘ f , i₂ ∘ g ] ∘ out X) → extend ≈ g extend-unique g g-commutes = begin - extend ≈⟨ (!-unique (algebras Y) (record { f = [ g , idC ] ; commutes = begin + extend ≈⟨ (!-unique (coalgebras Y) (record { f = [ g , idC ] ; commutes = begin out Y ∘ [ g , idC ] ≈⟨ ∘[] ⟩ [ out Y ∘ g , out Y ∘ idC ] ≈⟨ []-cong₂ g-commutes identityʳ ⟩ [ [ out Y ∘ f , i₂ ∘ g ] ∘ out X , out Y ] ≈˘⟨ []-cong₂ @@ -232,15 +262,15 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ f ∎ identityˡ' : ∀ {X} → extend (now X) ≈ idC - identityˡ' {X} = Terminal.⊤-id (algebras X) (record { f = extend (now X) ; commutes = begin - out X ∘ extend (now X) ≈⟨ pullˡ ((commutes (! (algebras X) {A = alg (now X)}))) ⟩ - ((idC +₁ (u (! (algebras X) {A = alg (now X)}))) ∘ α (alg (now X))) ∘ i₁ ≈⟨ pullʳ inject₁ ⟩ - (idC +₁ (u (! (algebras X) {A = alg (now X)}))) + identityˡ' {X} = Terminal.⊤-id (coalgebras X) (record { f = extend (now X) ; commutes = begin + out X ∘ extend (now X) ≈⟨ pullˡ ((commutes (! (coalgebras X) {A = alg (now X)}))) ⟩ + ((idC +₁ (u (! (coalgebras X) {A = alg (now X)}))) ∘ α (alg (now X))) ∘ i₁ ≈⟨ pullʳ inject₁ ⟩ + (idC +₁ (u (! (coalgebras 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 +₁ (u (! (algebras X) {A = alg (now X)}))) ∘ [ i₁ , i₂ ∘ i₁ ] ∘ out X ≈⟨ pullˡ ∘[] ⟩ - [ (idC +₁ (u (! (algebras X) {A = alg (now X)}))) ∘ i₁ - , (idC +₁ (u (! (algebras X) {A = alg (now X)}))) ∘ i₂ ∘ i₁ ] ∘ out X ≈⟨ []-cong₂ +₁∘i₁ (pullˡ +₁∘i₂) ⟩∘⟨refl ⟩ - [ i₁ ∘ idC , (i₂ ∘ (u (! (algebras X) {A = alg (now X)}))) ∘ i₁ ] ∘ out X ≈⟨ []-cong₂ refl assoc ⟩∘⟨refl ⟩ + (idC +₁ (u (! (coalgebras X) {A = alg (now X)}))) ∘ [ i₁ , i₂ ∘ i₁ ] ∘ out X ≈⟨ pullˡ ∘[] ⟩ + [ (idC +₁ (u (! (coalgebras X) {A = alg (now X)}))) ∘ i₁ + , (idC +₁ (u (! (coalgebras X) {A = alg (now X)}))) ∘ i₂ ∘ i₁ ] ∘ out X ≈⟨ []-cong₂ +₁∘i₁ (pullˡ +₁∘i₂) ⟩∘⟨refl ⟩ + [ i₁ ∘ idC , (i₂ ∘ (u (! (coalgebras 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 ∎ }) @@ -257,13 +287,13 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ extend-≈' : ∀ {X} {Y} {f g : X ⇒ D₀ Y} → f ≈ g → extend f ≈ extend g extend-≈' {X} {Y} {f} {g} eq = begin - u (! (algebras Y) {A = alg f }) ∘ i₁ {B = D₀ Y} ≈⟨ (!-unique (algebras Y) (record { f = (u (! (algebras Y) {A = alg g }) ∘ idC) ; commutes = begin - α (⊤ (algebras Y)) ∘ u (! (algebras Y)) ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩ - α (⊤ (algebras Y)) ∘ u (! (algebras Y)) ≈⟨ commutes (! (algebras Y)) ⟩ - (idC +₁ u (! (algebras Y))) ∘ α (alg g) ≈˘⟨ Functor.F-resp-≈ (delayF Y) identityʳ ⟩∘⟨ αf≈αg eq ⟩ - (idC +₁ u (! (algebras Y)) ∘ idC) ∘ α (alg f) ∎ })) + 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)) ∘ idC) ∘ α (alg f) ∎ })) ⟩∘⟨refl ⟩ - (u (! (algebras Y) {A = alg g }) ∘ idC) ∘ i₁ {B = D₀ Y} ≈⟨ identityʳ ⟩∘⟨refl ⟩ + (u (! (coalgebras Y) {A = alg g }) ∘ idC) ∘ i₁ {B = D₀ Y} ≈⟨ identityʳ ⟩∘⟨refl ⟩ extend g ∎ ``` @@ -271,6 +301,6 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ TODO -### Proposition 31 : the category of uniform-iteration algebras coincides with the category of search-algebras +### Proposition 31 : the category of uniform-iteration coalgebras coincides with the category of search-coalgebras TODO