From 2c8d4e07ab3e9e5dd1a32627b5b44f9fb3427345 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Wed, 16 Aug 2023 17:29:13 +0200 Subject: [PATCH] Working on ElgotMonad --- ElgotAlgebra.agda | 35 +++++++++------- Monad/ElgotMonad.agda | 95 +++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 115 insertions(+), 15 deletions(-) create mode 100644 Monad/ElgotMonad.agda diff --git a/ElgotAlgebra.agda b/ElgotAlgebra.agda index ced60a1..0e85bb5 100644 --- a/ElgotAlgebra.agda +++ b/ElgotAlgebra.agda @@ -45,14 +45,11 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where → f ≈ g → (f #) ≈ (g #) + --* -- (unguarded) Elgot-Algebra --* - record Elgot-Algebra : Set (o ⊔ ℓ ⊔ e) where - -- Object - field - A : Obj - + record Elgot-Algebra-on (A : Obj) : Set (o ⊔ ℓ ⊔ e) where -- iteration operator field _# : ∀ {X} → (X ⇒ A + X) → (X ⇒ A) @@ -116,6 +113,11 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where -- every elgot-algebra comes with a divergence constant !ₑ : ⊥ ⇒ A !ₑ = i₂ # + record Elgot-Algebra : Set (o ⊔ ℓ ⊔ e) where + field + A : Obj + algebra : Elgot-Algebra-on A + open Elgot-Algebra-on algebra public --* -- Here follows the proof of equivalence for unguarded and Id-guarded Elgot-Algebras @@ -146,16 +148,19 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where -- constructing an unguarded Elgot-Algebra from an Id-Guarded one Id-Guarded→Unguarded : ∀ {A : Obj} → Guarded-Elgot-Algebra (Id-Algebra A) → Elgot-Algebra - Id-Guarded→Unguarded gea = record - { _# = _# - ; #-Fixpoint = λ {X} {f} → trans #-Fixpoint (∘-resp-≈ˡ ([]-congˡ identityˡ)) - ; #-Uniformity = #-Uniformity - ; #-Folding = λ {X} {Y} {f} {h} → begin - ((f #) +₁ h) # ≈˘⟨ +-g-η ⟩ - [ (f # +₁ h)# ∘ i₁ , (f # +₁ h)# ∘ i₂ ] ≈⟨ []-cong₂ left right ⟩ - [ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₁ , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂ ] ≈⟨ +-g-η ⟩ - ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] #) ∎ - ; #-resp-≈ = #-resp-≈ + Id-Guarded→Unguarded gea = record + { A = A + ; algebra = record + { _# = _# + ; #-Fixpoint = λ {X} {f} → trans #-Fixpoint (∘-resp-≈ˡ ([]-congˡ identityˡ)) + ; #-Uniformity = #-Uniformity + ; #-Folding = λ {X} {Y} {f} {h} → begin + ((f #) +₁ h) # ≈˘⟨ +-g-η ⟩ + [ (f # +₁ h)# ∘ i₁ , (f # +₁ h)# ∘ i₂ ] ≈⟨ []-cong₂ left right ⟩ + [ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₁ , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂ ] ≈⟨ +-g-η ⟩ + ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] #) ∎ + ; #-resp-≈ = #-resp-≈ + } } where open Guarded-Elgot-Algebra gea diff --git a/Monad/ElgotMonad.agda b/Monad/ElgotMonad.agda new file mode 100644 index 0000000..c49f0a9 --- /dev/null +++ b/Monad/ElgotMonad.agda @@ -0,0 +1,95 @@ +open import Level +open import Categories.Category.Core +open import Categories.Category.Extensive.Bundle +open import Categories.Category.BinaryProducts +open import Categories.Category.Cocartesian +open import Categories.Category.Cartesian +open import Categories.Category.Extensive +open import ElgotAlgebra + +import Categories.Morphism.Reasoning as MR + +module Monad.ElgotMonad {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) where + open ExtensiveDistributiveCategory ED renaming (U to C; id to idC) + open HomReasoning + open Cocartesian (Extensive.cocartesian extensive) + open Cartesian (ExtensiveDistributiveCategory.cartesian ED) + open BinaryProducts products hiding (η) + open MR C + open Equiv + + open import Categories.Monad + open import Categories.Functor + + record IsPreElgot (T : Monad C) : Set (o ⊔ ℓ ⊔ e) where + open Monad T + 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 ED (T₀ X) + + module elgotalgebras {X} = Elgot-Algebra-on (elgotalgebras {X}) + + -- with the following associativity + field + assoc : ∀ {X Y Z} (f : Z ⇒ T₀ X + Z) (h : X ⇒ T₀ Y) → elgotalgebras._# (((μ.η _ ∘ T₁ h) +₁ idC) ∘ f) ≈ (μ.η _ ∘ T₁ h) ∘ (elgotalgebras._# {X}) f + + record PreElgotMonad : Set (o ⊔ ℓ ⊔ e) where + field + T : Monad C + isPreElgot : IsPreElgot T + + open IsPreElgot isPreElgot public + + record IsElgot (T : Monad C) : Set (o ⊔ ℓ ⊔ e) where + open Monad T + open Functor F renaming (F₀ to T₀; F₁ to T₁) + + -- iteration operator + field + _† : ∀ {X Y} → X ⇒ T₀ (Y + X) → X ⇒ T₀ Y + + -- laws + field + Fixpoint : ∀ {X Y} {f : X ⇒ T₀ (Y + X)} → f † ≈ (μ.η _ ∘ T₁ [ η.η _ , f † ]) ∘ f + Naturality : ∀ {X Y Z} {f : X ⇒ T₀ (Y + X)} {g : Y ⇒ T₀ Z} → (μ.η _ ∘ T₁ g) ∘ f † ≈ ((μ.η _ ∘ T₁ [ (T₁ i₁) ∘ g , η.η _ ∘ i₂ ]) ∘ f)† + Codiagonal : ∀ {X Y} {f : X ⇒ T₀ ((Y + X) + X)} → (T₁ [ idC , i₂ ] ∘ f )† ≈ f † † + Uniformity : ∀ {X Y Z} {f : X ⇒ T₀ (Y + X)} {g : Z ⇒ T₀ (Y + Z)} {h : Z ⇒ X} → f ∘ h ≈ (T₁ (idC +₁ h)) ∘ g → f † ∘ h ≈ g † + + record ElgotMonad : Set (o ⊔ ℓ ⊔ e) where + field + T : Monad C + isElgot : IsElgot T + + open IsElgot isElgot public + + -- elgot monads are pre-elgot + Elgot⇒PreElgot : ElgotMonad → PreElgotMonad + Elgot⇒PreElgot EM = record + { T = T + ; isPreElgot = record + { elgotalgebras = λ {X} → record + { _# = λ f → ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † + ; #-Fixpoint = λ {Y} {f} → begin + ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ≈⟨ Fixpoint ⟩ + (μ.η _ ∘ T₁ [ η.η _ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ]) ∘ ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) ≈⟨ pullˡ ∘[] ⟩ + [ (μ.η _ ∘ T₁ [ η.η _ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ]) ∘ T₁ i₁ + , (μ.η _ ∘ T₁ [ η.η _ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ]) ∘ η.η _ ∘ i₂ ] ∘ f ≈⟨ []-cong₂ (pullʳ (sym homomorphism)) (pullˡ (pullʳ (η.sym-commute [ η.η _ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ]))) ⟩∘⟨refl ⟩ + [ μ.η _ ∘ T₁ ([ η.η _ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ] ∘ i₁) + , (μ.η _ ∘ (η.η _ ∘ [ η.η _ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ])) ∘ i₂ ] ∘ f ≈⟨ []-cong₂ (∘-resp-≈ʳ (F-resp-≈ inject₁)) (pullʳ (pullʳ inject₂)) ⟩∘⟨refl ⟩ + [ μ.η _ ∘ (T₁ (η.η _)) + , μ.η _ ∘ η.η _ ∘ ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ] ∘ f ≈⟨ []-cong₂ (T.identityˡ) (cancelˡ T.identityʳ) ⟩∘⟨refl ⟩ + [ idC , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ] ∘ f ∎ + ; #-Uniformity = {! !} + ; #-Folding = {! !} + ; #-resp-≈ = {! !} + } + ; assoc = {! !} + } + } + where + open ElgotMonad EM + module T = Monad T + open T + open Functor F renaming (F₀ to T₀; F₁ to T₁)