mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
🎨 Cleanup and fix constraints.
This commit is contained in:
parent
55dcf598fc
commit
50fee48b17
SSH key fingerprint:
SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
1 changed files with 77 additions and 73 deletions
|
|
@ -67,108 +67,112 @@ initialPreElgot = record
|
||||||
})
|
})
|
||||||
; α-η = FreeObject.*-lift (freealgebras _) (T.η.η _)
|
; α-η = FreeObject.*-lift (freealgebras _) (T.η.η _)
|
||||||
; α-μ = α-μ
|
; α-μ = α-μ
|
||||||
; preserves = λ {X} {B} f → Elgot-Algebra-Morphism.preserves (((freeElgot B) FreeObject.*) (T.η.η B))
|
; preserves = λ {X} {B} f → Elgot-Algebra-Morphism.preserves (((freeElgot B) FreeObject.*) {A = record { A = T.F.F₀ B ; algebra = PreElgotMonad.elgotalgebras A }} (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 = record { A = T.F.F₀ X ; algebra = PreElgotMonad.elgotalgebras A }} (T.η.η X))
|
η' X = Elgot-Algebra-Morphism.h (_* {A = T-Alg X} (T.η.η X))
|
||||||
where open FreeObject (freeElgot 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
|
_#K = λ {B} {C} f → Elgot-Algebra._# (FreeObject.FX (freeElgot C)) {B} f
|
||||||
_#T = λ {B} {C} f → PreElgotMonad.elgotalgebras._# A {B} {C} 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} f = begin
|
||||||
|
η' Y ∘ K.₁ f ≈⟨ FreeObject.*-uniq
|
||||||
|
(freeElgot X)
|
||||||
|
{A = T-Alg Y}
|
||||||
|
(T.F.₁ f ∘ T.η.η X)
|
||||||
|
(record { h = η' Y ∘ K.₁ f ; preserves = pres₁ })
|
||||||
|
comm₁ ⟩
|
||||||
|
Elgot-Algebra-Morphism.h (FreeObject._* (freeElgot X) {A = T-Alg Y} (T.F.₁ f ∘ T.η.η _)) ≈⟨ sym (FreeObject.*-uniq
|
||||||
|
(freeElgot X)
|
||||||
|
{A = T-Alg Y}
|
||||||
|
(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
|
||||||
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ʳ (Elgot-Algebra-Morphism.preserves (((freeElgot X) FreeObject.*) (ηK.η Y ∘ f))) ⟩
|
(η' Y ∘ K.₁ f) ∘ (g #K) ≈⟨ pullʳ (K₁-preserves f g) ⟩
|
||||||
η' Y ∘ (((K.₁ f +₁ idC) ∘ g) #K) ≈⟨ Elgot-Algebra-Morphism.preserves (((freeElgot Y) FreeObject.*) {A = record
|
η' Y ∘ (((K.₁ f +₁ idC) ∘ g) #K) ≈⟨ η'-preserves ((K.₁ f +₁ idC) ∘ g) ⟩
|
||||||
{ 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ʳ (Elgot-Algebra-Morphism.preserves (((freeElgot X) FreeObject.*) (T.η.η X))) ⟩
|
(T.F.₁ f ∘ η' X) ∘ g #K ≈⟨ pullʳ (η'-preserves g) ⟩
|
||||||
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.pres 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 (freeElgot (K.₀ X)) (η' X) (record { h = η' X ∘ μK.η X ; preserves = pres₁ }) (cancelʳ monadK.identityʳ) ⟩
|
η' X ∘ μK.η X ≈⟨ FreeObject.*-uniq
|
||||||
Elgot-Algebra-Morphism.h (((freeElgot (K.₀ X)) FreeObject.*) {A = record
|
(freeElgot (K.₀ X))
|
||||||
{ A = T.F.F₀ X
|
{A = T-Alg X}
|
||||||
; algebra =
|
(η' X)
|
||||||
record
|
(record { h = η' X ∘ μK.η X ; preserves = pres₁ })
|
||||||
{ _# = λ Z → (A PreElgotMonad.elgotalgebras.#) Z
|
(cancelʳ monadK.identityʳ) ⟩
|
||||||
; #-Fixpoint = PreElgotMonad.elgotalgebras.#-Fixpoint A
|
Elgot-Algebra-Morphism.h (((freeElgot (K.₀ X)) FreeObject.*) {A = T-Alg X} (η' X)) ≈⟨ sym (FreeObject.*-uniq
|
||||||
; #-Uniformity = PreElgotMonad.elgotalgebras.#-Uniformity A
|
(freeElgot (K.₀ X))
|
||||||
; #-Folding = PreElgotMonad.elgotalgebras.#-Folding A
|
{A = T-Alg X}
|
||||||
; #-resp-≈ = PreElgotMonad.elgotalgebras.#-resp-≈ A
|
(η' X)
|
||||||
}
|
(record { h = T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X) ; preserves = pres₂ })
|
||||||
}} (η' X)) ≈⟨ sym (FreeObject.*-uniq (freeElgot (K.₀ X)) (η' X) (record { h = T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X) ; preserves = pres₂ }) (begin
|
comm) ⟩
|
||||||
(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) ∎
|
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ʳ (Elgot-Algebra-Morphism.preserves (((freeElgot (K.₀ X)) FreeObject.*) idC)) ⟩
|
(η' X ∘ μK.η X) ∘ (g #K) ≈⟨ pullʳ (μK-preserves g) ⟩
|
||||||
η' X ∘ ((μK.η X +₁ idC) ∘ g) #K ≈⟨ Elgot-Algebra-Morphism.preserves (((freeElgot X) FreeObject.*) (T.η.η X)) ⟩
|
η' X ∘ ((μK.η X +₁ idC) ∘ g) #K ≈⟨ η'-preserves ((μK.η X +₁ idC) ∘ g) ⟩
|
||||||
(((η' 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ʳ (Elgot-Algebra-Morphism.preserves (((freeElgot (K.₀ X)) FreeObject.*) (T.η.η (K.₀ X))))) ⟩
|
(T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X)) ∘ (g #K) ≈⟨ pullʳ (pullʳ (η'-preserves g)) ⟩
|
||||||
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 ∘ 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 ⟩
|
T.μ.η X ∘ ((extend (T.η.η _ ∘ η' _) +₁ idC) ∘ ((η' _ +₁ idC)) ∘ g) #T ≈⟨ (sym (elimʳ T.F.identity)) ⟩∘⟨refl ⟩
|
||||||
extend idC ∘ ((extend (T.η.η _ ∘ η' _) +₁ idC) ∘ ((η' _ +₁ idC)) ∘ g) #T ≈⟨ sym (PreElgotMonad.pres A ((extend (T.η.η (T.F.F₀ X) ∘ η' X) +₁ idC) ∘
|
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) ⟩
|
||||||
(η' (K.₀ X) +₁ idC) ∘ g) 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²)) ⟩
|
||||||
(((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) +₁ idC) ∘ (η' _ +₁ idC) ∘ g) #T) ≈⟨ #-resp-≈ (PreElgotMonad.elgotalgebras A) (pullˡ (+₁∘+₁ ○ +₁-cong₂ assoc identity²)) ⟩
|
||||||
(((T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X) +₁ idC) ∘ g) #T) ∎
|
(((T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X) +₁ idC) ∘ g) #T) ∎
|
||||||
where
|
comm : (T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X)) ∘ ηK.η (K.₀ X) ≈ η' X
|
||||||
μ-extend : extend idC ≈ T.μ.η X
|
comm = begin
|
||||||
μ-extend = begin
|
(T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X)) ∘ ηK.η (K.₀ X) ≈⟨ (refl⟩∘⟨ sym (commute (η' X))) ⟩∘⟨refl ⟩
|
||||||
T.μ.η _ ∘ T.F.₁ idC ≈⟨ elimʳ T.F.identity ⟩
|
(T.μ.η X ∘ η' _ ∘ K.₁ (η' X)) ∘ ηK.η (K.₀ X) ≈⟨ assoc ○ refl⟩∘⟨ (assoc ○ refl⟩∘⟨ sym (monadK.η.commute (η' X))) ⟩
|
||||||
T.μ.η X ∎
|
T.μ.η X ∘ η' _ ∘ ηK.η (T.F.F₀ X) ∘ η' X ≈⟨ refl⟩∘⟨ (pullˡ (FreeObject.*-lift (freealgebras _) (T.η.η _))) ⟩
|
||||||
|
T.μ.η X ∘ T.η.η _ ∘ η' X ≈⟨ cancelˡ (Monad.identityʳ T) ⟩
|
||||||
|
η' 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 (*-uniq (T.η.η X) (record
|
!-unique′ {A} f {X} = sym (FreeObject.*-uniq
|
||||||
{ h = α.η X
|
(freeElgot X)
|
||||||
; preserves = preserves _
|
{A = record { A = T.F.F₀ X ; algebra = PreElgotMonad.elgotalgebras A }}
|
||||||
}) α-η)
|
(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)
|
|
||||||
```
|
```
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue