{-# OPTIONS --lossy-unification #-}
open import Categories.Category.Core
open import Categories.Category.Distributive
open import Categories.Category.Restriction
open import Categories.Object.Terminal
open import Relation.Binary.Bundles using (Poset)
open import Monad.Helper
open import Data.Product using (_,_)
open import Algebra.Elgot
open import Category.Construction.ElgotAlgebras
open import Categories.FreeObjects.Free
open import Categories.Object.NaturalNumbers
open import Categories.Object.NaturalNumbers.Parametrized
open import Categories.Category.Construction.F-Algebras
import Categories.Morphism as M
import Categories.Morphism.Reasoning as MR
import Categories.Morphism.Properties as MP
import Monad.Instance.K as MIK
module Monad.Instance.K.Kleene {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) (MK : MIK.MonadK distributive) where
open import Category.Distributive.Helper distributive renaming (η to η-prod)
open Bundles
open MIK distributive
open MonadK MK
open Category C
open Equiv
open HomReasoning
open M C
open MR C
open MP C
open kleisliK using (extend; extend-≈)
open monadK using (μ)
open import Monad.Instance.K.Strong distributive MK
open import Monad.Instance.K.Commutative distributive MK
open import Monad.Instance.K.EquationalLifting distributive MK
open import Monad.Instance.K.Restriction distributive MK
open import Monad.Instance.K.OrderEnriched distributive MK
open Restriction KRestriction renaming (_↓ to _↓'; ↓-denestʳ to ↓-denestʳ'; ↓-cong to ↓-cong'; pidʳ to pidʳ'; ↓-comm to ↓-comm'; ↓-skew-comm to ↓-skew-comm')
open import Categories.Category.Restriction.Properties.Poset KRestriction
open import Categories.Category.Restriction.Properties KRestriction renaming (↓-idempotent to ↓-idempotent')
open import Categories.Object.NaturalNumbers.Parametrized.Properties.F-Algebras C cartesian coproducts
open import Categories.Monad.Commutative.Properties
open CommutativeProperties braided KCommutativeMonad
module BoundedIteration (PNNO : ParametrizedNNO C cartesian) where
private
module pnno = ParametrizedNNO PNNO
module nno = NNO (PNNO⇒NNO C cartesian PNNO)
open pnno using (universal; z; s; N)
open nno using () renaming (universal to nno-universal)
open monadK using (η; μ)
open kleisliK using (extend)
nno-iso : N ≅ ⊤ + N
nno-iso = Lambek.lambek (PNNO⇒Initial₁ PNNO)
pnno-iso : ∀ {X} → X × N ≅ X + X × N
pnno-iso {X} = Lambek.lambek (record { ⊥ = PNNO-Algebra X N z s ; ⊥-is-initial = PNNO⇒Initial₂ PNNO X })
1+n : N ⇒ ⊤ + N
1+n = M._≅_.from nno-iso
N-out : N ⇒ ⊤ + N
N-out = nno.universal i₁ (i₂ ∘ [ z , s ])
coherence : 1+n ≈ N-out
coherence = nno.unique IB IS
where
IB : i₁ ≈ 1+n ∘ z
IB = begin
i₁ ≈˘⟨ identityʳ ⟩
i₁ ∘ id ≈˘⟨ inject₁ ⟩
(id +₁ _) ∘ i₁ ≈⟨ nno.z-commute ⟩
1+n ∘ z ∎
IS : (i₂ ∘ [ z , s ]) ∘ 1+n ≈ 1+n ∘ s
IS = begin
(i₂ ∘ [ z , s ]) ∘ 1+n ≈˘⟨ inject₂ ⟩∘⟨refl ⟩
((id +₁ [ z , s ]) ∘ i₂) ∘ 1+n ≈⟨ nno.s-commute ⟩
1+n ∘ s ∎
N-out-zero : N-out ∘ z ≈ i₁
N-out-zero = sym nno.z-commute
N-out-succ : N-out ∘ s ≈ i₂
N-out-succ = begin
N-out ∘ s ≈˘⟨ nno.s-commute ⟩
(i₂ ∘ [ z , s ]) ∘ N-out ≈⟨ cancelʳ (∘-resp-≈ʳ (sym coherence) ○ _≅_.isoˡ nno-iso) ⟩
i₂ ∎
_#⟩ : ∀ {X A : Obj} → (X ⇒ K.₀ A + X) → X × N ⇒ K.₀ A
_#⟩ {X} {A} f = [ id , bot ] ∘ f ∘ universal id ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩)
PNNO-jointly-epic : ∀ {X Y} {f g : X × N ⇒ Y} → (f ∘ ⟨ id , z ∘ ! ⟩ ≈ g ∘ ⟨ id , z ∘ ! ⟩) → (f ∘ (id ×₁ s) ≈ g ∘ (id ×₁ s)) → f ≈ g
PNNO-jointly-epic {X} {Y} {f} {g} IB IS = begin
f ≈⟨ introʳ (M._≅_.isoˡ pnno-iso) ⟩
f ∘ [ ⟨ id , z ∘ ! ⟩ , (id ×₁ s) ] ∘ M._≅_.from pnno-iso ≈⟨ pullˡ ∘[] ⟩
[ f ∘ ⟨ id , z ∘ ! ⟩ , f ∘ (id ×₁ s) ] ∘ M._≅_.from pnno-iso ≈⟨ ([]-cong₂ IB IS) ⟩∘⟨refl ⟩
[ g ∘ ⟨ id , z ∘ ! ⟩ , g ∘ (id ×₁ s) ] ∘ M._≅_.from pnno-iso ≈˘⟨ pullˡ ∘[] ⟩
g ∘ [ ⟨ id , z ∘ ! ⟩ , (id ×₁ s) ] ∘ M._≅_.from pnno-iso ≈⟨ elimʳ (M._≅_.isoˡ pnno-iso) ⟩
g ∎
kleene₁ : ∀ {X Y} (f : X ⇒ K.₀ Y + X) → f #⟩ ⊑ (f # ∘ π₁)
kleene₁ {X} {Y} f = begin
f #⟩ ≈⟨ helper₁ ⟩
((f # ∘ h) ⇂ (f #⟩)) ≈⟨ ⇂-cong₂ helper₂ refl ⟩
(f # ∘ π₁) ⇂ (f #⟩) ∎
where
h : X × N ⇒ X
h = universal id ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩)
helper₁ : f #⟩ ⊑ (f # ∘ h)
helper₁ = begin
(f #⟩) ≈⟨ sym-assoc ⟩
([ id , bot ] ∘ f) ∘ h ≈⟨ ⊑∘ˡ single-iter ⟩
((f # ∘ h) ⇂ (([ id , bot ] ∘ f) ∘ h)) ≈⟨ ⇂-cong₂ refl assoc ⟩
(((f #) ∘ h) ⇂ (f #⟩)) ∎
where
single-iter : ([ id , bot ] ∘ f) ⊑ (f #)
single-iter = begin
[ id , bot ] ∘ f ≈˘⟨ []-cong₂ (extend∘F₁ monadK π₁ ⟨ η.η _ , id ⟩ ○ extend-≈ project₁ ○ kleisliK.identityˡ) (bot-restrict (f #)) ⟩∘⟨refl ⟩
[ extend π₁ ∘ K.₁ ⟨ η.η _ , id ⟩ , extend π₁ ∘ τ _ ∘ ⟨ f # , bot ⟩ ] ∘ f ≈˘⟨ ([]-cong₂ (∘-resp-≈ʳ equationalLifting) refl) ⟩∘⟨refl ⟩
[ extend π₁ ∘ τ _ ∘ Δ , extend π₁ ∘ τ _ ∘ ⟨ f # , bot ⟩ ] ∘ f ≈˘⟨ pullˡ ∘[] ⟩
extend π₁ ∘ [ τ _ ∘ Δ , τ _ ∘ ⟨ f # , bot ⟩ ] ∘ f ≈˘⟨ refl⟩∘⟨ pullˡ ∘[] ⟩
extend π₁ ∘ τ _ ∘ [ Δ , ⟨ f # , bot ⟩ ] ∘ f ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ([⟨⟩]≈⟨[]⟩ id id (f #) bot) ⟩∘⟨refl ⟩
extend π₁ ∘ τ _ ∘ ⟨ [ id , f # ] , [ id , bot ] ⟩ ∘ f ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩∘ ⟩
extend π₁ ∘ τ _ ∘ ⟨ [ id , f # ] ∘ f , [ id , bot ] ∘ f ⟩ ≈˘⟨ refl⟩∘⟨ (refl⟩∘⟨ (⟨⟩-cong₂ (#-Fixpoint (algebras _)) refl)) ⟩
extend π₁ ∘ τ _ ∘ ⟨ f # , [ id , bot ] ∘ f ⟩ ∎
helper₂ : f # ∘ h ≈ f # ∘ π₁
helper₂ = begin
f # ∘ h ≈˘⟨ pullˡ kleisliK.identityʳ ⟩
extend (f #) ∘ η.η _ ∘ h ≈⟨ refl⟩∘⟨ pnno.unique (sym IB₁) (sym IS₁) ⟩
extend (f #) ∘ universal (η.η _) (K.₁ f') ≈˘⟨ refl⟩∘⟨ (pnno.unique (sym (Step.IB₂ f')) (sym (Step.IS₂ f'))) ⟩
extend (f #) ∘ ((η.η X ∘ π₁ +₁ f' ×₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ N-out)) # ≈⟨ extend-preserve (f #) ((η.η _ ∘ π₁ +₁ f' ×₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ N-out)) ⟩
((extend (f #) +₁ id) ∘ (η.η _ ∘ π₁ +₁ f' ×₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ N-out)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ (pullˡ kleisliK.identityʳ) identityˡ)) ⟩
((f # ∘ π₁ +₁ f' ×₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ N-out)) # ≈⟨ #-Uniformity (algebras _) (sym uni-step) ⟩
((π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ N-out)) # ∘ (f # ×₁ id) ≈˘⟨ (#-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ (cancelˡ monadK.identityʳ) identity²))) ⟩∘⟨refl ⟩
((μ.η _ +₁ id) ∘ (η.η _ ∘ π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ N-out)) # ∘ (f # ×₁ id) ≈˘⟨ pullˡ (μ-preserve _) ⟩
μ.η _ ∘ ((η.η _ ∘ π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ N-out)) # ∘ (f # ×₁ id) ≈˘⟨ refl⟩∘⟨ (#-resp-≈ (algebras _) (∘-resp-≈ˡ (+₁-cong₂ refl (⟨⟩-unique id-comm id-comm))) ⟩∘⟨refl) ⟩
μ.η _ ∘ ((η.η (K.₀ Y) ∘ π₁ +₁ (id ×₁ id)) ∘ distributeˡ⁻¹ ∘ (id ×₁ N-out)) # ∘ (f # ×₁ id) ≈⟨ refl⟩∘⟨ ((pnno.unique (sym (Step.IB₂ id)) (sym (Step.IS₂ id))) ⟩∘⟨refl) ⟩
μ.η Y ∘ universal (η.η (K.₀ Y)) (K.₁ (id {K.₀ Y})) ∘ (f # ×₁ id) ≈⟨ refl⟩∘⟨ (pnno.unique pnno.commute₁ (∘-resp-≈ˡ (sym K.identity) ○ pnno.commute₂) ⟩∘⟨refl) ⟩
μ.η Y ∘ universal (η.η (K.₀ Y)) (id {K.₀ (K.₀ Y)}) ∘ (f # ×₁ id) ≈˘⟨ refl⟩∘⟨ pullˡ (pnno.unique (sym η-IB₁) (sym η-IS₁)) ⟩
μ.η _ ∘ η.η _ ∘ π₁ ∘ (f # ×₁ id) ≈⟨ cancelˡ monadK.identityʳ ⟩
π₁ {K.₀ Y} {N} ∘ (f # ×₁ id) ≈⟨ project₁ ⟩
f # ∘ π₁ ∎
where
f' = [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩
f'-fixpoint : f # ≈ f # ∘ f'
f'-fixpoint = begin
(f #) ≈⟨ #-Fixpoint (algebras _) ⟩
[ id , f # ] ∘ f ≈˘⟨ sym-assoc ○ pullˡ (assoc ○ sym ([]-unique case-i₁ case-i₂)) ⟩
[ π₁ , f # ∘ π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ [ id , f # ] , id ⟩ ∘ f ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ refl identityˡ) ⟩
[ π₁ , f # ∘ π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ [ id , f # ] ∘ f , f ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ (#-Fixpoint (algebras _)) refl ⟩
[ π₁ , f # ∘ π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ f # , f ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ (elimˡ ([]-unique id-comm-sym id-comm-sym))) ⟩
[ π₁ , f # ∘ π₂ ] ∘ distributeˡ⁻¹ ∘ (f # ×₁ (id +₁ id)) ∘ ⟨ id , f ⟩ ≈˘⟨ refl⟩∘⟨ (extendʳ (distributeˡ⁻¹-natural (f #) id id)) ⟩
[ π₁ , f # ∘ π₂ ] ∘ ((f # ×₁ id) +₁ (f # ×₁ id)) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ≈⟨ pullˡ ([]∘+₁ ○ []-cong₂ project₁ (pullʳ (project₂ ○ identityˡ))) ⟩
[ f # ∘ π₁ , f # ∘ π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ≈˘⟨ pullˡ ∘[] ⟩
f # ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ∎
where
case-i₁ : ([ π₁ , f # ∘ π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ [ id , f # ] , id ⟩) ∘ i₁ ≈ id
case-i₁ = begin
([ π₁ , f # ∘ π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ [ id , f # ] , id ⟩) ∘ i₁ ≈⟨ pullʳ (pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ inject₁ id-comm-sym)) ⟩
[ π₁ , f # ∘ π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ id , i₁ ∘ id ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identity² refl) ⟩
[ π₁ , f # ∘ π₂ ] ∘ distributeˡ⁻¹ ∘ (id ×₁ i₁) ∘ Δ ≈⟨ refl⟩∘⟨ (pullˡ distributeˡ⁻¹-i₁) ⟩
[ π₁ , f # ∘ π₂ ] ∘ i₁ ∘ Δ ≈⟨ pullˡ inject₁ ⟩
π₁ ∘ Δ ≈⟨ project₁ ⟩
id ∎
case-i₂ : ([ π₁ , f # ∘ π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ [ id , f # ] , id ⟩) ∘ i₂ ≈ f #
case-i₂ = begin
([ π₁ , f # ∘ π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ [ id , f # ] , id ⟩) ∘ i₂ ≈⟨ pullʳ (pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ inject₂ id-comm-sym)) ⟩
[ π₁ , f # ∘ π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ f # , i₂ ∘ id ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl) ⟩
[ π₁ , f # ∘ π₂ ] ∘ distributeˡ⁻¹ ∘ (id ×₁ i₂) ∘ ⟨ f # , id ⟩ ≈⟨ refl⟩∘⟨ (pullˡ distributeˡ⁻¹-i₂) ⟩
[ π₁ , f # ∘ π₂ ] ∘ i₂ ∘ ⟨ f # , id ⟩ ≈⟨ extendʳ inject₂ ⟩
f # ∘ π₂ ∘ ⟨ f # , id ⟩ ≈⟨ elimʳ project₂ ⟩
f # ∎
η-helper : ∀ {Z} → η.η Z ≈ (i₁ ∘ η.η _) #
η-helper = sym (#-Fixpoint (algebras _) ○ cancelˡ inject₁)
uni-step : ((π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ N-out)) ∘ (f # ×₁ id) ≈ (id +₁ (f # ×₁ id)) ∘ (f # ∘ π₁ +₁ f' ×₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ N-out)
uni-step = begin
((π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ N-out)) ∘ (f # ×₁ id) ≈⟨ pullʳ (pullʳ (×₁∘×₁ ○ ×₁-cong₂ id-comm-sym id-comm ○ sym ×₁∘×₁)) ⟩
(π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (f # ×₁ id) ∘ (id ×₁ N-out) ≈˘⟨ refl⟩∘⟨ extendʳ distributeˡ⁻¹-natural-id ⟩
(π₁ +₁ id) ∘ (f # ×₁ id +₁ f # ×₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ N-out) ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ project₁ identityˡ) ⟩
(f # ∘ π₁ +₁ f # ×₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ N-out) ≈⟨ (+₁-cong₂ refl (×₁-cong₂ f'-fixpoint refl)) ⟩∘⟨refl ⟩
(f # ∘ π₁ +₁ f # ∘ f' ×₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ N-out) ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ (×₁∘×₁ ○ ×₁-cong₂ refl identity²)) ⟩
(id +₁ (f # ×₁ id)) ∘ (f # ∘ π₁ +₁ f' ×₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ N-out) ∎
η-IB₁ : (η.η _ ∘ π₁) ∘ ⟨ id , z ∘ ! ⟩ ≈ η.η _
η-IB₁ = cancelʳ project₁
η-IS₁ : (η.η _ ∘ π₁) ∘ (id ×₁ s) ≈ id ∘ η.η _ ∘ π₁
η-IS₁ = pullʳ (project₁ ○ identityˡ) ○ sym identityˡ
IB₁ : (η.η _ ∘ h) ∘ ⟨ id , z ∘ ! ⟩ ≈ η.η _
IB₁ = cancelʳ (sym pnno.commute₁)
IS₁ : (η.η _ ∘ h) ∘ (id ×₁ s) ≈ (K.₁ f') ∘ η.η _ ∘ h
IS₁ = begin
(η.η _ ∘ h) ∘ (id ×₁ s) ≈⟨ pullʳ (sym pnno.commute₂) ⟩
η.η _ ∘ f' ∘ h ≈⟨ extendʳ (η.commute f') ⟩
(K.₁ f') ∘ η.η _ ∘ h ∎
module Step {Z} (p : Z ⇒ Z) where
q = (η.η Z ∘ π₁ +₁ p ×₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ N-out)
IB₂ : ((η.η _ ∘ π₁ +₁ p ×₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ N-out)) # ∘ ⟨ id , z ∘ ! ⟩ ≈ η.η _
IB₂ = begin
((η.η _ ∘ π₁ +₁ p ×₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ N-out)) # ∘ ⟨ id , z ∘ ! ⟩ ≈˘⟨ #-Uniformity (algebras _) uni-helper ⟩
((i₁ ∘ η.η _) #) ≈˘⟨ η-helper ⟩
η.η _ ∎
where
uni-helper : (id +₁ ⟨ id , z ∘ ! ⟩) ∘ i₁ ∘ η.η _ ≈ ((η.η _ ∘ π₁ +₁ p ×₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ N-out)) ∘ ⟨ id , z ∘ ! ⟩
uni-helper = begin
(id +₁ ⟨ id , z ∘ ! ⟩) ∘ i₁ ∘ η.η _ ≈⟨ pullˡ (inject₁ ○ identityʳ) ⟩
i₁ ∘ η.η _ ≈˘⟨ refl⟩∘⟨ elimʳ project₁ ⟩
i₁ ∘ η.η _ ∘ π₁ ∘ ⟨ id , ! ⟩ ≈˘⟨ pullˡ inject₁ ○ assoc²βε ⟩
(η.η _ ∘ π₁ +₁ p ×₁ id) ∘ i₁ ∘ ⟨ id , ! ⟩ ≈˘⟨ refl⟩∘⟨ pullˡ distributeˡ⁻¹-i₁ ⟩
(η.η _ ∘ π₁ +₁ p ×₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ i₁) ∘ ⟨ id , ! ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identity² refl) ⟩
(η.η _ ∘ π₁ +₁ p ×₁ id) ∘ distributeˡ⁻¹ ∘ ⟨ id , i₁ ∘ ! ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ refl (pullˡ (sym nno.z-commute)) ⟩
(η.η _ ∘ π₁ +₁ p ×₁ id) ∘ distributeˡ⁻¹ ∘ ⟨ id , N-out ∘ z ∘ ! ⟩ ≈˘⟨ pullʳ (pullʳ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identity² refl)) ⟩
((η.η _ ∘ π₁ +₁ p ×₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ N-out)) ∘ ⟨ id , z ∘ ! ⟩ ∎
pq-helper : q # ∘ (p ×₁ id) ≈ K.₁ p ∘ q #
pq-helper = begin
q # ∘ (p ×₁ id) ≈˘⟨ #-Uniformity (algebras _) uni-helper ⟩
((K.₁ p +₁ id) ∘ q) # ≈˘⟨ K-preserve p q ⟩
K.₁ p ∘ q # ∎
where
uni-helper : (id +₁ (p ×₁ id)) ∘ (K.₁ p +₁ id) ∘ q ≈ q ∘ (p ×₁ id)
uni-helper = begin
(id +₁ (p ×₁ id)) ∘ (K.₁ p +₁ id) ∘ (η.η _ ∘ π₁ +₁ p ×₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ N-out) ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟩
(K.₁ p +₁ (p ×₁ id)) ∘ (η.η _ ∘ π₁ +₁ p ×₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ N-out) ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ refl (×₁∘×₁ ○ ×₁-cong₂ refl identity²)) ⟩
(K.₁ p ∘ η.η _ ∘ π₁ +₁ (p ∘ p ×₁ id)) ∘ distributeˡ⁻¹ ∘ (id ×₁ N-out) ≈˘⟨ (+₁-cong₂ (extendʳ (η.commute p)) refl) ⟩∘⟨refl ⟩
(η.η _ ∘ p ∘ π₁ +₁ (p ∘ p ×₁ id)) ∘ distributeˡ⁻¹ ∘ (id ×₁ N-out) ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ (pullʳ project₁) (×₁∘×₁ ○ ×₁-cong₂ refl identity²)) ⟩
(η.η _ ∘ π₁ +₁ p ×₁ id) ∘ (p ×₁ id +₁ p ×₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ N-out) ≈⟨ refl⟩∘⟨ (extendʳ (distributeˡ⁻¹-natural p id id ○ ∘-resp-≈ʳ (×₁-cong₂ refl ([]-unique id-comm-sym id-comm-sym)))) ⟩
(η.η _ ∘ π₁ +₁ p ×₁ id) ∘ distributeˡ⁻¹ ∘ (p ×₁ id) ∘ (id ×₁ N-out) ≈˘⟨ pullʳ (pullʳ (×₁∘×₁ ○ ×₁-cong₂ id-comm-sym id-comm ○ sym ×₁∘×₁)) ⟩
((η.η _ ∘ π₁ +₁ p ×₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ N-out)) ∘ (p ×₁ id) ∎
IS₂ : q # ∘ (id ×₁ s)
≈ K.₁ p ∘ q #
IS₂ = begin
q # ∘ (id ×₁ s) ≈⟨ (#-Fixpoint (algebras _)) ⟩∘⟨refl ⟩
([ id , q # ] ∘ q) ∘ (id ×₁ s) ≈⟨ (pullˡ ([]∘+₁ ○ []-cong₂ identityˡ refl)) ⟩∘⟨refl ⟩
([ η.η _ ∘ π₁ , q # ∘ (p ×₁ id) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ N-out)) ∘ (id ×₁ s) ≈⟨ (([]-cong₂ refl pq-helper) ⟩∘⟨refl) ⟩∘⟨refl ⟩
([ η.η _ ∘ π₁ , K.₁ p ∘ q # ] ∘ distributeˡ⁻¹ ∘ (id ×₁ N-out)) ∘ (id ×₁ s) ≈⟨ pullʳ (pullʳ (×₁∘×₁ ○ ×₁-cong₂ identity² N-out-succ)) ⟩
[ η.η _ ∘ π₁ , K.₁ p ∘ q # ] ∘ distributeˡ⁻¹ ∘ (id ×₁ i₂) ≈⟨ refl⟩∘⟨ distributeˡ⁻¹-i₂ ⟩
[ η.η _ ∘ π₁ , K.₁ p ∘ q # ] ∘ i₂ ≈⟨ inject₂ ⟩
K.₁ p ∘ q # ∎
kleene₂ : ∀ {X Y} (f : X ⇒ K.₀ Y + X) (g : X ⇒ K.₀ Y) → (f #⟩) ⊑ (g ∘ π₁) → (f #) ⊑ g
kleene₂ {X} {Y} f g leq = ⊑-trans (⊑-trans (⊑-cong₂ refl u-law ⊑-refl) leq₁) (⊑-trans (⊑-cong₂ refl eq₂ ⊑-refl) leq₂)
where
u : X × N ⇒ K.₀ N + (X × N)
u = (η.η _ ∘ π₂ +₁ (id ×₁ s)) ∘ distributeʳ⁻¹ ∘ (f ×₁ id)
leq₁ : (extend (f #⟩) ∘ τ (X , N) ∘ ⟨ id , u # ∘ ⟨ id , z ∘ ! ⟩ ⟩) ⊑ (extend (g ∘ π₁) ∘ τ (X , N) ∘ ⟨ id , u # ∘ ⟨ id , z ∘ ! ⟩ ⟩)
leq₁ = ⊑∘ˡ {f = extend (f #⟩)} {g = extend (g ∘ π₁)} (begin
extend (f #⟩) ≈⟨ extend-≈ leq ⟩
extend (extend π₁ ∘ τ _ ∘ ⟨ g ∘ π₁ , f #⟩ ⟩) ≈⟨ kleisliK.assoc ⟩
extend π₁ ∘ extend (τ _ ∘ ⟨ g ∘ π₁ , f #⟩ ⟩) ≈˘⟨ refl⟩∘⟨ (extend∘F₁ monadK (τ (K.₀ Y , Y) ∘ (id ×₁ (f #⟩))) ⟨ g ∘ π₁ , id ⟩ ○ extend-≈ (pullʳ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ identityʳ))) ⟩
extend π₁ ∘ extend (τ _ ∘ (id ×₁ (f #⟩))) ∘ K.₁ ⟨ g ∘ π₁ , id ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (sym K.homomorphism ○ K.F-resp-≈ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ kleisliK.identityʳ identity²)) ⟩
extend π₁ ∘ extend (τ _ ∘ (id ×₁ (f #⟩))) ∘ K.₁ (extend (g ∘ π₁) ×₁ id) ∘ K.₁ ⟨ η.η _ , id ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ equationalLifting ⟩
extend π₁ ∘ extend (τ _ ∘ (id ×₁ (f #⟩))) ∘ K.₁ (extend (g ∘ π₁) ×₁ id) ∘ τ _ ∘ Δ ≈˘⟨ refl⟩∘⟨ (pullʳ (assoc ○ extendʳ (τ-comm-id (extend (g ∘ π₁))))) ⟩
extend π₁ ∘ (extend (τ _ ∘ (id ×₁ (f #⟩))) ∘ τ _ ∘ (extend (g ∘ π₁) ×₁ id)) ∘ Δ ≈˘⟨ refl⟩∘⟨ (pullˡ (sym (τ-kleisli-assoc _ _))) ⟩
extend π₁ ∘ τ _ ∘ (extend (g ∘ π₁) ×₁ extend (f #⟩)) ∘ Δ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ×₁∘Δ ⟩
extend π₁ ∘ τ _ ∘ ⟨ extend (g ∘ π₁) , extend (f #⟩) ⟩ ∎)
u-law : f # ≈ extend (f #⟩) ∘ τ _ ∘ ⟨ id , u # ∘ ⟨ id , z ∘ ! ⟩ ⟩
u-law = begin
f # ≈⟨ u-step₂ ⟩
((extend (f #⟩) ∘ τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ u))# ∘ ⟨ id , ⟨ id , z ∘ ! ⟩ ⟩ ≈˘⟨ u-step₁ ⟩
extend (f #⟩) ∘ τ _ ∘ ⟨ id , u # ∘ ⟨ id , z ∘ ! ⟩ ⟩ ∎
where
u-step₁ : (extend (f #⟩) ∘ τ _ ∘ ⟨ id , u # ∘ ⟨ id , z ∘ ! ⟩ ⟩) ≈ ((extend (f #⟩) ∘ τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ u))# ∘ ⟨ id , ⟨ id , z ∘ ! ⟩ ⟩
u-step₁ = begin
(extend (f #⟩) ∘ τ _ ∘ ⟨ id , u # ∘ ⟨ id , z ∘ ! ⟩ ⟩) ≈˘⟨ refl⟩∘⟨ (refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl)) ⟩
extend (f #⟩) ∘ τ _ ∘ (id ×₁ u #) ∘ ⟨ id , ⟨ id , z ∘ ! ⟩ ⟩ ≈⟨ refl⟩∘⟨ (pullˡ (τ-comm u)) ⟩
extend (f #⟩) ∘ ((τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ u)) # ∘ ⟨ id , ⟨ id , z ∘ ! ⟩ ⟩ ≈⟨ pullˡ (extend-preserve _ _ ○ #-resp-≈ (algebras Y) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²))) ⟩
((extend (f #⟩) ∘ τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ u))# ∘ ⟨ id , ⟨ id , z ∘ ! ⟩ ⟩ ∎
u-step₂ : f # ≈ ((extend (f #⟩) ∘ τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ u))# ∘ ⟨ id , ⟨ id , z ∘ ! ⟩ ⟩
u-step₂ = begin
f # ≈˘⟨ elimʳ (sym pnno.commute₁) ⟩
f # ∘ h ∘ ⟨ id , z ∘ ! ⟩ ≈⟨ extendʳ (sym strengthened) ⟩
((extend (f #⟩) ∘ τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ u))# ∘ ⟨ π₁ , ⟨ h , π₂ ⟩ ⟩ ∘ ⟨ id , z ∘ ! ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ project₁ (⟨⟩∘ ○ ⟨⟩-cong₂ (sym pnno.commute₁) project₂)) ⟩
((extend (f #⟩) ∘ τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ u))# ∘ ⟨ id , ⟨ id , z ∘ ! ⟩ ⟩ ∎
where
f' : X ⇒ X
f' = [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩
h : X × N ⇒ X
h = universal id f'
h-succ : h ∘ (id ×₁ s) ≈ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ h , f ∘ h ⟩
h-succ = begin
h ∘ (id ×₁ s) ≈˘⟨ pnno.commute₂ ⟩
([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩) ∘ h ≈⟨ pullʳ (pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ refl)) ⟩
[ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ h , f ∘ h ⟩ ∎
#⟩-succ : f #⟩ ∘ (id ×₁ s) ≈ [ id , bot ] ∘ f ∘ f' ∘ h
#⟩-succ = begin
([ id , bot ] ∘ f ∘ universal id ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩)) ∘ (id ×₁ s) ≈⟨ pullʳ (pullʳ (sym pnno.commute₂)) ⟩
[ id , bot ] ∘ f ∘ f' ∘ h ∎
strengthened : ((extend (f #⟩) ∘ τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ u)) # ∘ ⟨ π₁ , ⟨ h , π₂ ⟩ ⟩ ≈ f # ∘ h
strengthened = begin
((extend (f #⟩) ∘ τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ u)) # ∘ ⟨ π₁ , ⟨ h , π₂ ⟩ ⟩ ≈˘⟨ #-Uniformity (algebras _) (sym uni-helper₁) ⟩
((π₂ +₁ π₁) ∘ distributeˡ⁻¹ ∘ ⟨ id ×₁ s , f ∘ h ⟩) # ≈⟨ #-Uniformity (algebras _) (sym uni-helper₂) ⟩
f # ∘ h ∎
where
helper-dual : ∀ {A B D} (w : A ⇒ B + D) → (id +₁ ⟨ id , i₂ ∘ π₂ ⟩) ∘ distributeˡ⁻¹ ∘ ⟨ id , w ⟩ ≈ (id +₁ ⟨ id , w ∘ π₁ ⟩) ∘ distributeˡ⁻¹ ∘ ⟨ id , w ⟩
helper-dual w = begin
(id +₁ ⟨ id , i₂ ∘ π₂ ⟩) ∘ distributeˡ⁻¹ ∘ ⟨ id , w ⟩ ≈˘⟨ (+₁-cong₂ ×₁-η (⟨⟩-cong₂ ×₁-η refl)) ⟩∘⟨refl ⟩
(⟨ π₁ , π₂ ⟩ +₁ ⟨ ⟨ π₁ , π₂ ⟩ , i₂ ∘ π₂ ⟩) ∘ distributeˡ⁻¹ ∘ ⟨ id , w ⟩ ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ (project₁ ○ identityˡ) identityˡ) (⟨⟩∘ ○ ⟨⟩-cong₂ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ (project₁ ○ identityˡ) identityˡ) (pullʳ project₁ ○ project₂))) ⟩
(π₁ ×₁ id +₁ p) ∘ (⟨ id ×₁ i₁ , π₂ ⟩ +₁ ⟨ id ×₁ i₂ , π₂ ⟩) ∘ distributeˡ⁻¹ ∘ ⟨ id , w ⟩ ≈⟨ refl⟩∘⟨ extendʳ dist-step ⟩
(π₁ ×₁ id +₁ p) ∘ distributeˡ⁻¹ ∘ ⟨ id , π₂ ⟩ ∘ ⟨ id , w ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ project₂) ⟩
(π₁ ×₁ id +₁ p) ∘ distributeˡ⁻¹ ∘ ⟨ ⟨ id , w ⟩ , w ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ (cancelʳ project₁) ((pullʳ project₂) ○ identityˡ)) ⟩
(π₁ ×₁ id +₁ p) ∘ distributeˡ⁻¹ ∘ (⟨ id , w ⟩ ×₁ id) ∘ ⟨ id , w ⟩ ≈˘⟨ refl⟩∘⟨ (extendʳ distributeˡ⁻¹-natural-id) ⟩
(π₁ ×₁ id +₁ p) ∘ (⟨ id , w ⟩ ×₁ id +₁ ⟨ id , w ⟩ ×₁ id) ∘ distributeˡ⁻¹ ∘ ⟨ id , w ⟩ ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ (×₁∘×₁ ○ (×₁-cong₂ project₁ identity²) ○ ⟨⟩-unique id-comm id-comm) (⟨⟩∘ ○ ⟨⟩-cong₂ ((×₁∘×₁ ○ ×₁-cong₂ project₁ identity²) ○ ⟨⟩-unique id-comm id-comm) (pullʳ project₁ ○ pullˡ project₂))) ⟩
(id +₁ ⟨ id , w ∘ π₁ ⟩) ∘ distributeˡ⁻¹ ∘ ⟨ id , w ⟩ ∎
where
p = ⟨ π₁ ×₁ id , π₂ ∘ π₁ ⟩
dist-step : (⟨ id ×₁ i₁ , π₂ ⟩ +₁ ⟨ id ×₁ i₂ , π₂ ⟩) ∘ distributeˡ⁻¹ ≈ distributeˡ⁻¹ ∘ ⟨ id , π₂ ⟩
dist-step = Iso⇒Mono (IsIso.iso isIsoˡ) _ _ (begin
distributeˡ ∘ (⟨ id ×₁ i₁ , π₂ ⟩ +₁ ⟨ id ×₁ i₂ , π₂ ⟩) ∘ distributeˡ⁻¹ ≈⟨ pullˡ ([]∘+₁ ○ []-cong₂ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl) (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl)) ⟩
[ ⟨ id ×₁ i₁ , i₁ ∘ π₂ ⟩ , ⟨ id ×₁ i₂ , i₂ ∘ π₂ ⟩ ] ∘ distributeˡ⁻¹ ≈⟨ ([⟨⟩]≈⟨[]⟩ _ _ _ _) ⟩∘⟨refl ⟩
⟨ distributeˡ , (π₂ +₁ π₂) ⟩ ∘ distributeˡ⁻¹ ≈⟨ ⟨⟩∘ ○ ⟨⟩-cong₂ (IsIso.isoʳ isIsoˡ) distributeˡ⁻¹-π₂ ⟩
⟨ id , π₂ ⟩ ≈˘⟨ cancelˡ (IsIso.isoʳ isIsoˡ) ⟩
distributeˡ ∘ distributeˡ⁻¹ ∘ ⟨ id , π₂ ⟩ ∎)
helper : ∀ {A B D} (w : A ⇒ B + D) → (⟨ id , i₁ ∘ π₂ ⟩ +₁ id) ∘ distributeˡ⁻¹ ∘ ⟨ id , w ⟩ ≈ (⟨ id , w ∘ π₁ ⟩ +₁ id) ∘ distributeˡ⁻¹ ∘ ⟨ id , w ⟩
helper w = begin
(⟨ id , i₁ ∘ π₂ ⟩ +₁ id) ∘ distributeˡ⁻¹ ∘ ⟨ id , w ⟩ ≈˘⟨ (+₁-cong₂ (⟨⟩-cong₂ ×₁-η refl) ×₁-η) ⟩∘⟨refl ⟩
(⟨ ⟨ π₁ , π₂ ⟩ , i₁ ∘ π₂ ⟩ +₁ ⟨ π₁ , π₂ ⟩) ∘ distributeˡ⁻¹ ∘ ⟨ id , w ⟩ ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ (⟨⟩∘ ○ ⟨⟩-cong₂ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ (project₁ ○ identityˡ) identityˡ) ((pullʳ project₁) ○ project₂)) (×₁∘⟨⟩ ○ ⟨⟩-cong₂ (project₁ ○ identityˡ) identityˡ)) ⟩
(p +₁ π₁ ×₁ id) ∘ (⟨ id ×₁ i₁ , π₂ ⟩ +₁ ⟨ id ×₁ i₂ , π₂ ⟩) ∘ distributeˡ⁻¹ ∘ ⟨ id , w ⟩ ≈⟨ refl⟩∘⟨ extendʳ dist-step ⟩
(p +₁ π₁ ×₁ id) ∘ distributeˡ⁻¹ ∘ ⟨ id , π₂ ⟩ ∘ ⟨ id , w ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ project₂) ⟩
(p +₁ π₁ ×₁ id) ∘ distributeˡ⁻¹ ∘ ⟨ ⟨ id , w ⟩ , w ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ (cancelʳ project₁) ((pullʳ project₂) ○ identityˡ)) ⟩
(p +₁ π₁ ×₁ id) ∘ distributeˡ⁻¹ ∘ (⟨ id , w ⟩ ×₁ id) ∘ ⟨ id , w ⟩ ≈˘⟨ refl⟩∘⟨ (extendʳ distributeˡ⁻¹-natural-id) ⟩
(p +₁ π₁ ×₁ id) ∘ (⟨ id , w ⟩ ×₁ id +₁ ⟨ id , w ⟩ ×₁ id) ∘ distributeˡ⁻¹ ∘ ⟨ id , w ⟩ ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ (⟨⟩∘ ○ ⟨⟩-cong₂ ((×₁∘×₁ ○ ×₁-cong₂ project₁ identity²) ○ ⟨⟩-unique id-comm id-comm) (pullʳ project₁ ○ pullˡ project₂)) ((×₁∘×₁ ○ ×₁-cong₂ project₁ identity²) ○ ⟨⟩-unique id-comm id-comm)) ⟩
(⟨ id , w ∘ π₁ ⟩ +₁ id) ∘ distributeˡ⁻¹ ∘ ⟨ id , w ⟩ ∎
where
p = ⟨ π₁ ×₁ id , π₂ ∘ π₁ ⟩
dist-step : (⟨ id ×₁ i₁ , π₂ ⟩ +₁ ⟨ id ×₁ i₂ , π₂ ⟩) ∘ distributeˡ⁻¹ ≈ distributeˡ⁻¹ ∘ ⟨ id , π₂ ⟩
dist-step = Iso⇒Mono (IsIso.iso isIsoˡ) _ _ (begin
distributeˡ ∘ (⟨ id ×₁ i₁ , π₂ ⟩ +₁ ⟨ id ×₁ i₂ , π₂ ⟩) ∘ distributeˡ⁻¹ ≈⟨ pullˡ ([]∘+₁ ○ []-cong₂ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl) (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl)) ⟩
[ ⟨ id ×₁ i₁ , i₁ ∘ π₂ ⟩ , ⟨ id ×₁ i₂ , i₂ ∘ π₂ ⟩ ] ∘ distributeˡ⁻¹ ≈⟨ ([⟨⟩]≈⟨[]⟩ _ _ _ _) ⟩∘⟨refl ⟩
⟨ distributeˡ , (π₂ +₁ π₂) ⟩ ∘ distributeˡ⁻¹ ≈⟨ ⟨⟩∘ ○ ⟨⟩-cong₂ (IsIso.isoʳ isIsoˡ) distributeˡ⁻¹-π₂ ⟩
⟨ id , π₂ ⟩ ≈˘⟨ cancelˡ (IsIso.isoʳ isIsoˡ) ⟩
distributeˡ ∘ distributeˡ⁻¹ ∘ ⟨ id , π₂ ⟩ ∎)
uni-helper₁ : ((extend (f #⟩) ∘ τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ u)) ∘ ⟨ π₁ , ⟨ h , π₂ ⟩ ⟩ ≈ (id +₁ ⟨ π₁ , ⟨ h , π₂ ⟩ ⟩) ∘ (π₂ +₁ π₁) ∘ distributeˡ⁻¹ ∘ ⟨ id ×₁ s , f ∘ h ⟩
uni-helper₁ = begin
((extend (f #⟩) ∘ τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ u)) ∘ ⟨ π₁ , ⟨ h , π₂ ⟩ ⟩ ≈⟨ pullʳ (pullʳ (∘-resp-≈ˡ (×₁-cong₂ (sym identity²) sym-assoc ○ sym ×₁∘×₁) ○ pullʳ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ refl identityˡ)))) ⟩
(extend (f #⟩) ∘ τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ (η.η _ ∘ π₂ +₁ (id ×₁ s)) ∘ distributeʳ⁻¹) ∘ ⟨ π₁ , ⟨ f ∘ h , π₂ ⟩ ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (×₁∘×₁ ○ ×₁-cong₂ identity² refl) ⟩
(extend (f #⟩) ∘ τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ (η.η _ ∘ π₂ +₁ (id ×₁ s))) ∘ (id ×₁ distributeʳ⁻¹) ∘ ⟨ π₁ , ⟨ f ∘ h , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (extendʳ (sym (distributeˡ⁻¹-natural id (η.η _ ∘ π₂) (id ×₁ s)))) ⟩
(extend (f #⟩) ∘ τ _ +₁ id) ∘ (id ×₁ (η.η _ ∘ π₂) +₁ id ×₁ (id ×₁ s)) ∘ distributeˡ⁻¹ ∘ (id ×₁ distributeʳ⁻¹) ∘ ⟨ π₁ , ⟨ f ∘ h , π₂ ⟩ ⟩ ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ assoc identityˡ) ⟩
(extend (f #⟩) ∘ τ _ ∘ (id ×₁ (η.η _ ∘ π₂)) +₁ id ×₁ (id ×₁ s)) ∘ distributeˡ⁻¹ ∘ (id ×₁ distributeʳ⁻¹) ∘ ⟨ π₁ , ⟨ f ∘ h , π₂ ⟩ ⟩ ≈˘⟨ (+₁-cong₂ (∘-resp-≈ʳ (∘-resp-≈ʳ (×₁∘×₁ ○ ×₁-cong₂ identity² refl))) refl) ⟩∘⟨refl ⟩
(extend (f #⟩) ∘ τ _ ∘ (id ×₁ (η.η _)) ∘ (id ×₁ π₂) +₁ id ×₁ (id ×₁ s)) ∘ distributeˡ⁻¹ ∘ (id ×₁ distributeʳ⁻¹) ∘ ⟨ π₁ , ⟨ f ∘ h , π₂ ⟩ ⟩ ≈⟨ (+₁-cong₂ (∘-resp-≈ʳ (pullˡ (τ-η _))) refl) ⟩∘⟨refl ⟩
(extend (f #⟩) ∘ η.η _ ∘ (id ×₁ π₂) +₁ id ×₁ (id ×₁ s)) ∘ distributeˡ⁻¹ ∘ (id ×₁ distributeʳ⁻¹) ∘ ⟨ π₁ , ⟨ f ∘ h , π₂ ⟩ ⟩ ≈⟨ (+₁-cong₂ (pullˡ kleisliK.identityʳ) refl) ⟩∘⟨refl ⟩
(f #⟩ ∘ (id ×₁ π₂) +₁ id ×₁ (id ×₁ s)) ∘ distributeˡ⁻¹ ∘ (id ×₁ distributeʳ⁻¹) ∘ ⟨ π₁ , ⟨ f ∘ h , π₂ ⟩ ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁-cong₂ refl (elimʳ swap∘swap)) ⟩∘⟨refl ⟩
(f #⟩ ∘ (id ×₁ π₂) +₁ id ×₁ (id ×₁ s)) ∘ distributeˡ⁻¹ ∘ (id ×₁ distributeʳ⁻¹ ∘ swap ∘ swap) ∘ ⟨ π₁ , ⟨ f ∘ h , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁-cong₂ refl (extendʳ distributeʳ⁻¹∘swap)) ⟩∘⟨refl ⟩
(f #⟩ ∘ (id ×₁ π₂) +₁ id ×₁ (id ×₁ s)) ∘ distributeˡ⁻¹ ∘ (id ×₁ (swap +₁ swap) ∘ distributeˡ⁻¹ ∘ swap) ∘ ⟨ π₁ , ⟨ f ∘ h , π₂ ⟩ ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (×₁∘×₁ ○ ×₁-cong₂ identity² refl) ⟩
(f #⟩ ∘ (id ×₁ π₂) +₁ id ×₁ (id ×₁ s)) ∘ distributeˡ⁻¹ ∘ (id ×₁ (swap +₁ swap)) ∘ (id ×₁ distributeˡ⁻¹ ∘ swap) ∘ ⟨ π₁ , ⟨ f ∘ h , π₂ ⟩ ⟩ ≈⟨ ∘-resp-≈ʳ (extendʳ (sym (distributeˡ⁻¹-natural _ _ _))) ○ pullˡ +₁∘+₁ ⟩
((f #⟩ ∘ (id ×₁ π₂)) ∘ (id ×₁ swap) +₁ (id ×₁ (id ×₁ s)) ∘ (id ×₁ swap)) ∘ distributeˡ⁻¹ ∘ (id ×₁ distributeˡ⁻¹ ∘ swap) ∘ ⟨ π₁ , ⟨ f ∘ h , π₂ ⟩ ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (×₁∘×₁ ○ ×₁-cong₂ identity² refl) ⟩
((f #⟩ ∘ (id ×₁ π₂)) ∘ (id ×₁ swap) +₁ (id ×₁ (id ×₁ s)) ∘ (id ×₁ swap)) ∘ distributeˡ⁻¹ ∘ (id ×₁ distributeˡ⁻¹) ∘ (id ×₁ swap) ∘ ⟨ π₁ , ⟨ f ∘ h , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ swap∘⟨⟩) ⟩
((f #⟩ ∘ (id ×₁ π₂)) ∘ (id ×₁ swap) +₁ (id ×₁ (id ×₁ s)) ∘ (id ×₁ swap)) ∘ distributeˡ⁻¹ ∘ (id ×₁ distributeˡ⁻¹) ∘ ⟨ π₁ , ⟨ π₂ , f ∘ h ⟩ ⟩ ≈⟨ (+₁-cong₂ (pullʳ (×₁∘×₁ ○ ×₁-cong₂ identity² project₂)) (×₁∘×₁ ○ ×₁-cong₂ identity² (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl))) ⟩∘⟨refl ⟩
(f #⟩ ∘ (id ×₁ π₁) +₁ (id ×₁ ⟨ π₂ , s ∘ π₁ ⟩)) ∘ distributeˡ⁻¹ ∘ (id ×₁ distributeˡ⁻¹) ∘ ⟨ π₁ , ⟨ π₂ , f ∘ h ⟩ ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ cancelˡ (_≅_.isoˡ ×-assoc) ⟩
(f #⟩ ∘ (id ×₁ π₁) +₁ (id ×₁ ⟨ π₂ , s ∘ π₁ ⟩)) ∘ distributeˡ⁻¹ ∘ (id ×₁ distributeˡ⁻¹) ∘ _≅_.to ×-assoc ∘ _≅_.from ×-assoc ∘ ⟨ π₁ , ⟨ π₂ , f ∘ h ⟩ ⟩ ≈⟨ refl⟩∘⟨ (sym-assoc ○ extendʳ (assoc ○ distributeˡ⁻¹-assoc)) ⟩
(f #⟩ ∘ (id ×₁ π₁) +₁ (id ×₁ ⟨ π₂ , s ∘ π₁ ⟩)) ∘ (_≅_.to ×-assoc +₁ _≅_.to ×-assoc) ∘ distributeˡ⁻¹ ∘ _≅_.from ×-assoc ∘ ⟨ π₁ , ⟨ π₂ , f ∘ h ⟩ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (assocʳ∘⟨⟩ ○ ⟨⟩-cong₂ ×₁-η refl) ⟩
(f #⟩ ∘ (id ×₁ π₁) +₁ (id ×₁ ⟨ π₂ , s ∘ π₁ ⟩)) ∘ (_≅_.to ×-assoc +₁ _≅_.to ×-assoc) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ∘ h ⟩ ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ (pullʳ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ project₁)) (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ (⟨⟩∘ ○ ⟨⟩-cong₂ project₂ (pullʳ project₁)))) ⟩
(f #⟩ ∘ ⟨ π₁ ∘ π₁ , π₂ ∘ π₁ ⟩ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ , s ∘ π₂ ∘ π₁ ⟩ ⟩) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ∘ h ⟩ ≈⟨ (+₁-cong₂ (∘-resp-≈ʳ (sym ⟨⟩∘ ○ elimˡ ×₁-η)) refl) ⟩∘⟨refl ⟩
(f #⟩ ∘ π₁ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ , s ∘ π₂ ∘ π₁ ⟩ ⟩) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ∘ h ⟩ ≈⟨ (+₁-cong₂ assoc²βε refl) ⟩∘⟨refl ⟩
([ id , bot ] ∘ f ∘ h ∘ π₁ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ , s ∘ π₂ ∘ π₁ ⟩ ⟩) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ∘ h ⟩ ≈˘⟨ +₁-cong₂ (∘-resp-≈ʳ project₂) refl ⟩∘⟨refl ⟩
([ id , bot ] ∘ π₂ ∘ ⟨ id , f ∘ h ∘ π₁ ⟩ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ , s ∘ π₂ ∘ π₁ ⟩ ⟩) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ∘ h ⟩ ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ assoc identityʳ) ⟩
([ id , bot ] ∘ π₂ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ , s ∘ π₂ ∘ π₁ ⟩ ⟩) ∘ (⟨ id , f ∘ h ∘ π₁ ⟩ +₁ id) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ∘ h ⟩ ≈⟨ refl⟩∘⟨ (+₁-cong₂ (⟨⟩-cong₂ refl sym-assoc) refl) ⟩∘⟨refl ⟩
([ id , bot ] ∘ π₂ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ , s ∘ π₂ ∘ π₁ ⟩ ⟩) ∘ (⟨ id , (f ∘ h) ∘ π₁ ⟩ +₁ id) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ∘ h ⟩ ≈˘⟨ refl⟩∘⟨ helper (f ∘ h) ⟩
([ id , bot ] ∘ π₂ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ , s ∘ π₂ ∘ π₁ ⟩ ⟩) ∘ (⟨ id , i₁ ∘ π₂ ⟩ +₁ id) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ∘ h ⟩ ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ ((pullʳ project₂) ○ cancelˡ inject₁) identityʳ) ⟩
(π₂ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ , s ∘ π₂ ∘ π₁ ⟩ ⟩) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ∘ h ⟩ ≈⟨ (+₁-cong₂ refl (⟨⟩-cong₂ refl (⟨⟩-cong₂ (sym small-step) refl))) ⟩∘⟨refl ⟩
(π₂ +₁ ⟨ π₁ ∘ π₁ , ⟨ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ h ∘ π₁ , i₂ ∘ π₂ ⟩ , s ∘ π₂ ∘ π₁ ⟩ ⟩) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ∘ h ⟩ ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityʳ (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ (cancelʳ project₁)) (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ (pullʳ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ))) (pullʳ (pullʳ (pullʳ project₁ ○ identityʳ)))))) ⟩
(π₂ +₁ ⟨ π₁ ∘ π₁ ∘ π₁ , ⟨ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (h ∘ π₁ ×₁ id) , s ∘ π₂ ∘ π₁ ∘ π₁ ⟩ ⟩) ∘ (id +₁ ⟨ id , i₂ ∘ π₂ ⟩) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ∘ h ⟩ ≈⟨ refl⟩∘⟨ helper-dual (f ∘ h) ⟩
(π₂ +₁ ⟨ π₁ ∘ π₁ ∘ π₁ , ⟨ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (h ∘ π₁ ×₁ id) , s ∘ π₂ ∘ π₁ ∘ π₁ ⟩ ⟩) ∘ (id +₁ ⟨ id , (f ∘ h) ∘ π₁ ⟩) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ∘ h ⟩ ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityʳ (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ (pullʳ project₁ ○ identityʳ)) (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ (pullʳ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ)) ○ sym (pullʳ (pullʳ ⟨⟩∘))) (pullʳ (pullʳ (pullʳ project₁ ○ identityʳ)))))) ⟩
(π₂ +₁ ⟨ π₁ ∘ π₁ , ⟨ ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ h , f ∘ h ⟩) ∘ π₁ , s ∘ π₂ ∘ π₁ ⟩ ⟩) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ∘ h ⟩ ≈˘⟨ (+₁-cong₂ refl (⟨⟩-cong₂ refl (⟨⟩-cong₂ (pullˡ ((sym pnno.commute₂) ○ assoc²βε ○ ∘-resp-≈ʳ (∘-resp-≈ʳ (⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ refl)))) refl))) ⟩∘⟨refl ⟩
(π₂ +₁ ⟨ π₁ ∘ π₁ , ⟨ h ∘ (id ×₁ s) ∘ π₁ , s ∘ π₂ ∘ π₁ ⟩ ⟩) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ∘ h ⟩ ≈˘⟨ (+₁-cong₂ refl (⟨⟩∘ ○ ⟨⟩-cong₂ refl (⟨⟩∘ ○ ⟨⟩-cong₂ assoc assoc))) ⟩∘⟨refl ⟩
(π₂ +₁ ⟨ π₁ , ⟨ h ∘ (id ×₁ s) , s ∘ π₂ ⟩ ⟩ ∘ π₁) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ∘ h ⟩ ≈˘⟨ (+₁-cong₂ refl (pullˡ (⟨⟩∘ ○ ⟨⟩-cong₂ (project₁ ○ identityˡ) (⟨⟩∘ ○ ⟨⟩-cong₂ refl project₂)))) ⟩∘⟨refl ⟩
(π₂ +₁ ⟨ π₁ , ⟨ h , π₂ ⟩ ⟩ ∘ (id ×₁ s) ∘ π₁) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ∘ h ⟩ ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ (project₂ ○ identityˡ) (pullʳ project₁)) ⟩
(π₂ +₁ ⟨ π₁ , ⟨ h , π₂ ⟩ ⟩ ∘ π₁) ∘ ((id ×₁ s) ×₁ id +₁ (id ×₁ s) ×₁ id) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ∘ h ⟩ ≈⟨ refl⟩∘⟨ (extendʳ (distributeˡ⁻¹-natural (id ×₁ s) id id)) ⟩
(π₂ +₁ ⟨ π₁ , ⟨ h , π₂ ⟩ ⟩ ∘ π₁) ∘ distributeˡ⁻¹ ∘ ((id ×₁ s) ×₁ (id +₁ id)) ∘ ⟨ id , f ∘ h ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ (elimˡ ([]-unique id-comm-sym id-comm-sym))) ⟩
(π₂ +₁ ⟨ π₁ , ⟨ h , π₂ ⟩ ⟩ ∘ π₁) ∘ distributeˡ⁻¹ ∘ ⟨ id ×₁ s , f ∘ h ⟩ ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ refl) ⟩
(id +₁ ⟨ π₁ , ⟨ h , π₂ ⟩ ⟩) ∘ (π₂ +₁ π₁) ∘ distributeˡ⁻¹ ∘ ⟨ id ×₁ s , f ∘ h ⟩ ∎
where
small-step : [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ h ∘ π₁ , i₂ ∘ π₂ ⟩ ≈ π₂
small-step = begin
[ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ h ∘ π₁ , i₂ ∘ π₂ ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl) ⟩
[ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (id ×₁ i₂) ∘ ⟨ h ∘ π₁ , π₂ ⟩ ≈⟨ refl⟩∘⟨ (pullˡ distributeˡ⁻¹-i₂) ⟩
[ π₁ , π₂ ] ∘ i₂ ∘ ⟨ h ∘ π₁ , π₂ ⟩ ≈⟨ pullˡ inject₂ ⟩
π₂ ∘ ⟨ h ∘ π₁ , π₂ ⟩ ≈⟨ project₂ ⟩
π₂ ∎
uni-helper₂ : f ∘ h ≈ (id +₁ h) ∘ (π₂ +₁ π₁) ∘ distributeˡ⁻¹ ∘ ⟨ id ×₁ s , f ∘ h ⟩
uni-helper₂ = sym (begin
(id +₁ h) ∘ (π₂ +₁ π₁) ∘ distributeˡ⁻¹ ∘ ⟨ id ×₁ s , f ∘ h ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟩
(id +₁ h) ∘ (π₂ +₁ π₁) ∘ distributeˡ⁻¹ ∘ ((id ×₁ s) ×₁ id) ∘ ⟨ id , f ∘ h ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (sym distributeˡ⁻¹-natural-id) ⟩
(id +₁ h) ∘ (π₂ +₁ π₁) ∘ ((id ×₁ s) ×₁ id +₁ (id ×₁ s) ×₁ id) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ∘ h ⟩ ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ refl) ○ pullˡ (+₁∘+₁ ○ +₁-cong₂ (project₂ ○ identityˡ) (pullʳ project₁)) ⟩
(π₂ +₁ h ∘ (id ×₁ s) ∘ π₁) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ∘ h ⟩ ≈⟨ (+₁-cong₂ refl ((pullˡ h-succ) ○ assoc²βε)) ⟩∘⟨refl ⟩
(π₂ +₁ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ h , f ∘ h ⟩ ∘ π₁) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ∘ h ⟩ ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityʳ (pullʳ (pullʳ ((⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ (cancelʳ project₁)) project₂) ○ sym ⟨⟩∘)))) ⟩
(π₂ +₁ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ h ∘ π₁ ∘ π₁ , π₂ ⟩) ∘ ((id +₁ ⟨ id , (f ∘ h) ∘ π₁ ⟩)) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ∘ h ⟩ ≈˘⟨ refl⟩∘⟨ helper-dual (f ∘ h) ⟩
(π₂ +₁ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ h ∘ π₁ ∘ π₁ , π₂ ⟩) ∘ (id +₁ ⟨ id , i₂ ∘ π₂ ⟩) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ∘ h ⟩ ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityʳ (pullʳ (pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ (cancelʳ project₁)) project₂)))) ⟩
(π₂ +₁ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ h ∘ π₁ , i₂ ∘ π₂ ⟩) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ∘ h ⟩ ≈˘⟨ (+₁-cong₂ refl (∘-resp-≈ʳ (∘-resp-≈ʳ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl)))) ⟩∘⟨refl ⟩
(π₂ +₁ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (id ×₁ i₂) ∘ ⟨ h ∘ π₁ , π₂ ⟩) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ∘ h ⟩ ≈⟨ (+₁-cong₂ refl (∘-resp-≈ʳ (pullˡ distributeˡ⁻¹-i₂))) ⟩∘⟨refl ⟩
(π₂ +₁ [ π₁ , π₂ ] ∘ i₂ ∘ ⟨ h ∘ π₁ , π₂ ⟩) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ∘ h ⟩ ≈⟨ (+₁-cong₂ refl (pullˡ inject₂ ○ project₂)) ⟩∘⟨refl ⟩
(π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ∘ h ⟩ ≈⟨ pullˡ distributeˡ⁻¹-π₂ ○ project₂ ⟩
f ∘ h ∎)
eq₂ : (extend (g ∘ π₁) ∘ τ _ ∘ ⟨ id , u # ∘ ⟨ id , z ∘ ! ⟩ ⟩) ≈ (g ⇂ (u # ∘ ⟨ id , z ∘ ! ⟩))
eq₂ = begin
extend (g ∘ π₁) ∘ τ _ ∘ ⟨ id , u # ∘ ⟨ id , z ∘ ! ⟩ ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identity² refl) ⟩
extend (g ∘ π₁) ∘ τ _ ∘ (id ×₁ u #) ∘ ⟨ id , ⟨ id , z ∘ ! ⟩ ⟩ ≈⟨ refl⟩∘⟨ (pullˡ (τ-comm u)) ⟩
extend (g ∘ π₁) ∘ ((τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ u)) # ∘ ⟨ id , ⟨ id , z ∘ ! ⟩ ⟩ ≈⟨ pullˡ ((extend-preserve _ _) ○ #-resp-≈ (algebras Y) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²))) ⟩
((extend (g ∘ π₁) ∘ τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ u)) # ∘ ⟨ id , ⟨ id , z ∘ ! ⟩ ⟩ ≈˘⟨ (#-resp-≈ (algebras Y) (∘-resp-≈ˡ (+₁-cong₂ (pullˡ (extend∘F₁ monadK _ _ ○ extend-≈ project₁)) refl))) ⟩∘⟨refl ⟩
((extend π₁ ∘ K.₁ (g ×₁ id) ∘ τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ u)) # ∘ ⟨ id , ⟨ id , z ∘ ! ⟩ ⟩ ≈˘⟨ #-resp-≈ (algebras Y) (∘-resp-≈ˡ (+₁-cong₂ (∘-resp-≈ʳ (τ-comm-id g)) refl)) ⟩∘⟨refl ⟩
((extend π₁ ∘ τ _ ∘ (g ×₁ id) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ u)) # ∘ ⟨ id , ⟨ id , z ∘ ! ⟩ ⟩ ≈˘⟨ pullˡ (sym (#-Uniformity (algebras Y) (sym by-uni))) ⟩
((extend π₁ ∘ τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ u)) # ∘ (g ×₁ id) ∘ ⟨ id , ⟨ id , z ∘ ! ⟩ ⟩ ≈⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟩
((extend π₁ ∘ τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ u)) # ∘ ⟨ g , ⟨ id , z ∘ ! ⟩ ⟩ ≈˘⟨ pullˡ ((extend-preserve _ _) ○ #-resp-≈ (algebras Y) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²))) ⟩
extend π₁ ∘ ((τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ u)) # ∘ ⟨ g , ⟨ id , z ∘ ! ⟩ ⟩ ≈˘⟨ refl⟩∘⟨ (pullˡ (τ-comm u)) ⟩
extend π₁ ∘ τ _ ∘ (id ×₁ u #) ∘ ⟨ g , ⟨ id , z ∘ ! ⟩ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl) ⟩
extend π₁ ∘ τ _ ∘ ⟨ g , u # ∘ ⟨ id , z ∘ ! ⟩ ⟩ ∎
where
by-uni : ((extend π₁ ∘ τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ u)) ∘ (g ×₁ id) ≈ (id +₁ g ×₁ id) ∘ (extend π₁ ∘ τ _ ∘ (g ×₁ id) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ u)
by-uni = begin
((extend π₁ ∘ τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ u)) ∘ (g ×₁ id) ≈⟨ pullʳ (pullʳ ((×₁∘×₁ ○ ×₁-cong₂ id-comm-sym id-comm) ○ sym ×₁∘×₁)) ⟩
(extend π₁ ∘ τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (g ×₁ id) ∘ (id ×₁ u) ≈˘⟨ refl⟩∘⟨ (extendʳ distributeˡ⁻¹-natural-id) ⟩
(extend π₁ ∘ τ _ +₁ id) ∘ (g ×₁ id +₁ g ×₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ u) ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ assoc id-comm-sym) ○ sym (pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ refl)) ⟩
(id +₁ g ×₁ id) ∘ (extend π₁ ∘ τ _ ∘ (g ×₁ id) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ u) ∎
leq₂ : (g ⇂ (u # ∘ ⟨ id , z ∘ ! ⟩)) ⊑ g
leq₂ = begin
(g ⇂ ((u #) ∘ ⟨ id , z ∘ ! ⟩)) ≈⟨ ⇂-cong₂ ⊑-refl refl ⟩
((g ⇂ g) ⇂ ((u #) ∘ ⟨ id , z ∘ ! ⟩)) ≈⟨ ⇂-assoc ⟩
(g ⇂ (g ⇂ ((u #) ∘ ⟨ id , z ∘ ! ⟩))) ∎