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. "1f4e5460d7adb961460cde3d5f7734aec97f0a9b" and "55dcf598fc9100a13e6811ce8df39bb3569ee41b" have entirely different histories.
1f4e5460d7
...
55dcf598fc
6 changed files with 131 additions and 168 deletions
|
|
@ -17,7 +17,7 @@ open import Categories.Category.Core
|
|||
```agda
|
||||
module Category.Construction.PreElgotMonads {o ℓ e} (ambient : Ambient o ℓ e) where
|
||||
open Ambient ambient
|
||||
open import Monad.PreElgot ambient
|
||||
open import Monad.ElgotMonad ambient
|
||||
open import Algebra.ElgotAlgebra ambient
|
||||
open HomReasoning
|
||||
open Equiv
|
||||
|
|
|
|||
|
|
@ -1,5 +1,7 @@
|
|||
<!--
|
||||
```agda
|
||||
{-# OPTIONS --allow-unsolved-metas #-}
|
||||
|
||||
open import Level
|
||||
open import Category.Instance.AmbientCategory using (Ambient)
|
||||
open import Categories.Monad.Construction.Kleisli
|
||||
|
|
@ -9,16 +11,54 @@ open import Categories.Functor
|
|||
```
|
||||
-->
|
||||
|
||||
## Summary
|
||||
This file introduces Elgot Monads.
|
||||
|
||||
TODO: Probably only Pre-Elgot is needed
|
||||
|
||||
- [X] *Definition 13* Pre-Elgot Monads
|
||||
- [ ] *Definition 13* strong pre-Elgot
|
||||
- [X] *Definition 14* Elgot Monads
|
||||
- [ ] *Definition 14* strong Elgot
|
||||
- [ ] *Proposition 15* (Strong) Elgot monads are (strong) pre-Elgot
|
||||
|
||||
## Code
|
||||
|
||||
```agda
|
||||
module Misc.Monad.Elgot {o ℓ e} (ambient : Ambient o ℓ e) where
|
||||
module Monad.ElgotMonad {o ℓ e} (ambient : Ambient o ℓ e) where
|
||||
open Ambient ambient
|
||||
open HomReasoning
|
||||
open MR C
|
||||
open Equiv
|
||||
open import Algebra.ElgotAlgebra ambient
|
||||
open import Monad.PreElgot ambient
|
||||
```
|
||||
|
||||
### *Definition 13*: Pre-Elgot Monads
|
||||
|
||||
```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
|
||||
field
|
||||
elgotalgebras : ∀ {X} → Elgot-Algebra-on (T₀ X)
|
||||
|
||||
module elgotalgebras {X} = Elgot-Algebra-on (elgotalgebras {X})
|
||||
|
||||
-- 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
|
||||
|
||||
record PreElgotMonad : Set (o ⊔ ℓ ⊔ e) where
|
||||
field
|
||||
T : Monad C
|
||||
isPreElgot : IsPreElgot T
|
||||
|
||||
open IsPreElgot isPreElgot public
|
||||
```
|
||||
### *Definition 14*: Elgot Monads
|
||||
|
||||
```agda
|
||||
|
|
@ -50,7 +90,7 @@ module Misc.Monad.Elgot {o ℓ e} (ambient : Ambient o ℓ e) where
|
|||
open IsElgot isElgot public
|
||||
```
|
||||
|
||||
### *Proposition 15*: Elgot monads are pre-Elgot
|
||||
### *Proposition 15*: (Strong) Elgot monads are (strong) pre-Elgot
|
||||
|
||||
-- elgot monads are pre-elgot
|
||||
Elgot⇒PreElgot : ElgotMonad → PreElgotMonad
|
||||
|
|
@ -107,4 +147,4 @@ module Misc.Monad.Elgot {o ℓ e} (ambient : Ambient o ℓ e) where
|
|||
open ElgotMonad EM
|
||||
module T = Monad T
|
||||
open T using (F; η; μ)
|
||||
open Functor F renaming (F₀ to T₀; F₁ to T₁)
|
||||
open Functor F renaming (F₀ to T₀; F₁ to T₁)
|
||||
|
|
@ -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.Compositionality ambient MK
|
||||
|
||||
open Equiv
|
||||
open HomReasoning
|
||||
|
|
|
|||
|
|
@ -1,3 +1,5 @@
|
|||
# TODO: every KX satisfies compositionality
|
||||
|
||||
```agda
|
||||
{-# OPTIONS --allow-unsolved-metas #-}
|
||||
open import Level
|
||||
|
|
@ -6,10 +8,8 @@ open import Category.Instance.AmbientCategory
|
|||
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.Compositionality {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where
|
||||
open Ambient ambient
|
||||
open MIK ambient
|
||||
open MonadK MK
|
||||
|
|
@ -20,9 +20,9 @@ open MIK ambient
|
|||
open MonadK MK
|
||||
open import Algebra.ElgotAlgebra ambient
|
||||
open import Algebra.UniformIterationAlgebra ambient
|
||||
open import Monad.PreElgot ambient
|
||||
open import Monad.ElgotMonad ambient
|
||||
open import Monad.Instance.K ambient
|
||||
open import Monad.Instance.K.Elgot ambient MK
|
||||
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
|
||||
|
|
@ -37,22 +37,22 @@ open M C
|
|||
# K is a pre-Elgot monad
|
||||
|
||||
```agda
|
||||
-- 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
|
||||
|
||||
isPreElgot : IsPreElgot monadK
|
||||
isPreElgot = record
|
||||
{ elgotalgebras = λ {X} → elgot X
|
||||
; extend-preserves = λ 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 }
|
||||
|
||||
strongPreElgot : IsStrongPreElgot KStrong
|
||||
strongPreElgot = record
|
||||
{ preElgot = isPreElgot
|
||||
; strengthen-preserves = τ-comm
|
||||
}
|
||||
|
||||
-- initialPreElgot :
|
||||
initialPreElgot : IsInitial PreElgotMonads preElgot
|
||||
initialPreElgot = record
|
||||
{ ! = !′
|
||||
|
|
@ -67,112 +67,108 @@ initialPreElgot = record
|
|||
})
|
||||
; α-η = FreeObject.*-lift (freealgebras _) (T.η.η _)
|
||||
; α-μ = α-μ
|
||||
; preserves = λ {X} {B} f → Elgot-Algebra-Morphism.preserves (((freeElgot B) FreeObject.*) {A = record { A = T.F.F₀ B ; algebra = PreElgotMonad.elgotalgebras A }} (T.η.η B))
|
||||
; 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-≈)
|
||||
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 = Elgot-Algebra-Morphism.h (_* {A = T-Alg X} (T.η.η X))
|
||||
η' X = Elgot-Algebra-Morphism.h (_* {A = record { A = T.F.F₀ X ; algebra = PreElgotMonad.elgotalgebras A }} (T.η.η 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
|
||||
-- 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 ∎
|
||||
η' 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ʳ (K₁-preserves f g) ⟩
|
||||
η' Y ∘ (((K.₁ f +₁ idC) ∘ g) #K) ≈⟨ η'-preserves ((K.₁ f +₁ idC) ∘ g) ⟩
|
||||
(η' 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 ∎
|
||||
((η' 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 (PreElgotMonad.extend-preserves A ((η' X +₁ idC) ∘ g) (T.η.η Y ∘ f)) ⟩
|
||||
(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 ∎
|
||||
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 ∎
|
||||
((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))
|
||||
{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) ∎
|
||||
η' 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ʳ (μK-preserves g) ⟩
|
||||
η' X ∘ ((μK.η X +₁ idC) ∘ g) #K ≈⟨ η'-preserves ((μK.η X +₁ idC) ∘ g) ⟩
|
||||
(η' 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) ∎
|
||||
(((η' 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 (PreElgotMonad.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 (PreElgotMonad.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-≈ (PreElgotMonad.elgotalgebras A) (pullˡ (+₁∘+₁ ○ +₁-cong₂ ((elimʳ T.F.identity) ⟩∘⟨ (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) ∎
|
||||
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 ∎
|
||||
(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 (FreeObject.*-uniq
|
||||
(freeElgot X)
|
||||
{A = record { A = T.F.F₀ X ; algebra = PreElgotMonad.elgotalgebras A }}
|
||||
(T.η.η X)
|
||||
(record { h = α.η X ; preserves = preserves _ })
|
||||
α-η)
|
||||
!-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)
|
||||
```
|
||||
|
|
|
|||
|
|
@ -1,73 +0,0 @@
|
|||
<!--
|
||||
```agda
|
||||
{-# OPTIONS --allow-unsolved-metas #-}
|
||||
|
||||
open import Level
|
||||
open import Category.Instance.AmbientCategory using (Ambient)
|
||||
open import Categories.Monad.Construction.Kleisli
|
||||
open import Categories.Monad
|
||||
open import Categories.Monad.Strong
|
||||
open import Categories.Monad.Relative renaming (Monad to RMonad)
|
||||
open import Categories.Functor
|
||||
open import Data.Product using (_,_)
|
||||
```
|
||||
-->
|
||||
|
||||
```agda
|
||||
module Monad.PreElgot {o ℓ e} (ambient : Ambient o ℓ e) where
|
||||
open Ambient ambient
|
||||
open HomReasoning
|
||||
open MR C
|
||||
open Equiv
|
||||
open import Algebra.ElgotAlgebra ambient
|
||||
```
|
||||
|
||||
# (strong) pre-Elgot monads
|
||||
|
||||
```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
|
||||
field
|
||||
elgotalgebras : ∀ {X} → Elgot-Algebra-on (T₀ X)
|
||||
|
||||
module elgotalgebras {X} = Elgot-Algebra-on (elgotalgebras {X})
|
||||
|
||||
-- where kleisli lifting preserves iteration
|
||||
field
|
||||
extend-preserves : ∀ {X Y Z} (f : Z ⇒ T₀ X + Z) (h : X ⇒ T₀ Y)
|
||||
→ elgotalgebras._# ((extend h +₁ idC) ∘ f) ≈ extend h ∘ elgotalgebras._# {X} f
|
||||
|
||||
record PreElgotMonad : Set (o ⊔ ℓ ⊔ e) where
|
||||
field
|
||||
T : Monad C
|
||||
isPreElgot : IsPreElgot T
|
||||
|
||||
open IsPreElgot isPreElgot public
|
||||
|
||||
record IsStrongPreElgot (SM : StrongMonad monoidal) : Set (o ⊔ ℓ ⊔ e) where
|
||||
open StrongMonad SM using (M; strengthen)
|
||||
open Monad M using (F)
|
||||
|
||||
-- M is pre-Elgot
|
||||
field
|
||||
preElgot : IsPreElgot M
|
||||
|
||||
open IsPreElgot preElgot public
|
||||
|
||||
-- and strength is iteration preserving
|
||||
field
|
||||
strengthen-preserves : ∀ {X Y Z} (f : Z ⇒ F.₀ Y + Z)
|
||||
→ strengthen.η (X , Y) ∘ (idC ⁂ elgotalgebras._# f) ≈ elgotalgebras._# ((strengthen.η (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ f))
|
||||
|
||||
record StrongPreElgotMonad : Set (o ⊔ ℓ ⊔ e) where
|
||||
field
|
||||
SM : StrongMonad monoidal
|
||||
isStrongPreElgot : IsStrongPreElgot SM
|
||||
|
||||
open IsStrongPreElgot isStrongPreElgot public
|
||||
```
|
||||
|
||||
Loading…
Reference in a new issue