open import Level
open import Categories.Category.Core
open import Categories.Monad.Commutative
open import Categories.Monad.Strong
open import Categories.Category.Distributive
open import Data.Product using (_,_) renaming (_×_ to _×f_)
open import Categories.FreeObjects.Free
open import Monad.Helper

import Categories.Morphism as M
import Categories.Morphism.Reasoning as MR
import Categories.Morphism.Properties as MP
import Monad.Instance.K as MIK


-- K is a Commutative Monad

module Monad.Instance.K.Commutative {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) (MK : MIK.MonadK distributive) where
open import Category.Distributive.Helper distributive renaming (η to η-prod)
open Bundles
open MIK distributive
open MonadK MK
open FreeObject using (*-uniq)
open import Monad.Instance.K.Strong distributive MK
open import Category.Construction.ElgotAlgebras cocartesian
open import Algebra.Elgot cocartesian
open import Algebra.Elgot.Free cocartesian using (FreeElgotAlgebra; elgotForgetfulF)
open import Algebra.Elgot.Stable distributive using (IsStableFreeElgotAlgebra; IsStableFreeElgotAlgebraˡ; isStable⇒isStableˡ)

open Category C
open Equiv
open HomReasoning
open MP C
open MR C
open M C

open monadK using (μ)
open kleisliK using (extend)
open strongK using (strengthen)
open IsStableFreeElgotAlgebra using (♯-law; ♯-preserving; ♯-unique)
open IsStableFreeElgotAlgebraˡ using (♯ˡ-unique; ♯ˡ-preserving; ♯ˡ-law)

σ : ∀ ((X , Y) : Obj ×f Obj) → K.₀ X × Y ⇒ K.₀ (X × Y)
σ _ = K.₁ swap ∘ (τ _) ∘ swap

σ-η : ∀ {X Y} → σ (X , Y) ∘ (η _ ×₁ id) ≈ η _
σ-η = begin
  σ (_ , _) ∘ (η _ ×₁ id)                   ≈⟨ pullʳ (pullʳ swap∘×₁) ⟩
  K.₁ swap ∘ τ (_ , _) ∘ (id ×₁ η _) ∘ 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 # ×₁ id) ≈ ((σ _ +₁ id) ∘ distributeʳ⁻¹ ∘ (h ×₁ id))#
σ-comm {X} {Y} {Z} h = begin
  (K.₁ swap ∘ τ _ ∘ swap) ∘ (h # ×₁ id)                                       ≈⟨ pullʳ (pullʳ swap∘×₁) ⟩
  K.₁ swap ∘ τ _ ∘ (id ×₁ h #) ∘ swap                                         ≈⟨ refl⟩∘⟨ (pullˡ (τ-comm h)) ⟩
  K.₁ swap ∘ ((τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)) # ∘ swap               ≈⟨ pullˡ (Elgot-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) (η _ ∘ swap))) ⟩
  ((K.₁ swap +₁ id) ∘ (τ (Y , X) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)) # ∘ swap ≈⟨ sym (#-Uniformity (algebras _) (sym by-uni)) ⟩
  ((σ (X , Y) +₁ id) ∘ distributeʳ⁻¹ ∘ (h ×₁ id)) #                           ∎
  where
    by-uni : ((K.₁ swap +₁ id) ∘ (τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)) ∘ swap ≈ (id +₁ swap) ∘ (σ (X , Y) +₁ id) ∘ distributeʳ⁻¹ ∘ (h ×₁ id)
    by-uni = begin
      ((K.₁ swap +₁ id) ∘ (τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)) ∘ swap                 ≈⟨ pullʳ (pullʳ (pullʳ (sym swap∘×₁))) ⟩
      (K.₁ swap +₁ id) ∘ (τ (Y , X) +₁ id) ∘ distributeˡ⁻¹ ∘ swap ∘ (h ×₁ id)             ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ distributeˡ⁻¹∘swap ⟩
      (K.₁ swap +₁ id) ∘ (τ (Y , X) +₁ id) ∘ ((swap +₁ swap) ∘ distributeʳ⁻¹) ∘ (h ×₁ id) ≈⟨ pullˡ +₁∘+₁ ⟩
      (K.₁ swap ∘ τ _ +₁ id ∘ id) ∘ ((swap +₁ swap) ∘ distributeʳ⁻¹) ∘ (h ×₁ id)          ≈⟨ pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ assoc (elimˡ identity²))) ⟩
      ((σ _ +₁ swap) ∘ distributeʳ⁻¹) ∘ (h ×₁ id)                                         ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ○ sym-assoc ⟩
      (id +₁ swap) ∘ (σ (X , Y) +₁ id) ∘ distributeʳ⁻¹ ∘ (h ×₁ id)                        ∎

σ-natural : ∀ {X Y Z U} (f : X ⇒ Y) (g : Z ⇒ U) → σ _ ∘ (K.₁ f ×₁ g) ≈ K.₁ (f ×₁ g) ∘ σ _
σ-natural {X} {Y} {Z} {U} f g = begin 
  σ _ ∘ (K.₁ f ×₁ g)                       ≈⟨ pullʳ (pullʳ swap∘×₁) ⟩ 
  K.₁ swap ∘ τ _ ∘ (g ×₁ K.₁ f) ∘ swap     ≈⟨ refl⟩∘⟨ ((pullˡ (strengthen.commute (g , f))) ○ assoc) ⟩ 
  K.₁ swap ∘ K.₁ (g ×₁ f) ∘ τ _ ∘ swap     ≈⟨ pullˡ (sym monadK.F.homomorphism) ⟩ 
  K.₁ (swap ∘ (g ×₁ f)) ∘ τ _ ∘ swap       ≈⟨ (monadK.F.F-resp-≈ swap∘×₁) ⟩∘⟨refl ⟩ 
  K.₁ ((f ×₁ g) ∘ swap) ∘ τ _ ∘ swap       ≈⟨ monadK.F.homomorphism ⟩∘⟨refl ⟩ 
  (K.₁ ((f ×₁ g)) ∘ K.₁ swap) ∘ τ _ ∘ swap ≈⟨ assoc ⟩ 
  K.₁ (f ×₁ g) ∘ σ _                       ∎ 

σ-μ-η-comm : ∀ {A B} → μ.η (A × B) ∘ K.₁ (σ _) ∘ σ _ ≈ σ _ ∘ (μ.η _ ×₁ id)
σ-μ-η-comm {A} {B} = begin 
  μ.η (A × B) ∘ K.₁ (σ _) ∘ σ _                     ≈⟨ refl⟩∘⟨ (pullˡ (sym monadK.F.homomorphism)) ⟩ 
  μ.η _ ∘ K.₁ (σ _ ∘ swap) ∘ τ _ ∘ swap             ≈⟨ refl⟩∘⟨ ((monadK.F.F-resp-≈ (pullʳ (cancelʳ swap∘swap))) ⟩∘⟨refl) ⟩ 
  μ.η _ ∘ K.₁ (K.₁ swap ∘ τ _) ∘ τ _ ∘ swap         ≈⟨ refl⟩∘⟨ (monadK.F.homomorphism ⟩∘⟨refl) ⟩ 
  μ.η _ ∘ (K.₁ (K.₁ swap) ∘ K.₁ (τ _)) ∘ τ _ ∘ swap ≈⟨ pullˡ (pullˡ (μ.commute swap)) ⟩ 
  (((K.₁ swap) ∘ μ.η _) ∘ K.₁ (τ _)) ∘ τ _ ∘ swap   ≈⟨ assoc²αε ○ refl⟩∘⟨ (sym assoc²βε) ⟩ 
  (K.₁ swap) ∘ (μ.η _ ∘ K.₁ (τ _) ∘ τ _) ∘ swap     ≈⟨ refl⟩∘⟨ (pushˡ strongK.μ-η-comm) ⟩ 
  K.₁ swap ∘ τ _ ∘ (id ×₁ μ.η _) ∘ swap             ≈˘⟨ pullʳ (pullʳ swap∘×₁) ⟩ 
  σ _ ∘ (μ.η _ ×₁ id)                               ∎

σ-π₁ : ∀ {A B} → K.₁ π₁ ∘ σ (A , B) ≈ π₁
σ-π₁ {A} {B} = begin 
  K.₁ π₁ ∘ σ _        ≈⟨ pullˡ (sym K.homomorphism ○ K.F-resp-≈ project₁) ⟩ 
  K.₁ π₂ ∘ τ _ ∘ swap ≈⟨ pullˡ (τ-π₂ (B , A)) ⟩ 
  π₂ ∘ swap           ≈⟨ project₂ ⟩ 
  π₁                  ∎

σ-kleisli-assoc : ∀ {X Y Z U} (f : X ⇒ K.₀ Y) (g : Z ⇒ K.₀ U) → extend (σ _ ∘ (f ×₁ id)) ∘ σ _ ∘ (id ×₁ extend g) ≈ σ _ ∘ (extend f ×₁ extend g)
σ-kleisli-assoc {X} {Y} {Z} {U} f g = begin 
  extend (σ _ ∘ (f ×₁ id)) ∘ σ _ ∘ (id ×₁ extend g)      ≈˘⟨ pullˡ (extend∘F₁ monadK (σ _) (f ×₁ id)) ⟩ 
  extend (σ _) ∘ K.₁ (f ×₁ id) ∘ σ _ ∘ (id ×₁ extend g)  ≈⟨ refl⟩∘⟨ (pullˡ (sym (σ-natural f id)) ○ assoc) ⟩ 
  extend (σ _) ∘ σ _ ∘ (K.₁ f ×₁ id) ∘ (id ×₁ extend g)  ≈⟨ pullˡ (assoc ○ σ-μ-η-comm) ○ assoc ⟩
  σ _ ∘ (μ.η _ ×₁ id) ∘ (K.₁ f ×₁ id) ∘ (id ×₁ extend g) ≈⟨ refl⟩∘⟨ (pullˡ (×₁∘×₁ ○ ×₁-cong₂ refl identity²)) ⟩ 
  σ _ ∘ (extend f ×₁ id) ∘ (id ×₁ extend g)              ≈⟨ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ identityʳ identityˡ) ⟩
  σ _ ∘ (extend f ×₁ extend g) ∎

