From f92fbc76edabd811737807284551624cd858e589 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Sat, 28 Oct 2023 17:37:01 +0200 Subject: [PATCH] =?UTF-8?q?=F0=9F=9A=A7=20Work=20on=20commutativity=20of?= =?UTF-8?q?=20K?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Monad/Instance/K/Commutative.lagda.md | 84 +++++++++++++++++++++++ src/Monad/Instance/K/Strong.lagda.md | 57 +++++++-------- 2 files changed, 113 insertions(+), 28 deletions(-) create mode 100644 src/Monad/Instance/K/Commutative.lagda.md diff --git a/src/Monad/Instance/K/Commutative.lagda.md b/src/Monad/Instance/K/Commutative.lagda.md new file mode 100644 index 0000000..5bed959 --- /dev/null +++ b/src/Monad/Instance/K/Commutative.lagda.md @@ -0,0 +1,84 @@ + + +```agda +module Monad.Instance.K.Commutative {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where + open Ambient ambient + open MIK ambient + open MonadK MK + open import Monad.Instance.K.Strong ambient MK + open import Category.Construction.UniformIterationAlgebras ambient + open import Algebra.UniformIterationAlgebra ambient + open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF; IsStableFreeUniformIterationAlgebra) + + open Equiv + open HomReasoning + open MR C + -- open M C +``` + +# K is a commutative monad +The proof is analogous to the ones for strength, this is the relevant diagram is: + + + + +```agda + KCommutative : CommutativeMonad {C = C} {V = monoidal} symmetric KStrong + KCommutative = record { commutes = commutes' } + where + open monadK using (μ) + open StrongMonad KStrong + open IsStableFreeUniformIterationAlgebra using (♯-law; ♯-preserving; ♯-unique) + open Uniform-Iteration-Algebra using (#-Uniformity; #-Fixpoint; #-resp-≈) + + -- some helper definitions to make our life easier + η = λ Z → FreeObject.η (freealgebras Z) + _♯ = λ {A X Y} f → IsStableFreeUniformIterationAlgebra.[_,_]♯ {Y = X} (stable X) {X = A} (algebras Y) f + _# = λ {A} {X} f → Uniform-Iteration-Algebra._# (algebras A) {X = X} f + + σ : ∀ ((X , Y) : Obj ×f Obj) → K.₀ X × Y ⇒ K.₀ (X × Y) + σ _ = K.₁ swap ∘ (τ _) ∘ swap + commutes' : ∀ {X Y : Obj} → μ.η _ ∘ K.₁ (σ _) ∘ τ (K.₀ X , Y) ≈ μ.η _ ∘ K.₁ (τ _) ∘ σ _ + commutes' {X} {Y} = begin + μ.η _ ∘ K.₁ (σ _) ∘ τ _ ≈⟨ ♯-unique (stable _) (σ _) (μ.η (X × Y) ∘ K.₁ (σ _) ∘ τ _) comm₁ comm₂ ⟩ + (σ _) ♯ ≈⟨ sym (♯-unique (stable _) (σ _) (μ.η _ ∘ K.₁ (τ _) ∘ σ _) comm₃ {! !}) ⟩ + μ.η _ ∘ K.₁ (τ _) ∘ σ _ ∎ + where + comm₁ : σ _ ≈ (μ.η _ ∘ K.₁ (σ _) ∘ τ _) ∘ (idC ⁂ η _) + comm₁ = sym (begin + (μ.η _ ∘ K.₁ (σ _) ∘ τ _) ∘ (idC ⁂ η _) ≈⟨ pullʳ (pullʳ (τ-η _)) ⟩ + μ.η _ ∘ K.₁ (σ _) ∘ η _ ≈⟨ refl⟩∘⟨ (K₁η _) ⟩ + μ.η _ ∘ η _ ∘ σ _ ≈⟨ cancelˡ monadK.identityʳ ⟩ + σ _ ∎) + comm₂ : ∀ {Z : Obj} (h : Z ⇒ K.₀ Y + Z) → (μ.η _ ∘ K.₁ (σ _) ∘ τ _) ∘ (idC ⁂ h #) ≈ ((μ.η _ ∘ K.₁ (σ _) ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# + comm₂ {Z} h = begin + (μ.η _ ∘ K.₁ (σ _) ∘ τ _) ∘ (idC ⁂ h #) ≈⟨ pullʳ (pullʳ (♯-preserving (stable _) (η _) h)) ⟩ + μ.η _ ∘ K.₁ (σ _) ∘ ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ refl⟩∘⟨ (Uniform-Iteration-Algebra-Morphism.preserves ((freealgebras _ FreeObject.*) (η _ ∘ σ _))) ⟩ + μ.η _ ∘ ((K.₁ (σ _) +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) idC) ⟩ + ((μ.η _ +₁ idC) ∘ (K.₁ (σ _) +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ +₁∘+₁) ⟩ + ((μ.η _ ∘ K.₁ (σ _) +₁ idC ∘ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ +₁∘+₁) ⟩ + (((μ.η _ ∘ K.₁ (σ _)) ∘ τ _ +₁ (idC ∘ idC) ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) ((+₁-cong₂ assoc (elimˡ identity²)) ⟩∘⟨refl) ⟩ + ((μ.η _ ∘ K.₁ (σ _) ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∎ + comm₃ : σ _ ≈ (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ η _) + comm₃ = sym (begin + -- idea use swap epi and K.₁ swap mono: + {- + K.₁ swap ∘ (μ.η _ ∘ K.₁ (K.₁ swap ∘ τ _) ∘ σ _) ∘ (idC ⁂ η _) ∘ swap + ≈ (μ.η _ ∘ K.₁ (σ _) ∘ (τ _)) ∘ (η _ ⁂ idC) + -} + (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ η _) ≈⟨ {! !} ⟩ + {! !} ≈⟨ {! !} ⟩ + {! !} ≈⟨ {! !} ⟩ + {! !} ≈⟨ {! !} ⟩ + σ _ ∎) +``` \ No newline at end of file diff --git a/src/Monad/Instance/K/Strong.lagda.md b/src/Monad/Instance/K/Strong.lagda.md index 0934431..5077bb7 100644 --- a/src/Monad/Instance/K/Strong.lagda.md +++ b/src/Monad/Instance/K/Strong.lagda.md @@ -58,6 +58,35 @@ The following diagram demonstrates this: open kleisliK using (extend) open monadK using (μ) + -- defining τ + private + -- some helper definitions to make our life easier + η = λ Z → FreeObject.η (freealgebras Z) + _♯ = λ {A X Y} f → IsStableFreeUniformIterationAlgebra.[_,_]♯ {Y = X} (stable X) {X = A} (algebras Y) f + _# = λ {A} {X} f → Uniform-Iteration-Algebra._# (algebras A) {X = X} f + + open IsStableFreeUniformIterationAlgebra using (♯-law; ♯-preserving; ♯-unique) + open Uniform-Iteration-Algebra using (#-Uniformity; #-Fixpoint; #-resp-≈) + + module _ (P : Category.Obj (CProduct C C)) where + private + X = proj₁ P + Y = proj₂ P + τ : X × K.₀ Y ⇒ K.₀ (X × Y) + τ = η (X × Y) ♯ + + τ-η : τ ∘ (idC ⁂ η Y) ≈ η (X × Y) + τ-η = sym (♯-law (stable Y) (η (X × Y))) + + τ-comm : ∀ {X Y Z : Obj} (h : Z ⇒ K.₀ Y + Z) → τ (X , Y) ∘ (idC ⁂ h #) ≈ ((τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# + τ-comm {X} {Y} {Z} h = ♯-preserving (stable Y) (η (X × Y)) h + + K₁η : ∀ {X Y} (f : X ⇒ Y) → K.₁ f ∘ η X ≈ η Y ∘ f + K₁η {X} {Y} f = begin + K.₁ f ∘ η X ≈⟨ (sym (F₁⇒extend monadK f)) ⟩∘⟨refl ⟩ + extend (η Y ∘ f) ∘ η X ≈⟨ kleisliK.identityʳ ⟩ + η Y ∘ f ∎ + KStrength : Strength monoidal monadK KStrength = record { strengthen = ntHelper (record { η = τ ; commute = commute' }) @@ -67,34 +96,6 @@ The following diagram demonstrates this: ; strength-assoc = strength-assoc' } where - open IsStableFreeUniformIterationAlgebra using (♯-law; ♯-preserving; ♯-unique) - open Uniform-Iteration-Algebra using (#-Uniformity; #-Fixpoint; #-resp-≈) - - -- some helper definitions to make our life easier - η = λ Z → FreeObject.η (freealgebras Z) - _♯ = λ {A X Y} f → IsStableFreeUniformIterationAlgebra.[_,_]♯ {Y = X} (stable X) {X = A} (algebras Y) f - _# = λ {A} {X} f → Uniform-Iteration-Algebra._# (algebras A) {X = X} f - - -- defining τ - module _ (P : Category.Obj (CProduct C C)) where - private - X = proj₁ P - Y = proj₂ P - τ : X × K.₀ Y ⇒ K.₀ (X × Y) - τ = η (X × Y) ♯ - - τ-η : τ ∘ (idC ⁂ η Y) ≈ η (X × Y) - τ-η = sym (♯-law (stable Y) (η (X × Y))) - - τ-comm : ∀ {X Y Z : Obj} (h : Z ⇒ K.₀ Y + Z) → τ (X , Y) ∘ (idC ⁂ h #) ≈ ((τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# - τ-comm {X} {Y} {Z} h = ♯-preserving (stable Y) (η (X × Y)) h - - K₁η : ∀ {X Y} (f : X ⇒ Y) → K.₁ f ∘ η X ≈ η Y ∘ f - K₁η {X} {Y} f = begin - K.₁ f ∘ η X ≈⟨ (sym (F₁⇒extend monadK f)) ⟩∘⟨refl ⟩ - extend (η Y ∘ f) ∘ η X ≈⟨ kleisliK.identityʳ ⟩ - η Y ∘ f ∎ - commute' : ∀ {P₁ : Category.Obj (CProduct C C)} {P₂ : Category.Obj (CProduct C C)} (fg : _[_,_] (CProduct C C) P₁ P₂) → τ P₂ ∘ ((proj₁ fg) ⁂ K.₁ (proj₂ fg)) ≈ K.₁ ((proj₁ fg) ⁂ (proj₂ fg)) ∘ τ P₁ commute' {(U , V)} {(W , X)} (f , g) = begin