Show that K is initial pre-Elgot

src/Category/Construction/PreElgotMonads.lagda.md

@@ -0,0 +1,118 @@
+<!--
+```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)
+```

src/Monad/ElgotMonad.lagda.md

@@ -4,7 +4,9 @@
 
 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
 ```
 -->
@@ -36,6 +38,7 @@ 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
@@ -46,8 +49,8 @@ module Monad.ElgotMonad {o ℓ e} (ambient : Ambient o ℓ e) where
 
     -- with the following associativity
     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
     field
@@ -89,7 +92,6 @@ 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 
@@ -146,4 +148,3 @@ 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₁)
-```

src/Monad/Instance/K/PreElgot.lagda.md

@@ -2,6 +2,13 @@
 ```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
 ```
 -->
@@ -17,6 +24,9 @@ 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
@@ -27,14 +37,138 @@ 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)
-_# = λ {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
 
-preElgot : IsPreElgot monadK
+isPreElgot : IsPreElgot monadK
-preElgot = record
+isPreElgot = record
   { 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 = 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)
 ```