module Monad.Instance.K.Commutative {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where
open Ambient ambient
open MIK ambient
open MonadK MK
open import Monad.Instance.K.Strong ambient MK
open import Monad.Instance.K.EquationalLifting ambient 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 Equiv
open HomReasoning
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)
First we establish some facts about σ
σ : ∀ ((X , Y) : Obj ×f Obj) → K.₀ X × Y ⇒ K.₀ (X × Y)
σ _ = K.₁ swap ∘ (τ _) ∘ swap
σ-η : ∀ {X Y} → σ (X , Y) ∘ (η _ ⁂ idC) ≈ η _
σ-η = begin
σ (_ , _) ∘ (η _ ⁂ idC) ≈⟨ pullʳ (pullʳ swap∘⁂) ⟩
K.₁ swap ∘ τ (_ , _) ∘ (idC ⁂ η _) ∘ swap ≈⟨ refl⟩∘⟨ (pullˡ (τ-η _)) ⟩
K.₁ swap ∘ η _ ∘ swap ≈⟨ pullˡ (K₁η swap) ⟩
(η _ ∘ swap) ∘ swap ≈⟨ cancelʳ swap∘swap ⟩
η (_ × _) ∎
σ-comm : ∀ {X Y Z} (h : Z ⇒ K.₀ X + Z) → σ (X , Y) ∘ (h # ⁂ idC) ≈ ((σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC))#
σ-comm {X} {Y} {Z} h = begin
(K.₁ swap ∘ τ _ ∘ swap) ∘ (h # ⁂ idC) ≈⟨ pullʳ (pullʳ swap∘⁂) ⟩
K.₁ swap ∘ τ _ ∘ (idC ⁂ h #) ∘ swap ≈⟨ refl⟩∘⟨ (pullˡ (τ-comm h)) ⟩
K.₁ swap ∘ ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∘ swap ≈⟨ pullˡ (Elgot-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) (η _ ∘ swap))) ⟩
((K.₁ swap +₁ idC) ∘ (τ (Y , X) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∘ swap ≈⟨ sym (#-Uniformity (algebras _) (sym by-uni)) ⟩
((σ (X , Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) # ∎
where
by-uni : ((K.₁ swap +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ swap ≈ (idC +₁ swap) ∘ (σ (X , Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)
by-uni = begin
((K.₁ swap +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ swap ≈⟨ pullʳ (pullʳ (pullʳ (sym swap∘⁂))) ⟩
(K.₁ swap +₁ idC) ∘ (τ (Y , X) +₁ idC) ∘ distributeˡ⁻¹ ∘ swap ∘ (h ⁂ idC) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ distributeˡ⁻¹∘swap ⟩
(K.₁ swap +₁ idC) ∘ (τ (Y , X) +₁ idC) ∘ ((swap +₁ swap) ∘ distributeʳ⁻¹) ∘ (h ⁂ idC) ≈⟨ pullˡ +₁∘+₁ ⟩
(K.₁ swap ∘ τ _ +₁ idC ∘ idC) ∘ ((swap +₁ swap) ∘ distributeʳ⁻¹) ∘ (h ⁂ idC) ≈⟨ pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ assoc (elimˡ identity²))) ⟩
((σ _ +₁ swap) ∘ distributeʳ⁻¹) ∘ (h ⁂ idC) ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ○ sym-assoc ⟩
(idC +₁ swap) ∘ (σ (X , Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ∎
σ-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.₁ (σ _) ∘ σ _ ≈ σ _ ∘ (μ.η _ ⁂ idC)
σ-μ-η-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 ∘ τ _ ∘ (idC ⁂ μ.η _) ∘ swap ≈˘⟨ pullʳ (pullʳ swap∘⁂) ⟩
σ _ ∘ (μ.η _ ⁂ idC) ∎
σ-π₁ : ∀ {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 ⁂ idC)) ∘ σ _ ∘ (idC ⁂ extend g) ≈ σ _ ∘ (extend f ⁂ extend g)
σ-kleisli-assoc {X} {Y} {Z} {U} f g = begin
extend (σ _ ∘ (f ⁂ idC)) ∘ σ _ ∘ (idC ⁂ extend g) ≈˘⟨ pullˡ (extend∘F₁ monadK (σ _) (f ⁂ idC)) ⟩
extend (σ _) ∘ K.₁ (f ⁂ idC) ∘ σ _ ∘ (idC ⁂ extend g) ≈⟨ refl⟩∘⟨ (pullˡ (sym (σ-natural f idC)) ○ assoc) ⟩
extend (σ _) ∘ σ _ ∘ (K.₁ f ⁂ idC) ∘ (idC ⁂ extend g) ≈⟨ pullˡ (assoc ○ σ-μ-η-comm) ○ assoc ⟩
σ _ ∘ (μ.η _ ⁂ idC) ∘ (K.₁ f ⁂ idC) ∘ (idC ⁂ extend g) ≈⟨ refl⟩∘⟨ (pullˡ (⁂∘⁂ ○ ⁂-cong₂ refl identity²)) ⟩
σ _ ∘ (extend f ⁂ idC) ∘ (idC ⁂ extend g) ≈⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identityʳ identityˡ) ⟩
σ _ ∘ (extend f ⁂ extend g) ∎
The key lemma is that τ* ∘ σ ∘ (f’ # ⁂ g’ #) = σ ∘ τ* ∘ (f’ # ⁂ g’ #) for any f’ = (η + id) ∘ f g’ = (η + id) ∘ g where f : X → K Y + X g : Z → K U + Z
private
comm-helper : ∀ {X Y Z U} (f : X ⇒ K.₀ Y + X) (g : Z ⇒ K.₀ U + Z) → extend (τ _) ∘ σ _ ∘ (((η _ +₁ idC) ∘ f) # ⁂ ((η _ +₁ idC) ∘ g) #) ≈ extend (σ _) ∘ τ _ ∘ (((η _ +₁ idC) ∘ f) # ⁂ ((η _ +₁ idC) ∘ g) #)
comm-helper {X} {Y} {Z} {U} f g = begin
extend (τ _) ∘ σ _ ∘ (f' # ⁂ g' #) ≈⟨ τσ ⟩
extend ([ σ _ ∘ ( f' # ⁂ idC ) , τ _ ∘ (idC ⁂ g' #) ]) ∘ w # ≈⟨ sym στ ⟩
extend (σ _) ∘ τ _ ∘ (((η _ +₁ idC) ∘ f) # ⁂ ((η _ +₁ idC) ∘ g) #) ∎
where
f' = (η _ +₁ idC) ∘ f
g' = (η _ +₁ idC) ∘ g
w = [ i₁ ∘ K.₁ i₁ ∘ τ _ , (K.₁ i₂ ∘ σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')
w-law₁ : f' # ∘ π₁ ≈ extend [ f' # ∘ π₁ , η _ ∘ π₁ ] ∘ w #
w-law₁ = sym (begin
extend [ f' # ∘ π₁ , η _ ∘ π₁ ] ∘ w # ≈⟨ step₁ ⟩
([ i₁ ∘ π₁ , (f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ g))# ≈⟨ sym step₂ ⟩
(f' #) ∘ π₁ ∎)
where
h = (π₁ +₁ (π₁ +₁ π₁ ⁂ idC) ∘ distributeˡ⁻¹ ∘ ⟨ idC , g ∘ π₂ ⟩) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC)
by-uni : (idC +₁ π₁) ∘ (idC +₁ ∇) ∘ h ≈ f' ∘ π₁
by-uni = begin
(idC +₁ π₁) ∘ (idC +₁ ∇) ∘ h ≈⟨ pullˡ +₁∘+₁ ○ pullˡ (+₁∘+₁ ○ +₁-cong₂ (elimˡ identity²) (pullʳ (pullˡ []∘+₁))) ⟩
(π₁ +₁ π₁ ∘ [ (idC ∘ π₁) , (idC ∘ (π₁ ⁂ idC)) ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , g ∘ π₂ ⟩) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ≈⟨ (+₁-cong₂ refl (pullˡ ∘[] ○ ([]-cong₂ (refl⟩∘⟨ identityˡ) ((refl⟩∘⟨ identityˡ) ○ π₁∘⁂)) ⟩∘⟨refl)) ⟩∘⟨refl ⟩
(π₁ +₁ [ π₁ ∘ π₁ , π₁ ∘ π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , g ∘ π₂ ⟩) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ≈⟨ (+₁-cong₂ refl (pullˡ ((sym ∘[]) ⟩∘⟨refl ○ pullʳ distributeˡ⁻¹-π₁))) ⟩∘⟨refl ⟩
(π₁ +₁ (π₁ ∘ π₁) ∘ ⟨ idC , g ∘ π₂ ⟩) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ≈⟨ (+₁-cong₂ refl (cancelʳ project₁)) ⟩∘⟨refl ⟩
(π₁ +₁ π₁) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ≈⟨ pullˡ distributeʳ⁻¹-π₁ ⟩
π₁ ∘ (f' ⁂ idC) ≈⟨ π₁∘⁂ ⟩
f' ∘ π₁ ∎
step₁ : extend [ f' # ∘ π₁ , η _ ∘ π₁ ] ∘ w # ≈ ([ i₁ ∘ π₁ , (f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ g))#
step₁ = begin
extend [ f' # ∘ π₁ , η _ ∘ π₁ ] ∘ w # ≈⟨ extend-preserve [ (f' #) ∘ π₁ , η (K.₀ Y) ∘ π₁ ] w ⟩
((extend [ f' # ∘ π₁ , η _ ∘ π₁ ] +₁ idC) ∘ 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) ∘ π₁) ∘ σ _ +₁ idC)) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ 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.₁ π₁ ∘ σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ ⁂-cong₂ identity² refl)) ⟩
([ i₁ ∘ extend (f' # ∘ π₁) ∘ τ _ , (K.₁ π₁ ∘ σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ (η _ +₁ idC)) ∘ (idC ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (sym (distributeˡ⁻¹-natural idC (η (K.₀ U)) idC)) ○ assoc)) ⟩
([ i₁ ∘ extend (f' # ∘ π₁) ∘ τ _ , (K.₁ π₁ ∘ σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ (idC ⁂ η _ +₁ idC ⁂ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ ([]∘+₁ ○ []-cong₂ assoc²' (elimʳ (⟨⟩-unique id-comm id-comm)))) ⟩
([ i₁ ∘ extend (f' # ∘ π₁) ∘ τ _ ∘ (idC ⁂ η _) , (K.₁ π₁ ∘ σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (refl⟩∘⟨ (refl⟩∘⟨ (τ-η _) ○ kleisliK.identityʳ)) ((+₁-cong₂ σ-π₁ refl) ⟩∘⟨refl)) ⟩∘⟨refl) ⟩
([ i₁ ∘ f' # ∘ π₁ , (π₁ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (refl⟩∘⟨ ((#-Fixpoint (algebras _)) ⟩∘⟨refl ○ assoc ○ refl⟩∘⟨ (sym π₁∘⁂))) refl) ⟩∘⟨refl) ⟩
([ i₁ ∘ [ idC , f' # ] ∘ π₁ ∘ (f' ⁂ idC) , (π₁ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g)) # ≈˘⟨ #-resp-≈ (algebras _) (pullˡ ([]∘+₁ ○ []-cong₂ assoc²' assoc)) ⟩
([ i₁ ∘ [ idC , f' # ] ∘ π₁ , (π₁ +₁ idC) ∘ distributeʳ⁻¹ ] ∘ ((f' ⁂ idC) +₁ (f' ⁂ idC)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (distributeˡ⁻¹-natural f' idC idC))) ⟩
([ i₁ ∘ [ idC , f' # ] ∘ π₁ , (π₁ +₁ idC) ∘ distributeʳ⁻¹ ] ∘ (distributeˡ⁻¹ ∘ (f' ⁂ (idC +₁ idC))) ∘ (idC ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identityʳ (elimˡ ([]-unique id-comm-sym id-comm-sym))))) ⟩
([ i₁ ∘ [ idC , f' # ] ∘ π₁ , (π₁ +₁ idC) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (f' ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (refl⟩∘⟨ refl⟩∘⟨ sym distributeʳ⁻¹-π₁) refl) ⟩∘⟨refl) ⟩
([ i₁ ∘ [ idC , f' # ] ∘ (π₁ +₁ π₁) ∘ distributeʳ⁻¹ , (π₁ +₁ idC) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (f' ⁂ g)) # ≈˘⟨ #-resp-≈ (algebras _) (pullˡ ([]∘+₁ ○ []-cong₂ assoc²' refl)) ⟩
([ i₁ ∘ [ idC , f' # ] ∘ (π₁ +₁ π₁) , (π₁ +₁ idC) ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (f' ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ pullˡ distribute₄) ⟩
([ i₁ ∘ [ idC , f' # ] ∘ (π₁ +₁ π₁) , (π₁ +₁ idC) ] ∘ ([ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ (f' ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ (pullˡ (∘[] ○ []-cong₂ []∘+₁ []∘+₁))) ⟩
(([ [ ((i₁ ∘ [ idC , f' # ] ∘ (π₁ +₁ π₁)) ∘ i₁) , (((π₁ +₁ idC)) ∘ i₁) ] , [ ((i₁ ∘ [ idC , f' # ] ∘ (π₁ +₁ π₁)) ∘ i₂) , (((π₁ +₁ idC)) ∘ i₂) ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ (f' ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (assoc ○ ([]-cong₂ ([]-cong₂ ((refl⟩∘⟨ []∘+₁) ⟩∘⟨refl ○ pullʳ inject₁) +₁∘i₁) ([]-cong₂ ((refl⟩∘⟨ []∘+₁) ⟩∘⟨refl ○ pullʳ inject₂) +₁∘i₂)) ⟩∘⟨refl) ⟩
([ [ (i₁ ∘ idC ∘ π₁) , i₁ ∘ π₁ ] , [ i₁ ∘ f' # ∘ π₁ , i₂ ∘ idC ] ] ∘ ((distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ (f' ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ ([]-cong₂ (refl⟩∘⟨ identityˡ) refl ○ sym ∘[]) refl) ⟩∘⟨ assoc) ⟩
([ i₁ ∘ [ π₁ , π₁ ] , f' # ∘ π₁ +₁ idC ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ (f' ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ ([]∘+₁ ○ []-cong₂ assoc refl)) ⟩
([ i₁ ∘ [ π₁ , π₁ ] ∘ distributeˡ⁻¹ , (f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ g))# ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (refl⟩∘⟨ distributeˡ⁻¹-π₁) refl) ⟩∘⟨refl) ⟩
([ i₁ ∘ π₁ , (f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ g))# ∎
step₂ : (f' #) ∘ π₁ ≈ ([ i₁ ∘ π₁ , (f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ g))#
step₂ = begin
(f' #) ∘ π₁ ≈˘⟨ #-Uniformity (algebras _) by-uni ⟩
((idC +₁ ∇) ∘ h)# ≈⟨ #-Diamond (algebras _) h ⟩
([ i₁ , ((idC +₁ ∇) ∘ h) # +₁ idC ] ∘ h) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (+₁-cong₂ (#-Uniformity (algebras _) by-uni) refl)) ⟩∘⟨refl) ⟩
([ i₁ , (f' # ∘ π₁) +₁ idC ] ∘ h) # ≈⟨ #-resp-≈ (algebras _) (pullˡ []∘+₁) ⟩
([ (i₁ ∘ π₁) , (((f' # ∘ π₁) +₁ idC) ∘ (π₁ +₁ π₁ ⁂ idC) ∘ distributeˡ⁻¹ ∘ ⟨ idC , g ∘ π₂ ⟩) ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC)) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (pullˡ (+₁∘+₁ ○ +₁-cong₂ assoc identityˡ))) ⟩∘⟨refl) ⟩
([ (i₁ ∘ π₁) , ((f' # ∘ π₁ ∘ π₁ +₁ (π₁ ⁂ idC)) ∘ distributeˡ⁻¹ ∘ ⟨ idC , g ∘ π₂ ⟩) ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC)) # ≈˘⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (pullˡ (+₁∘+₁ ○ +₁-cong₂ (pullʳ π₁∘⁂) identityˡ))) ⟩∘⟨refl) ⟩
([ (i₁ ∘ π₁) , (f' # ∘ π₁ +₁ idC) ∘ ((π₁ ⁂ idC) +₁ (π₁ ⁂ idC)) ∘ distributeˡ⁻¹ ∘ ⟨ idC , g ∘ π₂ ⟩ ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC)) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (refl⟩∘⟨ (pullˡ (distributeˡ⁻¹-natural π₁ idC idC ○ refl⟩∘⟨ ⁂-cong₂ refl ([]-unique id-comm-sym id-comm-sym)) ○ assoc))) ⟩∘⟨refl) ⟩
([ (i₁ ∘ π₁) , ((f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹ ∘ (π₁ ⁂ idC) ∘ ⟨ idC , g ∘ π₂ ⟩) ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC)) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (refl⟩∘⟨ (refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ)))) ⟩∘⟨refl) ⟩
([ (i₁ ∘ π₁) , ((f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹ ∘ ⟨ π₁ , g ∘ π₂ ⟩) ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC)) # ≈˘⟨ #-resp-≈ (algebras _) (pullˡ ([]∘+₁ ○ []-cong₂ (pullʳ (π₁∘⁂ ○ identityˡ)) (assoc ○ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ identityˡ refl))) ⟩
([ (i₁ ∘ π₁) , ((f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹) ] ∘ (idC ⁂ g +₁ idC ⁂ g) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC)) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (distributeʳ⁻¹-natural g idC idC) ○ assoc)) ⟩
([ i₁ ∘ π₁ , (f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ ((idC +₁ idC) ⁂ g) ∘ (f' ⁂ idC))# ≈˘⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ ⁂-cong₂ (elimˡ ([]-unique id-comm-sym id-comm-sym)) identityʳ)) ⟩
([ i₁ ∘ π₁ , (f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ g))# ∎
w-law₂ : g' # ∘ π₂ ≈ extend [ η _ ∘ π₂ , g' # ∘ π₂ ] ∘ w #
w-law₂ = sym (begin
extend [ η _ ∘ π₂ , g' # ∘ π₂ ] ∘ w # ≈⟨ step₁ ⟩
([ i₁ ∘ π₂ , (g' # ∘ π₂ +₁ idC) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (f ⁂ g'))# ≈⟨ sym step₂ ⟩
g' # ∘ π₂ ∎)
where
h = (π₂ +₁ (π₂ +₁ idC ⁂ π₂) ∘ distributeʳ⁻¹ ∘ ⟨ f ∘ π₁ , idC ⟩) ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')
by-uni : (idC +₁ π₂) ∘ (idC +₁ ∇) ∘ h ≈ g' ∘ π₂
by-uni = begin
(idC +₁ π₂) ∘ (idC +₁ ∇) ∘ h ≈⟨ pullˡ +₁∘+₁ ○ pullˡ (+₁∘+₁ ○ +₁-cong₂ (elimˡ identity²) (pullʳ (pullˡ []∘+₁))) ⟩
(π₂ +₁ π₂ ∘ [ (idC ∘ π₂) , (idC ∘ (idC ⁂ π₂)) ] ∘ distributeʳ⁻¹ ∘ ⟨ f ∘ π₁ , idC ⟩) ∘ distributeˡ⁻¹ ∘ (idC ⁂ g') ≈⟨ (+₁-cong₂ refl (pullˡ ∘[] ○ ([]-cong₂ (refl⟩∘⟨ identityˡ) ((refl⟩∘⟨ identityˡ) ○ π₂∘⁂)) ⟩∘⟨refl)) ⟩∘⟨refl ⟩
(π₂ +₁ [ π₂ ∘ π₂ , π₂ ∘ π₂ ] ∘ distributeʳ⁻¹ ∘ ⟨ f ∘ π₁ , idC ⟩) ∘ distributeˡ⁻¹ ∘ (idC ⁂ g') ≈⟨ (+₁-cong₂ refl (pullˡ ((sym ∘[]) ⟩∘⟨refl ○ pullʳ distributeʳ⁻¹-π₂))) ⟩∘⟨refl ⟩
(π₂ +₁ (π₂ ∘ π₂) ∘ ⟨ f ∘ π₁ , idC ⟩) ∘ distributeˡ⁻¹ ∘ (idC ⁂ g') ≈⟨ (+₁-cong₂ refl (cancelʳ project₂)) ⟩∘⟨refl ⟩
(π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∘ (idC ⁂ g') ≈⟨ pullˡ distributeˡ⁻¹-π₂ ⟩
π₂ ∘ (idC ⁂ g') ≈⟨ π₂∘⁂ ⟩
g' ∘ π₂ ∎
step₁ : extend [ η _ ∘ π₂ , g' # ∘ π₂ ] ∘ w # ≈ ([ i₁ ∘ π₂ , (g' # ∘ π₂ +₁ idC) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (f ⁂ g'))#
step₁ = begin
extend [ η _ ∘ π₂ , g' # ∘ π₂ ] ∘ w # ≈⟨ extend-preserve _ w ⟩
((extend [ η _ ∘ π₂ , g' # ∘ π₂ ] +₁ idC) ∘ 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' #) ∘ π₂) ∘ σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (pullʳ (pullˡ (extend∘F₁ monadK _ i₁ ○ kleisliK.extend-≈ inject₁ ○ Monad⇒Kleisli⇒Monad monadK π₂))) refl) ⟩∘⟨refl) ⟩
([ i₁ ∘ K.₁ π₂ ∘ τ _ , (extend (g' # ∘ π₂) ∘ σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')) # ≈˘⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (refl⟩∘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identity²))) ⟩∘⟨refl) ⟩
([ i₁ ∘ K.₁ π₂ ∘ τ _ , (extend (g' # ∘ π₂) ∘ σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ ((η _ +₁ idC) ⁂ idC) ∘ (f ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (refl⟩∘⟨ (pullˡ (sym (distributeʳ⁻¹-natural idC (η (K.₀ Y)) idC)) ○ assoc))) ⟩∘⟨refl) ⟩
([ i₁ ∘ K.₁ π₂ ∘ τ _ , (extend (g' # ∘ π₂) ∘ σ _ +₁ idC) ∘ ((η _ ⁂ idC) +₁ (idC ⁂ idC)) ∘ distributeʳ⁻¹ ∘ (f ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (pullˡ (+₁∘+₁ ○ +₁-cong₂ (pullʳ σ-η) (elimʳ (⟨⟩-unique id-comm id-comm))))) ⟩∘⟨refl) ⟩
([ i₁ ∘ K.₁ π₂ ∘ τ _ , (extend (g' # ∘ π₂) ∘ η _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (refl⟩∘⟨ τ-π₂ _) ((+₁-cong₂ kleisliK.identityʳ refl) ⟩∘⟨refl)) ⟩∘⟨refl) ⟩
([ i₁ ∘ π₂ , (g' # ∘ π₂ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (refl⟩∘⟨ (sym (π₂∘⁂ ○ identityˡ))) refl) ⟩∘⟨refl) ⟩
([ i₁ ∘ π₂ ∘ (f ⁂ idC) , (g' # ∘ π₂ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')) # ≈˘⟨ #-resp-≈ (algebras _) (pullˡ ([]∘+₁ ○ []-cong₂ assoc assoc)) ⟩
([ i₁ ∘ π₂ , (g' # ∘ π₂ +₁ idC) ∘ distributeʳ⁻¹ ] ∘ (f ⁂ idC +₁ f ⁂ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (distributeˡ⁻¹-natural f idC idC) ○ assoc)) ⟩
([ i₁ ∘ π₂ , (g' # ∘ π₂ +₁ idC) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (f ⁂ (idC +₁ idC)) ∘ (idC ⁂ g')) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identityʳ (elimˡ ([]-unique id-comm-sym id-comm-sym)))) ⟩
([ i₁ ∘ π₂ , (g' # ∘ π₂ +₁ idC) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (f ⁂ g')) # ∎
step₂ : g' # ∘ π₂ ≈ ([ i₁ ∘ π₂ , (g' # ∘ π₂ +₁ idC) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (f ⁂ g'))#
step₂ = begin
g' # ∘ π₂ ≈˘⟨ #-Uniformity (algebras _) by-uni ⟩
((idC +₁ ∇) ∘ h) # ≈⟨ #-Diamond (algebras _) h ⟩
([ i₁ , ((idC +₁ ∇) ∘ h) # +₁ idC ] ∘ h) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (+₁-cong₂ (#-Uniformity (algebras _) by-uni) refl)) ⟩∘⟨refl) ⟩
([ i₁ , g' # ∘ π₂ +₁ idC ] ∘ h) # ≈⟨ #-resp-≈ (algebras _) (pullˡ []∘+₁) ⟩
([ (i₁ ∘ π₂) , (((g' # ∘ π₂) +₁ idC) ∘ (π₂ +₁ idC ⁂ π₂) ∘ distributeʳ⁻¹ ∘ ⟨ f ∘ π₁ , idC ⟩) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (pullˡ (+₁∘+₁ ○ +₁-cong₂ assoc identityˡ))) ⟩∘⟨refl) ⟩
([ (i₁ ∘ π₂) , ((g' # ∘ π₂ ∘ π₂ +₁ (idC ⁂ π₂)) ∘ distributeʳ⁻¹ ∘ ⟨ f ∘ π₁ , idC ⟩) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')) # ≈˘⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (pullˡ (+₁∘+₁ ○ +₁-cong₂ (pullʳ π₂∘⁂) identityˡ))) ⟩∘⟨refl) ⟩
([ (i₁ ∘ π₂) , (g' # ∘ π₂ +₁ idC) ∘ ((idC ⁂ π₂) +₁ (idC ⁂ π₂)) ∘ distributeʳ⁻¹ ∘ ⟨ f ∘ π₁ , idC ⟩ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (refl⟩∘⟨ (pullˡ (distributeʳ⁻¹-natural π₂ idC idC ○ refl⟩∘⟨ ⁂-cong₂ ([]-unique id-comm-sym id-comm-sym) refl) ○ assoc))) ⟩∘⟨refl) ⟩
([ (i₁ ∘ π₂) , ((g' # ∘ π₂ +₁ idC) ∘ distributeʳ⁻¹ ∘ (idC ⁂ π₂) ∘ ⟨ f ∘ π₁ , idC ⟩) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (refl⟩∘⟨ (refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ identityʳ)))) ⟩∘⟨refl) ⟩
([ (i₁ ∘ π₂) , ((g' # ∘ π₂ +₁ idC) ∘ distributeʳ⁻¹ ∘ ⟨ f ∘ π₁ , π₂ ⟩) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')) # ≈˘⟨ #-resp-≈ (algebras _) (pullˡ ([]∘+₁ ○ []-cong₂ (pullʳ (π₂∘⁂ ○ identityˡ)) (assoc ○ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ refl identityˡ))) ⟩
([ (i₁ ∘ π₂) , ((g' # ∘ π₂ +₁ idC) ∘ distributeʳ⁻¹) ] ∘ (f ⁂ idC +₁ f ⁂ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (distributeˡ⁻¹-natural f idC idC) ○ assoc)) ⟩
([ i₁ ∘ π₂ , (g' # ∘ π₂ +₁ idC) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (f ⁂ (idC +₁ idC)) ∘ (idC ⁂ g'))# ≈˘⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ ⁂-cong₂ identityʳ (elimˡ ([]-unique id-comm-sym id-comm-sym)))) ⟩
([ i₁ ∘ π₂ , (g' # ∘ π₂ +₁ idC) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (f ⁂ g'))# ∎
τσ : extend (τ _) ∘ σ _ ∘ (f' # ⁂ g' #) ≈ extend ([ σ _ ∘ ( f' # ⁂ idC ) , τ _ ∘ (idC ⁂ 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' # ∘ π₁ , η _ ∘ π₁ ] ⁂ idC)) ∘ σ _ ∘ (idC ⁂ extend [ η _ ∘ π₂ , g' # ∘ π₂ ])) ∘ ⟨ w # , w # ⟩ ≈˘⟨ refl⟩∘⟨ (refl⟩∘⟨ (sym (σ-natural idC (extend [ η (K.₀ U) ∘ π₂ , (g' #) ∘ π₂ ])) ○ refl⟩∘⟨ ⁂-cong₂ monadK.F.identity refl)) ⟩∘⟨refl ⟩
extend (τ _) ∘ (extend (σ _ ∘ ([ f' # ∘ π₁ , η _ ∘ π₁ ] ⁂ idC)) ∘ K.₁ (idC ⁂ extend [ η _ ∘ π₂ , g' # ∘ π₂ ]) ∘ σ _) ∘ ⟨ w # , w # ⟩ ≈⟨ refl⟩∘⟨ (pullʳ (pullʳ (pullʳ (pullʳ (swap∘⟨⟩ ○ sym Δ∘))))) ⟩
extend (τ _) ∘ extend (σ _ ∘ ([ f' # ∘ π₁ , η _ ∘ π₁ ] ⁂ idC)) ∘ K.₁ (idC ⁂ extend [ η _ ∘ π₂ , g' # ∘ π₂ ]) ∘ K.₁ swap ∘ τ _ ∘ Δ ∘ w # ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (pullˡ equationalLifting) ⟩
extend (τ _) ∘ extend (σ _ ∘ ([ f' # ∘ π₁ , η _ ∘ π₁ ] ⁂ idC)) ∘ K.₁ (idC ⁂ extend [ η _ ∘ π₂ , g' # ∘ π₂ ]) ∘ K.₁ swap ∘ K.₁ ⟨ η _ , idC ⟩ ∘ w # ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym monadK.F.homomorphism ○ monadK.F.F-resp-≈ swap∘⟨⟩) ⟩
extend (τ _) ∘ extend (σ _ ∘ ([ f' # ∘ π₁ , η _ ∘ π₁ ] ⁂ idC)) ∘ K.₁ (idC ⁂ extend [ η _ ∘ π₂ , g' # ∘ π₂ ]) ∘ K.₁ ⟨ idC , η _ ⟩ ∘ w # ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym monadK.F.homomorphism ○ monadK.F.F-resp-≈ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identity² kleisliK.identityʳ)) ⟩
extend (τ _) ∘ extend (σ _ ∘ ([ f' # ∘ π₁ , η _ ∘ π₁ ] ⁂ idC)) ∘ K.₁ ⟨ idC , [ η _ ∘ π₂ , g' # ∘ π₂ ] ⟩ ∘ w # ≈⟨ refl⟩∘⟨ pullˡ (extend∘F₁ monadK (σ _ ∘ ([ (f' #) ∘ π₁ , η (K.₀ Y) ∘ π₁ ] ⁂ idC)) ⟨ idC , [ η (K.₀ U) ∘ π₂ , (g' #) ∘ π₂ ] ⟩) ⟩
extend (τ _) ∘ extend ((σ _ ∘ ([ f' # ∘ π₁ , η _ ∘ π₁ ] ⁂ idC)) ∘ ⟨ idC , [ η _ ∘ π₂ , 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 (τ _) ∘ σ _ ∘ (idC ⁂ η _) ∘ ( f' # ⁂ idC ) , extend (τ _) ∘ σ _ ∘ (η _ ⁂ idC) ∘ (idC ⁂ g' #) ]) ∘ w # ≈˘⟨ (kleisliK.extend-≈ ([]-cong₂ (refl⟩∘⟨ (pullˡ (sym (σ-natural idC (η _)) ○ refl⟩∘⟨ (⁂-cong₂ monadK.F.identity refl)) ○ assoc)) (refl⟩∘⟨ (sym (pullˡ σ-η))))) ⟩∘⟨refl ⟩
extend ([ extend (τ _) ∘ K.₁ (idC ⁂ η _) ∘ σ _ ∘ ( f' # ⁂ idC ) , extend (τ _) ∘ η _ ∘ (idC ⁂ g' #) ]) ∘ w # ≈⟨ (kleisliK.extend-≈ ([]-cong₂ (pullˡ (extend∘F₁ monadK (τ _) (idC ⁂ η _))) (pullˡ kleisliK.identityʳ))) ⟩∘⟨refl ⟩
extend ([ extend (τ _ ∘ (idC ⁂ η _)) ∘ σ _ ∘ ( f' # ⁂ idC ) , τ _ ∘ (idC ⁂ g' #) ]) ∘ w # ≈⟨ (kleisliK.extend-≈ ([]-cong₂ (elimˡ (kleisliK.extend-≈ (τ-η _) ○ kleisliK.identityˡ)) refl)) ⟩∘⟨refl ⟩
extend ([ σ _ ∘ ( f' # ⁂ idC ) , τ _ ∘ (idC ⁂ g' #) ]) ∘ w # ∎
στ : extend (σ _) ∘ τ _ ∘ (((η _ +₁ idC) ∘ f) # ⁂ ((η _ +₁ idC) ∘ g) #) ≈ extend ([ σ _ ∘ ( f' # ⁂ idC ) , τ _ ∘ (idC ⁂ g' #) ]) ∘ w #
στ = begin
extend (σ _) ∘ τ _ ∘ (((η _ +₁ idC) ∘ f) # ⁂ ((η _ +₁ idC) ∘ 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 (τ _ ∘ (idC ⁂ [ η (K.₀ U) ∘ π₂ , (g' #) ∘ π₂ ])) ∘ τ _ ∘ (extend [ (f' #) ∘ π₁ , η (K.₀ Y) ∘ π₁ ] ⁂ idC)) ∘ ⟨ w # , w # ⟩ ≈˘⟨ refl⟩∘⟨ (refl⟩∘⟨ (sym (strengthen.commute (μ.η (K.₀ Y) ∘ K.₁ [ (f' #) ∘ π₁ , η (K.₀ Y) ∘ π₁ ] , idC)) ○ refl⟩∘⟨ ⁂-cong₂ refl monadK.F.identity)) ⟩∘⟨refl ⟩
extend (σ _) ∘ (extend (τ _ ∘ (idC ⁂ [ η (K.₀ U) ∘ π₂ , (g' #) ∘ π₂ ])) ∘ K.₁ (extend [ (f' #) ∘ π₁ , η (K.₀ Y) ∘ π₁ ] ⁂ idC) ∘ τ _) ∘ ⟨ w # , w # ⟩ ≈⟨ refl⟩∘⟨ (pullʳ (pullʳ (refl⟩∘⟨ (sym Δ∘)))) ⟩
extend (σ _) ∘ extend (τ _ ∘ (idC ⁂ [ η (K.₀ U) ∘ π₂ , (g' #) ∘ π₂ ])) ∘ K.₁ (extend [ (f' #) ∘ π₁ , η (K.₀ Y) ∘ π₁ ] ⁂ idC) ∘ τ _ ∘ Δ ∘ (w #) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (pullˡ equationalLifting) ⟩
extend (σ _) ∘ extend (τ _ ∘ (idC ⁂ [ η (K.₀ U) ∘ π₂ , (g' #) ∘ π₂ ])) ∘ K.₁ (extend [ (f' #) ∘ π₁ , η (K.₀ Y) ∘ π₁ ] ⁂ idC) ∘ K.₁ ⟨ η _ , idC ⟩ ∘ (w #) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym monadK.F.homomorphism ○ monadK.F.F-resp-≈ ⁂∘⟨⟩) ⟩
extend (σ _) ∘ extend (τ _ ∘ (idC ⁂ [ η (K.₀ U) ∘ π₂ , (g' #) ∘ π₂ ])) ∘ K.₁ ⟨ extend [ (f' #) ∘ π₁ , η (K.₀ Y) ∘ π₁ ] ∘ η _ , idC ∘ idC ⟩ ∘ (w #) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (K.F-resp-≈ (⟨⟩-cong₂ kleisliK.identityʳ identity²)) ⟩∘⟨refl ⟩
extend (σ _) ∘ extend (τ _ ∘ (idC ⁂ [ η (K.₀ U) ∘ π₂ , (g' #) ∘ π₂ ])) ∘ K.₁ ⟨ [ (f' #) ∘ π₁ , η (K.₀ Y) ∘ π₁ ] , idC ⟩ ∘ (w #) ≈⟨ refl⟩∘⟨ (pullˡ (extend∘F₁ monadK _ _)) ⟩
extend (σ _) ∘ extend ((τ _ ∘ (idC ⁂ [ η (K.₀ U) ∘ π₂ , (g' #) ∘ π₂ ])) ∘ ⟨ [ (f' #) ∘ π₁ , η (K.₀ Y) ∘ π₁ ] , idC ⟩) ∘ (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 (σ _) ∘ τ _ ∘ (idC ⁂ η _) ∘ ( f' # ⁂ idC ) , extend (σ _) ∘ τ _ ∘ (η _ ⁂ idC) ∘ (idC ⁂ g' #) ]) ∘ (w #) ≈⟨ (kleisliK.extend-≈ ([]-cong₂ (refl⟩∘⟨ (pullˡ (τ-η _))) (refl⟩∘⟨ (pullˡ (sym (sym (strengthen.commute _) ○ refl⟩∘⟨ (⁂-cong₂ refl monadK.F.identity))) ○ assoc)))) ⟩∘⟨refl ⟩
extend ([ extend (σ _) ∘ η _ ∘ ( f' # ⁂ idC ) , extend (σ _) ∘ K.₁ (η _ ⁂ idC) ∘ τ _ ∘ (idC ⁂ g' #) ]) ∘ (w #) ≈⟨ (kleisliK.extend-≈ ([]-cong₂ (pullˡ kleisliK.identityʳ) (cancelˡ (extend∘F₁ monadK (σ _) (η _ ⁂ idC) ○ kleisliK.extend-≈ σ-η ○ kleisliK.identityˡ)))) ⟩∘⟨refl ⟩
extend ([ σ _ ∘ ( f' # ⁂ idC ) , τ _ ∘ (idC ⁂ g' #) ]) ∘ w # ∎
The proof of commutativity is then done by (left and right) stability using the above lemma.
KCommutative : Commutative {C = C} {V = monoidal} braided KStrong
Commutative.commutes KCommutative {X} {Y} = by-stability (algebras _) (σ _) law₁ law₂ pres₁ pres₂
where
law₁ : σ _ ≈ (μ.η _ ∘ K.₁ (σ _) ∘ τ _) ∘ (idC ⁂ η _)
law₁ = sym (begin
(μ.η _ ∘ K.₁ (σ _) ∘ τ _) ∘ (idC ⁂ η _) ≈⟨ pullʳ (pullʳ (τ-η _)) ⟩
μ.η _ ∘ K.₁ (σ _) ∘ η _ ≈⟨ refl⟩∘⟨ (K₁η _) ⟩
μ.η _ ∘ η _ ∘ σ _ ≈⟨ cancelˡ monadK.identityʳ ⟩
σ _ ∎)
law₂ : σ _ ≈ (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ η _)
law₂ = sym (begin
(μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ η _) ≈⟨ pullʳ (pullʳ (pullʳ (pullʳ swap∘⁂))) ⟩
μ.η _ ∘ K.₁ (τ _) ∘ K.₁ swap ∘ τ _ ∘ (η _ ⁂ idC) ∘ swap ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ refl (sym K.identity) ⟩∘⟨refl ⟩
μ.η _ ∘ K.₁ (τ _) ∘ K.₁ swap ∘ τ _ ∘ (η _ ⁂ K.₁ idC) ∘ swap ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (strengthen.commute (η _ , idC)) ⟩
μ.η _ ∘ K.₁ (τ _) ∘ K.₁ swap ∘ (K.₁ (η _ ⁂ idC) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (pullˡ (sym K.homomorphism)) ⟩
μ.η _ ∘ K.₁ (τ _) ∘ (K.₁ (swap ∘ (η _ ⁂ idC)) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ (pullˡ (pullˡ (sym K.homomorphism))) ⟩
μ.η _ ∘ (K.₁ (τ _ ∘ swap ∘ (η _ ⁂ idC)) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ (((K.F-resp-≈ (refl⟩∘⟨ swap∘⁂)) ⟩∘⟨refl) ⟩∘⟨refl) ⟩
μ.η _ ∘ (K.₁ (τ _ ∘ (idC ⁂ η _) ∘ swap) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ (K.F-resp-≈ (pullˡ (τ-η _))) ⟩∘⟨refl ⟩∘⟨refl ⟩
μ.η _ ∘ (K.₁ (η _ ∘ swap) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ ((K.homomorphism ⟩∘⟨refl) ⟩∘⟨refl) ⟩
μ.η _ ∘ ((K.₁ (η _) ∘ K.₁ swap) ∘ τ _) ∘ swap ≈⟨ pullˡ (pullˡ (cancelˡ monadK.identityˡ)) ⟩
(K.₁ swap ∘ τ _) ∘ swap ≈⟨ assoc ⟩
σ _ ∎)
pres₁ : ∀ {Z : Obj} (h : Z ⇒ K.₀ Y + Z) → (μ.η _ ∘ K.₁ (σ _) ∘ τ _) ∘ (idC ⁂ h #) ≈ ((μ.η _ ∘ K.₁ (σ _) ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#
pres₁ {Z} h = begin
(μ.η _ ∘ K.₁ (σ _) ∘ τ _) ∘ (idC ⁂ h #) ≈⟨ pullʳ (pullʳ (♯-preserving (stable _) (η _) h)) ⟩
μ.η _ ∘ K.₁ (σ _) ∘ ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ refl⟩∘⟨ (Elgot-Algebra-Morphism.preserves ((freealgebras _ FreeObject.*) (η _ ∘ σ _))) ⟩
μ.η _ ∘ ((K.₁ (σ _) +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ Elgot-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) idC) ⟩
((μ.η _ +₁ idC) ∘ (K.₁ (σ _) +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ +₁∘+₁) ⟩
((μ.η _ ∘ K.₁ (σ _) +₁ idC ∘ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ +₁∘+₁) ⟩
(((μ.η _ ∘ K.₁ (σ _)) ∘ τ _ +₁ (idC ∘ idC) ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) ((+₁-cong₂ assoc (elimˡ identity²)) ⟩∘⟨refl) ⟩
((μ.η _ ∘ K.₁ (σ _) ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∎
pres₂ : ∀ {Z : Obj} (h : Z ⇒ K.₀ Y + Z) → (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ h #) ≈ ((μ.η _ ∘ K.₁ (τ _) ∘ σ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#
pres₂ {Z} h = sym-assoc ⟩∘⟨refl ○ by-stabilityˡ (algebras _) (τ _ ∘ (idC ⁂ 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 # ⁂ idC) ≈ ((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #
ψ-left-iter {X} {Y} {U} h = begin
ψ ∘ (h # ⁂ idC) ≈⟨ pullʳ (σ-comm h) ⟩
extend (τ _) ∘ ((σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC))# ≈⟨ extend-preserve (τ (Y , U)) (((σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC))) ⟩
((extend (τ _) +₁ idC) ∘ (σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC))# ≈⟨ #-resp-≈ (algebras (Y × U)) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩
(((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #) ∎
law₁ˡ : (ψ ∘ (idC ⁂ (h #))) ∘ (η _ ⁂ idC) ≈ τ _ ∘ (idC ⁂ h #)
law₁ˡ = begin
(ψ ∘ (idC ⁂ (h #))) ∘ (η _ ⁂ idC) ≈⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ id-comm-sym id-comm) ⟩
ψ ∘ (η _ ∘ idC ⁂ idC ∘ h #) ≈⟨ refl⟩∘⟨ (sym ⁂∘⁂) ⟩
ψ ∘ (η X ⁂ idC) ∘ (idC ⁂ (h #)) ≈⟨ pullˡ (pullʳ σ-η ) ⟩
(extend (τ _) ∘ η _) ∘ (idC ⁂ h #) ≈⟨ kleisliK.identityʳ ⟩∘⟨refl ⟩
τ (X , Y) ∘ (idC ⁂ (h #)) ∎
law₂ˡ : ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ (η _ ⁂ idC) ≈ τ _ ∘ (idC ⁂ h #)
law₂ˡ = begin
((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∘ (η _ ⁂ idC) ≈⟨ sym (#-Uniformity (algebras _) (sym by-uni)) ⟩
((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ≈⟨ sym (τ-comm h) ⟩
τ (X , Y) ∘ (idC ⁂ (h #)) ∎
where
by-uni : ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ (η _ ⁂ idC) ≈ (idC +₁ (η _ ⁂ idC)) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)
by-uni = begin
((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ (η _ ⁂ idC) ≈⟨ pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ id-comm-sym id-comm ○ sym ⁂∘⁂)) ⟩
(ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (η _ ⁂ idC) ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ pullˡ (sym (distributeˡ⁻¹-natural _ _ _ ○ refl⟩∘⟨ ⁂-cong₂ refl ([]-unique id-comm-sym id-comm-sym))) ⟩
(ψ +₁ idC) ∘ ((η _ ⁂ idC +₁ η _ ⁂ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h) ≈⟨ pullˡ (pullˡ +₁∘+₁) ⟩
((ψ ∘ (η _ ⁂ idC) +₁ idC ∘ (η _ ⁂ idC)) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h) ≈⟨ assoc ○ (+₁-cong₂ (pullʳ σ-η) identityˡ) ⟩∘⟨refl ⟩
(extend (τ _) ∘ η _ +₁ η _ ⁂ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ (+₁-cong₂ kleisliK.identityʳ refl) ⟩∘⟨refl ⟩
(τ _ +₁ (η _ ⁂ idC)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ sym (pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ)) ⟩
(idC +₁ (η _ ⁂ idC)) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ∎
pres₁ˡ : ∀ {U} (g : U ⇒ K.₀ X + U) → (ψ ∘ (idC ⁂ h #)) ∘ (g # ⁂ idC) ≈ ((ψ ∘ (idC ⁂ h #) +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #
pres₁ˡ {U} g = begin
(ψ ∘ (idC ⁂ h #)) ∘ (g # ⁂ idC) ≈⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ id-comm-sym id-comm ○ sym ⁂∘⁂) ⟩
ψ ∘ (g # ⁂ idC) ∘ (idC ⁂ h #) ≈⟨ pullˡ (pullʳ (σ-comm g)) ⟩
(extend (τ _) ∘ ((σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) ∘ (idC ⁂ h #) ≈⟨ extend-preserve (τ (X , Y)) _ ⟩∘⟨refl ⟩
((extend (τ _) +₁ idC) ∘ (σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) # ∘ (idC ⁂ h #) ≈⟨ sym (#-Uniformity (algebras _) (sym by-uni)) ⟩
((ψ ∘ (idC ⁂ h #) +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))# ∎
where
by-uni : ((extend (τ _) +₁ idC) ∘ (σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) ∘ (idC ⁂ h #) ≈ (idC +₁ (idC ⁂ h #)) ∘ ((ψ ∘ (idC ⁂ h #)) +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)
by-uni = begin
((extend (τ _) +₁ idC) ∘ (σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) ∘ (idC ⁂ h #) ≈⟨ pullʳ (pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ id-comm id-comm-sym ○ sym ⁂∘⁂))) ⟩
(extend (τ _) +₁ idC) ∘ (σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (idC ⁂ (h #)) ∘ (g ⁂ idC) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym (distributeʳ⁻¹-natural _ _ _ ○ refl⟩∘⟨ ⁂-cong₂ ([]-unique id-comm-sym id-comm-sym) refl)) ⟩
(extend (τ _) +₁ idC) ∘ (σ _ +₁ idC) ∘ ((idC ⁂ h # +₁ idC ⁂ h #) ∘ distributeʳ⁻¹) ∘ (g ⁂ idC) ≈⟨ pullˡ +₁∘+₁ ○ pullˡ (pullˡ +₁∘+₁) ⟩
((ψ ∘ (idC ⁂ h #) +₁ (idC ∘ idC) ∘ (idC ⁂ h #)) ∘ distributeʳ⁻¹) ∘ (g ⁂ idC) ≈⟨ assoc ○ (+₁-cong₂ refl (elimˡ identity²)) ⟩∘⟨refl ⟩
(ψ ∘ (idC ⁂ h #) +₁ (idC ⁂ h #)) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟩
(idC +₁ (idC ⁂ h #)) ∘ ((ψ ∘ (idC ⁂ h #)) +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) ∎
pres₂ˡ : ∀ {U} (g : U ⇒ K.₀ X + U) → ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∘ (g # ⁂ idC) ≈ ((((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#
pres₂ˡ {U} g = begin
((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ (g # ⁂ idC) ≈⟨ στ ⟩
extend ψ ∘ extend (σ _) ∘ τ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ ((η _ +₁ idC) ∘ h) #) ≈⟨ refl⟩∘⟨ (sym (comm-helper g h)) ⟩
extend ψ ∘ extend (τ _) ∘ σ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ ((η _ +₁ idC) ∘ h) #) ≈⟨ sym τσ ⟩
((((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))# ∎
where
τσ : ((((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))# ≈ extend ψ ∘ extend (τ _) ∘ σ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ ((η _ +₁ idC) ∘ h) #)
τσ = begin
(((((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#) ≈˘⟨ #-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ kleisliK.identityʳ identity²)) ⟩
((extend (((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #) +₁ idC) ∘ (η _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) # ≈˘⟨ extend-preserve (((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #) ((η _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) ⟩
extend (((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #) ∘ ((η _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) # ≈⟨ refl⟩∘⟨ (#-resp-≈ (algebras _) ((+₁-cong₂ (sym σ-η) refl) ⟩∘⟨refl)) ⟩
extend (((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #) ∘ ((σ _ ∘ (η _ ⁂ idC) +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) # ≈˘⟨ refl⟩∘⟨ (σ-comm _ ○ #-resp-≈ (algebras _) helper) ⟩
extend (((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #) ∘ σ _ ∘ (((η _ +₁ idC) ∘ g)# ⁂ idC) ≈˘⟨ (kleisliK.extend-≈ (#-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ kleisliK.identityʳ identity²)))) ⟩∘⟨refl ⟩
extend ((((extend ψ +₁ idC) ∘ (η _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#)) ∘ σ _ ∘ (((η _ +₁ idC) ∘ g)# ⁂ idC) ≈˘⟨ (kleisliK.extend-≈ (extend-preserve ψ _)) ⟩∘⟨refl ⟩
extend (extend ψ ∘ (((η _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#)) ∘ σ _ ∘ (((η _ +₁ idC) ∘ g)# ⁂ idC) ≈˘⟨ pullˡ kleisliK.sym-assoc ⟩
extend ψ ∘ extend (((η _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#) ∘ σ _ ∘ (((η _ +₁ idC) ∘ g)# ⁂ idC) ≈˘⟨ refl⟩∘⟨ ((kleisliK.extend-≈ (#-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (sym (distributeˡ⁻¹-natural idC _ idC)))) ○ #-resp-≈ (algebras _) (pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ (τ-η _) (elimʳ (⟨⟩-unique id-comm id-comm)))) ○ assoc))) ⟩∘⟨refl) ⟩
extend ψ ∘ extend (((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (η _ +₁ idC)) ∘ (idC ⁂ h)) #) ∘ σ _ ∘ (((η _ +₁ idC) ∘ g)# ⁂ idC) ≈⟨ refl⟩∘⟨ (kleisliK.extend-≈ (#-resp-≈ (algebras _) (refl⟩∘⟨ (refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identity² refl))))) ⟩∘⟨refl ⟩
extend ψ ∘ extend (((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (η _ +₁ idC) ∘ h)) #) ∘ σ _ ∘ (((η _ +₁ idC) ∘ g)# ⁂ idC) ≈˘⟨ refl⟩∘⟨ ((kleisliK.extend-≈ (τ-comm _)) ⟩∘⟨refl) ⟩
extend ψ ∘ extend (τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #)) ∘ σ _ ∘ (((η _ +₁ idC) ∘ g)# ⁂ idC) ≈˘⟨ refl⟩∘⟨ (pullˡ (extend∘F₁ monadK (τ _) _)) ⟩
extend ψ ∘ extend (τ _) ∘ K.₁ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ∘ σ _ ∘ (((η _ +₁ idC) ∘ g)# ⁂ idC) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym (σ-natural idC (((η (K.₀ Y) +₁ idC) ∘ h) #))) ⟩
extend ψ ∘ extend (τ _) ∘ (σ _ ∘ (K.₁ idC ⁂ ((η _ +₁ idC) ∘ h) #)) ∘ (((η _ +₁ idC) ∘ g)# ⁂ idC) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (assoc ○ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ (elimˡ monadK.F.identity) identityʳ)) ⟩
extend ψ ∘ extend (τ _) ∘ σ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ ((η _ +₁ idC) ∘ h) #) ∎
where
helper : (σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (((η _ +₁ idC) ∘ g ⁂ idC)) ≈ (σ _ ∘ (η _ ⁂ idC) +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)
helper = sym (begin
(σ _ ∘ (η _ ⁂ idC) +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²) ⟩
(σ _ +₁ idC) ∘ ((η _ ⁂ idC) +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) ≈⟨ refl⟩∘⟨ (pullˡ ((+₁-cong₂ refl (sym (⟨⟩-unique id-comm id-comm))) ⟩∘⟨refl ○ distributeʳ⁻¹-natural idC (η (K.₀ X)) idC)) ⟩
(σ _ +₁ idC) ∘ (distributeʳ⁻¹ ∘ ((η _ +₁ idC) ⁂ idC)) ∘ (g ⁂ idC) ≈⟨ refl⟩∘⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ refl identity²) ⟩
(σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (((η _ +₁ idC) ∘ g ⁂ idC)) ∎)
στ : ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ (g # ⁂ idC) ≈ extend ψ ∘ extend (σ _) ∘ τ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ ((η _ +₁ idC) ∘ h) #)
στ = begin
((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ (g # ⁂ idC) ≈⟨ sym (#-Uniformity (algebras (X × Y)) (sym by-uni)) ⟩
((ψ ∘ ((g #) ⁂ idC) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) ((+₁-cong₂ (ψ-left-iter g) refl) ⟩∘⟨refl) ⟩
(((((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) # +₁ idC)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈˘⟨ #-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ kleisliK.identityʳ identity²)) ⟩
((extend (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) +₁ idC) ∘ (η _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈˘⟨ extend-preserve (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) ((η (U × K.₀ Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ⟩
extend (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) ∘ ((η _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ refl⟩∘⟨ (#-resp-≈ (algebras _) ((+₁-cong₂ (sym (τ-η _)) refl) ⟩∘⟨refl)) ⟩
extend (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) ∘ ((τ _ ∘ (idC ⁂ η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈˘⟨ refl⟩∘⟨ (τ-comm ((η (K.₀ Y) +₁ idC) ∘ h) ○ #-resp-≈ (algebras _) helper) ⟩
extend (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h)#) ≈˘⟨ (kleisliK.extend-≈ (#-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ kleisliK.identityʳ identity²)))) ⟩∘⟨refl ⟩
extend ((((extend ψ +₁ idC) ∘ (η _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#)) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ (kleisliK.extend-≈ (extend-preserve ψ ((η (K.₀ X × K.₀ Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)))) ⟩∘⟨refl ⟩
extend (extend ψ ∘ (((η _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#)) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ pullˡ kleisliK.sym-assoc ⟩
extend ψ ∘ extend (((η _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ refl⟩∘⟨ ((kleisliK.extend-≈ (#-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (sym (distributeʳ⁻¹-natural idC (η (K.₀ X)) idC)))) ○ #-resp-≈ (algebras _) (pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ σ-η (elimʳ (⟨⟩-unique id-comm id-comm)))) ○ assoc))) ⟩∘⟨refl) ⟩
extend ψ ∘ extend (((σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ ((η (K.₀ X) +₁ idC) ⁂ idC) ∘ (g ⁂ idC)) #) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈⟨ refl⟩∘⟨ (kleisliK.extend-≈ (#-resp-≈ (algebras _) (refl⟩∘⟨ (refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identity²))))) ⟩∘⟨refl ⟩
extend ψ ∘ extend (((σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ ((η (K.₀ X) +₁ idC) ∘ g ⁂ idC)) #) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ refl⟩∘⟨ ((kleisliK.extend-≈ (σ-comm ((η (K.₀ X) +₁ idC) ∘ g))) ⟩∘⟨refl) ⟩
extend ψ ∘ extend (σ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ idC)) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ refl⟩∘⟨ (pullˡ (extend∘F₁ monadK (σ _) (((η _ +₁ idC) ∘ g) # ⁂ idC))) ⟩
extend ψ ∘ extend (σ _) ∘ K.₁ (((η _ +₁ idC) ∘ g) # ⁂ idC) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym (strengthen.commute (((η (K.₀ X) +₁ idC) ∘ g) # , idC))) ⟩
extend ψ ∘ extend (σ _) ∘ (τ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ K.₁ idC)) ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (assoc ○ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identityʳ (elimˡ monadK.F.identity))) ⟩
extend ψ ∘ extend (σ _) ∘ τ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ ((η _ +₁ idC) ∘ h) #) ∎
where
by-uni : ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ ((g #) ⁂ idC) ≈ (idC +₁ (g #) ⁂ idC) ∘ (ψ ∘ ((g #) ⁂ idC) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)
by-uni = begin
((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ ((g #) ⁂ idC) ≈⟨ pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ id-comm-sym id-comm ○ sym ⁂∘⁂)) ⟩
(ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ ((g #) ⁂ idC) ∘ (idC ⁂ h) ≈˘⟨ refl⟩∘⟨ ((distributeˡ⁻¹-natural (g #) idC idC ○ refl⟩∘⟨ ⁂-cong₂ refl ([]-unique id-comm-sym id-comm-sym)) ⟩∘⟨refl ○ assoc) ⟩
(ψ +₁ idC) ∘ ((((g #) ⁂ idC) +₁ ((g #) ⁂ idC)) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h) ≈⟨ pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ (sym identityˡ) id-comm-sym ○ sym +₁∘+₁)) ⟩
(((idC +₁ (g #) ⁂ idC) ∘ (ψ ∘ ((g #) ⁂ idC) +₁ idC)) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h) ≈⟨ assoc² ⟩
(idC +₁ (g #) ⁂ idC) ∘ (ψ ∘ ((g #) ⁂ idC) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ∎
helper : (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (η _ +₁ idC) ∘ h) ≈ (τ _ ∘ (idC ⁂ η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)
helper = sym (begin
(τ _ ∘ (idC ⁂ η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²) ⟩
(τ _ +₁ idC) ∘ ((idC ⁂ η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ (pullˡ ((+₁-cong₂ refl (sym (⟨⟩-unique id-comm id-comm))) ⟩∘⟨refl ○ distributeˡ⁻¹-natural idC (η (K.₀ Y)) idC)) ⟩
(τ _ +₁ idC) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ (η _ +₁ idC))) ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² refl) ⟩
(τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (η _ +₁ idC) ∘ h) ∎)