bsc-leon-vatthauer/src/Monad/Instance/K/Commutative.lagda.md

<!--
```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, the relevant diagram is:

<!-- https://q.uiver.app/#q=WzAsNyxbMCwxLCJLWCBcXHRpbWVzIEtZIl0sWzEsMCwiSyhLWCBcXHRpbWVzIFkpIl0sWzIsMCwiSyhLKFggXFx0aW1lcyBZKSkiXSxbMywxLCJLKFggXFx0aW1lcyBZKSJdLFsxLDIsIksoWCBcXHRpbWVzIEtZKSJdLFsyLDIsIksoSyhYIFxcdGltZXMgWSkpIl0sWzAsNCwiS1ggXFx0aW1lcyBZIl0sWzAsMSwiXFx0YXUiXSxbMSwyLCJLXFxoYXR7XFx0YXV9Il0sWzIsMywiXFxtdSJdLFswLDQsIlxcaGF0e1xcdGF1fSIsMl0sWzQsNSwiS1xcdGF1IiwyXSxbNSwzLCJcXG11IiwyXSxbNiwwLCJpZCBcXHRpbWVzIFxcZXRhIl0sWzYsMywiXFxoYXR7XFx0YXV9IiwwLHsiY3VydmUiOjV9XSxbMCwzLCJcXGhhdHtcXHRhdX1eXFwjIl1d -->
<iframe class="quiver-embed" src="https://q.uiver.app/#q=WzAsNyxbMCwxLCJLWCBcXHRpbWVzIEtZIl0sWzEsMCwiSyhLWCBcXHRpbWVzIFkpIl0sWzIsMCwiSyhLKFggXFx0aW1lcyBZKSkiXSxbMywxLCJLKFggXFx0aW1lcyBZKSJdLFsxLDIsIksoWCBcXHRpbWVzIEtZKSJdLFsyLDIsIksoSyhYIFxcdGltZXMgWSkpIl0sWzAsNCwiS1ggXFx0aW1lcyBZIl0sWzAsMSwiXFx0YXUiXSxbMSwyLCJLXFxoYXR7XFx0YXV9Il0sWzIsMywiXFxtdSJdLFswLDQsIlxcaGF0e1xcdGF1fSIsMl0sWzQsNSwiS1xcdGF1IiwyXSxbNSwzLCJcXG11IiwyXSxbNiwwLCJpZCBcXHRpbWVzIFxcZXRhIl0sWzYsMywiXFxoYXR7XFx0YXV9IiwwLHsiY3VydmUiOjV9XSxbMCwzLCJcXGhhdHtcXHRhdX1eXFwjIl1d&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 using (strengthen)
      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

      σ-preserve : ∀ {X Y Z : Obj} (h : Z ⇒ K.₀ Y + Z) → σ (Y , X) ∘ (h # ⁂ idC) ≈ ((σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC))#
      {-
      K.₁ swap ∘ τ ∘ swap ∘ (h # ⁂ idC)
      ≈ K.₁ swap ∘ τ ∘ (idC ⁂ h #) ∘ swap
      ≈ K.₁ swap ∘ ()# ∘ swap
      ≈ ((K.₁ swap +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ swap
      -}
      σ-preserve {Z} h = {!   !}
      σ-preserve' : ∀ {X Y Z : Obj} (h : Z ⇒ K.₀ Y + Z) → σ (X , K.₀ Y) ∘ (idC ⁂ h #) ≈ ((σ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#
      σ-preserve' {Z} h = {!   !}
      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₃ 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 
            (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ η _) ≈⟨ pullʳ (pullʳ (pullʳ (pullʳ swap∘⁂))) ⟩ 
            μ.η _ ∘ K.₁ (τ _) ∘ K.₁ swap ∘ τ _ ∘ (η _ ⁂ idC) ∘ swap ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ refl (sym K.identity) ⟩∘⟨refl ⟩ 
            μ.η _ ∘ K.₁ (τ _) ∘ K.₁ swap ∘ τ _ ∘ (η _ ⁂ K.₁ idC) ∘ swap ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (strengthen.commute (η _ , idC)) ⟩ 
            μ.η _ ∘ K.₁ (τ _) ∘ K.₁ swap ∘ (K.₁ (η _ ⁂ idC) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (pullˡ (sym K.homomorphism)) ⟩ 
            μ.η _ ∘ K.₁ (τ _) ∘ (K.₁ (swap ∘ (η _ ⁂ idC)) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ (pullˡ (pullˡ (sym K.homomorphism))) ⟩ 
            μ.η _ ∘ (K.₁ (τ _ ∘ swap ∘ (η _ ⁂ idC)) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ (((K.F-resp-≈ (refl⟩∘⟨ swap∘⁂)) ⟩∘⟨refl) ⟩∘⟨refl) ⟩ 
            μ.η _ ∘ (K.₁ (τ _ ∘ (idC ⁂ η _) ∘ swap) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ (K.F-resp-≈ (pullˡ (τ-η _))) ⟩∘⟨refl ⟩∘⟨refl ⟩ 
            μ.η _ ∘ (K.₁ (η _ ∘ swap) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ ((K.homomorphism ⟩∘⟨refl) ⟩∘⟨refl) ⟩ 
            μ.η _ ∘ ((K.₁ (η _) ∘ K.₁ swap) ∘ τ _) ∘ swap ≈⟨ pullˡ (pullˡ (cancelˡ monadK.identityˡ)) ⟩ 
            (K.₁ swap ∘ τ _) ∘ swap ≈⟨ assoc ⟩ 
            σ _ ∎)
          comm₄ : ∀ {Z : Obj} (h : Z ⇒ K.₀ Y + Z) → (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ h #) ≈ ((μ.η _ ∘ K.₁ (τ _) ∘ σ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#
          comm₄ {Z} h = begin 
            (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ h #) ≈⟨ {!   !} ⟩ 
            (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ ((i₁ # ∘ idC) ⁂ h #) ≈˘⟨ {!   !} ⟩
            (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (((i₁ #) ⁂ h #)) ≈˘⟨ refl⟩∘⟨ ⟨⟩-cong₂ (#-Uniformity (algebras _) helper₁) {!   !} ⟩
            (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ ⟨ ((π₁ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # , ((π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ⟩ ≈⟨ {!   !} ⟩
            {!   !} ≈⟨ {!   !} ⟩
            {!   !} ≈⟨ {!   !} ⟩
            {!   !} ≈⟨ {!   !} ⟩
            ((μ.η _ ∘ K.₁ (τ _) ∘ σ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∎
            where
              -- this leads nowhere
              helper₁ : (idC +₁ π₁) ∘ (π₁ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈ i₁ ∘ π₁
              helper₁ = begin 
                (idC +₁ π₁) ∘ (π₁ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟩ 
                (π₁ +₁ π₁) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ {!   !} ⟩ 
                i₁ ∘ π₁ ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ π₁∘⁂ ⟩ 
                i₁ ∘ idC ∘ π₁ ≈⟨ refl⟩∘⟨ identityˡ ⟩ 
                i₁ ∘ π₁ ∎
              test : ((τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ swap ≈ ((τ (X , Y) ∘ swap +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #
              test = sym (#-Uniformity (algebras _) (sym (begin 
                ((τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ swap ≈⟨ pullʳ (pullʳ (sym swap∘⁂)) ⟩ 
                (τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ swap ∘ (h ⁂ idC) ≈⟨ refl⟩∘⟨ (pullˡ distributeˡ⁻¹∘swap) ⟩
                (τ (X , Y) +₁ idC) ∘ ((swap +₁ swap) ∘ distributeʳ⁻¹) ∘ (h ⁂ idC) ≈⟨ pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ (sym identityˡ) id-comm-sym)) ⟩
                ((idC ∘ τ (X , Y) ∘ swap +₁ swap ∘ idC) ∘ distributeʳ⁻¹) ∘ (h ⁂ idC) ≈⟨ assoc ○ (sym +₁∘+₁) ⟩∘⟨refl ⟩
                ((idC +₁ swap) ∘ (τ (X , Y) ∘ swap +₁ idC)) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈⟨ assoc ⟩
                (idC +₁ swap) ∘ (τ (X , Y) ∘ swap +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ∎)))
              helper : τ _ ∘ (h # ⁂ idC) ∘ swap ≈ ((τ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) # ∘ swap
              helper = {!   !}
              τ∘swap-preserving : τ (K.₀ Y , X) ∘ (h # ⁂ idC) ≈ ((τ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #
              τ∘swap-preserving = begin 
                τ (K.₀ Y , X) ∘ (h # ⁂ idC) ≈⟨ {!   !} ⟩ 
                τ (K.₀ Y , X) ∘ (h # ⁂ K.₁ idC) ≈⟨ {!   !} ⟩ 
                K.₁ (h # ⁂ idC) ∘ τ _ ≈⟨ {!   !} ⟩ 
                {!   !} ≈⟨ {!   !} ⟩ 
                ((τ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) # ∎
```