leonv/bsc-leon-vatthauer
1
0
Fork 0
mirror of https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git synced 2024-05-31 07:28:34 +02:00
Code Issues Projects Releases Packages Wiki Activity

Show that K is initial pre-Elgot

Browse source
This commit is contained in:
Leon Vatthauer 2023-11-15 19:25:35 +01:00
parent 60f60ce3bf
commit 55dcf598fc
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
2 changed files with 102 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Monad/ElgotMonad.lagda.md
View file

@ -4,7 +4,9 @@
open import Level open import Level
open import Category.Instance.AmbientCategory using (Ambient) open import Category.Instance.AmbientCategory using (Ambient)
open import Categories.Monad.Construction.Kleisli
open import Categories.Monad open import Categories.Monad
open import Categories.Monad.Relative renaming (Monad to RMonad)
open import Categories.Functor open import Categories.Functor
``` ```
--> -->
@ -36,6 +38,7 @@ module Monad.ElgotMonad {o ℓ e} (ambient : Ambient o ℓ e) where
```agda ```agda
record IsPreElgot (T : Monad C) : Set (o ⊔ ℓ ⊔ e) where record IsPreElgot (T : Monad C) : Set (o ⊔ ℓ ⊔ e) where
open Monad T open Monad T
open RMonad (Monad⇒Kleisli C T) using (extend)
open Functor F renaming (F₀ to T₀; F₁ to T₁) open Functor F renaming (F₀ to T₀; F₁ to T₁)
-- every TX needs to be equipped with an elgot algebra structure -- 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 -- with the following associativity
field field
assoc : ∀ {X Y Z} (f : Z ⇒ T₀ X + Z) (h : X ⇒ T₀ Y) pres : ∀ {X Y Z} (f : Z ⇒ T₀ X + Z) (h : X ⇒ T₀ Y)
→ elgotalgebras._# (((μ.η _ ∘ T₁ h) +₁ idC) ∘ f) ≈ (μ.η _ ∘ T₁ h) ∘ (elgotalgebras._# {X}) f → elgotalgebras._# ((extend h +₁ idC) ∘ f) ≈ extend h ∘ (elgotalgebras._# {X}) f
record PreElgotMonad : Set (o ⊔ ℓ ⊔ e) where record PreElgotMonad : Set (o ⊔ ℓ ⊔ e) where
field field
@ -89,7 +92,6 @@ module Monad.ElgotMonad {o ℓ e} (ambient : Ambient o ℓ e) where
### *Proposition 15*: (Strong) Elgot monads are (strong) pre-Elgot ### *Proposition 15*: (Strong) Elgot monads are (strong) pre-Elgot
```agda
-- elgot monads are pre-elgot -- elgot monads are pre-elgot
Elgot⇒PreElgot : ElgotMonad → PreElgotMonad Elgot⇒PreElgot : ElgotMonad → PreElgotMonad
Elgot⇒PreElgot EM = record Elgot⇒PreElgot EM = record
@ -146,4 +148,3 @@ module Monad.ElgotMonad {o ℓ e} (ambient : Ambient o ℓ e) where
module T = Monad T module T = Monad T
open T using (F; η; μ) open T using (F; η; μ)
open Functor F renaming (F₀ to T₀; F₁ to T₁) open Functor F renaming (F₀ to T₀; F₁ to T₁)
```

104
src/Monad/Instance/K/PreElgot.lagda.md
View file

@ -7,6 +7,8 @@ open import Categories.Object.Initial
open import Categories.NaturalTransformation open import Categories.NaturalTransformation
open import Categories.NaturalTransformation.Equivalence open import Categories.NaturalTransformation.Equivalence
open import Categories.Monad 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 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 ambient
open import Monad.Instance.K.Compositionality ambient MK open import Monad.Instance.K.Compositionality ambient MK
open import Monad.Instance.K.Commutative 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.PreElgotMonads ambient
open import Category.Construction.ElgotAlgebras ambient open import Category.Construction.ElgotAlgebras ambient
@ -34,16 +37,17 @@ open M C
# K is a pre-Elgot monad # K is a pre-Elgot monad
```agda ```agda
open kleisliK using (extend)
-- TODO fix global declarations on Commutative.lagda.md -- TODO fix global declarations on Commutative.lagda.md
-- open Elgot-Algebra-on using (#-Compositionality) -- 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 : IsPreElgot monadK
isPreElgot = record isPreElgot = record
{ elgotalgebras = λ {X} → elgot X { 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 : PreElgotMonad
preElgot = record { T = monadK ; isPreElgot = isPreElgot } preElgot = record { T = monadK ; isPreElgot = isPreElgot }
@ -59,19 +63,105 @@ initialPreElgot = record
!′ {A} = record !′ {A} = record
{ α = ntHelper (record { α = ntHelper (record
{ η = η' { η = η'
; commute = {!!} ; commute = commute
}) })
; α-η = {!!} ; α-η = FreeObject.*-lift (freealgebras _) (T.η.η _)
; α-μ = {!!} ; α-μ = α-μ
; preserves = λ {X} {B} f → Elgot-Algebra-Morphism.preserves (((freeElgot B) FreeObject.*) (T.η.η B))
} }
where where
open PreElgotMonad A using (T) open PreElgotMonad A using (T)
open RMonad (Monad⇒Kleisli C T) using (extend)
module T = Monad T module T = Monad T
open PreElgotMonad preElgot using () 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 : 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 = record { A = T.F.F₀ X ; algebra = PreElgotMonad.elgotalgebras A }} (T.η.η X))
where open FreeObject (freeElgot 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 !-unique′ {A} f {X} = sym (*-uniq (T.η.η X) (record
{ h = α.η X { h = α.η X
; preserves = preserves _ ; preserves = preserves _