{-# OPTIONS --allow-unsolved-metas --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
  open Bundles
  
  open MIK distributive
  open Terminal terminal using (!; !-unique; !-unique₂; ⊤)
  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.EquationalLifting.Restriction cartesianCategory
  restriction = kleisli-restriction KEquationalLiftingMonad
  open Restriction restriction
  open import Categories.Category.Restriction.Properties.Poset restriction
  open import Categories.Category.Restriction.Properties restriction
  open import Misc.Cases distributive
  open import Categories.Object.NaturalNumbers.Parametrized.Properties.F-Algebras C cartesian coproducts
 
  -- NOTE: f↓ = K.₁ π₁ ∘ τ _ ∘ ⟨ id , f ⟩

  -- restriction of f to domain of g
  _⇂_ : ∀ {X Y Z} (f : X ⇒ K.₀ Y) (g : X ⇒ K.₀ Z) → X ⇒ K.₀ Y
  f ⇂ g = extend π₁ ∘ τ _ ∘ ⟨ f , g ⟩

  -- lemmas on domain and restriction
  ⇂-cong₂ : ∀ {X Y Z} {f h : X ⇒ K.₀ Y} {g i : X ⇒ K.₀ Z} → f ≈ h → g ≈ i → f ⇂ g ≈ h ⇂ i
  ⇂-cong₂ eq₁ eq₂ = refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ eq₁ eq₂

  restrict-η : ∀ {X Y} {f : X ⇒ K.₀ Y} → η X ⇂ f ≈ f ↓
  restrict-η {X} {Y} {f} = begin 
    extend π₁ ∘ τ _ ∘ ⟨ η X , f ⟩                   ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟩
    extend π₁ ∘ τ _ ∘ (η X ⁂ id) ∘ ⟨ id , f ⟩       ≈⟨ refl⟩∘⟨ pullˡ (τ-comm-id (η X)) ⟩ 
    extend π₁ ∘ (K.₁ (η X ⁂ id) ∘ τ _) ∘ ⟨ id , f ⟩ ≈⟨ pullˡ (pullˡ (extend∘F₁ monadK π₁ (η X ⁂ id))) ⟩ 
    (extend (π₁ ∘ (η X ⁂ id)) ∘ τ _) ∘ ⟨ id , f ⟩   ≈⟨ (kleisliK.extend-≈ project₁ ⟩∘⟨refl) ⟩∘⟨refl ⟩ 
    (extend (η X ∘ π₁) ∘ τ _) ∘ ⟨ id , f ⟩          ≈⟨ pushˡ ((F₁⇒extend monadK π₁) ⟩∘⟨refl) ⟩ 
    K.₁ π₁ ∘ τ _ ∘ ⟨ id , f ⟩                       ∎

  restrict-law : ∀ {X Y Z} (f : X ⇒ K.₀ Y) (g : X ⇒ K.₀ Z) → f ⇂ g ≈ extend f ∘ g ↓
  restrict-law {X} {Y} {Z} f g = begin 
    extend π₁ ∘ τ (K.₀ Y , Z) ∘ ⟨ f , g ⟩                  ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟩ 
    extend π₁ ∘ τ (K.₀ Y , Z) ∘ (f ⁂ id) ∘ ⟨ id , g ⟩      ≈⟨ refl⟩∘⟨ (pullˡ (τ-comm-id f)) ⟩ 
    extend π₁ ∘ (K.₁ (f ⁂ id) ∘ τ (X , Z)) ∘ ⟨ id , g ⟩    ≈⟨ (refl⟩∘⟨ assoc) ○ pullˡ (pullʳ (sym K.homomorphism)) ⟩ 
    (μ.η _ ∘ K.₁ (π₁ ∘ (f ⁂ id))) ∘ τ (X , Z) ∘ ⟨ id , g ⟩ ≈⟨ (refl⟩∘⟨ ((K.F-resp-≈ π₁∘⁂) ○ K.homomorphism)) ⟩∘⟨refl ⟩ 
    (μ.η Y ∘ (K.₁ f ∘ K.₁ π₁)) ∘ τ (X , Z) ∘ ⟨ id , g ⟩    ≈⟨ sym-assoc ⟩∘⟨refl ○ assoc ⟩ 
    extend f ∘ K.₁ π₁ ∘ τ _ ∘ ⟨ id , g ⟩                   ∎

  ⇂∘ : ∀ {A X Y Z} {f : X ⇒ K.₀ Y} {g : X ⇒ K.₀ Z} {h : A ⇒ X} → (f ⇂ g) ∘ h ≈ (f ∘ h) ⇂ (g ∘ h)
  ⇂∘ {A} {X} {Y} {Z} {f} {g} {h} = pullʳ (pullʳ ⟨⟩∘)

  η↓ : ∀ {X Y} (f : X ⇒ K.₀ Y) → (η (K.₀ Y) ∘ f) ↓ ≈ η X
  η↓ {X} {Y} f = begin 
    K.₁ π₁ ∘ τ _ ∘ ⟨ id , η _ ∘ f ⟩        ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identity² refl) ⟩ 
    K.₁ π₁ ∘ τ _ ∘ (id ⁂ η _) ∘ ⟨ id , f ⟩ ≈⟨ refl⟩∘⟨ (pullˡ (τ-η _)) ⟩ 
    K.₁ π₁ ∘ η _ ∘ ⟨ id , f ⟩              ≈⟨ pullˡ (K₁η π₁) ⟩ 
    (η _ ∘ π₁) ∘ ⟨ id , f ⟩                ≈⟨ cancelʳ project₁ ⟩ 
    η _                                    ∎
  -- f ↓ == M₁ π₁ ∘ σ ∘ ⟨ id , f ⟩
  ⇂-assoc : ∀ {A X Y Z} {f : X ⇒ K.₀ Y} {g : X ⇒ K.₀ Z} {h : X ⇒ K.₀ A} → (f ⇂ g) ⇂ h ≈ f ⇂ (g ⇂ h)
  ⇂-assoc {A} {X} {Y} {Z} {f} {g} {h} = begin 
    (f ⇂ g) ⇂ h                     ≈⟨ restrict-law _ _ ○ ∘-resp-≈ˡ (extend-≈ (restrict-law _ _)) ⟩ 
    extend (extend f ∘ g ↓) ∘ h ↓   ≈˘⟨ pullˡ (sym kleisliK.assoc) ⟩ 
    extend f ∘ extend (g ↓) ∘ h ↓   ≈˘⟨ refl⟩∘⟨ ↓-denestʳ ⟩ 
    extend f ∘ ((extend g ∘ h ↓) ↓) ≈˘⟨ restrict-law _ _ ○ ∘-resp-≈ʳ (↓-cong (restrict-law _ _)) ⟩ 
    f ⇂ (g ⇂ h)                     ∎

  infixr  _⊑_

  -- This is an alternative definition of the order to the one in `Categories.Category.Restriction.Properties.Poset`
  -- But they are in fact equivalent, which is what we use to get `refl`, `trans` and `antisym`

  _⊑_ : ∀ {X Y} (f g : X ⇒ K.₀ Y) → Set e
  f ⊑ g = f ≈ g ⇂ f

  module PartialOrder where
    private
      _≤_ : ∀ {X Y} (f g : X ⇒ K.₀ Y) → Set e
      _≤_ {X} {Y} = _≤'_
        where open Poset (poset X Y) using () renaming (_≤_ to _≤'_) 
      
      ≤⇔⊑-helper : ∀ {X Y} {f g : X ⇒ K.₀ Y} → extend g ∘ K.₁ π₁ ∘ τ _ ∘ ⟨ id , f ⟩ ≈ extend π₁ ∘ τ _ ∘ ⟨ g , f ⟩
      ≤⇔⊑-helper {X} {Y} {f} {g} = begin 
        extend g ∘ K.₁ π₁ ∘ τ _ ∘ ⟨ id , f ⟩        ≈⟨ pullˡ (extend∘F₁ monadK g π₁) ⟩ 
        extend (g ∘ π₁) ∘ τ _ ∘ ⟨ id , f ⟩          ≈˘⟨ (extend-≈ project₁) ⟩∘⟨refl ⟩ 
        extend (π₁ ∘ (g ⁂ id)) ∘ τ _ ∘ ⟨ id , f ⟩   ≈˘⟨ pullˡ ((extend∘F₁ monadK π₁ (g ⁂ id))) ⟩ 
        extend π₁ ∘ K.₁ (g ⁂ id) ∘ τ _ ∘ ⟨ id , f ⟩ ≈˘⟨ refl⟩∘⟨ (extendʳ (strongK.strengthen.commute (g , id))) ⟩ 
        extend π₁ ∘ τ _ ∘ (g ⁂ K.₁ id) ∘ ⟨ id , f ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ (elimˡ K.identity)) ⟩ 
        extend π₁ ∘ τ _ ∘ ⟨ g , f ⟩                 ∎

      ≤⇒⊑ : ∀ {X Y} {f g : X ⇒ K.₀ Y} → f ≤ g → f ⊑ g
      ≤⇒⊑ {X} {Y} {f} {g} leq = begin 
        f                                           ≈⟨ leq ⟩ 
        extend g ∘ K.₁ π₁ ∘ τ _ ∘ ⟨ id , f ⟩        ≈⟨ ≤⇔⊑-helper ⟩ 
        extend π₁ ∘ τ _ ∘ ⟨ g , f ⟩                 ∎
      ⊑⇒≤ : ∀ {X Y} {f g : X ⇒ K.₀ Y} → f ⊑ g → f ≤ g
      ⊑⇒≤ {X} {Y} {f} {g} sqleq = begin 
        f                                    ≈⟨ sqleq ⟩ 
        extend π₁ ∘ τ _ ∘ ⟨ g , f ⟩          ≈˘⟨ ≤⇔⊑-helper ⟩  
        extend g ∘ K.₁ π₁ ∘ τ _ ∘ ⟨ id , f ⟩ ∎
    ⊑-refl : ∀ {X Y} {f : X ⇒ K.₀ Y} → f ⊑ f
    ⊑-refl {X} {Y} = ≤⇒⊑ (refl' refl)
      where open Poset (poset X Y) using () renaming (reflexive to refl')

    ⊑-trans : ∀ {X Y} {f g h : X ⇒ K.₀ Y} → f ⊑ g → g ⊑ h → f ⊑ h
    ⊑-trans {X} {Y} f⊑g g⊑h = ≤⇒⊑ (trans' (⊑⇒≤ f⊑g) (⊑⇒≤ g⊑h))
      where open Poset (poset X Y) using () renaming (trans to trans')

    ⊑-antisym : ∀ {X Y} {f g : X ⇒ K.₀ Y} → f ⊑ g → g ⊑ f → f ≈ g
    ⊑-antisym {X} {Y} f⊑g g⊑f = antisym' (⊑⇒≤ f⊑g) (⊑⇒≤ g⊑f)
      where open Poset (poset X Y) using () renaming (antisym to antisym')

  open PartialOrder

  ⊑∘ˡ : ∀ {A X Y} {f g : X ⇒ K.₀ Y} {h : A ⇒ X} → f ⊑ g → (f ∘ h) ⊑ (g ∘ h)
  ⊑∘ˡ {A} {X} {Y} {f} {g} {h} leq = begin 
    f ∘ h               ≈⟨ leq ⟩∘⟨refl ⟩ 
    (g ⇂ f) ∘ h         ≈⟨ ⇂∘ ⟩ 
    ((g ∘ h) ⇂ (f ∘ h)) ∎

  ⊑-cong₂ : ∀ {X Y} {f g h i : X ⇒ K.₀ Y} → f ≈ h → g ≈ i → f ⊑ g → h ⊑ i
  ⊑-cong₂ eq₁ eq₂ leq = (sym eq₁) ○ leq ○ ⇂-cong₂ eq₂ eq₁

  f↓⊑η : ∀ {X Y} {f : X ⇒ K.₀ Y} → f ↓ ⊑ η X
  f↓⊑η {X} {Y} {f} = begin 
    f ↓         ≈˘⟨ ↓-idempotent ⟩ 
    (f ↓)↓      ≈˘⟨ restrict-η ⟩ 
    η X ⇂ (f ↓) ∎

  -- -- bottom element of restriction order
  module bottom where
    bot : ∀ {X} {Y} → X ⇒ K.₀ Y
    bot = i₂ # -- by uniformity this should be equal to (i₂ # ∘ !)

    bot∘! : ∀ {X} {Y} → bot {X} {Y} ≈ bot {⊤} {Y} ∘ !
    bot∘! = #-Uniformity (algebras _) inject₂

    bot-absorbs : ∀ {X Y Z} {f : Z ⇒ X} → bot {X} {Y} ∘ f ≈ bot {Z} {Y}
    bot-absorbs {X} {Y} {Z} {f} = begin 
      bot {X} {Y} ∘ f ≈⟨ bot∘! ⟩∘⟨refl ⟩ 
      (bot ∘ !) ∘ f   ≈⟨ pullʳ (sym (!-unique (! ∘ f))) ⟩ 
      bot ∘ !         ≈˘⟨ bot∘! ⟩
      bot {Z} {Y}     ∎

    bot⊑f : ∀ {X} {Y} {f : X ⇒ K.₀ Y} → bot ⊑ f
    bot⊑f {X} {Y} {f} = sym (begin 
      extend π₁ ∘ τ _ ∘ ⟨ f , i₂ # ⟩                                      ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ identityʳ) ⟩ 
      extend π₁ ∘ τ _ ∘ (id ⁂ i₂ #) ∘ ⟨ f , id ⟩                          ≈⟨ refl⟩∘⟨ (pullˡ (τ-comm i₂)) ⟩ 
      extend π₁ ∘ ((τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ i₂))# ∘ ⟨ f , id ⟩ ≈⟨ refl⟩∘⟨ ((#-resp-≈ (algebras (K.₀ Y × Y)) (refl⟩∘⟨ distributeˡ⁻¹-i₂)) ⟩∘⟨refl) ⟩ 
      extend π₁ ∘ ((τ _ +₁ id) ∘ i₂)# ∘ ⟨ f , id ⟩                        ≈⟨ refl⟩∘⟨ ((#-resp-≈ (algebras (K.₀ Y × Y)) ((inject₂ ○ identityʳ))) ⟩∘⟨refl) ⟩ 
      extend π₁ ∘ i₂ # ∘ ⟨ f , id ⟩                                       ≈⟨ pullˡ (extend-preserve π₁ i₂) ⟩ 
      ((extend π₁ +₁ id) ∘ i₂) # ∘ ⟨ f , id ⟩                             ≈⟨ (#-resp-≈ (algebras Y) (inject₂ ○ identityʳ)) ⟩∘⟨refl ⟩ 
      i₂ # ∘ ⟨ f , id ⟩                                                   ≈˘⟨ #-Uniformity (algebras Y) inject₂ ⟩
      i₂ #                                                                ∎)
  open bottom

  τ-strict : ∀ {X Y Z} → τ (X , Y) ∘ (id ⁂ bot {Z} {Y}) ≈ bot
  τ-strict {X} {Y} {Z} = begin 
    τ _ ∘ (id ⁂ i₂ #)                           ≈⟨ τ-comm i₂ ⟩ 
    ((τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ i₂)) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ distributeˡ⁻¹-i₂) ⟩ 
    ((τ _ +₁ id) ∘ i₂) #                        ≈⟨ #-resp-≈ (algebras _) (inject₂ ○ identityʳ) ⟩ 
    (i₂ #)                                      ∎

  ∘-right-strict : ∀ {X Y Z} (f : X ⇒ K.₀ Y) → extend f ∘ bot {Z} {X} ≈ bot
  ∘-right-strict f = begin 
    extend f ∘ bot            ≈⟨ extend-preserve f i₂ ⟩
    ((extend f +₁ id) ∘ i₂) # ≈⟨ #-resp-≈ (algebras _) (inject₂ ○ identityʳ) ⟩
    bot                       ∎

  bot-restrict : ∀ {X Y Z} (f : X ⇒ K.₀ Y) → f ⇂ (bot {X} {Z}) ≈ bot
  bot-restrict f = begin 
    extend π₁ ∘ τ _ ∘ ⟨ f , bot ⟩             ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ identityʳ) ⟩ 
    extend π₁ ∘ τ _ ∘ (id ⁂ bot) ∘ ⟨ f , id ⟩ ≈⟨ refl⟩∘⟨ (pullˡ τ-strict) ⟩ 
    extend π₁ ∘ bot ∘ ⟨ f , id ⟩              ≈⟨ pullˡ (∘-right-strict π₁) ⟩ 
    bot ∘ ⟨ f , id ⟩                          ≈˘⟨ #-Uniformity (algebras _) inject₂ ⟩ 
    bot                                       ∎

  module BoundedIteration (PNNO : ParametrizedNNO C cartesian) where
    open import Misc.PrimitiveRecursion cartesian PNNO
    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 MK
    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 #⟩) ⟩                                      ∎)
        -- leq : f #⟩ ≈ extend π₁ ∘ τ _ ∘ ⟨ g ∘ π₁ , f #⟩ ⟩
        -- Proving u-law:
        -- 1. Show that extend (f #⟩) ∘ τ _ ∘ ⟨ id , u # ∘ ⟨ id , z ∘ ! ⟩ ⟩ ≈ ((extend (f #⟩) ∘ τ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ u))# ∘ ⟨ id , ⟨ id , z ∘ ! ⟩ ⟩   [[leq₁]]
        -- 2. Show that ((extend (f #⟩) ∘ τ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ u))# ∘ ⟨ id , ⟨ id , z ∘ ! ⟩ ⟩ ≈ f #                                                   [[eq₁]]
        -- -- 1. Proven by strengthening: show that ((extend (f #⟩) ∘ τ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ u))# ∘ ⟨ π₁ , ⟨ h , π₂ ⟩ ⟩ ≈ f # ∘ h                       [[strengthened]]
        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'  -- universal id (case f inl π₁ inr π₂)
              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 ∘ ! ⟩))) ∎