mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
Add category of strong pre elgot monads
This commit is contained in:
parent
d762e280ad
commit
d3712d4abd
SSH key fingerprint:
SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
2 changed files with 198 additions and 66 deletions
|
|
@ -57,7 +57,7 @@ PreElgotMonads = record
|
||||||
; identityˡ = identityˡ
|
; identityˡ = identityˡ
|
||||||
; identityʳ = identityʳ
|
; identityʳ = identityʳ
|
||||||
; identity² = identity²
|
; identity² = identity²
|
||||||
; equiv = λ {A} {B} → record { refl = refl ; sym = λ f → sym f ; trans = λ f g → trans f g }
|
; equiv = record { refl = refl ; sym = λ f → sym f ; trans = λ f g → trans f g }
|
||||||
; ∘-resp-≈ = λ f≈h g≈i → ∘-resp-≈ f≈h g≈i
|
; ∘-resp-≈ = λ f≈h g≈i → ∘-resp-≈ f≈h g≈i
|
||||||
}
|
}
|
||||||
where
|
where
|
||||||
|
|
|
||||||
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)
|
||||||
|
```
|
||||||
Loading…
Reference in a new issue