From 72560dfb59af4e799dd618dbd7024fdaba476c9b Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Thu, 17 Aug 2023 18:07:26 +0200 Subject: [PATCH] Added (pre) elgot monat --- Monad/ElgotMonad.agda | 65 ++++++++++++++++++++++++++++++++----------- 1 file changed, 49 insertions(+), 16 deletions(-) diff --git a/Monad/ElgotMonad.agda b/Monad/ElgotMonad.agda index c49f0a9..dc4299c 100644 --- a/Monad/ElgotMonad.agda +++ b/Monad/ElgotMonad.agda @@ -33,7 +33,8 @@ module Monad.ElgotMonad {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) w -- 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 + 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 @@ -49,13 +50,18 @@ module Monad.ElgotMonad {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) w -- iteration operator field _† : ∀ {X Y} → X ⇒ T₀ (Y + X) → X ⇒ T₀ Y + †-resp-≈ : ∀ {X Y} {f g : X ⇒ T₀ (Y + X)} → f ≈ g → f † ≈ g † -- 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 † + 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 @@ -72,24 +78,51 @@ module Monad.ElgotMonad {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) w { elgotalgebras = λ {X} → record { _# = λ f → ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ; #-Fixpoint = λ {Y} {f} → begin - ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ≈⟨ Fixpoint ⟩ + ([ 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₂ ] ∘ f ≈˘⟨ []-cong₂ + (pushʳ (homomorphism)) + (pushˡ (pushʳ (η.commute _))) + ⟩∘⟨refl ⟩ [ μ.η _ ∘ T₁ ([ η.η _ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ] ∘ i₁) - , (μ.η _ ∘ (η.η _ ∘ [ η.η _ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ])) ∘ i₂ ] ∘ f ≈⟨ []-cong₂ (∘-resp-≈ʳ (F-resp-≈ inject₁)) (pullʳ (pullʳ inject₂)) ⟩∘⟨refl ⟩ + , (μ.η _ ∘ (η.η _ ∘ [ η.η _ , ([ 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 = {! !} + , μ.η _ ∘ η.η _ ∘ ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ] ∘ f ≈⟨ []-cong₂ (T.identityˡ) (cancelˡ T.identityʳ) ⟩∘⟨refl ⟩ + [ idC , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ] ∘ f ∎ + ; #-Uniformity = λ {X} {Y} {f} {g} {h} H → sym (Uniformity (begin + ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ g) ∘ h ≈˘⟨ pushʳ H ⟩ + [ T₁ i₁ , η.η _ ∘ i₂ ] ∘ (idC +₁ h) ∘ f ≈⟨ pullˡ []∘+₁ ⟩ + [ T₁ i₁ ∘ idC , (η.η _ ∘ i₂) ∘ h ] ∘ f ≈⟨ []-cong₂ (trans identityʳ (F-resp-≈ (sym identityʳ))) assoc ⟩∘⟨refl ⟩ + [ T₁ (i₁ ∘ idC) , η.η _ ∘ i₂ ∘ h ] ∘ f ≈˘⟨ []-cong₂ (F-resp-≈ +₁∘i₁) (pullʳ +₁∘i₂) ⟩∘⟨refl ⟩ + [ T₁ ((idC +₁ h) ∘ i₁) , (η.η _ ∘ (idC +₁ h)) ∘ i₂ ] ∘ f ≈⟨ []-cong₂ homomorphism ( pushˡ (η.commute _)) ⟩∘⟨refl ⟩ + [ T₁ (idC +₁ h) ∘ T₁ i₁ , T₁ (idC +₁ h) ∘ η.η _ ∘ i₂ ] ∘ f ≈˘⟨ pullˡ ∘[] ⟩ + T₁ (idC +₁ h) ∘ [ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f ∎)) + ; #-Folding = λ {X} {Y} {f} {h} → begin + ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ ((([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) †) +₁ h))† ≈⟨ †-resp-≈ []∘+₁ ⟩ + [ T₁ i₁ ∘ ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † , (η.η _ ∘ i₂) ∘ h ] † ≈⟨ {! !} ⟩ + {! !} ≈⟨ {! !} ⟩ + [ [ T₁ i₁ ∘ idC , (η.η _ ∘ i₂) ∘ i₁ ] ∘ f , (η.η _ ∘ i₂) ∘ h ] † ≈˘⟨ †-resp-≈ ([]-cong₂ (pullˡ []∘+₁) (pullˡ inject₂)) ⟩ + [ [ T₁ i₁ , η.η _ ∘ i₂ ] ∘ (idC +₁ i₁) ∘ f , [ T₁ i₁ , η.η _ ∘ i₂ ] ∘ i₂ ∘ h ] † ≈˘⟨ †-resp-≈ ∘[] ⟩ + ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])† ∎ + ; #-resp-≈ = λ fg → †-resp-≈ (∘-resp-≈ʳ fg) + } + ; assoc = λ {X} {Y} {Z} f h → begin + -- TODO tidy up by moving doing sym outside, apply Naturality and then do `†-resp-≈ pullˡ` once. + ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ (μ.η Y ∘ T₁ h +₁ idC) ∘ f)† ≈⟨ †-resp-≈ (pullˡ []∘+₁) ⟩ + (([ T₁ i₁ ∘ μ.η _ ∘ T₁ h , (η.η _ ∘ i₂) ∘ idC ] ∘ f)†) ≈˘⟨ †-resp-≈ (∘-resp-≈ˡ ([]-cong₂ assoc (sym identityʳ))) ⟩ + ([ (T₁ i₁ ∘ μ.η _) ∘ T₁ h , η.η _ ∘ i₂ ] ∘ f)† ≈˘⟨ †-resp-≈ (∘-resp-≈ˡ ([]-congʳ (pullˡ (μ.commute _)))) ⟩ + ([ μ.η _ ∘ T₁ (T₁ i₁) ∘ T₁ h , η.η _ ∘ i₂ ] ∘ f)† ≈˘⟨ †-resp-≈ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ʳ homomorphism) (cancelˡ T.identityʳ))) ⟩ + ([ μ.η _ ∘ T₁ (T₁ i₁ ∘ h) , μ.η _ ∘ η.η _ ∘ η.η _ ∘ i₂ ] ∘ f)† ≈˘⟨ †-resp-≈ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ʳ (F-resp-≈ inject₁)) (∘-resp-≈ʳ (pullʳ inject₂)))) ⟩ + ([ μ.η _ ∘ T₁ ([ T₁ i₁ ∘ h , η.η _ ∘ i₂ ] ∘ i₁) , μ.η _ ∘ (η.η _ ∘ [ T₁ i₁ ∘ h , η.η _ ∘ i₂ ]) ∘ i₂ ] ∘ f)† ≈˘⟨ †-resp-≈ (∘-resp-≈ˡ ([]-cong₂ (pullʳ (sym homomorphism)) (pullʳ (pullˡ (η.sym-commute _))))) ⟩ + ([ (μ.η _ ∘ T₁ [ T₁ i₁ ∘ h , η.η _ ∘ i₂ ]) ∘ T₁ i₁ , (μ.η _ ∘ T₁ [ T₁ i₁ ∘ h , η.η _ ∘ i₂ ]) ∘ η.η _ ∘ i₂ ] ∘ f)† ≈˘⟨ †-resp-≈ (pullˡ ∘[]) ⟩ + ((μ.η _ ∘ T₁ [ T₁ i₁ ∘ h , η.η _ ∘ i₂ ]) ∘ [ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f)† ≈˘⟨ Naturality ⟩ + (μ.η Y ∘ T₁ h) ∘ ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f)† ∎ } } where open ElgotMonad EM module T = Monad T - open T + open T using (F; η; μ) open Functor F renaming (F₀ to T₀; F₁ to T₁)