<!--
```agda
{-# OPTIONS --allow-unsolved-metas #-}
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
open import Categories.Morphism.Properties
```
-->

```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 import Algebra.ElgotAlgebra ambient
open import Monad.Instance.K.ElgotAlgebra ambient MK

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

open monadK using (μ)
open kleisliK using (extend)
open strongK using (strengthen)
open IsStableFreeUniformIterationAlgebra using (♯-law; ♯-preserving; ♯-unique; ♯ˡ-unique; ♯ˡ-preserving; ♯ˡ-law)
open Uniform-Iteration-Algebra using (#-Uniformity; #-Fixpoint; #-resp-≈)
#-Compositionality = λ {A X Y : Obj} {f : X ⇒ K.₀ A + X} {h : Y ⇒ X + Y} → Elgot-Algebra-on.#-Compositionality (elgot A) {X} {Y} {f} {h}

-- some helper definitions to make our life easier
private
  η = λ Z → FreeObject.η (freealgebras Z)
  _♯ = λ {A X Y} f → IsStableFreeUniformIterationAlgebra.[_,_]♯ {Y = X} (stable X) {X = A} (algebras Y) f
  _♯ˡ = λ {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

σ-η : ∀ {X Y} → σ (X , Y) ∘ (η _ ⁂ idC) ≈ η _
σ-η = begin
  σ (_ , _) ∘ (η _ ⁂ idC) ≈⟨ pullʳ (pullʳ swap∘⁂) ⟩
  K.₁ swap ∘ τ (_ , _) ∘ (idC ⁂ η _) ∘ swap ≈⟨ refl⟩∘⟨ (pullˡ (τ-η _)) ⟩
    K.₁ swap ∘ η _ ∘ swap  ≈⟨ pullˡ (K₁η swap) ⟩
  (η _ ∘ swap) ∘ swap ≈⟨ cancelʳ swap∘swap ⟩
  η (_ × _) ∎

σ-comm : ∀ {X Y Z} (h : Z ⇒ K.₀ X + Z) → σ (X , Y) ∘ (h # ⁂ idC) ≈ ((σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC))#
σ-comm {X} {Y} {Z} h = begin
  (K.₁ swap ∘ τ _ ∘ swap) ∘ (h # ⁂ idC) ≈⟨ pullʳ (pullʳ swap∘⁂) ⟩
  K.₁ swap ∘ τ _ ∘ (idC ⁂ h #) ∘ swap ≈⟨ refl⟩∘⟨ (pullˡ (τ-comm h)) ⟩
  K.₁ swap ∘ ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∘ swap ≈⟨ pullˡ (Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) (η _ ∘ swap))) ⟩
  ((K.₁ swap +₁ idC) ∘ (τ (Y , X) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∘ swap ≈⟨ sym (#-Uniformity (algebras _) (sym by-uni)) ⟩
  ((σ (X , Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) # ∎
  where
    by-uni : ((K.₁ swap +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ swap ≈ (idC +₁ swap) ∘ (σ (X , Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)
    by-uni = begin
      ((K.₁ swap +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ swap ≈⟨ pullʳ (pullʳ (pullʳ (sym swap∘⁂))) ⟩
      (K.₁ swap +₁ idC) ∘ (τ (Y , X) +₁ idC) ∘ distributeˡ⁻¹ ∘ swap ∘ (h ⁂ idC) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ distributeˡ⁻¹∘swap ⟩
      (K.₁ swap +₁ idC) ∘ (τ (Y , X) +₁ idC) ∘ ((swap +₁ swap) ∘ distributeʳ⁻¹) ∘ (h ⁂ idC) ≈⟨ pullˡ +₁∘+₁ ⟩
      (K.₁ swap ∘ τ _ +₁ idC ∘ idC) ∘ ((swap +₁ swap) ∘ distributeʳ⁻¹) ∘ (h ⁂ idC) ≈⟨ pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ assoc (elimˡ identity²))) ⟩
      ((σ _ +₁ swap) ∘ distributeʳ⁻¹) ∘ (h ⁂ idC) ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ○ sym-assoc ⟩
      (idC +₁ swap) ∘ (σ (X , Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ∎

extend-preserve : ∀ {X Y Z} (f : X ⇒ K.₀ Y) (h : Z ⇒ K.₀ X + Z) → extend f ∘ h # ≈ ((extend f +₁ idC) ∘ h) #
extend-preserve {X} {Y} {Z} f h = begin
  (μ.η _ ∘ K.₁ f) ∘ h # ≈⟨ pullʳ (Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) (η _ ∘ f))) ⟩
  μ.η _ ∘ ((K.₁ f +₁ idC) ∘ h) # ≈⟨ Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) idC) ⟩
  ((μ.η _ +₁ idC) ∘ (K.₁ f +₁ idC) ∘ h) # ≈⟨ #-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩
  ((extend f +₁ idC) ∘ h) # ∎

proof-principle : ∀ {X Y} (f g : K.₀ X × K.₀ Y ⇒ K.₀ (X × Y)) → f ∘ (η _ ⁂ η _) ≈ g ∘ (η _ ⁂ η _) → (∀ {A} (h : A ⇒ K.₀ Y + A) → f ∘ (idC ⁂ h #) ≈ ((f +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#) → (∀ {A} (h : A ⇒ K.₀ X + A) → f ∘ (h # ⁂ idC) ≈ ((f +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #) → (∀ {A} (h : A ⇒ K.₀ Y + A) → g ∘ (idC ⁂ h #) ≈ ((g +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#) → (∀ {A} (h : A ⇒ K.₀ X + A) → g ∘ (h # ⁂ idC) ≈ ((g +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #) → f ≈ g
proof-principle {X} {Y} f g η-eq f-iter₁ f-iter₂ g-iter₁ g-iter₂ = begin 
  f ≈⟨ ♯-unique (stable _) (f ∘ (idC ⁂ η Y)) f refl (λ h → f-iter₁ h) ⟩ 
  (f ∘ (idC ⁂ η _)) ♯ ≈⟨ sym (♯-unique (stable _) (f ∘ (idC ⁂ η Y)) g helper₁ g-iter₁) ⟩ 
  g ∎
  where
    helper₁ : f ∘ (idC ⁂ η Y) ≈ g ∘ (idC ⁂ η Y)
    helper₁ = begin
      f ∘ (idC ⁂ η Y) ≈⟨ ♯ˡ-unique (stable _) (f ∘ (η X ⁂ η Y)) (f ∘ (idC ⁂ η Y)) (sym (pullʳ (⁂∘⁂ ○ (⁂-cong₂ identityˡ identityʳ)))) (comm₁ f f-iter₂) ⟩ 
      (f ∘ (η X ⁂ η Y)) ♯ˡ ≈⟨ sym (♯ˡ-unique (stable _) (f ∘ (η X ⁂ η Y)) (g ∘ (idC ⁂ η Y)) (sym (pullʳ (⁂∘⁂ ○ (⁂-cong₂ identityˡ identityʳ)) ○ sym η-eq)) (comm₁ g g-iter₂)) ⟩ 
      g ∘ (idC ⁂ η Y) ∎
      where
        comm₁ : ∀ (k : K.₀ X × K.₀ Y ⇒ K.₀ (X × Y)) (k-iter₂ : ∀ {A} (h : A ⇒ K.₀ X + A) → k ∘ (h # ⁂ idC) ≈ ((k +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #) {Z : Obj} (h : Z ⇒ K.₀ X + Z) → (k ∘ (idC ⁂ η Y)) ∘ (h # ⁂ idC) ≈ ((k ∘ (idC ⁂ η Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #
        comm₁ k k-iter₂ {Z} h = begin 
          (k ∘ (idC ⁂ η Y)) ∘ (h # ⁂ idC) ≈⟨ pullʳ ⁂∘⁂ ⟩ 
          k ∘ (idC ∘ h # ⁂ η Y ∘ idC) ≈⟨ refl⟩∘⟨ (⁂-cong₂ id-comm-sym id-comm) ⟩ 
          k ∘ (h # ∘ idC ⁂ idC ∘ η Y) ≈⟨ refl⟩∘⟨ sym ⁂∘⁂ ⟩ 
          k ∘ (h # ⁂ idC) ∘ (idC ⁂ η Y) ≈⟨ pullˡ (k-iter₂ h) ⟩ 
          (((k +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #) ∘ (idC ⁂ η Y) ≈⟨ sym (#-Uniformity (algebras _) uni-helper) ⟩ 
          ((k ∘ (idC ⁂ η Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) # ∎
          where
            uni-helper : (idC +₁ idC ⁂ η Y) ∘ (k ∘ (idC ⁂ η Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈ ((k +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) ∘ (idC ⁂ η Y)
            uni-helper = begin 
              (idC +₁ idC ⁂ η Y) ∘ (k ∘ (idC ⁂ η Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈⟨ pullˡ +₁∘+₁ ⟩ 
              (idC ∘ k ∘ (idC ⁂ η Y) +₁ (idC ⁂ η Y) ∘ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈⟨ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ⟩ 
              (k ∘ (idC ⁂ η Y) +₁ idC ∘ (idC ⁂ η Y)) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈⟨ (sym +₁∘+₁) ⟩∘⟨refl ⟩ 
              ((k +₁ idC) ∘ ((idC ⁂ η Y) +₁ (idC ⁂ η Y))) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈⟨ pullʳ (pullˡ (distribute₁' (η Y) idC idC)) ⟩ 
              (k +₁ idC) ∘ (distributeʳ⁻¹ ∘ ((idC +₁ idC) ⁂ η Y)) ∘ (h ⁂ idC) ≈⟨ refl⟩∘⟨ pullʳ ⁂∘⁂ ⟩ 
              (k +₁ idC) ∘ distributeʳ⁻¹ ∘ ((idC +₁ idC) ∘ h ⁂ η Y ∘ idC) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ (elimˡ ([]-unique id-comm-sym id-comm-sym)) identityʳ ⟩ 
              (k +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ η Y) ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ identityʳ identityˡ ⟩
              (k +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ∘ idC ⁂ idC ∘ η Y) ≈˘⟨ pullʳ (pullʳ ⁂∘⁂) ⟩
              ((k +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) ∘ (idC ⁂ η Y) ∎

KCommutative : CommutativeMonad {C = C} {V = monoidal} symmetric KStrong
KCommutative = record { commutes = commutes' }
  where
    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 #) ≈⟨ sym-assoc ⟩∘⟨refl ⟩
          ψ ∘ (idC ⁂ h #) ≈⟨ ♯ˡ-unique (stable _) (τ (X , Y) ∘ (idC ⁂ (h #))) (ψ ∘ (idC ⁂ (h #))) (sym comm₅)  comm₇   ⟩
          (τ _ ∘ (idC ⁂ h #)) ♯ˡ ≈⟨ sym (♯ˡ-unique (stable _) (τ (X , Y) ∘ (idC ⁂ (h #))) (((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #) (sym comm₆) comm₈) ⟩
          ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ≈⟨ #-resp-≈ (algebras _) ((+₁-cong₂ assoc refl) ⟩∘⟨refl)  ⟩
          ((μ.η _ ∘ K.₁ (τ _) ∘ σ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∎
          where
            ψ : ∀ {X Y} → K.₀ X × K.₀ Y ⇒ K.₀ (X × Y)
            ψ = extend (τ _) ∘ σ _
            comm₅ : (ψ ∘ (idC ⁂ (h #))) ∘ (η _ ⁂ idC) ≈ τ _ ∘ (idC ⁂ h #)
            comm₅ = begin 
              (ψ ∘ (idC ⁂ (h #))) ∘ (η _ ⁂ idC) ≈⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ id-comm-sym id-comm) ⟩ 
              ψ ∘ (η _ ∘ idC ⁂ idC ∘ h #) ≈⟨ refl⟩∘⟨ (sym ⁂∘⁂) ⟩ 
              ψ ∘ (η X ⁂ idC) ∘ (idC ⁂ (h #)) ≈⟨ pullˡ (pullʳ  σ-η  ) ⟩
              (extend (τ _) ∘ η _) ∘ (idC ⁂ h #)  ≈⟨ kleisliK.identityʳ ⟩∘⟨refl ⟩
              τ (X , Y) ∘ (idC ⁂ (h #)) ∎
            comm₆ : ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ (η _ ⁂ idC) ≈ τ _ ∘ (idC ⁂ h #)
            comm₆ = begin
              ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∘ (η _ ⁂ idC) ≈⟨ sym (#-Uniformity (algebras _) (sym by-uni)) ⟩
              ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ≈⟨ sym (τ-comm h) ⟩
              τ (X , Y) ∘ (idC ⁂ (h #)) ∎
              where
                by-uni : ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ (η _ ⁂ idC) ≈ (idC +₁ (η _ ⁂ idC)) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)
                by-uni = begin
                  ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ (η _ ⁂ idC) ≈⟨ pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ id-comm-sym id-comm ○ sym ⁂∘⁂)) ⟩
                  (ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (η _ ⁂ idC) ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ pullˡ (sym (distribute₁ _ _ _ ○ refl⟩∘⟨ ⁂-cong₂ refl ([]-unique id-comm-sym id-comm-sym))) ⟩
                  (ψ +₁ idC) ∘ ((η _ ⁂ idC +₁ η _ ⁂ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h) ≈⟨ pullˡ (pullˡ +₁∘+₁) ⟩
                  ((ψ ∘ (η _ ⁂ idC) +₁ idC ∘ (η _ ⁂ idC)) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h) ≈⟨ assoc ○ (+₁-cong₂ (pullʳ σ-η) identityˡ) ⟩∘⟨refl ⟩
                  (extend (τ _) ∘ η _ +₁ η _ ⁂ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ (+₁-cong₂ kleisliK.identityʳ refl) ⟩∘⟨refl ⟩
                  (τ _ +₁ (η _ ⁂ idC)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ sym (pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ)) ⟩
                  (idC +₁ (η _ ⁂ idC)) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ∎
            comm₇ : ∀ {U} (g : U ⇒ K.₀ X + U) → (ψ ∘ (idC ⁂ h #)) ∘ (g # ⁂ idC) ≈ ((ψ ∘ (idC ⁂ h #) +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #
            comm₇ {U} g = begin
              (ψ ∘ (idC ⁂ h #)) ∘ (g # ⁂ idC) ≈⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ id-comm-sym id-comm ○ sym ⁂∘⁂) ⟩
              ψ ∘ (g # ⁂ idC) ∘ (idC ⁂ h #) ≈⟨ pullˡ (pullʳ (σ-comm g)) ⟩
              (extend (τ _) ∘ ((σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) ∘ (idC ⁂ h #) ≈⟨ extend-preserve (τ (X , Y)) _ ⟩∘⟨refl ⟩
              ((extend (τ _) +₁ idC) ∘ (σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) # ∘ (idC ⁂ h #) ≈⟨ sym (#-Uniformity (algebras _) (sym by-uni)) ⟩
              ((ψ ∘ (idC ⁂ h #) +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))# ∎
              where
                by-uni : ((extend (τ _) +₁ idC) ∘ (σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) ∘ (idC ⁂ h #) ≈ (idC +₁ (idC ⁂ h #)) ∘ ((ψ ∘ (idC ⁂ h #)) +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)
                by-uni = begin
                  ((extend (τ _) +₁ idC) ∘ (σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) ∘ (idC ⁂ h #) ≈⟨ pullʳ (pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ id-comm id-comm-sym ○ sym ⁂∘⁂))) ⟩
                  (extend (τ _) +₁ idC) ∘ (σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (idC ⁂ (h #)) ∘ (g ⁂ idC) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym (distribute₁' _ _ _ ○ refl⟩∘⟨ ⁂-cong₂ ([]-unique id-comm-sym id-comm-sym) refl)) ⟩
                  (extend (τ _) +₁ idC) ∘ (σ _ +₁ idC) ∘ ((idC ⁂ h # +₁ idC ⁂ h #) ∘ distributeʳ⁻¹) ∘ (g ⁂ idC) ≈⟨ pullˡ +₁∘+₁ ○ pullˡ (pullˡ +₁∘+₁) ⟩
                  ((ψ ∘ (idC ⁂ h #) +₁ (idC ∘ idC) ∘ (idC ⁂ h #)) ∘ distributeʳ⁻¹) ∘ (g ⁂ idC) ≈⟨ assoc ○ (+₁-cong₂ refl (elimˡ identity²)) ⟩∘⟨refl ⟩
                  (ψ ∘ (idC ⁂ h #) +₁ (idC ⁂ h #)) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟩
                  (idC +₁ (idC ⁂ h #)) ∘ ((ψ ∘ (idC ⁂ h #)) +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) ∎
            comm₈ : ∀ {U} (g : U ⇒ K.₀ X + U) → ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∘ (g # ⁂ idC) ≈ ((((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#
            comm₈ {U} g = begin
              ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ (g # ⁂ idC) ≈⟨ {!!} ⟩ -- Uniformity
              ((((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) # +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-Compositionality ⟩
              ( [ (idC +₁ i₁) ∘ (ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) , i₂ ∘ i₂ ] ∘ [ i₁ , distributeˡ⁻¹ ∘ (idC ⁂ h) ]) # ∘ i₂ ≈⟨ {!!} ⟩
              ([ (ψ +₁ i₁) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) , i₂ ∘ i₂ ] ∘ [ i₁ , distributeˡ⁻¹ ∘ (idC ⁂ h) ]) # ∘ i₂ ≈⟨ {!!} ⟩
              [ [ (ψ +₁ i₁) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) , i₂ ∘ i₂ ] ∘ i₁ , [ (ψ +₁ i₁) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) , i₂ ∘ i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ] # ∘ i₂ ≈⟨ {!!} ⟩
              [ (ψ +₁ i₁) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) , [ (ψ +₁ i₁) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) , i₂ ∘ i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ] # ∘ i₂ ≈⟨ {!!} ⟩
              ([ (ψ +₁ i₁) ∘ distributeʳ⁻¹ , [ (ψ +₁ i₁) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) , i₂ ∘ i₂ ] ∘ distributeˡ⁻¹ ] ∘ (g ⁂ idC +₁ idC ⁂ h)) # ∘ i₂ ≈⟨ {!!} ⟩
              {!!} ≈⟨ {!!} ⟩
              {!!} ≈⟨ {!!} ⟩
              {!!} ≈⟨ {!!} ⟩
              {!!} ≈⟨ {!!} ⟩
              {!!} ≈⟨ {!!} ⟩
              {!!} ≈⟨ {!!} ⟩
              ([((ψ +₁ i₁) ∘ distributeʳ⁻¹) , (i₂ ∘ i₂ ∘ distributeʳ⁻¹) ] ∘ distributeˡ⁻¹ ∘ {!!}) # ∘ i₂ ∘ i₂ ≈⟨ {!!} ⟩
              {!!} ≈˘⟨ {!!} ⟩
              {!!} ≈˘⟨ {!!} ⟩
              {!!} ≈˘⟨ {!!} ⟩
              {!!} ≈˘⟨ {!!} ⟩
              ([ (idC +₁ i₁) ∘ (ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) , i₂ ∘ i₂ ] ∘ [ i₁ , distributeʳ⁻¹ ∘ (g ⁂ idC) ]) # ∘ i₂ ≈˘⟨  #-Compositionality ⟩
              ((((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))# ∎

```