mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
Compare commits
No commits in common. "55dcf598fc9100a13e6811ce8df39bb3569ee41b" and "a877cd3f256b6b8676c1a27f3fa96949fe68d247" have entirely different histories.
55dcf598fc
...
a877cd3f25
3 changed files with 9 additions and 262 deletions
|
|
@ -1,118 +0,0 @@
|
|||
<!--
|
||||
```agda
|
||||
open import Level
|
||||
open import Category.Instance.AmbientCategory
|
||||
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.Functor
|
||||
open import Categories.Monad.Construction.Kleisli
|
||||
open import Categories.Category.Core
|
||||
```
|
||||
-->
|
||||
|
||||
# The (functor) category of pre-Elgot monads.
|
||||
|
||||
```agda
|
||||
module Category.Construction.PreElgotMonads {o ℓ e} (ambient : Ambient o ℓ e) where
|
||||
open Ambient ambient
|
||||
open import Monad.ElgotMonad ambient
|
||||
open import Algebra.ElgotAlgebra ambient
|
||||
open HomReasoning
|
||||
open Equiv
|
||||
open M C
|
||||
open MR C
|
||||
|
||||
module _ (P S : PreElgotMonad) where
|
||||
private
|
||||
open PreElgotMonad P using () renaming (T to TP; elgotalgebras to P-elgots)
|
||||
open PreElgotMonad S using () renaming (T to TS; elgotalgebras to S-elgots)
|
||||
module TP = Monad TP
|
||||
module TS = Monad TS
|
||||
open RMonad (Monad⇒Kleisli C TP) using () renaming (extend to extendP)
|
||||
open RMonad (Monad⇒Kleisli C TS) using () renaming (extend to extendS)
|
||||
_#P = λ {X} {A} f → P-elgots._# {X} {A} f
|
||||
_#S = λ {X} {A} f → S-elgots._# {X} {A} f
|
||||
record PreElgotMonad-Morphism : Set (o ⊔ ℓ ⊔ e) where
|
||||
field
|
||||
α : NaturalTransformation TP.F TS.F
|
||||
module α = NaturalTransformation α
|
||||
field
|
||||
α-η : ∀ {X}
|
||||
→ α.η X ∘ TP.η.η X ≈ TS.η.η X
|
||||
α-μ : ∀ {X}
|
||||
→ α.η X ∘ TP.μ.η X ≈ TS.μ.η X ∘ TS.F.₁ (α.η X) ∘ α.η (TP.F.₀ X)
|
||||
preserves : ∀ {X A} (f : X ⇒ TP.F.₀ A + X) → α.η A ∘ f #P ≈ ((α.η A +₁ idC) ∘ f) #S
|
||||
|
||||
PreElgotMonads : Category (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) (o ⊔ e)
|
||||
PreElgotMonads = record
|
||||
{ Obj = PreElgotMonad
|
||||
; _⇒_ = PreElgotMonad-Morphism
|
||||
; _≈_ = λ f g → (PreElgotMonad-Morphism.α f) ≃ (PreElgotMonad-Morphism.α g)
|
||||
; id = id'
|
||||
; _∘_ = _∘'_
|
||||
; assoc = assoc
|
||||
; sym-assoc = sym-assoc
|
||||
; identityˡ = identityˡ
|
||||
; identityʳ = identityʳ
|
||||
; identity² = identity²
|
||||
; equiv = λ {A} {B} → record { refl = refl ; sym = λ f → sym f ; trans = λ f g → trans f g }
|
||||
; ∘-resp-≈ = λ f≈h g≈i → ∘-resp-≈ f≈h g≈i
|
||||
}
|
||||
where
|
||||
open Elgot-Algebra-on using (#-resp-≈)
|
||||
id' : ∀ {A : PreElgotMonad} → PreElgotMonad-Morphism A A
|
||||
id' {A} = record
|
||||
{ α = ntHelper (record
|
||||
{ η = λ _ → idC
|
||||
; commute = λ _ → id-comm-sym
|
||||
})
|
||||
; α-η = identityˡ
|
||||
; α-μ = sym (begin
|
||||
T.μ.η _ ∘ T.F.₁ idC ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩
|
||||
T.μ.η _ ∘ T.F.₁ idC ≈⟨ elimʳ T.F.identity ⟩
|
||||
T.μ.η _ ≈⟨ sym identityˡ ⟩
|
||||
idC ∘ T.μ.η _ ∎)
|
||||
; preserves = λ f → begin
|
||||
idC ∘ f # ≈⟨ identityˡ ⟩
|
||||
f # ≈⟨ sym (#-resp-≈ elgotalgebras (elimˡ ([]-unique id-comm-sym id-comm-sym))) ⟩
|
||||
((idC +₁ idC) ∘ f) # ∎
|
||||
}
|
||||
where
|
||||
open PreElgotMonad A using (T; elgotalgebras)
|
||||
module T = Monad T
|
||||
_# = λ {X} {A} f → elgotalgebras._# {X} {A} f
|
||||
_∘'_ : ∀ {X Y Z : PreElgotMonad} → PreElgotMonad-Morphism Y Z → PreElgotMonad-Morphism X Y → PreElgotMonad-Morphism X Z
|
||||
_∘'_ {X} {Y} {Z} f g = record
|
||||
{ α = αf ∘ᵥ αg
|
||||
; α-η = λ {A} → begin
|
||||
(αf.η A ∘ αg.η A) ∘ TX.η.η A ≈⟨ pullʳ (α-η g) ⟩
|
||||
αf.η A ∘ TY.η.η A ≈⟨ α-η f ⟩
|
||||
TZ.η.η A ∎
|
||||
; α-μ = λ {A} → begin
|
||||
(αf.η A ∘ αg.η A) ∘ TX.μ.η A ≈⟨ pullʳ (α-μ g) ⟩
|
||||
αf.η A ∘ TY.μ.η A ∘ TY.F.₁ (αg.η A) ∘ αg.η (TX.F.₀ A) ≈⟨ pullˡ (α-μ f) ⟩
|
||||
(TZ.μ.η A ∘ TZ.F.₁ (αf.η A) ∘ αf.η (TY.F.₀ A)) ∘ TY.F.₁ (αg.η A) ∘ αg.η (TX.F.₀ A) ≈⟨ assoc ○ refl⟩∘⟨ pullʳ (pullˡ (NaturalTransformation.commute αf (αg.η A))) ⟩
|
||||
TZ.μ.η A ∘ TZ.F.₁ (αf.η A) ∘ (TZ.F.₁ (αg.η A) ∘ αf.η (TX.F.₀ A)) ∘ αg.η (TX.F.₀ A) ≈⟨ refl⟩∘⟨ pullˡ (pullˡ (sym (Functor.homomorphism TZ.F))) ⟩
|
||||
TZ.μ.η A ∘ (TZ.F.₁ (αf.η A ∘ αg.η A) ∘ αf.η (TX.F.₀ A)) ∘ αg.η (TX.F.₀ A) ≈⟨ refl⟩∘⟨ assoc ⟩
|
||||
TZ.μ.η A ∘ TZ.F.₁ ((αf.η A ∘ αg.η A)) ∘ αf.η (TX.F.₀ A) ∘ αg.η (TX.F.₀ A) ∎
|
||||
; preserves = λ {A} {B} h → begin
|
||||
(αf.η B ∘ αg.η B) ∘ (h #X) ≈⟨ pullʳ (preserves g h) ⟩
|
||||
αf.η B ∘ ((αg.η B +₁ idC) ∘ h) #Y ≈⟨ preserves f ((αg.η B +₁ idC) ∘ h) ⟩
|
||||
(((αf.η B +₁ idC) ∘ (αg.η B +₁ idC) ∘ h) #Z) ≈⟨ #-resp-≈ (PreElgotMonad.elgotalgebras Z) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩
|
||||
(((αf.η B ∘ αg.η B +₁ idC) ∘ h) #Z) ∎
|
||||
}
|
||||
where
|
||||
module TX = Monad (PreElgotMonad.T X)
|
||||
module TY = Monad (PreElgotMonad.T Y)
|
||||
module TZ = Monad (PreElgotMonad.T Z)
|
||||
_#X = λ {A} {B} f → PreElgotMonad.elgotalgebras._# X {A} {B} f
|
||||
_#Y = λ {A} {B} f → PreElgotMonad.elgotalgebras._# Y {A} {B} f
|
||||
_#Z = λ {A} {B} f → PreElgotMonad.elgotalgebras._# Z {A} {B} f
|
||||
|
||||
open PreElgotMonad-Morphism using (α-η; α-μ; preserves)
|
||||
|
||||
open PreElgotMonad-Morphism f using () renaming (α to αf)
|
||||
open PreElgotMonad-Morphism g using () renaming (α to αg)
|
||||
```
|
||||
|
|
@ -4,9 +4,7 @@
|
|||
|
||||
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
|
||||
```
|
||||
-->
|
||||
|
|
@ -38,7 +36,6 @@ 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
|
||||
|
|
@ -49,8 +46,8 @@ module Monad.ElgotMonad {o ℓ e} (ambient : Ambient o ℓ e) where
|
|||
|
||||
-- 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
|
||||
assoc : ∀ {X Y Z} (f : Z ⇒ T₀ X + Z) (h : X ⇒ T₀ Y)
|
||||
→ elgotalgebras._# (((μ.η _ ∘ T₁ h) +₁ idC) ∘ f) ≈ (μ.η _ ∘ T₁ h) ∘ (elgotalgebras._# {X}) f
|
||||
|
||||
record PreElgotMonad : Set (o ⊔ ℓ ⊔ e) where
|
||||
field
|
||||
|
|
@ -92,6 +89,7 @@ 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
|
||||
|
|
@ -148,3 +146,4 @@ 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₁)
|
||||
```
|
||||
|
|
|
|||
|
|
@ -2,13 +2,6 @@
|
|||
```agda
|
||||
open import Level
|
||||
open import Category.Instance.AmbientCategory
|
||||
open import Categories.FreeObjects.Free
|
||||
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
|
||||
```
|
||||
-->
|
||||
|
|
@ -24,9 +17,6 @@ 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
|
||||
|
||||
open Equiv
|
||||
open HomReasoning
|
||||
|
|
@ -37,138 +27,14 @@ 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)
|
||||
-- TODO fix this import mess!!!
|
||||
-- _# = λ {A} {X} f → Uniform-Iteration-Algebra._# (algebras A) {X = X} f
|
||||
_# = λ {A} {X} f → Uniform-Iteration-Algebra._# (algebras A) {X = X} f
|
||||
|
||||
isPreElgot : IsPreElgot monadK
|
||||
isPreElgot = record
|
||||
preElgot : IsPreElgot monadK
|
||||
preElgot = record
|
||||
{ elgotalgebras = λ {X} → elgot X
|
||||
; pres = λ f h → sym (extend-preserve h f)
|
||||
; assoc = λ f h → sym (extend-preserve h f)
|
||||
}
|
||||
where open kleisliK using (extend)
|
||||
|
||||
preElgot : PreElgotMonad
|
||||
preElgot = record { T = monadK ; isPreElgot = isPreElgot }
|
||||
|
||||
-- initialPreElgot :
|
||||
initialPreElgot : IsInitial PreElgotMonads preElgot
|
||||
initialPreElgot = record
|
||||
{ ! = !′
|
||||
; !-unique = !-unique′
|
||||
}
|
||||
where
|
||||
!′ : ∀ {A : PreElgotMonad} → PreElgotMonad-Morphism preElgot A
|
||||
!′ {A} = record
|
||||
{ α = ntHelper (record
|
||||
{ η = η'
|
||||
; 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)
|
||||
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 _
|
||||
}) α-η)
|
||||
where
|
||||
open PreElgotMonad-Morphism f using (α; α-η; preserves)
|
||||
open PreElgotMonad A using (T)
|
||||
module T = Monad T
|
||||
open FreeObject (freeElgot X)
|
||||
```
|
||||
|
|
|
|||
Loading…
Reference in a new issue