mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
Compare commits
4 commits
1f4e5460d7
...
b74ecf373c
| Author | SHA1 | Date | |
|---|---|---|---|
b74ecf373c
|
|||
|
df288fccec
|
|||
|
d3712d4abd
|
|||
|
d762e280ad
|
7 changed files with 416 additions and 82 deletions
|
|
@ -47,72 +47,72 @@ module _ (P S : PreElgotMonad) where
|
|||
|
||||
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
|
||||
{ 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 = 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 using (α-η; α-μ; preserves)
|
||||
|
||||
open PreElgotMonad-Morphism f using () renaming (α to αf)
|
||||
open PreElgotMonad-Morphism g using () renaming (α to αg)
|
||||
open PreElgotMonad-Morphism f using () renaming (α to αf)
|
||||
open PreElgotMonad-Morphism g using () renaming (α to αg)
|
||||
```
|
||||
|
|
|
|||
132
src/Category/Construction/StrongPreElgotMonads.lagda.md
Normal file
132
src/Category/Construction/StrongPreElgotMonads.lagda.md
Normal file
|
|
@ -0,0 +1,132 @@
|
|||
<!--
|
||||
```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.Monad.Strong
|
||||
open import Categories.Category.Core
|
||||
open import Data.Product using (_,_)
|
||||
```
|
||||
-->
|
||||
|
||||
# The (functor) category of pre-Elgot monads.
|
||||
|
||||
```agda
|
||||
module Category.Construction.StrongPreElgotMonads {o ℓ e} (ambient : Ambient o ℓ e) where
|
||||
open Ambient ambient
|
||||
open import Monad.PreElgot ambient
|
||||
open import Algebra.ElgotAlgebra ambient
|
||||
open HomReasoning
|
||||
open Equiv
|
||||
open M C
|
||||
open MR C
|
||||
|
||||
module _ (P S : StrongPreElgotMonad) where
|
||||
private
|
||||
open StrongPreElgotMonad P using () renaming (SM to SMP; elgotalgebras to P-elgots)
|
||||
open StrongPreElgotMonad S using () renaming (SM to SMS; elgotalgebras to S-elgots)
|
||||
open StrongMonad SMP using () renaming (M to TP; strengthen to strengthenP)
|
||||
open StrongMonad SMS using () renaming (M to TS; strengthen to strengthenS)
|
||||
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 StrongPreElgotMonad-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)
|
||||
α-strength : ∀ {X Y}
|
||||
→ α.η (X × Y) ∘ strengthenP.η (X , Y) ≈ strengthenS.η (X , Y) ∘ (idC ⁂ α.η Y)
|
||||
α-preserves : ∀ {X A} (f : X ⇒ TP.F.₀ A + X) → α.η A ∘ f #P ≈ ((α.η A +₁ idC) ∘ f) #S
|
||||
|
||||
StrongPreElgotMonads : Category (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) (o ⊔ e)
|
||||
StrongPreElgotMonads = record
|
||||
{ Obj = StrongPreElgotMonad
|
||||
; _⇒_ = StrongPreElgotMonad-Morphism
|
||||
; _≈_ = λ f g → (StrongPreElgotMonad-Morphism.α f) ≃ (StrongPreElgotMonad-Morphism.α g)
|
||||
; id = id'
|
||||
; _∘_ = _∘'_
|
||||
; assoc = assoc
|
||||
; sym-assoc = sym-assoc
|
||||
; identityˡ = identityˡ
|
||||
; identityʳ = identityʳ
|
||||
; identity² = identity²
|
||||
; equiv = 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 : StrongPreElgotMonad} → StrongPreElgotMonad-Morphism A A
|
||||
id' {A} = record
|
||||
{ α = ntHelper (record { η = λ _ → idC ; commute = λ _ → id-comm-sym })
|
||||
; α-η = identityˡ
|
||||
; α-μ = sym (begin
|
||||
M.μ.η _ ∘ M.F.₁ idC ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩
|
||||
M.μ.η _ ∘ M.F.₁ idC ≈⟨ elimʳ M.F.identity ⟩
|
||||
M.μ.η _ ≈⟨ sym identityˡ ⟩
|
||||
idC ∘ M.μ.η _ ∎)
|
||||
; α-strength = λ {X} {Y} → sym (begin
|
||||
strengthen.η (X , Y) ∘ (idC ⁂ idC) ≈⟨ refl⟩∘⟨ (⁂-cong₂ refl (sym M.F.identity)) ⟩
|
||||
strengthen.η (X , Y) ∘ (idC ⁂ M.F.₁ idC) ≈⟨ strengthen.commute (idC , idC) ⟩
|
||||
M.F.₁ (idC ⁂ idC) ∘ strengthen.η (X , Y) ≈⟨ (M.F.F-resp-≈ (⟨⟩-unique id-comm id-comm) ○ M.F.identity) ⟩∘⟨refl ⟩
|
||||
idC ∘ strengthen.η (X , Y) ∎)
|
||||
; α-preserves = λ f → begin
|
||||
idC ∘ f # ≈⟨ identityˡ ⟩
|
||||
f # ≈⟨ sym (#-resp-≈ elgotalgebras (elimˡ ([]-unique id-comm-sym id-comm-sym))) ⟩
|
||||
((idC +₁ idC) ∘ f) # ∎
|
||||
}
|
||||
where
|
||||
open StrongPreElgotMonad A using (SM; elgotalgebras)
|
||||
open StrongMonad SM using (M; strengthen)
|
||||
_# = λ {X} {A} f → elgotalgebras._# {X} {A} f
|
||||
_∘'_ : ∀ {X Y Z : StrongPreElgotMonad} → StrongPreElgotMonad-Morphism Y Z → StrongPreElgotMonad-Morphism X Y → StrongPreElgotMonad-Morphism X Z
|
||||
_∘'_ {X} {Y} {Z} f g = record
|
||||
{ α = αf ∘ᵥ αg
|
||||
; α-η = λ {A} → begin
|
||||
(αf.η A ∘ αg.η A) ∘ MX.η.η A ≈⟨ pullʳ (α-η g) ⟩
|
||||
αf.η A ∘ MY.η.η A ≈⟨ α-η f ⟩
|
||||
MZ.η.η A ∎
|
||||
; α-μ = λ {A} → begin
|
||||
(αf.η A ∘ αg.η A) ∘ MX.μ.η A ≈⟨ pullʳ (α-μ g) ⟩
|
||||
αf.η A ∘ MY.μ.η A ∘ MY.F.₁ (αg.η A) ∘ αg.η (MX.F.₀ A) ≈⟨ pullˡ (α-μ f) ⟩
|
||||
(MZ.μ.η A ∘ MZ.F.₁ (αf.η A) ∘ αf.η (MY.F.₀ A)) ∘ MY.F.₁ (αg.η A) ∘ αg.η (MX.F.₀ A) ≈⟨ assoc ○ refl⟩∘⟨ pullʳ (pullˡ (NaturalTransformation.commute αf (αg.η A))) ⟩
|
||||
MZ.μ.η A ∘ MZ.F.₁ (αf.η A) ∘ (MZ.F.₁ (αg.η A) ∘ αf.η (MX.F.₀ A)) ∘ αg.η (MX.F.₀ A) ≈⟨ refl⟩∘⟨ pullˡ (pullˡ (sym (Functor.homomorphism MZ.F))) ⟩
|
||||
MZ.μ.η A ∘ (MZ.F.₁ (αf.η A ∘ αg.η A) ∘ αf.η (MX.F.₀ A)) ∘ αg.η (MX.F.₀ A) ≈⟨ refl⟩∘⟨ assoc ⟩
|
||||
MZ.μ.η A ∘ MZ.F.₁ ((αf.η A ∘ αg.η A)) ∘ αf.η (MX.F.₀ A) ∘ αg.η (MX.F.₀ A) ∎
|
||||
; α-strength = λ {A} {B} → begin
|
||||
(αf.η (A × B) ∘ αg.η (A × B)) ∘ strengthenX.η (A , B) ≈⟨ pullʳ (α-strength g) ⟩
|
||||
αf.η (A × B) ∘ strengthenY.η (A , B) ∘ (idC ⁂ αg.η B) ≈⟨ pullˡ (α-strength f) ⟩
|
||||
(strengthenZ.η (A , B) ∘ (idC ⁂ αf.η B)) ∘ (idC ⁂ αg.η B) ≈⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² refl) ⟩
|
||||
strengthenZ.η (A , B) ∘ (idC ⁂ (αf.η B ∘ αg.η B)) ∎
|
||||
; α-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-≈ (StrongPreElgotMonad.elgotalgebras Z) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩
|
||||
(((αf.η B ∘ αg.η B +₁ idC) ∘ h) #Z) ∎
|
||||
}
|
||||
where
|
||||
open StrongPreElgotMonad X using () renaming (SM to SMX)
|
||||
open StrongPreElgotMonad Y using () renaming (SM to SMY)
|
||||
open StrongPreElgotMonad Z using () renaming (SM to SMZ)
|
||||
open StrongMonad SMX using () renaming (M to MX; strengthen to strengthenX)
|
||||
open StrongMonad SMY using () renaming (M to MY; strengthen to strengthenY)
|
||||
open StrongMonad SMZ using () renaming (M to MZ; strengthen to strengthenZ)
|
||||
_#X = λ {A} {B} f → StrongPreElgotMonad.elgotalgebras._# X {A} {B} f
|
||||
_#Y = λ {A} {B} f → StrongPreElgotMonad.elgotalgebras._# Y {A} {B} f
|
||||
_#Z = λ {A} {B} f → StrongPreElgotMonad.elgotalgebras._# Z {A} {B} f
|
||||
|
||||
open StrongPreElgotMonad-Morphism using (α-η; α-μ; α-strength; α-preserves)
|
||||
|
||||
open StrongPreElgotMonad-Morphism f using () renaming (α to αf)
|
||||
open StrongPreElgotMonad-Morphism g using () renaming (α to αg)
|
||||
```
|
||||
|
|
@ -22,7 +22,7 @@ open import Category.Construction.UniformIterationAlgebras ambient
|
|||
open import Algebra.UniformIterationAlgebra ambient
|
||||
open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF; IsStableFreeUniformIterationAlgebra)
|
||||
open import Algebra.ElgotAlgebra ambient
|
||||
open import Monad.Instance.K.Elgot ambient MK
|
||||
open import Monad.Instance.K.ElgotAlgebra ambient MK
|
||||
|
||||
open Equiv
|
||||
open HomReasoning
|
||||
|
|
|
|||
|
|
@ -9,7 +9,7 @@ import Monad.Instance.K as MIK
|
|||
# Every KX is a free Elgot algebra
|
||||
|
||||
```agda
|
||||
module Monad.Instance.K.Elgot {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where
|
||||
module Monad.Instance.K.ElgotAlgebra {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where
|
||||
open Ambient ambient
|
||||
open MIK ambient
|
||||
open MonadK MK
|
||||
|
|
@ -22,7 +22,7 @@ open import Algebra.ElgotAlgebra ambient
|
|||
open import Algebra.UniformIterationAlgebra ambient
|
||||
open import Monad.PreElgot ambient
|
||||
open import Monad.Instance.K ambient
|
||||
open import Monad.Instance.K.Elgot ambient MK
|
||||
open import Monad.Instance.K.ElgotAlgebra ambient MK
|
||||
open import Monad.Instance.K.Commutative ambient MK
|
||||
open import Monad.Instance.K.Strong ambient MK
|
||||
open import Category.Construction.PreElgotMonads ambient
|
||||
|
|
@ -34,7 +34,7 @@ open MR C
|
|||
open M C
|
||||
```
|
||||
|
||||
# K is a pre-Elgot monad
|
||||
# K is the initial pre-Elgot monad
|
||||
|
||||
```agda
|
||||
isPreElgot : IsPreElgot monadK
|
||||
|
|
@ -47,14 +47,8 @@ isPreElgot = record
|
|||
preElgot : PreElgotMonad
|
||||
preElgot = record { T = monadK ; isPreElgot = isPreElgot }
|
||||
|
||||
strongPreElgot : IsStrongPreElgot KStrong
|
||||
strongPreElgot = record
|
||||
{ preElgot = isPreElgot
|
||||
; strengthen-preserves = τ-comm
|
||||
}
|
||||
|
||||
initialPreElgot : IsInitial PreElgotMonads preElgot
|
||||
initialPreElgot = record
|
||||
isInitialPreElgot : IsInitial PreElgotMonads preElgot
|
||||
isInitialPreElgot = record
|
||||
{ ! = !′
|
||||
; !-unique = !-unique′
|
||||
}
|
||||
|
|
|
|||
208
src/Monad/Instance/K/StrongPreElgot.lagda.md
Normal file
208
src/Monad/Instance/K/StrongPreElgot.lagda.md
Normal file
|
|
@ -0,0 +1,208 @@
|
|||
<!--
|
||||
```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.Strong
|
||||
open import Categories.Monad.Relative renaming (Monad to RMonad)
|
||||
open import Categories.Monad.Construction.Kleisli
|
||||
open import Data.Product using (_,_)
|
||||
open import Categories.Functor.Core
|
||||
import Monad.Instance.K as MIK
|
||||
```
|
||||
-->
|
||||
|
||||
```agda
|
||||
module Monad.Instance.K.StrongPreElgot {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where
|
||||
open Ambient ambient
|
||||
open MIK ambient
|
||||
open MonadK MK
|
||||
open import Algebra.ElgotAlgebra ambient
|
||||
open import Algebra.UniformIterationAlgebra ambient
|
||||
open import Monad.PreElgot ambient
|
||||
open import Monad.Instance.K ambient
|
||||
open import Monad.Instance.K.ElgotAlgebra ambient MK
|
||||
open import Monad.Instance.K.Commutative ambient MK
|
||||
open import Monad.Instance.K.Strong ambient MK
|
||||
open import Monad.Instance.K.PreElgot ambient MK
|
||||
open import Category.Construction.StrongPreElgotMonads ambient
|
||||
open import Category.Construction.ElgotAlgebras ambient
|
||||
open import Algebra.Properties ambient
|
||||
|
||||
open Equiv
|
||||
open HomReasoning
|
||||
open MR C
|
||||
open M C
|
||||
```
|
||||
|
||||
# K is the initial strong pre-Elgot monad
|
||||
|
||||
```agda
|
||||
isStrongPreElgot : IsStrongPreElgot KStrong
|
||||
isStrongPreElgot = record
|
||||
{ preElgot = isPreElgot
|
||||
; strengthen-preserves = τ-comm
|
||||
}
|
||||
|
||||
strongPreElgot : StrongPreElgotMonad
|
||||
strongPreElgot = record
|
||||
{ SM = KStrong
|
||||
; isStrongPreElgot = isStrongPreElgot
|
||||
}
|
||||
|
||||
isInitialStrongPreElgot : IsInitial StrongPreElgotMonads strongPreElgot
|
||||
isInitialStrongPreElgot = record { ! = !′ ; !-unique = !-unique′ }
|
||||
where
|
||||
!′ : ∀ {A : StrongPreElgotMonad} → StrongPreElgotMonad-Morphism strongPreElgot A
|
||||
!′ {A} = record
|
||||
{ α = ntHelper (record { η = η' ; commute = commute })
|
||||
; α-η = α-η
|
||||
; α-μ = α-μ
|
||||
; α-strength = α-strength
|
||||
; α-preserves = λ {X} {B} f → Elgot-Algebra-Morphism.preserves (((freeElgot B) FreeObject.*) {A = record { A = T.F.F₀ B ; algebra = StrongPreElgotMonad.elgotalgebras A }} (T.η.η B))
|
||||
}
|
||||
where
|
||||
open StrongPreElgotMonad A using (SM)
|
||||
module SM = StrongMonad SM
|
||||
open SM using (strengthen) renaming (M to T)
|
||||
open RMonad (Monad⇒Kleisli C T) using (extend)
|
||||
open monadK using () renaming (η to ηK; μ to μK)
|
||||
open strongK using () renaming (strengthen to strengthenK)
|
||||
open Elgot-Algebra-on using (#-resp-≈)
|
||||
T-Alg : ∀ (X : Obj) → Elgot-Algebra
|
||||
T-Alg X = record { A = T.F.₀ X ; algebra = StrongPreElgotMonad.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 = Elgot-Algebra-Morphism.h (_* {A = T-Alg X} (T.η.η X))
|
||||
where open FreeObject (freeElgot X)
|
||||
_#K = λ {B} {C} f → Elgot-Algebra._# (FreeObject.FX (freeElgot C)) {B} f
|
||||
_#T = λ {B} {C} f → StrongPreElgotMonad.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} = begin
|
||||
(η' Y ∘ K.₁ f) ∘ (g #K) ≈⟨ pullʳ (K₁-preserves f g) ⟩
|
||||
η' Y ∘ (((K.₁ f +₁ idC) ∘ g) #K) ≈⟨ η'-preserves ((K.₁ f +₁ idC) ∘ g) ⟩
|
||||
(((η' Y +₁ idC) ∘ (K.₁ f +₁ idC) ∘ g) #T) ≈⟨ #-resp-≈ (StrongPreElgotMonad.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ʳ (η'-preserves g) ⟩
|
||||
T.F.₁ f ∘ ((η' X +₁ idC) ∘ g) #T ≈⟨ (sym (F₁⇒extend T f)) ⟩∘⟨refl ⟩
|
||||
extend (T.η.η Y ∘ f) ∘ ((η' X +₁ idC) ∘ g) #T ≈⟨ sym (StrongPreElgotMonad.extend-preserves A ((η' X +₁ idC) ∘ g) (T.η.η Y ∘ f)) ⟩
|
||||
(((extend (T.η.η Y ∘ f) +₁ idC) ∘ (η' X +₁ idC) ∘ g) #T) ≈⟨ #-resp-≈ (StrongPreElgotMonad.elgotalgebras A) (pullˡ (+₁∘+₁ ○ +₁-cong₂ ((F₁⇒extend T f) ⟩∘⟨refl) identity²)) ⟩
|
||||
((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
|
||||
α-η {X} = FreeObject.*-lift (freealgebras X) (T.η.η X)
|
||||
α-μ : ∀ {X : Obj} → η' X ∘ μK.η X ≈ T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X)
|
||||
α-μ {X} = begin
|
||||
η' X ∘ μK.η X ≈⟨ FreeObject.*-uniq
|
||||
(freeElgot (K.₀ X))
|
||||
{A = T-Alg X}
|
||||
(η' X)
|
||||
(record { h = η' X ∘ μK.η X ; preserves = pres₁ })
|
||||
(cancelʳ monadK.identityʳ) ⟩
|
||||
Elgot-Algebra-Morphism.h (((freeElgot (K.₀ X)) FreeObject.*) {A = T-Alg X} (η' X)) ≈⟨ sym (FreeObject.*-uniq
|
||||
(freeElgot (K.₀ X))
|
||||
{A = T-Alg X}
|
||||
(η' X)
|
||||
(record { h = T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X) ; preserves = pres₂ })
|
||||
comm) ⟩
|
||||
T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X) ∎
|
||||
where
|
||||
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ʳ (μK-preserves g) ⟩
|
||||
η' X ∘ ((μK.η X +₁ idC) ∘ g) #K ≈⟨ η'-preserves ((μK.η X +₁ idC) ∘ g) ⟩
|
||||
(((η' X +₁ idC) ∘ (μK.η X +₁ idC) ∘ g) #T) ≈⟨ #-resp-≈ (StrongPreElgotMonad.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ʳ (η'-preserves g)) ⟩
|
||||
T.μ.η X ∘ T.F.₁ (η' X) ∘ (((η' (K.₀ X) +₁ idC) ∘ g) #T) ≈⟨ refl⟩∘⟨ ((sym (F₁⇒extend T (η' X))) ⟩∘⟨refl ○ sym (StrongPreElgotMonad.extend-preserves 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 ⟩
|
||||
extend idC ∘ ((extend (T.η.η _ ∘ η' _) +₁ idC) ∘ ((η' _ +₁ idC)) ∘ g) #T ≈⟨ sym (StrongPreElgotMonad.extend-preserves A ((extend (T.η.η (T.F.F₀ X) ∘ η' X) +₁ idC) ∘ (η' (K.₀ X) +₁ idC) ∘ g) idC) ⟩
|
||||
(((extend idC +₁ idC) ∘ (extend (T.η.η _ ∘ η' _) +₁ idC) ∘ ((η' _ +₁ idC)) ∘ g) #T) ≈⟨ #-resp-≈ (StrongPreElgotMonad.elgotalgebras A) (pullˡ (+₁∘+₁ ○ +₁-cong₂ ((elimʳ T.F.identity) ⟩∘⟨ (F₁⇒extend T (η' X))) identity²)) ⟩
|
||||
(((T.μ.η X ∘ T.F.₁ (η' X) +₁ idC) ∘ (η' _ +₁ idC) ∘ g) #T) ≈⟨ #-resp-≈ (StrongPreElgotMonad.elgotalgebras A) (pullˡ (+₁∘+₁ ○ +₁-cong₂ assoc identity²)) ⟩
|
||||
(((T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X) +₁ idC) ∘ g) #T) ∎
|
||||
comm : (T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X)) ∘ ηK.η (K.₀ X) ≈ η' X
|
||||
comm = 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 ∎
|
||||
α-strength : ∀ {X Y : Obj} → η' (X × Y) ∘ strengthenK.η (X , Y) ≈ strengthen.η (X , Y) ∘ (idC ⁂ η' Y)
|
||||
α-strength {X} {Y} = begin
|
||||
η' (X × Y) ∘ strengthenK.η (X , Y) ≈⟨ IsStableFreeUniformIterationAlgebra.♯-unique (stable Y) (T.η.η (X × Y)) (η' (X × Y) ∘ strengthenK.η (X , Y)) (sym pres₁) pres₃ ⟩
|
||||
IsStableFreeUniformIterationAlgebra.[ (stable Y) , Functor.₀ elgot-to-uniformF (T-Alg (X × Y)) ]♯ (T.η.η (X × Y)) ≈⟨ sym (IsStableFreeUniformIterationAlgebra.♯-unique (stable Y) (T.η.η (X × Y)) (strengthen.η (X , Y) ∘ (idC ⁂ η' Y)) (sym pres₂) pres₄) ⟩
|
||||
strengthen.η (X , Y) ∘ (idC ⁂ η' Y) ∎
|
||||
where
|
||||
pres₁ : (η' (X × Y) ∘ strengthenK.η (X , Y)) ∘ (idC ⁂ ηK.η Y) ≈ T.η.η (X × Y)
|
||||
pres₁ = begin
|
||||
(η' (X × Y) ∘ strengthenK.η (X , Y)) ∘ (idC ⁂ ηK.η Y) ≈⟨ pullʳ (τ-η (X , Y)) ⟩
|
||||
η' (X × Y) ∘ ηK.η (X × Y) ≈⟨ α-η ⟩
|
||||
T.η.η (X × Y) ∎
|
||||
pres₂ : (strengthen.η (X , Y) ∘ (idC ⁂ η' Y)) ∘ (idC ⁂ ηK.η Y) ≈ T.η.η (X × Y)
|
||||
pres₂ = begin
|
||||
(strengthen.η (X , Y) ∘ (idC ⁂ η' Y)) ∘ (idC ⁂ ηK.η Y) ≈⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² α-η) ⟩
|
||||
strengthen.η (X , Y) ∘ (idC ⁂ T.η.η Y) ≈⟨ SM.η-comm ⟩
|
||||
T.η.η (X × Y) ∎
|
||||
pres₃ : ∀ {Z : Obj} (h : Z ⇒ K.₀ Y + Z) → (η' (X × Y) ∘ strengthenK.η (X , Y)) ∘ (idC ⁂ h #K) ≈ ((η' (X × Y) ∘ strengthenK.η (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #T
|
||||
pres₃ {Z} h = begin
|
||||
(η' (X × Y) ∘ strengthenK.η (X , Y)) ∘ (idC ⁂ h #K) ≈⟨ pullʳ (τ-comm h) ⟩
|
||||
η' (X × Y) ∘ ((τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #K ≈⟨ η'-preserves ((τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ⟩
|
||||
((η' (X × Y) +₁ idC) ∘ (strengthenK.η (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #T ≈⟨ #-resp-≈ (StrongPreElgotMonad.elgotalgebras A) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩
|
||||
((η' (X × Y) ∘ strengthenK.η (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #T ∎
|
||||
pres₄ : ∀ {Z : Obj} (h : Z ⇒ K.₀ Y + Z) → (strengthen.η (X , Y) ∘ (idC ⁂ η' Y)) ∘ (idC ⁂ h #K) ≈ ((strengthen.η (X , Y) ∘ (idC ⁂ η' Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #T
|
||||
pres₄ {Z} h = begin
|
||||
(strengthen.η (X , Y) ∘ (idC ⁂ η' Y)) ∘ (idC ⁂ h #K) ≈⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² (η'-preserves h)) ⟩
|
||||
strengthen.η (X , Y) ∘ (idC ⁂ ((η' Y +₁ idC) ∘ h) #T) ≈⟨ StrongPreElgotMonad.strengthen-preserves A ((η' Y +₁ idC) ∘ h) ⟩
|
||||
((strengthen.η (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (η' Y +₁ idC) ∘ h)) #T ≈⟨ sym (#-resp-≈ (StrongPreElgotMonad.elgotalgebras A) (refl⟩∘⟨ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² refl)))) ⟩
|
||||
(((strengthen.η (X , Y) +₁ idC) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ (η' Y +₁ idC))) ∘ (idC ⁂ h)) #T) ≈⟨ sym (#-resp-≈ (StrongPreElgotMonad.elgotalgebras A) (refl⟩∘⟨ (pullˡ ((+₁-cong₂ refl (sym (⟨⟩-unique id-comm id-comm))) ⟩∘⟨refl ○ distribute₁ idC (η' Y) idC)))) ⟩
|
||||
((strengthen.η (X , Y) +₁ idC) ∘ ((idC ⁂ η' Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #T ≈⟨ #-resp-≈ (StrongPreElgotMonad.elgotalgebras A) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩
|
||||
((strengthen.η (X , Y) ∘ (idC ⁂ η' Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #T ∎
|
||||
!-unique′ : ∀ {A : StrongPreElgotMonad} (f : StrongPreElgotMonad-Morphism strongPreElgot A) → StrongPreElgotMonad-Morphism.α (!′ {A = A}) ≃ StrongPreElgotMonad-Morphism.α f
|
||||
!-unique′ {A} f {X} = sym (FreeObject.*-uniq
|
||||
(freeElgot X)
|
||||
{A = record { A = T.F.F₀ X ; algebra = StrongPreElgotMonad.elgotalgebras A }}
|
||||
(T.η.η X)
|
||||
(record { h = α.η X ; preserves = α-preserves _ })
|
||||
α-η)
|
||||
where
|
||||
open StrongPreElgotMonad-Morphism f using (α; α-η; α-preserves)
|
||||
open StrongPreElgotMonad A using (SM)
|
||||
open StrongMonad SM using () renaming (M to T)
|
||||
```
|
||||
|
|
@ -70,7 +70,7 @@ open import Monad.Instance.K.Strong
|
|||
The next step is to show that every *KX* satisfies compositionality, meaning that each *KX* is an Elgot algebra.
|
||||
|
||||
```agda
|
||||
open import Monad.Instance.K.Compositionality
|
||||
open import Monad.Instance.K.ElgotAlgebra
|
||||
```
|
||||
|
||||
and with this we can show that K is and equational lifting monad, i.e. a commutative monad satisfying the equational lifting law:
|
||||
|
|
@ -80,9 +80,9 @@ open import Monad.Instance.K.Commutative
|
|||
open import Monad.Instance.K.EquationalLifting
|
||||
```
|
||||
|
||||
and lastly we formalize the notion of *pre-Elgot monad* and show that **K** is pre-Elgot.
|
||||
and lastly we formalize the notion of *pre-Elgot monad* and show that **K** is the initial pre-Elgot monad.
|
||||
|
||||
```agda
|
||||
open import Monad.ElgotMonad
|
||||
-- open import Monad.Instance.K.PreElgot TODO
|
||||
open import Monad.PreElgot
|
||||
open import Monad.Instance.K.PreElgot
|
||||
```
|
||||
Loading…
Reference in a new issue