From 55dcf598fc9100a13e6811ce8df39bb3569ee41b Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Wed, 15 Nov 2023 19:25:35 +0100 Subject: [PATCH] Show that K is initial pre-Elgot --- src/Monad/ElgotMonad.lagda.md | 9 ++- src/Monad/Instance/K/PreElgot.lagda.md | 104 +++++++++++++++++++++++-- 2 files changed, 102 insertions(+), 11 deletions(-) diff --git a/src/Monad/ElgotMonad.lagda.md b/src/Monad/ElgotMonad.lagda.md index fd37d0e..b0d86f1 100644 --- a/src/Monad/ElgotMonad.lagda.md +++ b/src/Monad/ElgotMonad.lagda.md @@ -4,7 +4,9 @@ open import Level open import Category.Instance.AmbientCategory using (Ambient) +open import Categories.Monad.Construction.Kleisli open import Categories.Monad +open import Categories.Monad.Relative renaming (Monad to RMonad) open import Categories.Functor ``` --> @@ -36,6 +38,7 @@ module Monad.ElgotMonad {o ℓ e} (ambient : Ambient o ℓ e) where ```agda record IsPreElgot (T : Monad C) : Set (o ⊔ ℓ ⊔ e) where open Monad T + open RMonad (Monad⇒Kleisli C T) using (extend) open Functor F renaming (F₀ to T₀; F₁ to T₁) -- every TX needs to be equipped with an elgot algebra structure @@ -46,8 +49,8 @@ module Monad.ElgotMonad {o ℓ e} (ambient : Ambient o ℓ e) where -- with the following associativity field - assoc : ∀ {X Y Z} (f : Z ⇒ T₀ X + Z) (h : X ⇒ T₀ Y) - → elgotalgebras._# (((μ.η _ ∘ T₁ h) +₁ idC) ∘ f) ≈ (μ.η _ ∘ T₁ h) ∘ (elgotalgebras._# {X}) f + pres : ∀ {X Y Z} (f : Z ⇒ T₀ X + Z) (h : X ⇒ T₀ Y) + → elgotalgebras._# ((extend h +₁ idC) ∘ f) ≈ extend h ∘ (elgotalgebras._# {X}) f record PreElgotMonad : Set (o ⊔ ℓ ⊔ e) where field @@ -89,7 +92,6 @@ module Monad.ElgotMonad {o ℓ e} (ambient : Ambient o ℓ e) where ### *Proposition 15*: (Strong) Elgot monads are (strong) pre-Elgot -```agda -- elgot monads are pre-elgot Elgot⇒PreElgot : ElgotMonad → PreElgotMonad Elgot⇒PreElgot EM = record @@ -146,4 +148,3 @@ module Monad.ElgotMonad {o ℓ e} (ambient : Ambient o ℓ e) where module T = Monad T open T using (F; η; μ) open Functor F renaming (F₀ to T₀; F₁ to T₁) -``` diff --git a/src/Monad/Instance/K/PreElgot.lagda.md b/src/Monad/Instance/K/PreElgot.lagda.md index 9f02c95..1845f7c 100644 --- a/src/Monad/Instance/K/PreElgot.lagda.md +++ b/src/Monad/Instance/K/PreElgot.lagda.md @@ -7,6 +7,8 @@ open import Categories.Object.Initial open import Categories.NaturalTransformation open import Categories.NaturalTransformation.Equivalence open import Categories.Monad +open import Categories.Monad.Relative renaming (Monad to RMonad) +open import Categories.Monad.Construction.Kleisli import Monad.Instance.K as MIK ``` --> @@ -22,6 +24,7 @@ open import Monad.ElgotMonad ambient open import Monad.Instance.K ambient open import Monad.Instance.K.Compositionality ambient MK open import Monad.Instance.K.Commutative ambient MK +open import Monad.Instance.K.Strong ambient MK open import Category.Construction.PreElgotMonads ambient open import Category.Construction.ElgotAlgebras ambient @@ -34,16 +37,17 @@ open M C # K is a pre-Elgot monad ```agda -open kleisliK using (extend) -- TODO fix global declarations on Commutative.lagda.md -- open Elgot-Algebra-on using (#-Compositionality) -_# = λ {A} {X} f → Uniform-Iteration-Algebra._# (algebras A) {X = X} f +-- TODO fix this import mess!!! +-- _# = λ {A} {X} f → Uniform-Iteration-Algebra._# (algebras A) {X = X} f isPreElgot : IsPreElgot monadK isPreElgot = record { elgotalgebras = λ {X} → elgot X - ; assoc = λ f h → sym (extend-preserve h f) + ; pres = λ f h → sym (extend-preserve h f) } + where open kleisliK using (extend) preElgot : PreElgotMonad preElgot = record { T = monadK ; isPreElgot = isPreElgot } @@ -59,19 +63,105 @@ initialPreElgot = record !′ {A} = record { α = ntHelper (record { η = η' - ; commute = {!!} + ; commute = commute }) - ; α-η = {!!} - ; α-μ = {!!} + ; α-η = FreeObject.*-lift (freealgebras _) (T.η.η _) + ; α-μ = α-μ + ; preserves = λ {X} {B} f → Elgot-Algebra-Morphism.preserves (((freeElgot B) FreeObject.*) (T.η.η B)) } where open PreElgotMonad A using (T) + open RMonad (Monad⇒Kleisli C T) using (extend) module T = Monad T open PreElgotMonad preElgot using () + open monadK using () renaming (η to ηK; μ to μK) + open Elgot-Algebra-on using (#-resp-≈) η' : ∀ (X : Obj) → K.₀ X ⇒ T.F.₀ X η' X = Elgot-Algebra-Morphism.h (_* {A = record { A = T.F.F₀ X ; algebra = PreElgotMonad.elgotalgebras A }} (T.η.η X)) where open FreeObject (freeElgot X) - !-unique′ : ∀ {A : PreElgotMonad} (f : PreElgotMonad-Morphism preElgot A) → PreElgotMonad-Morphism.α !′ ≃ PreElgotMonad-Morphism.α f + commute : ∀ {X Y : Obj} (f : X ⇒ Y) → η' Y ∘ K.₁ f ≈ T.F.₁ f ∘ η' X + commute {X} {Y} f = begin + η' Y ∘ K.₁ f ≈⟨ *-uniq (T.F.₁ f ∘ T.η.η X) (record { h = η' Y ∘ K.₁ f ; preserves = pres₁ }) (begin + (η' Y ∘ K.₁ f) ∘ η ≈⟨ pullʳ (K₁η f) ⟩ + η' Y ∘ ηK.η _ ∘ f ≈⟨ pullˡ (FreeObject.*-lift (freealgebras Y) (T.η.η Y)) ⟩ + T.η.η Y ∘ f ≈⟨ NaturalTransformation.commute T.η f ⟩ + T.F.₁ f ∘ T.η.η X ∎) ⟩ + Elgot-Algebra-Morphism.h (_* {A = record { A = T.F.F₀ Y ; algebra = PreElgotMonad.elgotalgebras A }} (T.F.₁ f ∘ T.η.η _)) ≈⟨ sym (*-uniq (T.F.₁ f ∘ T.η.η X) (record { h = T.F.₁ f ∘ η' X ; preserves = pres₂ }) (begin + (T.F.₁ f ∘ η' X) ∘ η ≈⟨ pullʳ (FreeObject.*-lift (freealgebras X) (T.η.η X)) ⟩ + T.F.₁ f ∘ T.η.η X ∎)) ⟩ + T.F.₁ f ∘ η' X ∎ + where + open FreeObject (freeElgot X) + _#K = λ {B} {C} f → Elgot-Algebra._# (FreeObject.FX (freeElgot C)) {B} f + _#T = λ {B} {C} f → PreElgotMonad.elgotalgebras._# A {B} {C} f + pres₁ : ∀ {Z} {g : Z ⇒ K.₀ X + Z} → (η' Y ∘ K.₁ f) ∘ g #K ≈ ((η' Y ∘ K.₁ f +₁ idC) ∘ g) #T + pres₁ {Z} {g} = begin + (η' Y ∘ K.₁ f) ∘ (g #K) ≈⟨ pullʳ (Elgot-Algebra-Morphism.preserves (((freeElgot X) FreeObject.*) (ηK.η Y ∘ f))) ⟩ + η' Y ∘ (((K.₁ f +₁ idC) ∘ g) #K) ≈⟨ Elgot-Algebra-Morphism.preserves (((freeElgot Y) FreeObject.*) {A = record + { A = T.F.F₀ Y + ; algebra = + record + { _# = λ {X = X₁} → A PreElgotMonad.elgotalgebras.# + ; #-Fixpoint = PreElgotMonad.elgotalgebras.#-Fixpoint A + ; #-Uniformity = PreElgotMonad.elgotalgebras.#-Uniformity A + ; #-Folding = PreElgotMonad.elgotalgebras.#-Folding A + ; #-resp-≈ = PreElgotMonad.elgotalgebras.#-resp-≈ A + } + }} (T.η.η Y)) ⟩ + (((η' Y +₁ idC) ∘ (K.₁ f +₁ idC) ∘ g) #T) ≈⟨ #-resp-≈ (PreElgotMonad.elgotalgebras A) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩ + ((η' Y ∘ K.₁ f +₁ idC) ∘ g) #T ∎ + pres₂ : ∀ {Z} {g : Z ⇒ K.₀ X + Z} → (T.F.₁ f ∘ η' X) ∘ g #K ≈ ((T.F.₁ f ∘ η' X +₁ idC) ∘ g) #T + pres₂ {Z} {g} = begin + (T.F.₁ f ∘ η' X) ∘ g #K ≈⟨ pullʳ (Elgot-Algebra-Morphism.preserves (((freeElgot X) FreeObject.*) (T.η.η X))) ⟩ + T.F.₁ f ∘ ((η' X +₁ idC) ∘ g) #T ≈⟨ (sym (F₁⇒extend T f)) ⟩∘⟨refl ⟩ + extend (T.η.η Y ∘ f) ∘ ((η' X +₁ idC) ∘ g) #T ≈⟨ sym (PreElgotMonad.pres A ((η' X +₁ idC) ∘ g) (T.η.η Y ∘ f)) ⟩ + (((extend (T.η.η Y ∘ f) +₁ idC) ∘ (η' X +₁ idC) ∘ g) #T) ≈⟨ #-resp-≈ (PreElgotMonad.elgotalgebras A) (pullˡ (+₁∘+₁ ○ +₁-cong₂ ((F₁⇒extend T f) ⟩∘⟨refl) identity²)) ⟩ + ((T.F.₁ f ∘ η' X +₁ idC) ∘ g) #T ∎ + α-μ : ∀ {X : Obj} → η' X ∘ μK.η X ≈ T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X) + α-μ {X} = begin + η' X ∘ μK.η X ≈⟨ FreeObject.*-uniq (freeElgot (K.₀ X)) (η' X) (record { h = η' X ∘ μK.η X ; preserves = pres₁ }) (cancelʳ monadK.identityʳ) ⟩ + Elgot-Algebra-Morphism.h (((freeElgot (K.₀ X)) FreeObject.*) {A = record + { A = T.F.F₀ X + ; algebra = + record + { _# = λ Z → (A PreElgotMonad.elgotalgebras.#) Z + ; #-Fixpoint = PreElgotMonad.elgotalgebras.#-Fixpoint A + ; #-Uniformity = PreElgotMonad.elgotalgebras.#-Uniformity A + ; #-Folding = PreElgotMonad.elgotalgebras.#-Folding A + ; #-resp-≈ = PreElgotMonad.elgotalgebras.#-resp-≈ A + } + }} (η' X)) ≈⟨ sym (FreeObject.*-uniq (freeElgot (K.₀ X)) (η' X) (record { h = T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X) ; preserves = pres₂ }) (begin + (T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X)) ∘ ηK.η (K.₀ X) ≈⟨ (refl⟩∘⟨ sym (commute (η' X))) ⟩∘⟨refl ⟩ + (T.μ.η X ∘ η' _ ∘ K.₁ (η' X)) ∘ ηK.η (K.₀ X) ≈⟨ assoc ○ refl⟩∘⟨ (assoc ○ refl⟩∘⟨ sym (monadK.η.commute (η' X))) ⟩ + T.μ.η X ∘ η' _ ∘ ηK.η (T.F.F₀ X) ∘ η' X ≈⟨ refl⟩∘⟨ (pullˡ (FreeObject.*-lift (freealgebras _) (T.η.η _))) ⟩ + T.μ.η X ∘ T.η.η _ ∘ η' X ≈⟨ cancelˡ (Monad.identityʳ T) ⟩ + η' X ∎)) ⟩ + T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X) ∎ + where + _#K = λ {B} {C} f → Elgot-Algebra._# (FreeObject.FX (freeElgot C)) {B} f + _#T = λ {B} {C} f → PreElgotMonad.elgotalgebras._# A {B} {C} f + pres₁ : ∀ {Z} {g : Z ⇒ K.₀ (K.₀ X) + Z} → (η' X ∘ μK.η X) ∘ g #K ≈ ((η' X ∘ μK.η X +₁ idC) ∘ g) #T + pres₁ {Z} {g} = begin + (η' X ∘ μK.η X) ∘ (g #K) ≈⟨ pullʳ (Elgot-Algebra-Morphism.preserves (((freeElgot (K.₀ X)) FreeObject.*) idC)) ⟩ + η' X ∘ ((μK.η X +₁ idC) ∘ g) #K ≈⟨ Elgot-Algebra-Morphism.preserves (((freeElgot X) FreeObject.*) (T.η.η X)) ⟩ + (((η' X +₁ idC) ∘ (μK.η X +₁ idC) ∘ g) #T) ≈⟨ #-resp-≈ (PreElgotMonad.elgotalgebras A) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩ + (((η' X ∘ μK.η X +₁ idC) ∘ g) #T) ∎ + pres₂ : ∀ {Z} {g : Z ⇒ K.₀ (K.₀ X) + Z} → (T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X)) ∘ g #K ≈ ((T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X) +₁ idC) ∘ g) #T + pres₂ {Z} {g} = begin + (T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X)) ∘ (g #K) ≈⟨ pullʳ (pullʳ (Elgot-Algebra-Morphism.preserves (((freeElgot (K.₀ X)) FreeObject.*) (T.η.η (K.₀ X))))) ⟩ + T.μ.η X ∘ T.F.₁ (η' X) ∘ (((η' (K.₀ X) +₁ idC) ∘ g) #T) ≈⟨ refl⟩∘⟨ ((sym (F₁⇒extend T (η' X))) ⟩∘⟨refl ○ sym (PreElgotMonad.pres A ((η' (K.₀ X) +₁ idC) ∘ g) (T.η.η (T.F.F₀ X) ∘ η' X)) )⟩ + T.μ.η X ∘ ((extend (T.η.η _ ∘ η' _) +₁ idC) ∘ ((η' _ +₁ idC)) ∘ g) #T ≈⟨ (sym μ-extend) ⟩∘⟨refl ⟩ + extend idC ∘ ((extend (T.η.η _ ∘ η' _) +₁ idC) ∘ ((η' _ +₁ idC)) ∘ g) #T ≈⟨ sym (PreElgotMonad.pres A ((extend (T.η.η (T.F.F₀ X) ∘ η' X) +₁ idC) ∘ + (η' (K.₀ X) +₁ idC) ∘ g) idC) ⟩ + (((extend idC +₁ idC) ∘ (extend (T.η.η _ ∘ η' _) +₁ idC) ∘ ((η' _ +₁ idC)) ∘ g) #T) ≈⟨ #-resp-≈ (PreElgotMonad.elgotalgebras A) (pullˡ (+₁∘+₁ ○ +₁-cong₂ (μ-extend ⟩∘⟨ (F₁⇒extend T (η' X))) identity²)) ⟩ + (((T.μ.η X ∘ T.F.₁ (η' X) +₁ idC) ∘ (η' _ +₁ idC) ∘ g) #T) ≈⟨ #-resp-≈ (PreElgotMonad.elgotalgebras A) (pullˡ (+₁∘+₁ ○ +₁-cong₂ assoc identity²)) ⟩ + (((T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X) +₁ idC) ∘ g) #T) ∎ + where + μ-extend : extend idC ≈ T.μ.η X + μ-extend = begin + T.μ.η _ ∘ T.F.₁ idC ≈⟨ elimʳ T.F.identity ⟩ + T.μ.η X ∎ + !-unique′ : ∀ {A : PreElgotMonad} (f : PreElgotMonad-Morphism preElgot A) → PreElgotMonad-Morphism.α (!′ {A = A}) ≃ PreElgotMonad-Morphism.α f !-unique′ {A} f {X} = sym (*-uniq (T.η.η X) (record { h = α.η X ; preserves = preserves _