diff --git a/src/Monad/Instance/K/PreElgot.lagda.md b/src/Monad/Instance/K/PreElgot.lagda.md index 1845f7c..080f353 100644 --- a/src/Monad/Instance/K/PreElgot.lagda.md +++ b/src/Monad/Instance/K/PreElgot.lagda.md @@ -67,108 +67,112 @@ initialPreElgot = record }) ; α-η = FreeObject.*-lift (freealgebras _) (T.η.η _) ; α-μ = α-μ - ; preserves = λ {X} {B} f → Elgot-Algebra-Morphism.preserves (((freeElgot B) FreeObject.*) (T.η.η B)) + ; preserves = λ {X} {B} f → Elgot-Algebra-Morphism.preserves (((freeElgot B) FreeObject.*) {A = record { A = T.F.F₀ B ; algebra = PreElgotMonad.elgotalgebras A }} (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-≈) + T-Alg : ∀ (X : Obj) → Elgot-Algebra + T-Alg X = record { A = T.F.₀ X ; algebra = PreElgotMonad.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 = record { A = T.F.F₀ X ; algebra = PreElgotMonad.elgotalgebras A }} (T.η.η 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 → PreElgotMonad.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 ≈⟨ *-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 ∎ + η' 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 - 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 ∘ 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-≈ (PreElgotMonad.elgotalgebras A) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩ - ((η' Y ∘ K.₁ f +₁ idC) ∘ g) #T ∎ + ((η' 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)) ⟩ + (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 (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 ∎ + ((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 ∘ 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) ∎ + η' 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 - _#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 ∘ μ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-≈ (PreElgotMonad.elgotalgebras A) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩ - (((η' X ∘ μK.η X +₁ idC) ∘ g) #T) ∎ + (((η' 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 ∎ + (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 (PreElgotMonad.pres 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 (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₂ ((elimʳ T.F.identity) ⟩∘⟨ (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) ∎ + 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 ∎ !-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 _ - }) α-η) + !-unique′ {A} f {X} = sym (FreeObject.*-uniq + (freeElgot X) + {A = record { A = T.F.F₀ X ; algebra = PreElgotMonad.elgotalgebras A }} + (T.η.η X) + (record { h = α.η X ; preserves = preserves _ }) + α-η) where open PreElgotMonad-Morphism f using (α; α-η; preserves) open PreElgotMonad A using (T) module T = Monad T - open FreeObject (freeElgot X) ```