From d3712d4abd98ee8bbedba87470d0dfbc198eabfd Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Mon, 20 Nov 2023 10:34:52 +0100 Subject: [PATCH] Add category of strong pre elgot monads --- .../Construction/PreElgotMonads.lagda.md | 132 +++++++++--------- .../StrongPreElgotMonads.lagda.md | 132 ++++++++++++++++++ 2 files changed, 198 insertions(+), 66 deletions(-) create mode 100644 src/Category/Construction/StrongPreElgotMonads.lagda.md diff --git a/src/Category/Construction/PreElgotMonads.lagda.md b/src/Category/Construction/PreElgotMonads.lagda.md index 5bf16cd..1309679 100644 --- a/src/Category/Construction/PreElgotMonads.lagda.md +++ b/src/Category/Construction/PreElgotMonads.lagda.md @@ -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) ``` diff --git a/src/Category/Construction/StrongPreElgotMonads.lagda.md b/src/Category/Construction/StrongPreElgotMonads.lagda.md new file mode 100644 index 0000000..880a987 --- /dev/null +++ b/src/Category/Construction/StrongPreElgotMonads.lagda.md @@ -0,0 +1,132 @@ + + +# 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) +```