-- K satisfies the equational lifting law
equationalLifting : ∀ {X} → τ (K.₀ X , X) ∘ Δ {K.₀ X} ≈ K.₁ ⟨ η X , id ⟩
equationalLifting {X} = *-uniq (freealgebras _) (η _ ∘ ⟨ η X , id ⟩) (record { h = τ (K.₀ X , X) ∘ Δ ; preserves = preserves' }) commute
  where
  preserves' : ∀ {Z} {f : Z ⇒ K.₀ X + Z} → (τ (K.₀ X , X) ∘ Δ) ∘ f # ≈ ((τ (K.₀ X , X) ∘ Δ +₁ id) ∘ f) #
  preserves' {Z} {f} = begin 
    (τ (K.₀ X , X) ∘ Δ) ∘ f #                                 ≈⟨ pullʳ Δ∘ ⟩ 
    τ (K.₀ X , X) ∘ ⟨ f # , f # ⟩                             ≈⟨ refl⟩∘⟨ ((⟨⟩-cong₂ (sym identityˡ) (sym identityʳ)) ○ sym ×₁∘⟨⟩) ⟩ 
    τ (K.₀ X , X) ∘ (id ×₁ f #) ∘ ⟨ f # , id ⟩                ≈⟨ pullˡ (τ-comm f) ⟩ 
    ((τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ f))# ∘ ⟨ f # , id ⟩ ≈⟨ sym (#-Uniformity (algebras _) by-uni) ⟩
    ((τ (K.₀ X , X) ∘ Δ +₁ id) ∘ f) #                         ∎
    where
    by-uni : (id +₁ ⟨ f # , id ⟩) ∘ (τ (K.₀ X , X) ∘ Δ +₁ id) ∘ f ≈ ((τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ f)) ∘ ⟨ f # , id ⟩
    by-uni = begin 
      (id +₁ ⟨ f # , id ⟩) ∘ (τ (K.₀ X , X) ∘ Δ +₁ id) ∘ f     ≈⟨ pullˡ +₁∘+₁ ⟩ 
      (id ∘ τ (K.₀ X , X) ∘ Δ +₁ ⟨ f # , id ⟩ ∘ id) ∘ f        ≈⟨ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ⟩ 
      (τ (K.₀ X , X) ∘ Δ +₁ id ∘ ⟨ f # , id ⟩) ∘ f             ≈⟨ (sym +₁∘+₁) ⟩∘⟨refl ⟩ 
      ((τ _ +₁ id) ∘ (Δ +₁ ⟨ f # , id ⟩)) ∘ f                  ≈⟨ assoc ⟩ 
      (τ _ +₁ id) ∘ (Δ +₁ ⟨ f # , id ⟩) ∘ f                    ≈⟨ refl⟩∘⟨ distrib ⟩ 
      (τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ ⟨ f # , f ⟩                ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ identityˡ identityʳ ⟩ 
      (τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ ⟨ id ∘ f # , f ∘ id ⟩      ≈˘⟨ pullʳ (pullʳ ×₁∘⟨⟩) ⟩ 
      ((τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ f)) ∘ ⟨ f # , id ⟩ ∎
      where
      distrib : (Δ +₁ ⟨ f # , id ⟩) ∘ f ≈ distributeˡ⁻¹ ∘ ⟨ f # , f ⟩
      distrib = Iso⇒Mono (IsIso.iso isIsoˡ) ((Δ +₁ ⟨ f # , id ⟩) ∘ f) (distributeˡ⁻¹ ∘ ⟨ f # , f ⟩) (begin 
        distributeˡ ∘ (Δ +₁ ⟨ f # , id ⟩) ∘ f              ≈⟨ pullˡ []∘+₁ ⟩ 
        [ (id ×₁ i₁) ∘ Δ , (id ×₁ i₂) ∘ ⟨ f # , id ⟩ ] ∘ f ≈⟨ ([]-cong₂ ×₁∘Δ ×₁∘⟨⟩) ⟩∘⟨refl ⟩ 
        [ ⟨ id , i₁ ⟩ , ⟨ id ∘ f # , i₂ ∘ id ⟩ ] ∘ f       ≈⟨ ([]-unique 
                                                              (⟨⟩∘ ○ (⟨⟩-cong₂ inject₁ identityˡ)) 
                                                              (⟨⟩∘ ○ (⟨⟩-cong₂ (inject₂ ○ sym identityˡ) id-comm-sym))) ⟩∘⟨refl ⟩ 
        ⟨ [ id , f # ] , id ⟩ ∘ f                          ≈⟨ ⟨⟩∘ ⟩ 
        ⟨ [ id , f # ] ∘ f , id ∘ f ⟩                      ≈˘⟨ ⟨⟩-cong₂ (#-Fixpoint (algebras _)) (sym identityˡ) ⟩ 
        ⟨ f # , f ⟩                                        ≈˘⟨ cancelˡ (IsIso.isoʳ isIsoˡ) ⟩ 
        distributeˡ ∘ distributeˡ⁻¹ ∘ ⟨ f # , f ⟩          ∎)
  commute : (τ (K.₀ X , X) ∘ Δ) ∘ η _ ≈ η _ ∘ ⟨ η X , id ⟩
  commute = begin 
    (τ (K.₀ X , X) ∘ Δ) ∘ η _                  ≈⟨ pullʳ Δ∘ ⟩ 
    τ (K.₀ X , X) ∘ ⟨ η X , η X ⟩              ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ (sym identityˡ) (sym identityʳ) ○ sym ×₁∘⟨⟩) ⟩ 
    τ (K.₀ X , X) ∘ (id ×₁ η X) ∘ ⟨ η X , id ⟩ ≈⟨ pullˡ (τ-η _) ⟩ 
    η _ ∘ ⟨ η X , id ⟩                         ∎

-- Key helper lemma

private
  comm-helper : ∀ {X Y Z U} (f : X ⇒ K.₀ Y + X) (g : Z ⇒ K.₀ U + Z) → extend (τ _) ∘ σ _ ∘ (((η _ +₁ id) ∘ f) # ×₁ ((η _ +₁ id) ∘ g) #) ≈ extend (σ _) ∘ τ _ ∘ (((η _ +₁ id) ∘ f) # ×₁ ((η _ +₁ id) ∘ g) #)
  comm-helper {X} {Y} {Z} {U} f g = begin 
    extend (τ _) ∘ σ _ ∘ (f' # ×₁ g' #)                               ≈⟨ τσ ⟩ 
    extend ([ σ _ ∘ ( f' # ×₁ id ) , τ _ ∘ (id ×₁ g' #) ]) ∘ w #      ≈⟨ sym στ ⟩ 
    extend (σ _) ∘ τ _ ∘ (((η _ +₁ id) ∘ f) # ×₁ ((η _ +₁ id) ∘ g) #) ∎
    where
      f' = (η _ +₁ id) ∘ f
      g' = (η _ +₁ id) ∘ g
      w : X × Z ⇒ monadK.F.F₀ (X × K.₀ U + K.₀ Y × Z) + X × Z
      w = [ i₁ ∘ K.₁ i₁ ∘ τ _ , (K.₁ i₂ ∘ σ _ +₁ id) ∘ distributeʳ⁻¹ ∘ (f' ×₁ id) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ g')
      w-law₁ : f' # ∘ π₁ ≈ extend [ f' # ∘ π₁ , η _ ∘ π₁ ] ∘ w #
      w-law₁ = sym (begin
        extend [ f' # ∘ π₁ , η _ ∘ π₁ ] ∘ w #                                          ≈⟨ step₁ ⟩
        ([ i₁ ∘ π₁ , (f' # ∘ π₁ +₁ id) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (f' ×₁ g))# ≈⟨ sym step₂ ⟩
        (f' #) ∘ π₁                                                                    ∎)
        where
          h = (π₁ +₁ (π₁ +₁ π₁ ×₁ id) ∘ distributeˡ⁻¹ ∘ ⟨ id , g ∘ π₂ ⟩) ∘ distributeʳ⁻¹ ∘ (f' ×₁ id)
          by-uni : (id +₁ π₁) ∘ (id +₁ ∇) ∘ h ≈ f' ∘ π₁
          by-uni = begin 
            (id +₁ π₁) ∘ (id +₁ ∇) ∘ h                                                                                    ≈⟨ pullˡ +₁∘+₁ ○ pullˡ (+₁∘+₁ ○ +₁-cong₂ (elimˡ identity²) (pullʳ (pullˡ []∘+₁))) ⟩ 
            (π₁ +₁ π₁ ∘ [ (id ∘ π₁) , (id ∘ (π₁ ×₁ id)) ] ∘ distributeˡ⁻¹ ∘ ⟨ id , g ∘ π₂ ⟩) ∘ distributeʳ⁻¹ ∘ (f' ×₁ id) ≈⟨ (+₁-cong₂ refl (pullˡ ∘[] ○ ([]-cong₂ (refl⟩∘⟨ identityˡ) ((refl⟩∘⟨ identityˡ) ○ π₁∘×₁)) ⟩∘⟨refl)) ⟩∘⟨refl ⟩ 
            (π₁ +₁ [ π₁ ∘ π₁ , π₁ ∘ π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ id , g ∘ π₂ ⟩) ∘ distributeʳ⁻¹ ∘ (f' ×₁ id)                  ≈⟨ (+₁-cong₂ refl (pullˡ ((sym ∘[]) ⟩∘⟨refl ○ pullʳ distributeˡ⁻¹-π₁))) ⟩∘⟨refl ⟩ 
            (π₁ +₁ (π₁ ∘ π₁) ∘ ⟨ id , g ∘ π₂ ⟩) ∘ distributeʳ⁻¹ ∘ (f' ×₁ id)                                              ≈⟨ (+₁-cong₂ refl (cancelʳ project₁)) ⟩∘⟨refl ⟩ 
            (π₁ +₁ π₁) ∘ distributeʳ⁻¹ ∘ (f' ×₁ id)                                                                       ≈⟨ pullˡ distributeʳ⁻¹-π₁ ⟩ 
            π₁ ∘ (f' ×₁ id)                                                                                               ≈⟨ π₁∘×₁ ⟩ 
            f' ∘ π₁                                                                                                       ∎
          step₁ : extend [ f' # ∘ π₁ , η _ ∘ π₁ ] ∘ w # ≈ ([ i₁ ∘ π₁ , (f' # ∘ π₁ +₁ id) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (f' ×₁ g))#
          step₁ = begin
            extend [ f' # ∘ π₁ , η _ ∘ π₁ ] ∘ w #                                                                                                                                                                            ≈⟨ extend-preserve [ (f' #) ∘ π₁ , η (K.₀ Y) ∘ π₁ ] w ⟩ 
            ((extend [ f' # ∘ π₁ , η _ ∘ π₁ ] +₁ id) ∘ w) #                                                                                                                                                                  ≈⟨ #-resp-≈ (algebras _) (pullˡ (∘[] ○ []-cong₂ (pullˡ +₁∘i₁) (pullˡ (+₁∘+₁ ○ +₁-cong₂ (pullˡ (extend∘F₁ monadK [ (f' #) ∘ π₁ , η (K.₀ Y) ∘ π₁ ] i₂ ○ kleisliK.extend-≈ inject₂)) identity²)))) ⟩ 
            ([ (i₁ ∘ extend [ f' # ∘ π₁ , η _ ∘ π₁ ]) ∘ K.₁ i₁ ∘ τ _ , ((extend (η (K.₀ Y) ∘ π₁) ∘ σ _ +₁ id)) ∘ distributeʳ⁻¹ ∘ (f' ×₁ id) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ g')) #                                                ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (pullʳ (pullˡ (extend∘F₁ monadK [ f' # ∘ π₁ , η _ ∘ π₁ ] i₁ ○ kleisliK.extend-≈ inject₁))) ((+₁-cong₂ ((refl⟩∘⟨ monadK.F.homomorphism) ⟩∘⟨refl ○ (cancelˡ kleisliK.identityˡ) ⟩∘⟨refl) refl) ⟩∘⟨refl)) ⟩∘⟨refl) ⟩ 
            ([ i₁ ∘ extend (f' # ∘ π₁) ∘ τ _ , (K.₁ π₁ ∘ σ _ +₁ id) ∘ distributeʳ⁻¹ ∘ (f' ×₁ id) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ g')) #                                                                                           ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ refl⟩∘⟨ sym (×₁∘×₁ ○ ×₁-cong₂ identity² refl)) ⟩ 
            ([ i₁ ∘ extend (f' # ∘ π₁) ∘ τ _ , (K.₁ π₁ ∘ σ _ +₁ id) ∘ distributeʳ⁻¹ ∘ (f' ×₁ id) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ (η _ +₁ id)) ∘ (id ×₁ g)) #                                                                      ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (sym (distributeˡ⁻¹-natural id (η (K.₀ U)) id)) ○ assoc)) ⟩ 
            ([ i₁ ∘ extend (f' # ∘ π₁) ∘ τ _ , (K.₁ π₁ ∘ σ _ +₁ id) ∘ distributeʳ⁻¹ ∘ (f' ×₁ id) ] ∘ (id ×₁ η _ +₁ id ×₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ g)) #                                                                  ≈⟨ #-resp-≈ (algebras _) (pullˡ ([]∘+₁ ○ []-cong₂ assoc²βε (elimʳ (⟨⟩-unique id-comm id-comm)))) ⟩ 
            ([ i₁ ∘ extend (f' # ∘ π₁) ∘ τ _ ∘ (id ×₁ η _) , (K.₁ π₁ ∘ σ _ +₁ id) ∘ distributeʳ⁻¹ ∘ (f' ×₁ id) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ g)) #                                                                              ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (refl⟩∘⟨ (refl⟩∘⟨ (τ-η _) ○ kleisliK.identityʳ)) ((+₁-cong₂ σ-π₁ refl) ⟩∘⟨refl)) ⟩∘⟨refl) ⟩
            ([ i₁ ∘ f' # ∘ π₁ , (π₁ +₁ id) ∘ distributeʳ⁻¹ ∘ (f' ×₁ id) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ g)) #                                                                                                                     ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (refl⟩∘⟨ ((#-Fixpoint (algebras _)) ⟩∘⟨refl ○ assoc ○ refl⟩∘⟨ (sym π₁∘×₁))) refl) ⟩∘⟨refl) ⟩
            ([ i₁ ∘ [ id , f' # ] ∘ π₁ ∘ (f' ×₁ id) , (π₁ +₁ id) ∘ distributeʳ⁻¹ ∘ (f' ×₁ id) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ g)) #                                                                                               ≈˘⟨ #-resp-≈ (algebras _) (pullˡ ([]∘+₁ ○ []-cong₂ assoc²βε assoc)) ⟩ 
            ([ i₁ ∘ [ id , f' # ] ∘ π₁ , (π₁ +₁ id) ∘ distributeʳ⁻¹ ] ∘ ((f' ×₁ id) +₁ (f' ×₁ id)) ∘ distributeˡ⁻¹ ∘ (id ×₁ g)) #                                                                                            ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (distributeˡ⁻¹-natural f' id id))) ⟩ 
            ([ i₁ ∘ [ id , f' # ] ∘ π₁ , (π₁ +₁ id) ∘ distributeʳ⁻¹ ] ∘ (distributeˡ⁻¹ ∘ (f' ×₁ (id +₁ id))) ∘ (id ×₁ g)) #                                                                                                  ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (pullʳ (×₁∘×₁ ○ ×₁-cong₂ identityʳ (elimˡ ([]-unique id-comm-sym id-comm-sym))))) ⟩ 
            ([ i₁ ∘ [ id , f' # ] ∘ π₁ , (π₁ +₁ id) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (f' ×₁ g)) #                                                                                                                         ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (refl⟩∘⟨ refl⟩∘⟨ sym distributeʳ⁻¹-π₁) refl) ⟩∘⟨refl) ⟩ 
            ([ i₁ ∘ [ id , f' # ] ∘ (π₁ +₁ π₁) ∘ distributeʳ⁻¹ , (π₁ +₁ id) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (f' ×₁ g)) #                                                                                                 ≈˘⟨ #-resp-≈ (algebras _) (pullˡ ([]∘+₁ ○ []-cong₂ assoc²βε refl)) ⟩ 
            ([ i₁ ∘ [ id , f' # ] ∘ (π₁ +₁ π₁) , (π₁ +₁ id) ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (f' ×₁ g)) #                                                                                              ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ pullˡ distribute₄) ⟩ 
            ([ i₁ ∘ [ id , f' # ] ∘ (π₁ +₁ π₁) , (π₁ +₁ id) ] ∘ ([ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ (f' ×₁ g)) #                                                                  ≈⟨ #-resp-≈ (algebras _) (pullˡ (pullˡ (∘[] ○ []-cong₂ []∘+₁ []∘+₁))) ⟩ 
            (([ [ ((i₁ ∘ [ id , f' # ] ∘ (π₁ +₁ π₁)) ∘ i₁) , (((π₁ +₁ id)) ∘ i₁) ] , [ ((i₁ ∘ [ id , f' # ] ∘ (π₁ +₁ π₁)) ∘ i₂) , (((π₁ +₁ id)) ∘ i₂) ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ (f' ×₁ g)) # ≈⟨ #-resp-≈ (algebras _) (assoc ○ ([]-cong₂ ([]-cong₂ ((refl⟩∘⟨ []∘+₁) ⟩∘⟨refl ○ pullʳ inject₁) +₁∘i₁) ([]-cong₂ ((refl⟩∘⟨ []∘+₁) ⟩∘⟨refl ○ pullʳ inject₂) +₁∘i₂)) ⟩∘⟨refl) ⟩ 
            ([ [ (i₁ ∘ id ∘ π₁) , i₁ ∘ π₁ ] , [ i₁ ∘ f' # ∘ π₁ , i₂ ∘ id ] ] ∘ ((distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ (f' ×₁ g)) #                                                                             ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ ([]-cong₂ (refl⟩∘⟨ identityˡ) refl ○ sym ∘[]) refl) ⟩∘⟨ assoc) ⟩ 
            ([ i₁ ∘ [ π₁ , π₁ ] , f' # ∘ π₁ +₁ id ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ (f' ×₁ g)) #                                                                                                        ≈⟨ #-resp-≈ (algebras _) (pullˡ ([]∘+₁ ○ []-cong₂ assoc refl)) ⟩ 
            ([ i₁ ∘ [ π₁ , π₁ ] ∘ distributeˡ⁻¹ , (f' # ∘ π₁ +₁ id) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (f' ×₁ g))#                                                                                                          ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (refl⟩∘⟨ distributeˡ⁻¹-π₁) refl) ⟩∘⟨refl) ⟩ 
            ([ i₁ ∘ π₁ , (f' # ∘ π₁ +₁ id) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (f' ×₁ g))#                                                                                                                                   ∎
          step₂ : (f' #) ∘ π₁ ≈ ([ i₁ ∘ π₁ , (f' # ∘ π₁ +₁ id) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (f' ×₁ g))#
          step₂ = begin 
            (f' #) ∘ π₁                                                                                                                       ≈˘⟨ #-Uniformity (algebras _) by-uni ⟩ 
            ((id +₁ ∇) ∘ h)#                                                                                                                  ≈⟨ #-Diamond (algebras _) h ⟩
            ([ i₁ , ((id +₁ ∇) ∘ h) # +₁ id ] ∘ h) #                                                                                          ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (+₁-cong₂ (#-Uniformity (algebras _) by-uni) refl)) ⟩∘⟨refl) ⟩
            ([ i₁ , (f' # ∘ π₁) +₁ id ] ∘ h) #                                                                                                ≈⟨ #-resp-≈ (algebras _) (pullˡ []∘+₁) ⟩
            ([ (i₁ ∘ π₁) , (((f' # ∘ π₁) +₁ id) ∘ (π₁ +₁ π₁ ×₁ id) ∘ distributeˡ⁻¹ ∘ ⟨ id , g ∘ π₂ ⟩) ] ∘ distributeʳ⁻¹ ∘ (f' ×₁ id)) #       ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (pullˡ (+₁∘+₁ ○ +₁-cong₂ assoc identityˡ))) ⟩∘⟨refl) ⟩
            ([ (i₁ ∘ π₁) , ((f' # ∘ π₁ ∘ π₁ +₁ (π₁ ×₁ id)) ∘ distributeˡ⁻¹ ∘ ⟨ id , g ∘ π₂ ⟩) ] ∘ distributeʳ⁻¹ ∘ (f' ×₁ id)) #               ≈˘⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (pullˡ (+₁∘+₁ ○ +₁-cong₂ (pullʳ π₁∘×₁) identityˡ))) ⟩∘⟨refl) ⟩
            ([ (i₁ ∘ π₁) , (f' # ∘ π₁ +₁ id) ∘ ((π₁ ×₁ id) +₁ (π₁ ×₁ id)) ∘ distributeˡ⁻¹ ∘ ⟨ id , g ∘ π₂ ⟩ ] ∘ distributeʳ⁻¹ ∘ (f' ×₁ id)) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (refl⟩∘⟨ (pullˡ (distributeˡ⁻¹-natural π₁ id id ○ refl⟩∘⟨ ×₁-cong₂ refl ([]-unique id-comm-sym id-comm-sym)) ○ assoc))) ⟩∘⟨refl) ⟩
            ([ (i₁ ∘ π₁) , ((f' # ∘ π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (π₁ ×₁ id) ∘ ⟨ id , g ∘ π₂ ⟩) ] ∘ distributeʳ⁻¹ ∘ (f' ×₁ id)) #               ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (refl⟩∘⟨ (refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ)))) ⟩∘⟨refl) ⟩
            ([ (i₁ ∘ π₁) , ((f' # ∘ π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ ⟨ π₁ , g ∘ π₂ ⟩) ] ∘ distributeʳ⁻¹ ∘ (f' ×₁ id)) #                            ≈˘⟨ #-resp-≈ (algebras _) (pullˡ ([]∘+₁ ○ []-cong₂ (pullʳ (π₁∘×₁ ○ identityˡ)) (assoc ○ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ identityˡ refl))) ⟩
            ([ (i₁ ∘ π₁) , ((f' # ∘ π₁ +₁ id) ∘ distributeˡ⁻¹) ] ∘ (id ×₁ g +₁ id ×₁ g) ∘ distributeʳ⁻¹ ∘ (f' ×₁ id)) #                       ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (distributeʳ⁻¹-natural g id id) ○ assoc)) ⟩
            ([ i₁ ∘ π₁ , (f' # ∘ π₁ +₁ id) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ ((id +₁ id) ×₁ g) ∘ (f' ×₁ id))#                               ≈˘⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ refl⟩∘⟨ sym (×₁∘×₁ ○ ×₁-cong₂ (elimˡ ([]-unique id-comm-sym id-comm-sym)) identityʳ)) ⟩
            ([ i₁ ∘ π₁ , (f' # ∘ π₁ +₁ id) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (f' ×₁ g))#                                                    ∎
      w-law₂ : g' # ∘ π₂ ≈ extend [ η _ ∘ π₂ , g' # ∘ π₂ ] ∘ w #
      w-law₂ = sym (begin 
        extend [ η _ ∘ π₂ , g' # ∘ π₂ ] ∘ w #                                          ≈⟨ step₁ ⟩ 
        ([ i₁ ∘ π₂ , (g' # ∘ π₂ +₁ id) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (f ×₁ g'))# ≈⟨ sym step₂ ⟩ 
        g' # ∘ π₂                                                                      ∎)
        where
          h = (π₂ +₁ (π₂ +₁ id ×₁ π₂) ∘ distributeʳ⁻¹ ∘ ⟨ f ∘ π₁ , id ⟩) ∘ distributeˡ⁻¹ ∘ (id ×₁ g')
          by-uni : (id +₁ π₂) ∘ (id +₁ ∇) ∘ h ≈ g' ∘ π₂
          by-uni = begin 
            (id +₁ π₂) ∘ (id +₁ ∇) ∘ h                                                                                    ≈⟨ pullˡ +₁∘+₁ ○ pullˡ (+₁∘+₁ ○ +₁-cong₂ (elimˡ identity²) (pullʳ (pullˡ []∘+₁))) ⟩ 
            (π₂ +₁ π₂ ∘ [ (id ∘ π₂) , (id ∘ (id ×₁ π₂)) ] ∘ distributeʳ⁻¹ ∘ ⟨ f ∘ π₁ , id ⟩) ∘ distributeˡ⁻¹ ∘ (id ×₁ g') ≈⟨ (+₁-cong₂ refl (pullˡ ∘[] ○ ([]-cong₂ (refl⟩∘⟨ identityˡ) ((refl⟩∘⟨ identityˡ) ○ π₂∘×₁)) ⟩∘⟨refl)) ⟩∘⟨refl ⟩ 
            (π₂ +₁ [ π₂ ∘ π₂ , π₂ ∘ π₂ ] ∘ distributeʳ⁻¹ ∘ ⟨ f ∘ π₁ , id ⟩) ∘ distributeˡ⁻¹ ∘ (id ×₁ g')                  ≈⟨ (+₁-cong₂ refl (pullˡ ((sym ∘[]) ⟩∘⟨refl ○ pullʳ distributeʳ⁻¹-π₂))) ⟩∘⟨refl ⟩ 
            (π₂ +₁ (π₂ ∘ π₂) ∘ ⟨ f ∘ π₁ , id ⟩) ∘ distributeˡ⁻¹ ∘ (id ×₁ g')                                              ≈⟨ (+₁-cong₂ refl (cancelʳ project₂)) ⟩∘⟨refl ⟩ 
            (π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∘ (id ×₁ g')                                                                       ≈⟨ pullˡ distributeˡ⁻¹-π₂ ⟩ 
            π₂ ∘ (id ×₁ g')                                                                                               ≈⟨ π₂∘×₁ ⟩ 
            g' ∘ π₂                                                                                                       ∎
          step₁ : extend [ η _ ∘ π₂ , g' # ∘ π₂ ] ∘ w # ≈ ([ i₁ ∘ π₂ , (g' # ∘ π₂ +₁ id) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (f ×₁ g'))#
          step₁ = begin 
            extend [ η _ ∘ π₂ , g' # ∘ π₂ ] ∘ w #                                                                                                                        ≈⟨ extend-preserve _ w ⟩ 
            ((extend [ η _ ∘ π₂ , g' # ∘ π₂ ] +₁ id) ∘ w) #                                                                                                              ≈⟨ #-resp-≈ (algebras _) (pullˡ (∘[] ○ []-cong₂ (pullˡ +₁∘i₁) (pullˡ (+₁∘+₁ ○ +₁-cong₂ (pullˡ (extend∘F₁ monadK [ η (K.₀ U) ∘ π₂ , (g' #) ∘ π₂ ] i₂ ○ kleisliK.extend-≈ inject₂)) identity²)))) ⟩ 
            ([ (i₁ ∘ extend [ η _ ∘ π₂ , g' # ∘ π₂ ]) ∘ K.₁ i₁ ∘ τ _ , (extend ((g' #) ∘ π₂) ∘ σ _ +₁ id) ∘ distributeʳ⁻¹ ∘ (f' ×₁ id) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ g')) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (pullʳ (pullˡ (extend∘F₁ monadK _ i₁ ○ kleisliK.extend-≈ inject₁ ○ Monad⇒Kleisli⇒Monad monadK π₂))) refl) ⟩∘⟨refl) ⟩ 
            ([ i₁ ∘ K.₁ π₂ ∘ τ _ , (extend (g' # ∘ π₂) ∘ σ _ +₁ id) ∘ distributeʳ⁻¹ ∘ (f' ×₁ id) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ g')) #                                       ≈˘⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (refl⟩∘⟨ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ refl identity²))) ⟩∘⟨refl) ⟩ 
            ([ i₁ ∘ K.₁ π₂ ∘ τ _ , (extend (g' # ∘ π₂) ∘ σ _ +₁ id) ∘ distributeʳ⁻¹ ∘ ((η _ +₁ id) ×₁ id) ∘ (f ×₁ id) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ g')) #                  ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (refl⟩∘⟨ (pullˡ (sym (distributeʳ⁻¹-natural id (η (K.₀ Y)) id)) ○ assoc))) ⟩∘⟨refl) ⟩ 
            ([ i₁ ∘ K.₁ π₂ ∘ τ _ , (extend (g' # ∘ π₂) ∘ σ _ +₁ id) ∘ ((η _ ×₁ id) +₁ (id ×₁ id)) ∘ distributeʳ⁻¹ ∘ (f ×₁ id) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ g')) #          ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (pullˡ (+₁∘+₁ ○ +₁-cong₂ (pullʳ σ-η) (elimʳ (⟨⟩-unique id-comm id-comm))))) ⟩∘⟨refl) ⟩ 
            ([ i₁ ∘ K.₁ π₂ ∘ τ _ , (extend (g' # ∘ π₂) ∘ η _ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ×₁ id) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ g')) #                                        ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (refl⟩∘⟨ τ-π₂ _) ((+₁-cong₂ kleisliK.identityʳ refl) ⟩∘⟨refl)) ⟩∘⟨refl) ⟩ 
            ([ i₁ ∘ π₂ , (g' # ∘ π₂ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ×₁ id) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ g')) #                                                                 ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (refl⟩∘⟨ (sym (π₂∘×₁ ○ identityˡ))) refl) ⟩∘⟨refl) ⟩ 
            ([ i₁ ∘ π₂ ∘ (f ×₁ id) , (g' # ∘ π₂ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ×₁ id) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ g')) #                                                     ≈˘⟨ #-resp-≈ (algebras _) (pullˡ ([]∘+₁ ○ []-cong₂ assoc assoc)) ⟩ 
            ([ i₁ ∘ π₂ , (g' # ∘ π₂ +₁ id) ∘ distributeʳ⁻¹ ] ∘ (f ×₁ id +₁ f ×₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ g')) #                                                      ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (distributeˡ⁻¹-natural f id id) ○ assoc)) ⟩ 
            ([ i₁ ∘ π₂ , (g' # ∘ π₂ +₁ id) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (f ×₁ (id +₁ id)) ∘ (id ×₁ g')) #                                                         ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ identityʳ (elimˡ ([]-unique id-comm-sym id-comm-sym)))) ⟩ 
            ([ i₁ ∘ π₂ , (g' # ∘ π₂ +₁ id) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (f ×₁ g')) #                                                                              ∎
          step₂ : g' # ∘ π₂ ≈ ([ i₁ ∘ π₂ , (g' # ∘ π₂ +₁ id) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (f ×₁ g'))#
          step₂ = begin 
            g' # ∘ π₂                                                                                                                         ≈˘⟨ #-Uniformity (algebras _) by-uni ⟩ 
            ((id +₁ ∇) ∘ h) #                                                                                                                 ≈⟨ #-Diamond (algebras _) h ⟩
            ([ i₁ , ((id +₁ ∇) ∘ h) # +₁ id ] ∘ h) #                                                                                          ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (+₁-cong₂ (#-Uniformity (algebras _) by-uni) refl)) ⟩∘⟨refl) ⟩ 
            ([ i₁ , g' # ∘ π₂ +₁ id ] ∘ h) #                                                                                                  ≈⟨ #-resp-≈ (algebras _) (pullˡ []∘+₁) ⟩ 
            ([ (i₁ ∘ π₂) , (((g' # ∘ π₂) +₁ id) ∘ (π₂ +₁ id ×₁ π₂) ∘ distributeʳ⁻¹ ∘ ⟨ f ∘ π₁ , id ⟩) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ g')) #       ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (pullˡ (+₁∘+₁ ○ +₁-cong₂ assoc identityˡ))) ⟩∘⟨refl) ⟩ 
            ([ (i₁ ∘ π₂) , ((g' # ∘ π₂ ∘ π₂ +₁ (id ×₁ π₂)) ∘ distributeʳ⁻¹ ∘ ⟨ f ∘ π₁ , id ⟩) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ g')) #               ≈˘⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (pullˡ (+₁∘+₁ ○ +₁-cong₂ (pullʳ π₂∘×₁) identityˡ))) ⟩∘⟨refl) ⟩ 
            ([ (i₁ ∘ π₂) , (g' # ∘ π₂ +₁ id) ∘ ((id ×₁ π₂) +₁ (id ×₁ π₂)) ∘ distributeʳ⁻¹ ∘ ⟨ f ∘ π₁ , id ⟩ ] ∘ distributeˡ⁻¹ ∘ (id ×₁ g')) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (refl⟩∘⟨ (pullˡ (distributeʳ⁻¹-natural π₂ id id ○ refl⟩∘⟨ ×₁-cong₂ ([]-unique id-comm-sym id-comm-sym) refl) ○ assoc))) ⟩∘⟨refl) ⟩ 
            ([ (i₁ ∘ π₂) , ((g' # ∘ π₂ +₁ id) ∘ distributeʳ⁻¹ ∘ (id ×₁ π₂) ∘ ⟨ f ∘ π₁ , id ⟩) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ g')) #               ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (refl⟩∘⟨ (refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ identityʳ)))) ⟩∘⟨refl) ⟩ 
            ([ (i₁ ∘ π₂) , ((g' # ∘ π₂ +₁ id) ∘ distributeʳ⁻¹ ∘ ⟨ f ∘ π₁ , π₂ ⟩) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ g')) #                            ≈˘⟨ #-resp-≈ (algebras _) (pullˡ ([]∘+₁ ○ []-cong₂ (pullʳ (π₂∘×₁ ○ identityˡ)) (assoc ○ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ refl identityˡ))) ⟩ 
            ([ (i₁ ∘ π₂) , ((g' # ∘ π₂ +₁ id) ∘ distributeʳ⁻¹) ] ∘ (f ×₁ id +₁ f ×₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ g')) #                       ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (distributeˡ⁻¹-natural f id id) ○ assoc)) ⟩ 
            ([ i₁ ∘ π₂ , (g' # ∘ π₂ +₁ id) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (f ×₁ (id +₁ id)) ∘ (id ×₁ g'))#                               ≈˘⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ refl⟩∘⟨ sym (×₁∘×₁ ○ ×₁-cong₂ identityʳ (elimˡ ([]-unique id-comm-sym id-comm-sym)))) ⟩ 
            ([ i₁ ∘ π₂ , (g' # ∘ π₂ +₁ id) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (f ×₁ g'))#                                                    ∎
      τσ : extend (τ _) ∘ σ _ ∘ (f' # ×₁ g' #) ≈ extend ([ σ _ ∘ ( f' # ×₁ id ) , τ _ ∘ (id ×₁ g' #) ]) ∘ w #
      τσ = begin
        extend (τ _) ∘ σ _ ∘ (f' # ×₁ g' #)                                                                                                              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ w-law₁ w-law₂ ⟩ 
        extend (τ _) ∘ σ _ ∘ ⟨ extend [ f' # ∘ π₁ , η _ ∘ π₁ ] ∘ w # , extend [ η _ ∘ π₂ , g' # ∘ π₂ ] ∘ w # ⟩                                           ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym ×₁∘⟨⟩ ⟩ 
        extend (τ _) ∘ σ _ ∘ (extend [ f' # ∘ π₁ , η _ ∘ π₁ ] ×₁ extend [ η _ ∘ π₂ , g' # ∘ π₂ ]) ∘ ⟨ w # , w # ⟩                                        ≈⟨ refl⟩∘⟨ (pullˡ (sym (σ-kleisli-assoc [ (f' #) ∘ π₁ , η (K.₀ Y) ∘ π₁ ] [ η (K.₀ U) ∘ π₂ , (g' #) ∘ π₂ ]))) ⟩
        extend (τ _) ∘ (extend (σ _ ∘ ([ f' # ∘ π₁ , η _ ∘ π₁ ] ×₁ id)) ∘ σ _ ∘ (id ×₁ extend [ η _ ∘ π₂ , g' # ∘ π₂ ])) ∘ ⟨ w # , w # ⟩                 ≈˘⟨ refl⟩∘⟨ (refl⟩∘⟨ (sym (σ-natural id (extend [ η (K.₀ U) ∘ π₂ , (g' #) ∘ π₂ ])) ○ refl⟩∘⟨ ×₁-cong₂ monadK.F.identity refl)) ⟩∘⟨refl ⟩
        extend (τ _) ∘ (extend (σ _ ∘ ([ f' # ∘ π₁ , η _ ∘ π₁ ] ×₁ id)) ∘ K.₁ (id ×₁ extend [ η _ ∘ π₂ , g' # ∘ π₂ ]) ∘ σ _) ∘ ⟨ w # , w # ⟩             ≈⟨ refl⟩∘⟨ (pullʳ (pullʳ (pullʳ (pullʳ (swap∘⟨⟩ ○ sym Δ∘))))) ⟩
        extend (τ _) ∘ extend (σ _ ∘ ([ f' # ∘ π₁ , η _ ∘ π₁ ] ×₁ id)) ∘ K.₁ (id ×₁ extend [ η _ ∘ π₂ , g' # ∘ π₂ ]) ∘ K.₁ swap ∘ τ _ ∘ Δ ∘ w #          ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (pullˡ equationalLifting) ⟩
        extend (τ _) ∘ extend (σ _ ∘ ([ f' # ∘ π₁ , η _ ∘ π₁ ] ×₁ id)) ∘ K.₁ (id ×₁ extend [ η _ ∘ π₂ , g' # ∘ π₂ ]) ∘ K.₁ swap ∘ K.₁ ⟨ η _ , id ⟩ ∘ w # ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym monadK.F.homomorphism ○ monadK.F.F-resp-≈ swap∘⟨⟩) ⟩
        extend (τ _) ∘ extend (σ _ ∘ ([ f' # ∘ π₁ , η _ ∘ π₁ ] ×₁ id)) ∘ K.₁ (id ×₁ extend [ η _ ∘ π₂ , g' # ∘ π₂ ]) ∘ K.₁ ⟨ id , η _ ⟩ ∘ w #            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym monadK.F.homomorphism ○ monadK.F.F-resp-≈ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identity² kleisliK.identityʳ)) ⟩
        extend (τ _) ∘ extend (σ _ ∘ ([ f' # ∘ π₁ , η _ ∘ π₁ ] ×₁ id)) ∘ K.₁ ⟨ id , [ η _ ∘ π₂ , g' # ∘ π₂ ] ⟩ ∘ w #                                     ≈⟨ refl⟩∘⟨ pullˡ (extend∘F₁ monadK (σ _ ∘ ([ (f' #) ∘ π₁ , η (K.₀ Y) ∘ π₁ ] ×₁ id)) ⟨ id , [ η (K.₀ U) ∘ π₂ , (g' #) ∘ π₂ ] ⟩) ⟩ 
        extend (τ _) ∘ extend ((σ _ ∘ ([ f' # ∘ π₁ , η _ ∘ π₁ ] ×₁ id)) ∘ ⟨ id , [ η _ ∘ π₂ , g' # ∘ π₂ ] ⟩) ∘ w #                                       ≈⟨ refl⟩∘⟨ ((kleisliK.extend-≈ (pullʳ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ))) ⟩∘⟨refl) ⟩
        extend (τ _) ∘ extend (σ _ ∘ ⟨ [ f' # ∘ π₁ , η _ ∘ π₁ ] , [ η _ ∘ π₂ , g' # ∘ π₂ ] ⟩) ∘ w #                                                      ≈˘⟨ refl⟩∘⟨ (pullˡ (extend∘F₁ monadK (σ _) ⟨ [ f' # ∘ π₁ , η _ ∘ π₁ ] , [ η _ ∘ π₂ , g' # ∘ π₂ ] ⟩)) ⟩
        extend (τ _) ∘ extend (σ _) ∘ K.₁ ⟨ [ f' # ∘ π₁ , η _ ∘ π₁ ] , [ η _ ∘ π₂ , g' # ∘ π₂ ] ⟩ ∘ w #                                                  ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (monadK.F.F-resp-≈ (⟨⟩-unique (∘[] ○ []-cong₂ project₁ project₁) (∘[] ○ []-cong₂ project₂ project₂))) ⟩∘⟨refl ⟩ -- TODO use sym [⟨⟩]≈⟨[]⟩
        extend (τ _) ∘ extend (σ _) ∘ K.₁ [ ⟨ f' # ∘ π₁ , η _ ∘ π₂ ⟩ , ⟨ η _ ∘ π₁ , g' # ∘ π₂ ⟩ ] ∘ w #                                                  ≈⟨ refl⟩∘⟨ (pullˡ (extend∘F₁ monadK (σ _) [ ⟨ f' # ∘ π₁ , η _ ∘ π₂ ⟩ , ⟨ η _ ∘ π₁ , g' # ∘ π₂ ⟩ ])) ⟩ 
        extend (τ _) ∘ extend (σ _ ∘ [ ⟨ f' # ∘ π₁ , η _ ∘ π₂ ⟩ , ⟨ η _ ∘ π₁ , g' # ∘ π₂ ⟩ ]) ∘ w #                                                      ≈⟨ pullˡ kleisliK.sym-assoc ⟩ 
        extend (extend (τ _) ∘ σ _ ∘ [ ⟨ f' # ∘ π₁ , η _ ∘ π₂ ⟩ , ⟨ η _ ∘ π₁ , g' # ∘ π₂ ⟩ ]) ∘ w #                                                      ≈⟨ (kleisliK.extend-≈ (refl⟩∘⟨ ∘[] ○ ∘[])) ⟩∘⟨refl ⟩ 
        extend ([ extend (τ _) ∘ σ _ ∘ ⟨ f' # ∘ π₁ , η _ ∘ π₂ ⟩ , extend (τ _) ∘ σ _ ∘ ⟨ η _ ∘ π₁ , g' # ∘ π₂ ⟩ ]) ∘ w #                                 ≈˘⟨ (kleisliK.extend-≈ ([]-cong₂ (refl⟩∘⟨ refl⟩∘⟨ (×₁∘×₁ ○ ⟨⟩-cong₂ (identityˡ ⟩∘⟨refl) (identityʳ ⟩∘⟨refl))) (refl⟩∘⟨ refl⟩∘⟨ ((×₁∘×₁ ○ ⟨⟩-cong₂ (identityʳ ⟩∘⟨refl) (identityˡ ⟩∘⟨refl)))))) ⟩∘⟨refl ⟩ 
        extend ([ extend (τ _) ∘ σ _ ∘ (id ×₁ η _) ∘ ( f' # ×₁ id ) , extend (τ _) ∘ σ _ ∘ (η _ ×₁ id) ∘ (id ×₁ g' #) ]) ∘ w #                           ≈˘⟨ (kleisliK.extend-≈ ([]-cong₂ (refl⟩∘⟨ (pullˡ (sym (σ-natural id (η _)) ○ refl⟩∘⟨ (×₁-cong₂ monadK.F.identity refl)) ○ assoc)) (refl⟩∘⟨ (sym (pullˡ σ-η))))) ⟩∘⟨refl ⟩ 
        extend ([ extend (τ _) ∘ K.₁ (id ×₁ η _) ∘ σ _ ∘ ( f' # ×₁ id ) , extend (τ _) ∘ η _ ∘ (id ×₁ g' #) ]) ∘ w #                                     ≈⟨ (kleisliK.extend-≈ ([]-cong₂ (pullˡ (extend∘F₁ monadK (τ _) (id ×₁ η _))) (pullˡ kleisliK.identityʳ))) ⟩∘⟨refl ⟩ 
        extend ([ extend (τ _ ∘ (id ×₁ η _)) ∘ σ _ ∘ ( f' # ×₁ id ) , τ _ ∘ (id ×₁ g' #) ]) ∘ w #                                                        ≈⟨ (kleisliK.extend-≈ ([]-cong₂ (elimˡ (kleisliK.extend-≈ (τ-η _) ○ kleisliK.identityˡ)) refl)) ⟩∘⟨refl ⟩ 
        extend ([ σ _ ∘ ( f' # ×₁ id ) , τ _ ∘ (id ×₁ g' #) ]) ∘ w #                                                                                     ∎

      στ : extend (σ _) ∘ τ _ ∘ (((η _ +₁ id) ∘ f) # ×₁ ((η _ +₁ id) ∘ g) #) ≈ extend ([ σ _ ∘ ( f' # ×₁ id ) , τ _ ∘ (id ×₁ g' #) ]) ∘ w #
      στ = begin 
        extend (σ _) ∘ τ _ ∘ (((η _ +₁ id) ∘ f) # ×₁ ((η _ +₁ id) ∘ g) #)                                                                                       ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ w-law₁ w-law₂ ⟩ 
        extend (σ _) ∘ τ _ ∘ ⟨ extend [ f' # ∘ π₁ , η _ ∘ π₁ ] ∘ w # , extend [ η _ ∘ π₂ , g' # ∘ π₂ ] ∘ w # ⟩                                                  ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym ×₁∘⟨⟩ ⟩ 
        extend (σ _) ∘ τ _ ∘ (extend [ f' # ∘ π₁ , η _ ∘ π₁ ] ×₁ extend [ η _ ∘ π₂ , g' # ∘ π₂ ]) ∘ ⟨ w # , w # ⟩                                               ≈⟨ refl⟩∘⟨ (pullˡ (sym (τ-kleisli-assoc [ (f' #) ∘ π₁ , η (K.₀ Y) ∘ π₁ ] [ η (K.₀ U) ∘ π₂ , (g' #) ∘ π₂ ]))) ⟩ 
        extend (σ _) ∘ (extend (τ _ ∘ (id ×₁ [ η (K.₀ U) ∘ π₂ , (g' #) ∘ π₂ ])) ∘ τ _ ∘ (extend [ (f' #) ∘ π₁ , η (K.₀ Y) ∘ π₁ ] ×₁ id)) ∘ ⟨ w # , w # ⟩        ≈˘⟨ refl⟩∘⟨ (refl⟩∘⟨ (sym (strengthen.commute (μ.η (K.₀ Y) ∘ K.₁ [ (f' #) ∘ π₁ , η (K.₀ Y) ∘ π₁ ] , id)) ○ refl⟩∘⟨ ×₁-cong₂ refl monadK.F.identity)) ⟩∘⟨refl ⟩ 
        extend (σ _) ∘ (extend (τ _ ∘ (id ×₁ [ η (K.₀ U) ∘ π₂ , (g' #) ∘ π₂ ])) ∘ K.₁ (extend [ (f' #) ∘ π₁ , η (K.₀ Y) ∘ π₁ ] ×₁ id) ∘ τ _) ∘ ⟨ w # , w # ⟩    ≈⟨ refl⟩∘⟨ (pullʳ (pullʳ (refl⟩∘⟨ (sym Δ∘)))) ⟩ 
        extend (σ _) ∘ extend (τ _ ∘ (id ×₁ [ η (K.₀ U) ∘ π₂ , (g' #) ∘ π₂ ])) ∘ K.₁ (extend [ (f' #) ∘ π₁ , η (K.₀ Y) ∘ π₁ ] ×₁ id) ∘ τ _ ∘ Δ ∘ (w #)          ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (pullˡ equationalLifting) ⟩ 
        extend (σ _) ∘ extend (τ _ ∘ (id ×₁ [ η (K.₀ U) ∘ π₂ , (g' #) ∘ π₂ ])) ∘ K.₁ (extend [ (f' #) ∘ π₁ , η (K.₀ Y) ∘ π₁ ] ×₁ id) ∘ K.₁ ⟨ η _ , id ⟩ ∘ (w #) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym monadK.F.homomorphism ○ monadK.F.F-resp-≈ ×₁∘⟨⟩) ⟩ 
        extend (σ _) ∘ extend (τ _ ∘ (id ×₁ [ η (K.₀ U) ∘ π₂ , (g' #) ∘ π₂ ])) ∘ K.₁ ⟨ extend [ (f' #) ∘ π₁ , η (K.₀ Y) ∘ π₁ ] ∘ η _ , id ∘ id ⟩ ∘ (w #)        ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (K.F-resp-≈ (⟨⟩-cong₂ kleisliK.identityʳ identity²)) ⟩∘⟨refl ⟩ 
        extend (σ _) ∘ extend (τ _ ∘ (id ×₁ [ η (K.₀ U) ∘ π₂ , (g' #) ∘ π₂ ])) ∘ K.₁ ⟨ [ (f' #) ∘ π₁ , η (K.₀ Y) ∘ π₁ ] , id ⟩ ∘ (w #)                          ≈⟨ refl⟩∘⟨ (pullˡ (extend∘F₁ monadK _ _)) ⟩
        extend (σ _) ∘ extend ((τ _ ∘ (id ×₁ [ η (K.₀ U) ∘ π₂ , (g' #) ∘ π₂ ])) ∘ ⟨ [ (f' #) ∘ π₁ , η (K.₀ Y) ∘ π₁ ] , id ⟩) ∘ (w #)                            ≈⟨ refl⟩∘⟨ ((kleisliK.extend-≈ (pullʳ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ identityʳ))) ⟩∘⟨refl) ⟩ 
        extend (σ _) ∘ extend (τ _ ∘ ⟨ [ (f' #) ∘ π₁ , η (K.₀ Y) ∘ π₁ ] , [ η (K.₀ U) ∘ π₂ , (g' #) ∘ π₂ ] ⟩) ∘ (w #)                                           ≈⟨ pullˡ kleisliK.sym-assoc ⟩ 
        extend (extend (σ _) ∘ τ _ ∘ ⟨ [ (f' #) ∘ π₁ , η (K.₀ Y) ∘ π₁ ] , [ η (K.₀ U) ∘ π₂ , (g' #) ∘ π₂ ] ⟩) ∘ (w #)                                           ≈⟨ (kleisliK.extend-≈ (refl⟩∘⟨ refl⟩∘⟨ sym ([⟨⟩]≈⟨[]⟩ ((f' #) ∘ π₁) (η (K.₀ U) ∘ π₂) (η (K.₀ Y) ∘ π₁) ((g' #) ∘ π₂)))) ⟩∘⟨refl ⟩ 
        extend (extend (σ _) ∘ τ _ ∘ [ ⟨ (f' #) ∘ π₁ , η (K.₀ U) ∘ π₂ ⟩ , ⟨ η (K.₀ Y) ∘ π₁ , (g' #) ∘ π₂ ⟩ ]) ∘ (w #)                                           ≈⟨ (kleisliK.extend-≈ (refl⟩∘⟨ ∘[] ○ ∘[])) ⟩∘⟨refl ⟩ 
        extend ([ extend (σ _) ∘ τ _ ∘ ⟨ (f' #) ∘ π₁ , η (K.₀ U) ∘ π₂ ⟩ , extend (σ _) ∘ τ _ ∘ ⟨ η (K.₀ Y) ∘ π₁ , (g' #) ∘ π₂ ⟩ ]) ∘ (w #)                      ≈˘⟨ (kleisliK.extend-≈ ([]-cong₂ (refl⟩∘⟨ refl⟩∘⟨ (×₁∘×₁ ○ ⟨⟩-cong₂ (identityˡ ⟩∘⟨refl) (identityʳ ⟩∘⟨refl))) (refl⟩∘⟨ refl⟩∘⟨ (×₁∘×₁ ○ ⟨⟩-cong₂ (identityʳ ⟩∘⟨refl) (identityˡ ⟩∘⟨refl))))) ⟩∘⟨refl ⟩ 
        extend ([ extend (σ _) ∘ τ _ ∘ (id ×₁ η _) ∘ ( f' # ×₁ id ) , extend (σ _) ∘ τ _ ∘ (η _ ×₁ id) ∘ (id ×₁ g' #) ]) ∘ (w #)                                ≈⟨ (kleisliK.extend-≈ ([]-cong₂ (refl⟩∘⟨ (pullˡ (τ-η _))) (refl⟩∘⟨ (pullˡ (sym (sym (strengthen.commute _) ○ refl⟩∘⟨ (×₁-cong₂ refl monadK.F.identity))) ○ assoc)))) ⟩∘⟨refl ⟩ 
        extend ([ extend (σ _) ∘ η _ ∘ ( f' # ×₁ id ) , extend (σ _) ∘ K.₁ (η _ ×₁ id) ∘ τ _ ∘ (id ×₁ g' #) ]) ∘ (w #)                                          ≈⟨ (kleisliK.extend-≈ ([]-cong₂ (pullˡ kleisliK.identityʳ) (cancelˡ (extend∘F₁ monadK (σ _) (η _ ×₁ id) ○ kleisliK.extend-≈ σ-η ○ kleisliK.identityˡ)))) ⟩∘⟨refl ⟩ 
        extend ([ σ _ ∘ ( f' # ×₁ id ) , τ _ ∘ (id ×₁ g' #) ]) ∘ w #                                                                                            ∎

KCommutative : Commutative {C = C} {V = monoidal} braided KStrong
Commutative.commutes KCommutative {X} {Y} = by-stability (algebras _) (σ _) law₁ law₂ pres₁ pres₂
  where
  law₁ : σ _ ≈ ((μ.η _ ∘ K.₁ (σ _)) ∘ τ _) ∘ (id ×₁ η _)
  law₁ = sym (begin 
    ((μ.η _ ∘ K.₁ (σ _)) ∘ τ _) ∘ (id ×₁ η _) ≈⟨ pullʳ (τ-η _) ⟩ 
    (μ.η _ ∘ K.₁ (σ _)) ∘ η _                 ≈⟨ pullʳ (K₁η _) ⟩
    μ.η _ ∘ η _ ∘ σ _                       ≈⟨ cancelˡ monadK.identityʳ ⟩
    σ _                                     ∎)
  law₂ : σ _ ≈ ((μ.η _ ∘ K.₁ (τ _)) ∘ σ _) ∘ (id ×₁ η _)
  law₂ = sym (begin 
    ((μ.η _ ∘ K.₁ (τ _)) ∘ σ _) ∘ (id ×₁ η _)                       ≈⟨ pullʳ (pullʳ (pullʳ swap∘×₁)) ⟩ 
    (μ.η _ ∘ K.₁ (τ _)) ∘ K.₁ swap ∘ τ _ ∘ (η _ ×₁ id) ∘ swap       ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ×₁-cong₂ refl (sym K.identity) ⟩∘⟨refl ⟩ 
    (μ.η _ ∘ K.₁ (τ _)) ∘ K.₁ swap ∘ τ _ ∘ (η _ ×₁ K.₁ id) ∘ swap   ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (strengthen.commute (η _ , id)) ⟩ 
    (μ.η _ ∘ K.₁ (τ _)) ∘ K.₁ swap ∘ (K.₁ (η _ ×₁ id) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ pullˡ (pullˡ (sym K.homomorphism)) ⟩ 
    (μ.η _ ∘ K.₁ (τ _)) ∘ (K.₁ (swap ∘ (η _ ×₁ id)) ∘ τ _) ∘ swap   ≈⟨ pullʳ (pullˡ (pullˡ (sym K.homomorphism))) ⟩ 
    μ.η _ ∘ (K.₁ (τ _ ∘ swap ∘ (η _ ×₁ id)) ∘ τ _) ∘ swap           ≈⟨ refl⟩∘⟨ (((K.F-resp-≈ (refl⟩∘⟨ swap∘×₁)) ⟩∘⟨refl) ⟩∘⟨refl) ⟩ 
    μ.η _ ∘ (K.₁ (τ _ ∘ (id ×₁ η _) ∘ 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 ⟩ 
    σ _                                                             ∎)
  pres₁ : ∀ {Z : Obj} (h : Z ⇒ K.₀ Y + Z) → ((μ.η _ ∘ K.₁ (σ _)) ∘ τ _) ∘ (id ×₁ h #) ≈ (((μ.η _ ∘ K.₁ (σ _)) ∘ τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h))#
  pres₁ {Z} h = begin 
    ((μ.η _ ∘ K.₁ (σ _)) ∘ τ _) ∘ (id ×₁ h #)                                       ≈⟨ pullʳ (♯-preserving (stable _) (η _) h) ⟩ 
    (μ.η _ ∘ K.₁ (σ _)) ∘ ((τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)) #               ≈⟨ pullʳ (Elgot-Algebra-Morphism.preserves ((freealgebras _ FreeObject.*) (η _ ∘ σ _))) ⟩
    μ.η _ ∘ ((K.₁ (σ _) +₁ id) ∘ (τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)) #         ≈⟨ Elgot-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) id) ⟩
    ((μ.η _ +₁ id) ∘ (K.₁ (σ _) +₁ id) ∘ (τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ +₁∘+₁) ⟩
    ((μ.η _ ∘ K.₁ (σ _) +₁ id ∘ id) ∘ (τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)) #    ≈⟨ #-resp-≈ (algebras _) (pullˡ +₁∘+₁) ⟩
    (((μ.η _ ∘ K.₁ (σ _)) ∘ τ _ +₁ (id ∘ id) ∘ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)) #   ≈⟨ #-resp-≈ (algebras _) ((+₁-cong₂ refl (elimˡ identity²)) ⟩∘⟨refl) ⟩
    (((μ.η _ ∘ K.₁ (σ _)) ∘ τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h))#                ∎
  pres₂ : ∀ {Z : Obj} (h : Z ⇒ K.₀ Y + Z) → ((μ.η _ ∘ K.₁ (τ _)) ∘ σ _) ∘ (id ×₁ h #) ≈ (((μ.η _ ∘ K.₁ (τ _)) ∘ σ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h))#
  pres₂ {Z} h = by-stabilityˡ (algebras _) (τ _ ∘ (id ×₁ h #)) (sym law₁ˡ) (sym law₂ˡ) pres₁ˡ pres₂ˡ
    where
    ψ : ∀ {X Y} → K.₀ X × K.₀ Y ⇒ K.₀ (X × Y)
    ψ = extend (τ _) ∘ σ _
    ψ-left-iter : ∀ {X Y U} (h : X ⇒ K.₀ Y + X) → ψ {Y} {U} ∘ (h # ×₁ id) ≈ ((ψ +₁ id) ∘ distributeʳ⁻¹ ∘ (h ×₁ id)) #
    ψ-left-iter {X} {Y} {U} h = begin 
      ψ ∘ (h # ×₁ id)                                                   ≈⟨ pullʳ (σ-comm h) ⟩ 
      extend (τ _) ∘ ((σ _ +₁ id) ∘ distributeʳ⁻¹ ∘ (h ×₁ id))#         ≈⟨ extend-preserve (τ (Y , U)) (((σ _ +₁ id) ∘ distributeʳ⁻¹ ∘ (h ×₁ id))) ⟩ 
      ((extend (τ _) +₁ id) ∘ (σ _ +₁ id) ∘ distributeʳ⁻¹ ∘ (h ×₁ id))# ≈⟨ #-resp-≈ (algebras (Y × U)) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩ 
      (((ψ +₁ id) ∘ distributeʳ⁻¹ ∘ (h ×₁ id)) #)                       ∎
    law₁ˡ : (ψ ∘ (id ×₁ (h #))) ∘ (η _ ×₁ id) ≈ τ _ ∘ (id ×₁ h #)
    law₁ˡ = begin 
      (ψ ∘ (id ×₁ (h #))) ∘ (η _ ×₁ id)  ≈⟨ pullʳ (×₁∘×₁ ○ ×₁-cong₂ id-comm-sym id-comm) ⟩ 
      ψ ∘ (η _ ∘ id ×₁ id ∘ h #)         ≈⟨ refl⟩∘⟨ (sym ×₁∘×₁) ⟩ 
      ψ ∘ (η X ×₁ id) ∘ (id ×₁ (h #))    ≈⟨ pullˡ (pullʳ  σ-η  ) ⟩
      (extend (τ _) ∘ η _) ∘ (id ×₁ h #) ≈⟨ kleisliK.identityʳ ⟩∘⟨refl ⟩
      τ (X , Y) ∘ (id ×₁ (h #))          ∎
    law₂ˡ : ((ψ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h))# ∘ (η _ ×₁ id) ≈ τ _ ∘ (id ×₁ h #)
    law₂ˡ = begin
      ((ψ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)) # ∘ (η _ ×₁ id) ≈⟨ sym (#-Uniformity (algebras _) (sym by-uni)) ⟩
      ((τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h))#              ≈⟨ sym (τ-comm h) ⟩
      τ (X , Y) ∘ (id ×₁ (h #))                               ∎
      where
        by-uni : ((ψ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)) ∘ (η _ ×₁ id) ≈ (id +₁ (η _ ×₁ id)) ∘ (τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)
        by-uni = begin
          ((ψ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)) ∘ (η _ ×₁ id)               ≈⟨ pullʳ (pullʳ (×₁∘×₁ ○ ×₁-cong₂ id-comm-sym id-comm ○ sym ×₁∘×₁)) ⟩
          (ψ +₁ id) ∘ distributeˡ⁻¹ ∘ (η _ ×₁ id) ∘ (id ×₁ h)                 ≈⟨ refl⟩∘⟨ pullˡ (sym (distributeˡ⁻¹-natural _ _ _ ○ refl⟩∘⟨ ×₁-cong₂ refl ([]-unique id-comm-sym id-comm-sym))) ⟩
          (ψ +₁ id) ∘ ((η _ ×₁ id +₁ η _ ×₁ id) ∘ distributeˡ⁻¹) ∘ (id ×₁ h)  ≈⟨ pullˡ (pullˡ +₁∘+₁) ⟩
          ((ψ ∘ (η _ ×₁ id) +₁ id ∘ (η _ ×₁ id)) ∘ distributeˡ⁻¹) ∘ (id ×₁ h) ≈⟨ assoc ○ (+₁-cong₂ (pullʳ σ-η) identityˡ) ⟩∘⟨refl ⟩
          (extend (τ _) ∘ η _ +₁ η _ ×₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)       ≈⟨ (+₁-cong₂ kleisliK.identityʳ refl) ⟩∘⟨refl ⟩
          (τ _ +₁ (η _ ×₁ id)) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)                    ≈⟨ sym (pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ)) ⟩
          (id +₁ (η _ ×₁ id)) ∘ (τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)       ∎
    pres₁ˡ : ∀ {U} (g : U ⇒ K.₀ X + U) → (ψ ∘ (id ×₁ h #)) ∘ (g # ×₁ id) ≈ ((ψ ∘ (id ×₁ h #) +₁ id) ∘ distributeʳ⁻¹ ∘ (g ×₁ id)) #
    pres₁ˡ {U} g = begin
      (ψ ∘ (id ×₁ h #)) ∘ (g # ×₁ id)                                                  ≈⟨ pullʳ (×₁∘×₁ ○ ×₁-cong₂ id-comm-sym id-comm ○ sym ×₁∘×₁) ⟩
      ψ ∘ (g # ×₁ id) ∘ (id ×₁ h #)                                                    ≈⟨ pullˡ (pullʳ (σ-comm g)) ⟩
      (extend (τ _) ∘ ((σ _ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ×₁ id)) #) ∘ (id ×₁ h #)       ≈⟨ extend-preserve (τ (X , Y)) _ ⟩∘⟨refl ⟩
      ((extend (τ _) +₁ id) ∘ (σ _ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ×₁ id)) # ∘ (id ×₁ h #) ≈⟨ sym (#-Uniformity (algebras _) (sym by-uni)) ⟩
      ((ψ ∘ (id ×₁ h #) +₁ id) ∘ distributeʳ⁻¹ ∘ (g ×₁ id))#                           ∎
      where
        by-uni : ((extend (τ _) +₁ id) ∘ (σ _ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ×₁ id)) ∘ (id ×₁ h #) ≈ (id +₁ (id ×₁ h #)) ∘ ((ψ ∘ (id ×₁ h #)) +₁ id) ∘ distributeʳ⁻¹ ∘ (g ×₁ id)
        by-uni = begin
          ((extend (τ _) +₁ id) ∘ (σ _ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ×₁ id)) ∘ (id ×₁ h #)              ≈⟨ pullʳ (pullʳ (pullʳ (×₁∘×₁ ○ ×₁-cong₂ id-comm id-comm-sym ○ sym ×₁∘×₁))) ⟩
          (extend (τ _) +₁ id) ∘ (σ _ +₁ id) ∘ distributeʳ⁻¹ ∘ (id ×₁ (h #)) ∘ (g ×₁ id)              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym (distributeʳ⁻¹-natural _ _ _ ○ refl⟩∘⟨ ×₁-cong₂ ([]-unique id-comm-sym id-comm-sym) refl)) ⟩
          (extend (τ _) +₁ id) ∘ (σ _ +₁ id) ∘ ((id ×₁ h # +₁ id ×₁ h #) ∘ distributeʳ⁻¹) ∘ (g ×₁ id) ≈⟨ pullˡ +₁∘+₁ ○ pullˡ (pullˡ +₁∘+₁) ⟩
          ((ψ ∘ (id ×₁ h #) +₁ (id ∘ id) ∘ (id ×₁ h #)) ∘ distributeʳ⁻¹) ∘ (g ×₁ id)                  ≈⟨ assoc ○ (+₁-cong₂ refl (elimˡ identity²)) ⟩∘⟨refl ⟩
          (ψ ∘ (id ×₁ h #) +₁ (id ×₁ h #)) ∘ distributeʳ⁻¹ ∘ (g ×₁ id)                                ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟩
          (id +₁ (id ×₁ h #)) ∘ ((ψ ∘ (id ×₁ h #)) +₁ id) ∘ distributeʳ⁻¹ ∘ (g ×₁ id)                 ∎
    pres₂ˡ : ∀ {U} (g : U ⇒ K.₀ X + U) → ((ψ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)) # ∘ (g # ×₁ id) ≈ ((((ψ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h))# +₁ id) ∘ distributeʳ⁻¹ ∘ (g ×₁ id))#
    pres₂ˡ {U} g = begin
      ((ψ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h))# ∘ (g # ×₁ id) ≈⟨ στ ⟩
      extend ψ ∘ extend (σ _) ∘ τ _ ∘ (((η _ +₁ id) ∘ g) # ×₁ ((η _ +₁ id) ∘ h) #)    ≈⟨ refl⟩∘⟨ (sym (comm-helper g h)) ⟩
      extend ψ ∘ extend (τ _) ∘ σ _ ∘ (((η _ +₁ id) ∘ g) # ×₁ ((η _ +₁ id) ∘ h) #)    ≈⟨ sym τσ ⟩
      ((((ψ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h))# +₁ id) ∘ distributeʳ⁻¹ ∘ (g ×₁ id))# ∎
      where
        τσ : ((((ψ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h))# +₁ id) ∘ distributeʳ⁻¹ ∘ (g ×₁ id))# ≈ extend ψ ∘ extend (τ _) ∘ σ _ ∘ (((η _ +₁ id) ∘ g) # ×₁ ((η _ +₁ id) ∘ h) #)
        τσ = begin 
          (((((ψ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h))# +₁ id) ∘ distributeʳ⁻¹ ∘ (g ×₁ id))#)                                        ≈˘⟨ #-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ kleisliK.identityʳ identity²)) ⟩ 
          ((extend (((ψ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)) #) +₁ id) ∘ (η _ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ×₁ id)) #                 ≈˘⟨ extend-preserve (((ψ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)) #) ((η _ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ×₁ id)) ⟩ 
          extend (((ψ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)) #) ∘ ((η _ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ×₁ id)) #                         ≈⟨ refl⟩∘⟨ (#-resp-≈ (algebras _) ((+₁-cong₂ (sym σ-η) refl) ⟩∘⟨refl)) ⟩ 
          extend (((ψ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)) #) ∘ ((σ _ ∘ (η _ ×₁ id) +₁ id) ∘ distributeʳ⁻¹ ∘ (g ×₁ id)) #           ≈˘⟨ refl⟩∘⟨ (σ-comm _ ○ #-resp-≈ (algebras _) helper) ⟩ 
          extend (((ψ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)) #) ∘ σ _ ∘ (((η _ +₁ id) ∘ g)# ×₁ id)                                    ≈˘⟨ (kleisliK.extend-≈ (#-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ kleisliK.identityʳ identity²)))) ⟩∘⟨refl ⟩ 
          extend ((((extend ψ +₁ id) ∘ (η _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h))#)) ∘ σ _ ∘ (((η _ +₁ id) ∘ g)# ×₁ id)              ≈˘⟨ (kleisliK.extend-≈ (extend-preserve ψ _)) ⟩∘⟨refl ⟩ 
          extend (extend ψ ∘ (((η _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h))#)) ∘ σ _ ∘ (((η _ +₁ id) ∘ g)# ×₁ id)                      ≈˘⟨ pullˡ kleisliK.sym-assoc ⟩ 
          extend ψ ∘ extend (((η _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h))#) ∘ σ _ ∘ (((η _ +₁ id) ∘ g)# ×₁ id)                        ≈˘⟨ refl⟩∘⟨ ((kleisliK.extend-≈ (#-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (sym (distributeˡ⁻¹-natural id _ id)))) ○ #-resp-≈ (algebras _) (pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ (τ-η _) (elimʳ (⟨⟩-unique id-comm id-comm)))) ○ assoc))) ⟩∘⟨refl) ⟩ 
          extend ψ ∘ extend (((τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ (η _ +₁ id)) ∘ (id ×₁ h)) #) ∘ σ _ ∘ (((η _ +₁ id) ∘ g)# ×₁ id) ≈⟨ refl⟩∘⟨ (kleisliK.extend-≈ (#-resp-≈ (algebras _) (refl⟩∘⟨ (refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ identity² refl))))) ⟩∘⟨refl ⟩ 
          extend ψ ∘ extend (((τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ (η _ +₁ id) ∘ h)) #) ∘ σ _ ∘ (((η _ +₁ id) ∘ g)# ×₁ id)         ≈˘⟨ refl⟩∘⟨ ((kleisliK.extend-≈ (τ-comm _)) ⟩∘⟨refl) ⟩ 
          extend ψ ∘ extend (τ _ ∘ (id ×₁ ((η _ +₁ id) ∘ h) #)) ∘ σ _ ∘ (((η _ +₁ id) ∘ g)# ×₁ id)                                 ≈˘⟨ refl⟩∘⟨ (pullˡ (extend∘F₁ monadK (τ _) _)) ⟩ 
          extend ψ ∘ extend (τ _) ∘ K.₁ (id ×₁ ((η _ +₁ id) ∘ h) #) ∘ σ _ ∘ (((η _ +₁ id) ∘ g)# ×₁ id)                             ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym (σ-natural id (((η (K.₀ Y) +₁ id) ∘ h) #))) ⟩ 
          extend ψ ∘ extend (τ _) ∘ (σ _ ∘ (K.₁ id ×₁ ((η _ +₁ id) ∘ h) #)) ∘ (((η _ +₁ id) ∘ g)# ×₁ id)                           ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (assoc ○ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂  (elimˡ monadK.F.identity) identityʳ)) ⟩ 
          extend ψ ∘ extend (τ _) ∘ σ _ ∘ (((η _ +₁ id) ∘ g) # ×₁ ((η _ +₁ id) ∘ h) #)                                             ∎
          where
            helper : (σ _ +₁ id) ∘ distributeʳ⁻¹ ∘ (((η _ +₁ id) ∘ g ×₁ id)) ≈ (σ _ ∘ (η _ ×₁ id) +₁ id) ∘ distributeʳ⁻¹ ∘ (g ×₁ id)
            helper = sym (begin
              (σ _ ∘ (η _ ×₁ id) +₁ id) ∘ distributeʳ⁻¹ ∘ (g ×₁ id)           ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²) ⟩
              (σ _ +₁ id) ∘ ((η _ ×₁ id) +₁ id) ∘ distributeʳ⁻¹ ∘ (g ×₁ id)   ≈⟨ refl⟩∘⟨ (pullˡ ((+₁-cong₂ refl (sym (⟨⟩-unique id-comm id-comm))) ⟩∘⟨refl ○ distributeʳ⁻¹-natural id (η (K.₀ X)) id)) ⟩
              (σ _ +₁ id) ∘ (distributeʳ⁻¹ ∘ ((η _ +₁ id) ×₁ id)) ∘ (g ×₁ id) ≈⟨ refl⟩∘⟨ pullʳ (×₁∘×₁ ○ ×₁-cong₂ refl identity²) ⟩
              (σ _ +₁ id) ∘ distributeʳ⁻¹ ∘ (((η _ +₁ id) ∘ g ×₁ id))         ∎)
        στ : ((ψ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h))# ∘ (g # ×₁ id) ≈ extend ψ ∘ extend (σ _) ∘ τ _ ∘ (((η _ +₁ id) ∘ g) # ×₁ ((η _ +₁ id) ∘ h) #)
        στ = begin
          ((ψ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h))# ∘ (g # ×₁ id)                                                                          ≈⟨ sym (#-Uniformity (algebras (X × Y)) (sym by-uni)) ⟩ 
          ((ψ ∘ ((g #) ×₁ id) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)) #                                                                       ≈⟨ #-resp-≈ (algebras _) ((+₁-cong₂ (ψ-left-iter g) refl) ⟩∘⟨refl) ⟩
          (((((ψ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ×₁ id)) # +₁ id)) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)) #                                             ≈˘⟨ #-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ kleisliK.identityʳ identity²)) ⟩
          ((extend (((ψ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ×₁ id)) #) +₁ id) ∘ (η _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)) #                        ≈˘⟨ extend-preserve (((ψ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ×₁ id)) #) ((η (U × K.₀ Y) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)) ⟩
          extend (((ψ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ×₁ id)) #) ∘ ((η _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)) #                                ≈⟨ refl⟩∘⟨ (#-resp-≈ (algebras _) ((+₁-cong₂ (sym (τ-η _)) refl) ⟩∘⟨refl)) ⟩
          extend (((ψ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ×₁ id)) #) ∘ ((τ _ ∘ (id ×₁ η _) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)) #                  ≈˘⟨ refl⟩∘⟨ (τ-comm ((η (K.₀ Y) +₁ id) ∘ h) ○ #-resp-≈ (algebras _) helper) ⟩
          extend (((ψ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ×₁ id)) #) ∘ τ _ ∘ (id ×₁ ((η _ +₁ id) ∘ h)#)                                           ≈˘⟨ (kleisliK.extend-≈ (#-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ kleisliK.identityʳ identity²)))) ⟩∘⟨refl ⟩
          extend ((((extend ψ +₁ id) ∘ (η _ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ×₁ id))#)) ∘ τ _ ∘ (id ×₁ ((η _ +₁ id) ∘ h) #)                    ≈˘⟨ (kleisliK.extend-≈ (extend-preserve ψ ((η (K.₀ X × K.₀ Y) +₁ id) ∘ distributeʳ⁻¹ ∘ (g ×₁ id)))) ⟩∘⟨refl ⟩
          extend (extend ψ ∘ (((η _ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ×₁ id))#)) ∘ τ _ ∘ (id ×₁ ((η _ +₁ id) ∘ h) #)                            ≈˘⟨ pullˡ kleisliK.sym-assoc ⟩
          extend ψ ∘ extend (((η _ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ×₁ id))#) ∘ τ _ ∘ (id ×₁ ((η _ +₁ id) ∘ h) #)                              ≈˘⟨ refl⟩∘⟨ ((kleisliK.extend-≈ (#-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (sym (distributeʳ⁻¹-natural id (η (K.₀ X)) id)))) ○ #-resp-≈ (algebras _) (pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ σ-η (elimʳ (⟨⟩-unique id-comm id-comm)))) ○ assoc))) ⟩∘⟨refl) ⟩
          extend ψ ∘ extend (((σ _ +₁ id) ∘ distributeʳ⁻¹ ∘ ((η (K.₀ X) +₁ id) ×₁ id) ∘ (g ×₁ id)) #) ∘ τ _ ∘ (id ×₁ ((η _ +₁ id) ∘ h) #) ≈⟨ refl⟩∘⟨ (kleisliK.extend-≈ (#-resp-≈ (algebras _) (refl⟩∘⟨ (refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ refl identity²))))) ⟩∘⟨refl ⟩
          extend ψ ∘ extend (((σ _ +₁ id) ∘ distributeʳ⁻¹ ∘ ((η (K.₀ X) +₁ id) ∘ g ×₁ id)) #) ∘ τ _ ∘ (id ×₁ ((η _ +₁ id) ∘ h) #)         ≈˘⟨ refl⟩∘⟨ ((kleisliK.extend-≈ (σ-comm ((η (K.₀ X) +₁ id) ∘ g))) ⟩∘⟨refl) ⟩
          extend ψ ∘ extend (σ _ ∘ (((η _ +₁ id) ∘ g) # ×₁ id)) ∘ τ _ ∘ (id ×₁ ((η _ +₁ id) ∘ h) #)                                       ≈˘⟨ refl⟩∘⟨ (pullˡ (extend∘F₁ monadK (σ _) (((η _ +₁ id) ∘ g) # ×₁ id))) ⟩
          extend ψ ∘ extend (σ _) ∘ K.₁ (((η _ +₁ id) ∘ g) # ×₁ id) ∘ τ _ ∘ (id ×₁ ((η _ +₁ id) ∘ h) #)                                   ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym (strengthen.commute (((η (K.₀ X) +₁ id) ∘ g) # , id))) ⟩
          extend ψ ∘ extend (σ _) ∘ (τ _ ∘ (((η _ +₁ id) ∘ g) # ×₁ K.₁ id)) ∘ (id ×₁ ((η _ +₁ id) ∘ h) #)                                 ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (assoc ○ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ identityʳ (elimˡ monadK.F.identity))) ⟩
          extend ψ ∘ extend (σ _) ∘ τ _ ∘ (((η _ +₁ id) ∘ g) # ×₁ ((η _ +₁ id) ∘ h) #)                                                    ∎
          where
            by-uni : ((ψ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)) ∘ ((g #) ×₁ id) ≈ (id +₁ (g #) ×₁ id) ∘ (ψ ∘ ((g #) ×₁ id) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)
            by-uni = begin 
              ((ψ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)) ∘ ((g #) ×₁ id)                         ≈⟨ pullʳ (pullʳ (×₁∘×₁ ○ ×₁-cong₂ id-comm-sym id-comm ○ sym ×₁∘×₁)) ⟩ 
              (ψ +₁ id) ∘ distributeˡ⁻¹ ∘ ((g #) ×₁ id) ∘ (id ×₁ h)                           ≈˘⟨ refl⟩∘⟨ ((distributeˡ⁻¹-natural (g #) id id ○ refl⟩∘⟨ ×₁-cong₂ refl ([]-unique id-comm-sym id-comm-sym)) ⟩∘⟨refl ○ assoc) ⟩ 
              (ψ +₁ id) ∘ ((((g #) ×₁ id) +₁ ((g #) ×₁ id)) ∘ distributeˡ⁻¹) ∘ (id ×₁ h)      ≈⟨ pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ (sym identityˡ) id-comm-sym ○ sym +₁∘+₁)) ⟩ 
              (((id +₁ (g #) ×₁ id) ∘ (ψ ∘ ((g #) ×₁ id) +₁ id)) ∘ distributeˡ⁻¹) ∘ (id ×₁ h) ≈⟨ assoc²αε ⟩ 
              (id +₁ (g #) ×₁ id) ∘ (ψ ∘ ((g #) ×₁ id) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)     ∎
            helper : (τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ (η _ +₁ id) ∘ h) ≈ (τ _ ∘ (id ×₁ η _) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)
            helper = sym (begin 
              (τ _ ∘ (id ×₁ η _) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)           ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²) ⟩ 
              (τ _ +₁ id) ∘ ((id ×₁ η _) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ h)   ≈⟨ refl⟩∘⟨ (pullˡ ((+₁-cong₂ refl (sym (⟨⟩-unique id-comm id-comm))) ⟩∘⟨refl ○ distributeˡ⁻¹-natural id (η (K.₀ Y)) id)) ⟩ 
              (τ _ +₁ id) ∘ (distributeˡ⁻¹ ∘ (id ×₁ (η _ +₁ id))) ∘ (id ×₁ h) ≈⟨ refl⟩∘⟨ pullʳ (×₁∘×₁ ○ ×₁-cong₂ identity² refl) ⟩ 
              (τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ (η _ +₁ id) ∘ h)           ∎)

KCommutativeMonad : CommutativeMonad {V = monoidal} braided
KCommutativeMonad = record 
  { strongMonad = KStrong
  ; commutative = KCommutative
  }