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:55dcf598fc9100a13e6811ce8df39bb3569ee41b
Branches Tags
leonv:main
leonv:Abgabe
..
compare: leonv:a877cd3f256b6b8676c1a27f3fa96949fe68d247
Branches Tags
leonv:main
leonv:Abgabe

No commits in common. "55dcf598fc9100a13e6811ce8df39bb3569ee41b" and "a877cd3f256b6b8676c1a27f3fa96949fe68d247" have entirely different histories.
55dcf598fc ... a877cd3f25

3 changed files with 9 additions and 262 deletions
Show stats Expand all files Collapse all files

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

@ -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)
```

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

@ -4,9 +4,7 @@
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
``` ```
--> -->
@ -38,7 +36,6 @@ 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
@ -49,8 +46,8 @@ module Monad.ElgotMonad {o ℓ e} (ambient : Ambient o ℓ e) where
-- with the following associativity -- with the following associativity
field field
pres : ∀ {X Y Z} (f : Z ⇒ T₀ X + Z) (h : X ⇒ T₀ Y) assoc : ∀ {X Y Z} (f : Z ⇒ T₀ X + Z) (h : X ⇒ T₀ Y)
→ elgotalgebras._# ((extend h +₁ idC) ∘ f) ≈ extend h ∘ (elgotalgebras._# {X}) f → elgotalgebras._# (((μ.η _ ∘ T₁ h) +₁ idC) ∘ f) ≈ (μ.η _ ∘ T₁ h) ∘ (elgotalgebras._# {X}) f
record PreElgotMonad : Set (o ⊔ ℓ ⊔ e) where record PreElgotMonad : Set (o ⊔ ℓ ⊔ e) where
field field
@ -92,6 +89,7 @@ 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
@ -148,3 +146,4 @@ 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₁)
```

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

@ -2,13 +2,6 @@
```agda ```agda
open import Level open import Level
open import Category.Instance.AmbientCategory 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 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 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.ElgotAlgebras ambient
open Equiv open Equiv
open HomReasoning open HomReasoning
@ -37,138 +27,14 @@ 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)
-- 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 preElgot : IsPreElgot monadK
isPreElgot = record preElgot = record
{ elgotalgebras = λ {X} → elgot X { 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)
``` ```