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

Compare commits

base: leonv:1f4e5460d7adb961460cde3d5f7734aec97f0a9b
Branches Tags
leonv:main
leonv:Abgabe
..
compare: leonv:55dcf598fc9100a13e6811ce8df39bb3569ee41b
Branches Tags
leonv:main
leonv:Abgabe

No commits in common. "1f4e5460d7adb961460cde3d5f7734aec97f0a9b" and "55dcf598fc9100a13e6811ce8df39bb3569ee41b" have entirely different histories.
1f4e5460d7 ... 55dcf598fc

6 changed files with 131 additions and 168 deletions
Show stats Expand all files Collapse all files

2
src/Category/Construction/PreElgotMonads.lagda.md
View file

@ -17,7 +17,7 @@ open import Categories.Category.Core
```agda ```agda
module Category.Construction.PreElgotMonads {o ℓ e} (ambient : Ambient o ℓ e) where module Category.Construction.PreElgotMonads {o ℓ e} (ambient : Ambient o ℓ e) where
open Ambient ambient open Ambient ambient
open import Monad.PreElgot ambient open import Monad.ElgotMonad ambient
open import Algebra.ElgotAlgebra ambient open import Algebra.ElgotAlgebra ambient
open HomReasoning open HomReasoning
open Equiv open Equiv

48
src/Misc/Monad/Elgot.lagda.md → src/Monad/ElgotMonad.lagda.md
View file

@ -1,5 +1,7 @@
<!-- <!--
```agda ```agda
{-# OPTIONS --allow-unsolved-metas #-}
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.Construction.Kleisli
@ -9,16 +11,54 @@ open import Categories.Functor
``` ```
--> -->
## Summary
This file introduces Elgot Monads.
TODO: Probably only Pre-Elgot is needed
- [X] *Definition 13* Pre-Elgot Monads
- [ ] *Definition 13* strong pre-Elgot
- [X] *Definition 14* Elgot Monads
- [ ] *Definition 14* strong Elgot
- [ ] *Proposition 15* (Strong) Elgot monads are (strong) pre-Elgot
## Code
```agda ```agda
module Misc.Monad.Elgot {o ℓ e} (ambient : Ambient o ℓ e) where module Monad.ElgotMonad {o ℓ e} (ambient : Ambient o ℓ e) where
open Ambient ambient open Ambient ambient
open HomReasoning open HomReasoning
open MR C open MR C
open Equiv open Equiv
open import Algebra.ElgotAlgebra ambient open import Algebra.ElgotAlgebra ambient
open import Monad.PreElgot ambient
``` ```
### *Definition 13*: Pre-Elgot Monads
```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
field
elgotalgebras : ∀ {X} → Elgot-Algebra-on (T₀ X)
module elgotalgebras {X} = Elgot-Algebra-on (elgotalgebras {X})
-- with the following associativity
field
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
T : Monad C
isPreElgot : IsPreElgot T
open IsPreElgot isPreElgot public
```
### *Definition 14*: Elgot Monads ### *Definition 14*: Elgot Monads
```agda ```agda
@ -50,7 +90,7 @@ module Misc.Monad.Elgot {o ℓ e} (ambient : Ambient o ℓ e) where
open IsElgot isElgot public open IsElgot isElgot public
``` ```
### *Proposition 15*: Elgot monads are pre-Elgot ### *Proposition 15*: (Strong) Elgot monads are (strong) pre-Elgot
-- elgot monads are pre-elgot -- elgot monads are pre-elgot
Elgot⇒PreElgot : ElgotMonad → PreElgotMonad Elgot⇒PreElgot : ElgotMonad → PreElgotMonad
@ -107,4 +147,4 @@ module Misc.Monad.Elgot {o ℓ e} (ambient : Ambient o ℓ e) where
open ElgotMonad EM open ElgotMonad EM
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₁)

2
src/Monad/Instance/K/Commutative.lagda.md
View file

