From df288fccecd9c3110fbaeb47f51aaee812f0f960 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Mon, 20 Nov 2023 11:38:33 +0100 Subject: [PATCH] =?UTF-8?q?=E2=9C=A8=20Proof=20that=20K=20is=20initial=20s?= =?UTF-8?q?trong=20pre-Elgot?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Monad/Instance/K/PreElgot.lagda.md | 12 +- src/Monad/Instance/K/StrongPreElgot.lagda.md | 209 +++++++++++++++++++ 2 files changed, 212 insertions(+), 9 deletions(-) create mode 100644 src/Monad/Instance/K/StrongPreElgot.lagda.md diff --git a/src/Monad/Instance/K/PreElgot.lagda.md b/src/Monad/Instance/K/PreElgot.lagda.md index 7b603e2..17452f0 100644 --- a/src/Monad/Instance/K/PreElgot.lagda.md +++ b/src/Monad/Instance/K/PreElgot.lagda.md @@ -34,7 +34,7 @@ open MR C open M C ``` -# K is the initial (strong) pre-Elgot monad +# K is the initial pre-Elgot monad ```agda isPreElgot : IsPreElgot monadK @@ -47,14 +47,8 @@ isPreElgot = record preElgot : PreElgotMonad preElgot = record { T = monadK ; isPreElgot = isPreElgot } -strongPreElgot : IsStrongPreElgot KStrong -strongPreElgot = record - { preElgot = isPreElgot - ; strengthen-preserves = τ-comm - } - -initialPreElgot : IsInitial PreElgotMonads preElgot -initialPreElgot = record +isInitialPreElgot : IsInitial PreElgotMonads preElgot +isInitialPreElgot = record { ! = !′ ; !-unique = !-unique′ } diff --git a/src/Monad/Instance/K/StrongPreElgot.lagda.md b/src/Monad/Instance/K/StrongPreElgot.lagda.md new file mode 100644 index 0000000..9a3ccfb --- /dev/null +++ b/src/Monad/Instance/K/StrongPreElgot.lagda.md @@ -0,0 +1,209 @@ + + +```agda +module Monad.Instance.K.StrongPreElgot {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where +open Ambient ambient +open MIK ambient +open MonadK MK +open import Algebra.ElgotAlgebra ambient +open import Algebra.UniformIterationAlgebra ambient +open import Monad.PreElgot ambient +open import Monad.Instance.K ambient +open import Monad.Instance.K.ElgotAlgebra ambient MK +open import Monad.Instance.K.Commutative ambient MK +open import Monad.Instance.K.Strong ambient MK +open import Monad.Instance.K.PreElgot ambient MK +open import Category.Construction.StrongPreElgotMonads ambient +open import Category.Construction.ElgotAlgebras ambient +open import Algebra.Properties ambient + +open Equiv +open HomReasoning +open MR C +open M C +``` + +# K is the initial strong pre-Elgot monad + +```agda +isStrongPreElgot : IsStrongPreElgot KStrong +isStrongPreElgot = record + { preElgot = isPreElgot + ; strengthen-preserves = τ-comm + } + +strongPreElgot : StrongPreElgotMonad +strongPreElgot = record + { SM = KStrong + ; isStrongPreElgot = isStrongPreElgot + } + +isInitialStrongPreElgot : IsInitial StrongPreElgotMonads strongPreElgot +isInitialStrongPreElgot = record { ! = !′ ; !-unique = !-unique′ } + where + !′ : ∀ {A : StrongPreElgotMonad} → StrongPreElgotMonad-Morphism strongPreElgot A + !′ {A} = record + { α = ntHelper (record { η = η' ; commute = commute }) + ; α-η = α-η + ; α-μ = α-μ + ; α-strength = α-strength + ; α-preserves = λ {X} {B} f → Elgot-Algebra-Morphism.preserves (((freeElgot B) FreeObject.*) {A = record { A = T.F.F₀ B ; algebra = StrongPreElgotMonad.elgotalgebras A }} (T.η.η B)) + } + where + open StrongPreElgotMonad A using (SM) + module SM = StrongMonad SM + open SM using (strengthen) renaming (M to T) + open RMonad (Monad⇒Kleisli C T) using (extend) + open monadK using () renaming (η to ηK; μ to μK) + open strongK using () renaming (strengthen to strengthenK) + open Elgot-Algebra-on using (#-resp-≈) + T-Alg : ∀ (X : Obj) → Elgot-Algebra + T-Alg X = record { A = T.F.₀ X ; algebra = StrongPreElgotMonad.elgotalgebras A } + K-Alg : ∀ (X : Obj) → Elgot-Algebra + K-Alg X = record { A = K.₀ X ; algebra = elgot X } + η' : ∀ (X : Obj) → K.₀ X ⇒ T.F.₀ X + η' X = Elgot-Algebra-Morphism.h (_* {A = T-Alg X} (T.η.η X)) + where open FreeObject (freeElgot X) + _#K = λ {B} {C} f → Elgot-Algebra._# (FreeObject.FX (freeElgot C)) {B} f + _#T = λ {B} {C} f → StrongPreElgotMonad.elgotalgebras._# A {B} {C} f + -- some preservation facts that follow immediately, since these things are elgot-algebra-morphisms. + K₁-preserves : ∀ {X Y Z : Obj} (f : X ⇒ Y) (g : Z ⇒ K.₀ X + Z) → K.₁ f ∘ (g #K) ≈ ((K.₁ f +₁ idC) ∘ g) #K + K₁-preserves {X} {Y} {Z} f g = Elgot-Algebra-Morphism.preserves (((freeElgot X) FreeObject.*) {A = K-Alg Y} (ηK.η _ ∘ f)) + μK-preserves : ∀ {X Y : Obj} (g : Y ⇒ K.₀ (K.₀ X) + Y) → μK.η X ∘ g #K ≈ ((μK.η X +₁ idC) ∘ g) #K + μK-preserves {X} g = Elgot-Algebra-Morphism.preserves (((freeElgot (K.₀ X)) FreeObject.*) {A = K-Alg X} idC) + η'-preserves : ∀ {X Y : Obj} (g : Y ⇒ K.₀ X + Y) → η' X ∘ g #K ≈ ((η' X +₁ idC) ∘ g) #T + η'-preserves {X} g = Elgot-Algebra-Morphism.preserves (((freeElgot X) FreeObject.*) {A = T-Alg X} (T.η.η X)) + commute : ∀ {X Y : Obj} (f : X ⇒ Y) → η' Y ∘ K.₁ f ≈ T.F.₁ f ∘ η' X + commute {X} {Y} f = begin + η' Y ∘ K.₁ f ≈⟨ FreeObject.*-uniq + (freeElgot X) + {A = T-Alg Y} + (T.F.₁ f ∘ T.η.η X) + (record { h = η' Y ∘ K.₁ f ; preserves = pres₁ }) + comm₁ ⟩ + Elgot-Algebra-Morphism.h (FreeObject._* (freeElgot X) {A = T-Alg Y} (T.F.₁ f ∘ T.η.η _)) ≈⟨ sym (FreeObject.*-uniq + (freeElgot X) + {A = T-Alg Y} + (T.F.₁ f ∘ T.η.η X) + (record { h = T.F.₁ f ∘ η' X ; preserves = pres₂ }) + (pullʳ (FreeObject.*-lift (freealgebras X) (T.η.η X)))) ⟩ + T.F.₁ f ∘ η' X ∎ + where + 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ʳ (K₁-preserves f g) ⟩ + η' Y ∘ (((K.₁ f +₁ idC) ∘ g) #K) ≈⟨ η'-preserves ((K.₁ f +₁ idC) ∘ g) ⟩ + (((η' Y +₁ idC) ∘ (K.₁ f +₁ idC) ∘ g) #T) ≈⟨ #-resp-≈ (StrongPreElgotMonad.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ʳ (η'-preserves g) ⟩ + T.F.₁ f ∘ ((η' X +₁ idC) ∘ g) #T ≈⟨ (sym (F₁⇒extend T f)) ⟩∘⟨refl ⟩ + extend (T.η.η Y ∘ f) ∘ ((η' X +₁ idC) ∘ g) #T ≈⟨ sym (StrongPreElgotMonad.extend-preserves A ((η' X +₁ idC) ∘ g) (T.η.η Y ∘ f)) ⟩ + (((extend (T.η.η Y ∘ f) +₁ idC) ∘ (η' X +₁ idC) ∘ g) #T) ≈⟨ #-resp-≈ (StrongPreElgotMonad.elgotalgebras A) (pullˡ (+₁∘+₁ ○ +₁-cong₂ ((F₁⇒extend T f) ⟩∘⟨refl) identity²)) ⟩ + ((T.F.₁ f ∘ η' X +₁ idC) ∘ g) #T ∎ + comm₁ : (η' Y ∘ K.₁ f) ∘ _ ≈ T.F.₁ f ∘ T.η.η X + comm₁ = 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 ∎ + α-η : ∀ {X : Obj} → η' X ∘ ηK.η X ≈ T.η.η X + α-η {X} = FreeObject.*-lift (freealgebras X) (T.η.η X) + α-μ : ∀ {X : Obj} → η' X ∘ μK.η X ≈ T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X) + α-μ {X} = begin + η' X ∘ μK.η X ≈⟨ FreeObject.*-uniq + (freeElgot (K.₀ X)) + {A = T-Alg X} + (η' X) + (record { h = η' X ∘ μK.η X ; preserves = pres₁ }) + (cancelʳ monadK.identityʳ) ⟩ + Elgot-Algebra-Morphism.h (((freeElgot (K.₀ X)) FreeObject.*) {A = T-Alg X} (η' X)) ≈⟨ sym (FreeObject.*-uniq + (freeElgot (K.₀ X)) + {A = T-Alg X} + (η' X) + (record { h = T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X) ; preserves = pres₂ }) + comm) ⟩ + T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X) ∎ + where + 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ʳ (μK-preserves g) ⟩ + η' X ∘ ((μK.η X +₁ idC) ∘ g) #K ≈⟨ η'-preserves ((μK.η X +₁ idC) ∘ g) ⟩ + (((η' X +₁ idC) ∘ (μK.η X +₁ idC) ∘ g) #T) ≈⟨ #-resp-≈ (StrongPreElgotMonad.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ʳ (η'-preserves g)) ⟩ + T.μ.η X ∘ T.F.₁ (η' X) ∘ (((η' (K.₀ X) +₁ idC) ∘ g) #T) ≈⟨ refl⟩∘⟨ ((sym (F₁⇒extend T (η' X))) ⟩∘⟨refl ○ sym (StrongPreElgotMonad.extend-preserves A ((η' (K.₀ X) +₁ idC) ∘ g) (T.η.η (T.F.F₀ X) ∘ η' X)) )⟩ + T.μ.η X ∘ ((extend (T.η.η _ ∘ η' _) +₁ idC) ∘ ((η' _ +₁ idC)) ∘ g) #T ≈⟨ (sym (elimʳ T.F.identity)) ⟩∘⟨refl ⟩ + extend idC ∘ ((extend (T.η.η _ ∘ η' _) +₁ idC) ∘ ((η' _ +₁ idC)) ∘ g) #T ≈⟨ sym (StrongPreElgotMonad.extend-preserves A ((extend (T.η.η (T.F.F₀ X) ∘ η' X) +₁ idC) ∘ (η' (K.₀ X) +₁ idC) ∘ g) idC) ⟩ + (((extend idC +₁ idC) ∘ (extend (T.η.η _ ∘ η' _) +₁ idC) ∘ ((η' _ +₁ idC)) ∘ g) #T) ≈⟨ #-resp-≈ (StrongPreElgotMonad.elgotalgebras A) (pullˡ (+₁∘+₁ ○ +₁-cong₂ ((elimʳ T.F.identity) ⟩∘⟨ (F₁⇒extend T (η' X))) identity²)) ⟩ + (((T.μ.η X ∘ T.F.₁ (η' X) +₁ idC) ∘ (η' _ +₁ idC) ∘ g) #T) ≈⟨ #-resp-≈ (StrongPreElgotMonad.elgotalgebras A) (pullˡ (+₁∘+₁ ○ +₁-cong₂ assoc identity²)) ⟩ + (((T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X) +₁ idC) ∘ g) #T) ∎ + comm : (T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X)) ∘ ηK.η (K.₀ X) ≈ η' X + comm = 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 ∎ + α-strength : ∀ {X Y : Obj} → η' (X × Y) ∘ strengthenK.η (X , Y) ≈ strengthen.η (X , Y) ∘ (idC ⁂ η' Y) + α-strength {X} {Y} = begin + η' (X × Y) ∘ strengthenK.η (X , Y) ≈⟨ IsStableFreeUniformIterationAlgebra.♯-unique (stable Y) (T.η.η (X × Y)) (η' (X × Y) ∘ strengthenK.η (X , Y)) (sym pres₁) pres₃ ⟩ + IsStableFreeUniformIterationAlgebra.[ (stable Y) , Functor.₀ elgot-to-uniformF (T-Alg (X × Y)) ]♯ (T.η.η (X × Y)) ≈⟨ sym (IsStableFreeUniformIterationAlgebra.♯-unique (stable Y) (T.η.η (X × Y)) (strengthen.η (X , Y) ∘ (idC ⁂ η' Y)) (sym pres₂) pres₄) ⟩ + strengthen.η (X , Y) ∘ (idC ⁂ η' Y) ∎ + where + pres₁ : (η' (X × Y) ∘ strengthenK.η (X , Y)) ∘ (idC ⁂ ηK.η Y) ≈ T.η.η (X × Y) + pres₁ = begin + (η' (X × Y) ∘ strengthenK.η (X , Y)) ∘ (idC ⁂ ηK.η Y) ≈⟨ pullʳ (τ-η (X , Y)) ⟩ + η' (X × Y) ∘ ηK.η (X × Y) ≈⟨ α-η ⟩ + T.η.η (X × Y) ∎ + pres₂ : (strengthen.η (X , Y) ∘ (idC ⁂ η' Y)) ∘ (idC ⁂ ηK.η Y) ≈ T.η.η (X × Y) + pres₂ = begin + (strengthen.η (X , Y) ∘ (idC ⁂ η' Y)) ∘ (idC ⁂ ηK.η Y) ≈⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² α-η) ⟩ + strengthen.η (X , Y) ∘ (idC ⁂ T.η.η Y) ≈⟨ SM.η-comm ⟩ + T.η.η (X × Y) ∎ + pres₃ : ∀ {Z : Obj} (h : Z ⇒ K.₀ Y + Z) → (η' (X × Y) ∘ strengthenK.η (X , Y)) ∘ (idC ⁂ h #K) ≈ ((η' (X × Y) ∘ strengthenK.η (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #T + pres₃ {Z} h = begin + (η' (X × Y) ∘ strengthenK.η (X , Y)) ∘ (idC ⁂ h #K) ≈⟨ pullʳ (τ-comm h) ⟩ + η' (X × Y) ∘ ((τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #K ≈⟨ η'-preserves ((τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ⟩ + ((η' (X × Y) +₁ idC) ∘ (strengthenK.η (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #T ≈⟨ #-resp-≈ (StrongPreElgotMonad.elgotalgebras A) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩ + ((η' (X × Y) ∘ strengthenK.η (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #T ∎ + pres₄ : ∀ {Z : Obj} (h : Z ⇒ K.₀ Y + Z) → (strengthen.η (X , Y) ∘ (idC ⁂ η' Y)) ∘ (idC ⁂ h #K) ≈ ((strengthen.η (X , Y) ∘ (idC ⁂ η' Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #T + pres₄ {Z} h = begin + (strengthen.η (X , Y) ∘ (idC ⁂ η' Y)) ∘ (idC ⁂ h #K) ≈⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² (η'-preserves h)) ⟩ + strengthen.η (X , Y) ∘ (idC ⁂ ((η' Y +₁ idC) ∘ h) #T) ≈⟨ StrongPreElgotMonad.strengthen-preserves A ((η' Y +₁ idC) ∘ h) ⟩ + ((strengthen.η (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (η' Y +₁ idC) ∘ h)) #T ≈⟨ sym (#-resp-≈ (StrongPreElgotMonad.elgotalgebras A) (refl⟩∘⟨ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² refl)))) ⟩ + (((strengthen.η (X , Y) +₁ idC) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ (η' Y +₁ idC))) ∘ (idC ⁂ h)) #T) ≈⟨ sym (#-resp-≈ (StrongPreElgotMonad.elgotalgebras A) (refl⟩∘⟨ (pullˡ ((+₁-cong₂ refl (sym (⟨⟩-unique id-comm id-comm))) ⟩∘⟨refl ○ distribute₁ idC (η' Y) idC)))) ⟩ + -- ((strengthen.η (X , Y) +₁ idC) ∘ ((idC ⁂ η' Y) +₁ (idC ⁂ idC)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #T ≈⟨ {! !} ⟩ + ((strengthen.η (X , Y) +₁ idC) ∘ ((idC ⁂ η' Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #T ≈⟨ #-resp-≈ (StrongPreElgotMonad.elgotalgebras A) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩ + ((strengthen.η (X , Y) ∘ (idC ⁂ η' Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #T ∎ + !-unique′ : ∀ {A : StrongPreElgotMonad} (f : StrongPreElgotMonad-Morphism strongPreElgot A) → StrongPreElgotMonad-Morphism.α (!′ {A = A}) ≃ StrongPreElgotMonad-Morphism.α f + !-unique′ {A} f {X} = sym (FreeObject.*-uniq + (freeElgot X) + {A = record { A = T.F.F₀ X ; algebra = StrongPreElgotMonad.elgotalgebras A }} + (T.η.η X) + (record { h = α.η X ; preserves = α-preserves _ }) + α-η) + where + open StrongPreElgotMonad-Morphism f using (α; α-η; α-preserves) + open StrongPreElgotMonad A using (SM) + open StrongMonad SM using () renaming (M to T) +```