🚧 Work on commutativity of K

src/Monad/Instance/K/Commutative.lagda.md

@@ -0,0 +1,84 @@
+<!--
+```agda
+open import Level
+open import Category.Instance.AmbientCategory
+open import Monad.Commutative
+open import Categories.Monad.Strong
+open import Data.Product using (_,_) renaming (_×_ to _×f_)
+open import Categories.FreeObjects.Free
+import Monad.Instance.K as MIK
+```
+-->
+
+```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:
+
+<!-- https://q.uiver.app/#q=WzAsNyxbMCwxLCJLWCBcXHRpbWVzIEtZIl0sWzEsMCwiSyhLWCBcXHRpbWVzIFkpIl0sWzIsMCwiSyhLKFggXFx0aW1lcyBZKSkiXSxbMywxLCJLKFggXFx0aW1lcyBZKSJdLFsxLDIsIksoWCBcXHRpbWVzIEtZKSJdLFsyLDIsIksoSyhYIFxcdGltZXMgWSkpIl0sWzAsNCwiS1ggXFx0aW1lcyBZIl0sWzAsMSwiXFx0YXUiXSxbMSwyLCJcXGhhdHtcXHRhdX1eKiJdLFsyLDMsIlxcbXUiXSxbMCw0LCJcXGhhdHtcXHRhdX0iLDJdLFs0LDUsIlxcdGF1XioiLDJdLFs1LDMsIlxcbXUiLDJdLFs2LDAsImlkIFxcdGltZXMgXFxldGEiXSxbNiwzLCJcXGhhdHtcXHRhdX0iLDAseyJjdXJ2ZSI6NX1dLFswLDMsIlxcaGF0e1xcdGF1fV5cXCMiXV0= -->
+<iframe class="quiver-embed" src="https://q.uiver.app/#q=WzAsNyxbMCwxLCJLWCBcXHRpbWVzIEtZIl0sWzEsMCwiSyhLWCBcXHRpbWVzIFkpIl0sWzIsMCwiSyhLKFggXFx0aW1lcyBZKSkiXSxbMywxLCJLKFggXFx0aW1lcyBZKSJdLFsxLDIsIksoWCBcXHRpbWVzIEtZKSJdLFsyLDIsIksoSyhYIFxcdGltZXMgWSkpIl0sWzAsNCwiS1ggXFx0aW1lcyBZIl0sWzAsMSwiXFx0YXUiXSxbMSwyLCJcXGhhdHtcXHRhdX1eKiJdLFsyLDMsIlxcbXUiXSxbMCw0LCJcXGhhdHtcXHRhdX0iLDJdLFs0LDUsIlxcdGF1XioiLDJdLFs1LDMsIlxcbXUiLDJdLFs2LDAsImlkIFxcdGltZXMgXFxldGEiXSxbNiwzLCJcXGhhdHtcXHRhdX0iLDAseyJjdXJ2ZSI6NX1dLFswLDMsIlxcaGF0e1xcdGF1fV5cXCMiXV0=&embed" width="974" height="688" style="border-radius: 8px; border: none;"></iframe>
+
+```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 ⁂ η _) ≈⟨ {!   !} ⟩ 
+            {!   !} ≈⟨ {!   !} ⟩ 
+            {!   !} ≈⟨ {!   !} ⟩ 
+            {!   !} ≈⟨ {!   !} ⟩ 
+            σ _ ∎)
+```

src/Monad/Instance/K/Strong.lagda.md

@@ -58,24 +58,16 @@ The following diagram demonstrates this:
   open kleisliK using (extend)
   open monadK using (μ)
 
-  KStrength : Strength monoidal monadK
+  -- defining τ
-  KStrength = record
+  private
-    { strengthen = ntHelper (record { η = τ ; commute = commute' })
-    ; identityˡ = identityˡ'
-    ; η-comm = λ {A} {B} → τ-η (A , B)
-    ; μ-η-comm = μ-η-comm'
-    ; 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 τ
+  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
@@ -95,6 +87,15 @@ The following diagram demonstrates this:
     extend (η Y ∘ f) ∘ η X ≈⟨ kleisliK.identityʳ ⟩ 
     η Y ∘ f                ∎
 
+  KStrength : Strength monoidal monadK
+  KStrength = record
+    { strengthen = ntHelper (record { η = τ ; commute = commute' })
+    ; identityˡ = identityˡ'
+    ; η-comm = λ {A} {B} → τ-η (A , B)
+    ; μ-η-comm = μ-η-comm'
+    ; strength-assoc = strength-assoc'
+    }
+    where
       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