@ -22,7 +22,7 @@ open import Category.Construction.UniformIterationAlgebras ambient
open import Algebra.UniformIterationAlgebra ambient open import Algebra.UniformIterationAlgebra ambient
open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF; IsStableFreeUniformIterationAlgebra) open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF; IsStableFreeUniformIterationAlgebra)
open import Algebra.ElgotAlgebra ambient open import Algebra.ElgotAlgebra ambient
open import Monad.Instance.K.Elgot ambient MK open import Monad.Instance.K.Compositionality ambient MK
open Equiv open Equiv
open HomReasoning open HomReasoning

6
src/Monad/Instance/K/Elgot.lagda.md → src/Monad/Instance/K/Compositionality.lagda.md
View file

@ -1,3 +1,5 @@
# TODO: every KX satisfies compositionality
```agda ```agda
{-# OPTIONS --allow-unsolved-metas #-} {-# OPTIONS --allow-unsolved-metas #-}
open import Level open import Level
@ -6,10 +8,8 @@ open import Category.Instance.AmbientCategory
import Monad.Instance.K as MIK import Monad.Instance.K as MIK
``` ```
# Every KX is a free Elgot algebra
```agda ```agda
module Monad.Instance.K.Elgot {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where module Monad.Instance.K.Compositionality {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where
open Ambient ambient open Ambient ambient
open MIK ambient open MIK ambient
open MonadK MK open MonadK MK

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

@ -20,9 +20,9 @@ open MIK ambient
open MonadK MK open MonadK MK
open import Algebra.ElgotAlgebra ambient open import Algebra.ElgotAlgebra ambient
open import Algebra.UniformIterationAlgebra ambient open import Algebra.UniformIterationAlgebra ambient
open import Monad.PreElgot ambient open import Monad.ElgotMonad ambient
open import Monad.Instance.K ambient open import Monad.Instance.K ambient
open import Monad.Instance.K.Elgot 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 Monad.Instance.K.Strong ambient MK
open import Category.Construction.PreElgotMonads ambient open import Category.Construction.PreElgotMonads ambient
@ -37,22 +37,22 @@ open M C
# K is a pre-Elgot monad # K is a pre-Elgot monad
```agda ```agda
-- TODO fix global declarations on Commutative.lagda.md
-- open Elgot-Algebra-on using (#-Compositionality)
-- 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
; extend-preserves = λ f h → sym (extend-preserve h f) ; pres = λ f h → sym (extend-preserve h f)
} }
where open kleisliK using (extend) where open kleisliK using (extend)
preElgot : PreElgotMonad preElgot : PreElgotMonad
preElgot = record { T = monadK ; isPreElgot = isPreElgot } preElgot = record { T = monadK ; isPreElgot = isPreElgot }
strongPreElgot : IsStrongPreElgot KStrong -- initialPreElgot :
strongPreElgot = record
{ preElgot = isPreElgot
; strengthen-preserves = τ-comm
}
initialPreElgot : IsInitial PreElgotMonads preElgot initialPreElgot : IsInitial PreElgotMonads preElgot
initialPreElgot = record initialPreElgot = record
{ ! = !′ { ! = !′
@ -67,112 +67,108 @@ initialPreElgot = record
}) })
; α-η = FreeObject.*-lift (freealgebras _) (T.η.η _) ; α-η = FreeObject.*-lift (freealgebras _) (T.η.η _)
; α-μ = α-μ ; α-μ = α-μ
; preserves = λ {X} {B} f → Elgot-Algebra-Morphism.preserves (((freeElgot B) FreeObject.*) {A = record { A = T.F.F₀ B ; algebra = PreElgotMonad.elgotalgebras A }} (T.η.η B)) ; 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) open RMonad (Monad⇒Kleisli C T) using (extend)
module T = Monad T module T = Monad T
open PreElgotMonad preElgot using ()
open monadK using () renaming (η to ηK; μ to μK) open monadK using () renaming (η to ηK; μ to μK)
open Elgot-Algebra-on using (#-resp-≈) 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 : Obj) → K.₀ X ⇒ T.F.₀ X
η' X = Elgot-Algebra-Morphism.h (_* {A = T-Alg X} (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)
_#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 : Obj} (f : X ⇒ Y) → η' Y ∘ K.₁ f ≈ T.F.₁ f ∘ η' X
commute {X} {Y} f = begin commute {X} {Y} f = begin
η' Y ∘ K.₁ f ≈⟨ FreeObject.*-uniq η' Y ∘ K.₁ f ≈⟨ *-uniq (T.F.₁ f ∘ T.η.η X) (record { h = η' Y ∘ K.₁ f ; preserves = pres₁ }) (begin
(freeElgot X) (η' Y ∘ K.₁ f) ∘ η ≈⟨ pullʳ (K₁η f) ⟩
{A = T-Alg Y} η' Y ∘ ηK.η _ ∘ f ≈⟨ pullˡ (FreeObject.*-lift (freealgebras Y) (T.η.η Y)) ⟩
(T.F.₁ f ∘ T.η.η X) T.η.η Y ∘ f ≈⟨ NaturalTransformation.commute T.η f ⟩
(record { h = η' Y ∘ K.₁ f ; preserves = pres₁ }) T.F.₁ f ∘ T.η.η X ∎) ⟩
comm₁ ⟩ 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
Elgot-Algebra-Morphism.h (FreeObject._* (freeElgot X) {A = T-Alg Y} (T.F.₁ f ∘ T.η.η _)) ≈⟨ sym (FreeObject.*-uniq (T.F.₁ f ∘ η' X) ∘ η ≈⟨ pullʳ (FreeObject.*-lift (freealgebras X) (T.η.η X)) ⟩
(freeElgot X) T.F.₁ f ∘ T.η.η X ∎)) ⟩
{A = T-Alg Y} T.F.₁ f ∘ η' X ∎
(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 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 : Z ⇒ K.₀ X + Z} → (η' Y ∘ K.₁ f) ∘ g #K ≈ ((η' Y ∘ K.₁ f +₁ idC) ∘ g) #T
pres₁ {Z} {g} = begin pres₁ {Z} {g} = begin
(η' Y ∘ K.₁ f) ∘ (g #K) ≈⟨ pullʳ (K₁-preserves f g) ⟩ (η' Y ∘ K.₁ f) ∘ (g #K) ≈⟨ pullʳ (Elgot-Algebra-Morphism.preserves (((freeElgot X) FreeObject.*) (ηK.η Y ∘ f))) ⟩
η' Y ∘ (((K.₁ f +₁ idC) ∘ g) #K) ≈⟨ η'-preserves ((K.₁ f +₁ idC) ∘ g) ⟩ η' 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 +₁ 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 : Z ⇒ K.₀ X + Z} → (T.F.₁ f ∘ η' X) ∘ g #K ≈ ((T.F.₁ f ∘ η' X +₁ idC) ∘ g) #T
pres₂ {Z} {g} = begin pres₂ {Z} {g} = begin
(T.F.₁ f ∘ η' X) ∘ g #K ≈⟨ pullʳ (η'-preserves g) ⟩ (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 ⟩ T.F.₁ f ∘ ((η' X +₁ idC) ∘ g) #T ≈⟨ (sym (F₁⇒extend T f)) ⟩∘⟨refl ⟩
extend (T.η.η Y ∘ f) ∘ ((η' X +₁ idC) ∘ g) #T ≈⟨ sym (PreElgotMonad.extend-preserves A ((η' X +₁ idC) ∘ g) (T.η.η Y ∘ f)) ⟩ 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²)) ⟩ (((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 : Obj} → η' X ∘ μK.η X ≈ T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X)
α-μ {X} = begin α-μ {X} = begin
η' X ∘ μK.η X ≈⟨ FreeObject.*-uniq η' X ∘ μK.η X ≈⟨ FreeObject.*-uniq (freeElgot (K.₀ X)) (η' X) (record { h = η' X ∘ μK.η X ; preserves = pres₁ }) (cancelʳ monadK.identityʳ) ⟩
(freeElgot (K.₀ X)) Elgot-Algebra-Morphism.h (((freeElgot (K.₀ X)) FreeObject.*) {A = record
{A = T-Alg X} { A = T.F.F₀ X
(η' X) ; algebra =
(record { h = η' X ∘ μK.η X ; preserves = pres₁ }) record
(cancelʳ monadK.identityʳ) ⟩ { _# = λ Z → (A PreElgotMonad.elgotalgebras.#) Z
Elgot-Algebra-Morphism.h (((freeElgot (K.₀ X)) FreeObject.*) {A = T-Alg X} (η' X)) ≈⟨ sym (FreeObject.*-uniq ; #-Fixpoint = PreElgotMonad.elgotalgebras.#-Fixpoint A
(freeElgot (K.₀ X)) ; #-Uniformity = PreElgotMonad.elgotalgebras.#-Uniformity A
{A = T-Alg X} ; #-Folding = PreElgotMonad.elgotalgebras.#-Folding A
(η' X) ; #-resp-≈ = PreElgotMonad.elgotalgebras.#-resp-≈ A
(record { h = T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X) ; preserves = pres₂ }) }
comm) ⟩ }} (η' 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) ∎ (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 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 : Z ⇒ K.₀ (K.₀ X) + Z} → (η' X ∘ μK.η X) ∘ g #K ≈ ((η' X ∘ μK.η X +₁ idC) ∘ g) #T
pres₁ {Z} {g} = begin pres₁ {Z} {g} = begin
(η' X ∘ μK.η X) ∘ (g #K) ≈⟨ pullʳ (μK-preserves g) ⟩ (η' X ∘ μK.η X) ∘ (g #K) ≈⟨ pullʳ (Elgot-Algebra-Morphism.preserves (((freeElgot (K.₀ X)) FreeObject.*) idC)) ⟩
η' X ∘ ((μK.η X +₁ idC) ∘ g) #K ≈⟨ η'-preserves ((μK.η X +₁ idC) ∘ g) ⟩ η' 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 +₁ 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 : 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 pres₂ {Z} {g} = begin
(T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X)) ∘ (g #K) ≈⟨ pullʳ (pullʳ (η'-preserves g)) ⟩ (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.extend-preserves A ((η' (K.₀ X) +₁ idC) ∘ g) (T.η.η (T.F.F₀ X) ∘ η' 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 (elimʳ T.F.identity)) ⟩∘⟨refl ⟩ T.μ.η X ∘ ((extend (T.η.η _ ∘ η' _) +₁ idC) ∘ ((η' _ +₁ idC)) ∘ g) #T ≈⟨ (sym μ-extend) ⟩∘⟨refl ⟩
extend idC ∘ ((extend (T.η.η _ ∘ η' _) +₁ idC) ∘ ((η' _ +₁ idC)) ∘ g) #T ≈⟨ sym (PreElgotMonad.extend-preserves A ((extend (T.η.η (T.F.F₀ X) ∘ η' X) +₁ idC) ∘ (η' (K.₀ X) +₁ idC) ∘ g) idC) ⟩ extend idC ∘ ((extend (T.η.η _ ∘ η' _) +₁ idC) ∘ ((η' _ +₁ idC)) ∘ g) #T ≈⟨ sym (PreElgotMonad.pres A ((extend (T.η.η (T.F.F₀ X) ∘ η' X) +₁ 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²)) ⟩ (η' (K.₀ X) +₁ idC) ∘ g) idC) ⟩
(((T.μ.η X ∘ T.F.₁ (η' X) +₁ idC) ∘ (η' _ +₁ idC) ∘ g) #T) ≈⟨ #-resp-≈ (PreElgotMonad.elgotalgebras A) (pullˡ (+₁∘+₁ ○ +₁-cong₂ assoc identity²)) ⟩ (((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) ∘ η' (K.₀ X) +₁ idC) ∘ g) #T) ∎ (((T.μ.η X ∘ T.F.₁ (η' X) +₁ idC) ∘ (η' _ +₁ idC) ∘ g) #T) ≈⟨ #-resp-≈ (PreElgotMonad.elgotalgebras A) (pullˡ (+₁∘+₁ ○ +₁-cong₂ assoc identity²)) ⟩
comm : (T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X)) ∘ ηK.η (K.₀ X) ≈ η' X (((T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X) +₁ idC) ∘ g) #T) ∎
comm = begin where
(T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X)) ∘ ηK.η (K.₀ X) ≈⟨ (refl⟩∘⟨ sym (commute (η' X))) ⟩∘⟨refl ⟩ μ-extend : extend idC ≈ T.μ.η X
(T.μ.η X ∘ η' _ ∘ K.₁ (η' X)) ∘ ηK.η (K.₀ X) ≈⟨ assoc ○ refl⟩∘⟨ (assoc ○ refl⟩∘⟨ sym (monadK.η.commute (η' X))) ⟩ μ-extend = begin
T.μ.η X ∘ η' _ ∘ ηK.η (T.F.F₀ X) ∘ η' X ≈⟨ refl⟩∘⟨ (pullˡ (FreeObject.*-lift (freealgebras _) (T.η.η _))) ⟩ T.μ.η _ ∘ T.F.₁ idC ≈⟨ elimʳ T.F.identity ⟩
T.μ.η X ∘ T.η.η _ ∘ η' X ≈⟨ cancelˡ (Monad.identityʳ T) ⟩ T.μ.η X ∎
η' X ∎
!-unique′ : ∀ {A : PreElgotMonad} (f : PreElgotMonad-Morphism preElgot A) → PreElgotMonad-Morphism.α (!′ {A = A}) ≃ PreElgotMonad-Morphism.α f !-unique′ : ∀ {A : PreElgotMonad} (f : PreElgotMonad-Morphism preElgot A) → PreElgotMonad-Morphism.α (!′ {A = A}) ≃ PreElgotMonad-Morphism.α f
!-unique′ {A} f {X} = sym (FreeObject.*-uniq !-unique′ {A} f {X} = sym (*-uniq (T.η.η X) (record
(freeElgot X) { h = α.η X
{A = record { A = T.F.F₀ X ; algebra = PreElgotMonad.elgotalgebras A }} ; preserves = preserves _
(T.η.η X) }) α-η)
(record { h = α.η X ; preserves = preserves _ })
α-η)
where where
open PreElgotMonad-Morphism f using (α; α-η; preserves) open PreElgotMonad-Morphism f using (α; α-η; preserves)
open PreElgotMonad A using (T) open PreElgotMonad A using (T)
module T = Monad T module T = Monad T
open FreeObject (freeElgot X)
``` ```

73
src/Monad/PreElgot.lagda.md
View file

@ -1,73 +0,0 @@
<!--
```agda
{-# OPTIONS --allow-unsolved-metas #-}
open import Level
open import Category.Instance.AmbientCategory using (Ambient)
open import Categories.Monad.Construction.Kleisli
open import Categories.Monad
open import Categories.Monad.Strong
open import Categories.Monad.Relative renaming (Monad to RMonad)
open import Categories.Functor
open import Data.Product using (_,_)
```
-->
```agda
module Monad.PreElgot {o ℓ e} (ambient : Ambient o ℓ e) where
open Ambient ambient
open HomReasoning
open MR C
open Equiv
open import Algebra.ElgotAlgebra ambient
```
# (strong) pre-Elgot monads
```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
field
elgotalgebras : ∀ {X} → Elgot-Algebra-on (T₀ X)
module elgotalgebras {X} = Elgot-Algebra-on (elgotalgebras {X})
-- where kleisli lifting preserves iteration
field
extend-preserves : ∀ {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
T : Monad C
isPreElgot : IsPreElgot T
open IsPreElgot isPreElgot public
record IsStrongPreElgot (SM : StrongMonad monoidal) : Set (o ⊔ ℓ ⊔ e) where
open StrongMonad SM using (M; strengthen)
open Monad M using (F)
-- M is pre-Elgot
field
preElgot : IsPreElgot M
open IsPreElgot preElgot public
-- and strength is iteration preserving
field
strengthen-preserves : ∀ {X Y Z} (f : Z ⇒ F.₀ Y + Z)
→ strengthen.η (X , Y) ∘ (idC ⁂ elgotalgebras._# f) ≈ elgotalgebras._# ((strengthen.η (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ f))
record StrongPreElgotMonad : Set (o ⊔ ℓ ⊔ e) where
field
SM : StrongMonad monoidal
isStrongPreElgot : IsStrongPreElgot SM
open IsStrongPreElgot isStrongPreElgot public
```