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
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ʳ (pullʳ (τ-η _)) ⟩ 
    μ.η _ ∘ K.₁ (σ _) ∘ η _                 ≈⟨ refl⟩∘⟨ (K₁η _) ⟩
    μ.η _ ∘ η _ ∘ σ _                       ≈⟨ cancelˡ monadK.identityʳ ⟩
    σ _                                     ∎)
  law₂ : σ _ ≈ (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (id ⁂ η _)
  law₂ = sym (begin 
    (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (id ⁂ η _)                       ≈⟨ pullʳ (pullʳ (pullʳ (pullʳ swap∘⁂))) ⟩ 
    μ.η _ ∘ K.₁ (τ _) ∘ K.₁ swap ∘ τ _ ∘ (η _ ⁂ id) ∘ swap       ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ refl (sym K.identity) ⟩∘⟨refl ⟩ 
    μ.η _ ∘ K.₁ (τ _) ∘ K.₁ swap ∘ τ _ ∘ (η _ ⁂ K.₁ id) ∘ swap   ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (strengthen.commute (η _ , id)) ⟩ 
    μ.η _ ∘ K.₁ (τ _) ∘ K.₁ swap ∘ (K.₁ (η _ ⁂ id) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (pullˡ (sym K.homomorphism)) ⟩ 
    μ.η _ ∘ K.₁ (τ _) ∘ (K.₁ (swap ∘ (η _ ⁂ id)) ∘ τ _) ∘ swap   ≈⟨ refl⟩∘⟨ (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ʳ (pullʳ (♯-preserving (stable _) (η _) h)) ⟩ 
    μ.η _ ∘ K.₁ (σ _) ∘ ((τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #                   ≈⟨ refl⟩∘⟨ (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₂ assoc (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 = sym-assoc ⟩∘⟨refl ○ by-stabilityˡ (algebras _) (τ _ ∘ (id ⁂ h #)) (sym law₁ˡ) (sym law₂ˡ) pres₁ˡ pres₂ˡ ○ #-resp-≈ (algebras _) ((+₁-cong₂ assoc refl) ⟩∘⟨refl)
    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
  }