open import Level
open import Categories.Category.Core
open import Categories.Object.NaturalNumbers.Parametrized
open import Categories.Category.Distributive
open import Categories.Object.Terminal
open import Monad.Instance.Delay
open import Monad.Instance.Delay.Quotient

import Categories.Morphism as M
import Categories.Morphism.Reasoning as MR
import Categories.Morphism.Properties as MP

module Monad.Instance.Delay.Quotient.Theorem.Condition3-1 {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) (DM : DelayM (Distributive.cocartesian distributive)) (PNNO : ParametrizedNNO C (Distributive.cartesian distributive)) (DQ : DelayQ distributive DM PNNO) where
  open import Categories.Diagram.Coequalizer C
  open Category C
  open import Category.Distributive.Helper distributive
  open import Monad.Instance.K distributive
  open import Monad.Strong.Helper cartesian
  open Bundles 
  open import Algebra.Elgot cocartesian
  open import Algebra.Search cocartesian DM
  open import Algebra.Search.Properties cocartesian DM

  open import Monad.Instance.Delay.Quotient.Theorem.Conditions distributive DM PNNO DQ
  open import Monad.Instance.Delay.Strong distributive DM
  open Equiv
  open HomReasoning
  open M C
  open MR C
  open MP C
  open DelayM DM
  open Coit
  open D-Monad
  open D-Kleisli
  -- open D-Strong
  open τ-mod
  open DelayQ DQ
  private
    module PNNO = ParametrizedNNO PNNO
  open PNNO using (s; z; N)
  open import Monad.Instance.Delay.Iota distributive DM PNNO
  open Terminal terminal using (⊤; !; !-unique; !-unique₂)
  open Later∘Extend

  -- preparatory definitions and facts
  module _ {X : Obj} where
    open import Object.NaturalNumbers.Primitive cartesian coproducts (PNNO⇒NNO C cartesian PNNO)
    open import Object.NaturalNumbers.Parametrized.Primitive cartesian coproducts PNNO

    w : D₀ X × D₀ ⊤ ⇒ D₀ X + D₀ X × D₀ ⊤
    w = [ i₁ ∘ π₁ , i₂ ∘ (earlier ⁂ id) ] ∘ distributeˡ⁻¹ ∘ (id ⁂ out)

    w-now : w ∘ (id ⁂ now) ≈ i₁ ∘ π₁
    w-now = begin 
      ([ i₁ ∘ π₁ , i₂ ∘ (earlier ⁂ id) ] ∘ distributeˡ⁻¹ ∘ (id ⁂ out)) ∘ (id ⁂ now) ≈⟨ pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² unitlaw)) ⟩ 
      [ i₁ ∘ π₁ , i₂ ∘ (earlier ⁂ id) ] ∘ distributeˡ⁻¹ ∘ (id ⁂ i₁)                 ≈⟨ refl⟩∘⟨ distributeˡ⁻¹-i₁ ⟩ 
      [ i₁ ∘ π₁ , i₂ ∘ (earlier ⁂ id) ] ∘ i₁                                        ≈⟨ inject₁ ⟩ 
      i₁ ∘ π₁                                                                       ∎

    w-later : w ∘ (id ⁂ later) ≈ i₂ ∘ (earlier ⁂ id)
    w-later = begin 
      ([ i₁ ∘ π₁ , i₂ ∘ (earlier ⁂ id) ] ∘ distributeˡ⁻¹ ∘ (id ⁂ out)) ∘ (id ⁂ later) ≈⟨ pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² laterlaw)) ⟩ 
      [ i₁ ∘ π₁ , i₂ ∘ (earlier ⁂ id) ] ∘ distributeˡ⁻¹ ∘ (id ⁂ i₂)                   ≈⟨ refl⟩∘⟨ distributeˡ⁻¹-i₂ ⟩ 
      [ i₁ ∘ π₁ , i₂ ∘ (earlier ⁂ id) ] ∘ i₂                                          ≈⟨ inject₂ ⟩ 
      i₂ ∘ (earlier ⁂ id)                                                             ∎

    -- bounded subtraction
    monus : N ⇒ N
    monus = NNO-universal-primitive z π₂

    monus-zero : monus ∘ z ≈ z
    monus-zero = NNO-universal-primitive-zero z π₂

    monus-succ : monus ∘ s ≈ id
    monus-succ = NNO-universal-primitive-succ z π₂ ○ project₂

    D-jointly-epic-product : ∀ {X Y Z} {f g : D₀ Z × D₀ X ⇒ Y} → (f ∘ (now ⁂ now) ≈ g ∘ (now ⁂ now)) → (f ∘ (later ⁂ now) ≈ g ∘ (later ⁂ now)) → (f ∘ (now ⁂ later) ≈ g ∘ (now ⁂ later)) → (f ∘ (later ⁂ later) ≈ g ∘ (later ⁂ later)) → f ≈ g
    D-jointly-epic-product {X} {Y} {Z} {f} {g} now-now later-now now-later later-later = begin 
      f                                 ≈⟨ introʳ (⟨⟩-unique (id-comm ○ ∘-resp-≈ˡ (sym out⁻¹∘out)) (id-comm ○ ∘-resp-≈ˡ (sym out⁻¹∘out))) ⟩ 
      f ∘ (out⁻¹ ∘ out ⁂ out⁻¹ ∘ out)   ≈˘⟨ refl⟩∘⟨ ⁂∘⁂ ⟩ 
      f ∘ (out⁻¹ ⁂ out⁻¹) ∘ (out ⁂ out) ≈⟨ extendʳ (distribution ○ helper ○ sym distribution) ⟩ 
      g ∘ (out⁻¹ ⁂ out⁻¹) ∘ (out ⁂ out) ≈⟨ refl⟩∘⟨ ⁂∘⁂ ⟩ 
      g ∘ (out⁻¹ ∘ out ⁂ out⁻¹ ∘ out)   ≈⟨ elimʳ (⟨⟩-unique (id-comm ○ ∘-resp-≈ˡ (sym out⁻¹∘out)) (id-comm ○ ∘-resp-≈ˡ (sym out⁻¹∘out))) ⟩ 
      g                                 ∎
      where
      distribution : ∀ {h : D₀ Z × D₀ X ⇒ Y} → h ∘ (out⁻¹ ⁂ out⁻¹) ≈ [ [ h ∘ (now ⁂ now) , h ∘ (later ⁂ now) ] , [ h ∘ (now ⁂ later) , h ∘ (later ⁂ later) ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹
      distribution {h} = Iso⇒Epi (IsIso.iso isIsoˡ) (h ∘ (out⁻¹ ⁂ out⁻¹)) ([ [ h ∘ (now ⁂ now) , h ∘ (later ⁂ now) ] , [ h ∘ (now ⁂ later) , h ∘ (later ⁂ later) ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹) (begin 
        (h ∘ (out⁻¹ ⁂ out⁻¹)) ∘ distributeˡ                                                                                                                          ≈⟨ ∘[] ○ []-cong₂ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identityʳ refl)) (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identityʳ refl)) ⟩ 
        [ h ∘ (out⁻¹ ⁂ now) , h ∘ (out⁻¹ ⁂ later) ]                                                                                                                  ≈⟨ []-cong₂ distribution-helper₁ distribution-helper₂ ⟩ 
        [ [ h ∘ (now ⁂ now) , h ∘ (later ⁂ now) ] ∘ distributeʳ⁻¹ , [ h ∘ (now ⁂ later) , h ∘ (later ⁂ later) ] ∘ distributeʳ⁻¹ ]                                    ≈˘⟨ []∘+₁ ⟩ 
        [ [ h ∘ (now ⁂ now) , h ∘ (later ⁂ now) ] , [ h ∘ (now ⁂ later) , h ∘ (later ⁂ later) ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹)                                 ≈˘⟨ pullʳ (cancelʳ (IsIso.isoˡ isIsoˡ)) ⟩ 
        ([ [ h ∘ (now ⁂ now) , h ∘ (later ⁂ now) ] , [ h ∘ (now ⁂ later) , h ∘ (later ⁂ later) ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹) ∘ distributeˡ ∎)
        where
        distribution-helper₁ : h ∘ (out⁻¹ ⁂ now) ≈ [ h ∘ (now ⁂ now) , h ∘ (later ⁂ now) ] ∘ distributeʳ⁻¹
        distribution-helper₁ = Iso⇒Epi (IsIso.iso isIsoʳ) (h ∘ (out⁻¹ ⁂ now)) ([ h ∘ (now ⁂ now) , h ∘ (later ⁂ now) ] ∘ distributeʳ⁻¹) (begin 
          (h ∘ (out⁻¹ ⁂ now)) ∘ distributeʳ                                       ≈⟨ ∘[] ○ []-cong₂ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ refl identityʳ)) (pullʳ (⁂∘⁂ ○ ⁂-cong₂ refl identityʳ)) ⟩ 
          [ h ∘ (now ⁂ now) , h ∘ (later ⁂ now) ]                                 ≈˘⟨ cancelʳ (IsIso.isoˡ isIsoʳ) ⟩ 
          ([ h ∘ (now ⁂ now) , h ∘ (later ⁂ now) ] ∘ distributeʳ⁻¹) ∘ distributeʳ ∎)
        distribution-helper₂ : h ∘ (out⁻¹ ⁂ later) ≈ [ h ∘ (now ⁂ later) , h ∘ (later ⁂ later) ] ∘ distributeʳ⁻¹
        distribution-helper₂ = Iso⇒Epi (IsIso.iso isIsoʳ) (h ∘ (out⁻¹ ⁂ later)) ([ h ∘ (now ⁂ later) , h ∘ (later ⁂ later) ] ∘ distributeʳ⁻¹) (begin 
          (h ∘ (out⁻¹ ⁂ later)) ∘ distributeʳ                                         ≈⟨ ∘[] ○ []-cong₂ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ refl identityʳ)) (pullʳ (⁂∘⁂ ○ ⁂-cong₂ refl identityʳ)) ⟩ 
          [ h ∘ (now ⁂ later) , h ∘ (later ⁂ later) ]                                 ≈˘⟨ cancelʳ (IsIso.isoˡ isIsoʳ) ⟩ 
          ([ h ∘ (now ⁂ later) , h ∘ (later ⁂ later) ] ∘ distributeʳ⁻¹) ∘ distributeʳ ∎)
      helper : [ [ f ∘ (now ⁂ now) , f ∘ (later ⁂ now) ] , [ f ∘ (now ⁂ later) , f ∘ (later ⁂ later) ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ≈ [ [ g ∘ (now ⁂ now) , g ∘ (later ⁂ now) ] , [ g ∘ (now ⁂ later) , g ∘ (later ⁂ later) ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹
      helper = ∘-resp-≈ˡ ([]-cong₂ ([]-cong₂ now-now later-now) ([]-cong₂ now-later later-later))

    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ˡ nno-iso) ⟩ 
      f ∘ [ ⟨ id , z ∘ ! ⟩ , (id ⁂ s) ] ∘ M._≅_.from nno-iso     ≈⟨ pullˡ ∘[] ⟩ 
      [ f ∘ ⟨ id , z ∘ ! ⟩ , f ∘ (id ⁂ s) ] ∘ M._≅_.from nno-iso ≈⟨ ([]-cong₂ IB IS) ⟩∘⟨refl ⟩ 
      [ g ∘ ⟨ id , z ∘ ! ⟩ , g ∘ (id ⁂ s) ] ∘ M._≅_.from nno-iso ≈˘⟨ pullˡ ∘[] ⟩ 
      g ∘ [ ⟨ id , z ∘ ! ⟩ , (id ⁂ s) ] ∘ M._≅_.from nno-iso     ≈⟨ elimʳ (M._≅_.isoˡ nno-iso) ⟩ 
      g                                                          ∎

    u : D₀ (X × N) × D₀ ⊤ ⇒ D₀ (X × N) + D₀ (X × N) × D₀ ⊤
    u = [ (i₁ ∘ π₁) , [ i₂ ∘ (now ∘ (id ⁂ monus) ⁂ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ id) ] ∘ distributeˡ⁻¹ ∘ (id ⁂ out)

    u-now : u ∘ (id ⁂ now) ≈ i₁ ∘ π₁
    u-now = begin 
      u ∘ (id ⁂ now) ≈⟨ pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² unitlaw)) ⟩ 
      [ i₁ ∘ π₁ , [ i₂ ∘ (now ∘ (id ⁂ monus) ⁂ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ id) ] ∘ distributeˡ⁻¹ ∘ (id ⁂ i₁) ≈⟨ refl⟩∘⟨ distributeˡ⁻¹-i₁ ⟩ 
      [ i₁ ∘ π₁ , [ i₂ ∘ (now ∘ (id ⁂ monus) ⁂ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ id) ] ∘ i₁ ≈⟨ inject₁ ⟩ 
      i₁ ∘ π₁ ∎

    u-later : u ∘ (later ⁂ later) ≈ i₂
    u-later = begin 
      u ∘ (later ⁂ later)                                                                                                           ≈˘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identityˡ identityʳ) ⟩ 
      u ∘ (id ⁂ later) ∘ (later ⁂ id)                                                                                               ≈⟨ pullʳ (pullʳ (pullˡ (⁂∘⁂ ○ ⁂-cong₂ identity² laterlaw))) ⟩ 
      [ i₁ ∘ π₁ , [ i₂ ∘ (now ∘ (id ⁂ monus) ⁂ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ id) ] ∘ distributeˡ⁻¹ ∘ (id ⁂ i₂) ∘ (later ⁂ id) ≈⟨ refl⟩∘⟨ (pullˡ distributeˡ⁻¹-i₂) ⟩ 
      [ i₁ ∘ π₁ , [ i₂ ∘ (now ∘ (id ⁂ monus) ⁂ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ id) ] ∘ i₂ ∘ (later ⁂ id)                        ≈⟨ extendʳ inject₂ ⟩ 
      [ i₂ ∘ (now ∘ (id ⁂ monus) ⁂ id) , i₂ ] ∘ (distributeʳ⁻¹ ∘ (out ⁂ id)) ∘ (later ⁂ id)                                         ≈⟨ refl⟩∘⟨ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ laterlaw identity²)) ⟩
      [ i₂ ∘ (now ∘ (id ⁂ monus) ⁂ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (i₂ ⁂ id)                                                           ≈⟨ refl⟩∘⟨ distributeʳ⁻¹-i₂ ⟩ 
      [ i₂ ∘ (now ∘ (id ⁂ monus) ⁂ id) , i₂ ] ∘ i₂                                                                                  ≈⟨ inject₂ ⟩ 
      i₂                                                                                                                            ∎

    u-zero : u ∘ (now ∘ ⟨ id , z ∘ ! ⟩ ⁂ later) ≈ i₂ ∘ (now ∘ ⟨ id , z ∘ ! ⟩ ⁂ id)
    u-zero = begin 
      ([ i₁ ∘ π₁ , [ i₂ ∘ (now ∘ (id ⁂ monus) ⁂ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ id) ] ∘ distributeˡ⁻¹ ∘ (id ⁂ out)) ∘ (now ∘ ⟨ id , z ∘ ! ⟩ ⁂ later)             ≈˘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identityˡ identityʳ) ⟩ 
      ([ i₁ ∘ π₁ , [ i₂ ∘ (now ∘ (id ⁂ monus) ⁂ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ id) ] ∘ distributeˡ⁻¹ ∘ (id ⁂ out)) ∘ (id ⁂ later) ∘ (now ∘ ⟨ id , z ∘ ! ⟩ ⁂ id) ≈⟨ pullʳ (pullʳ (pullˡ (⁂∘⁂ ○ ⁂-cong₂ identity² laterlaw))) ⟩ 
      [ i₁ ∘ π₁ , [ i₂ ∘ (now ∘ (id ⁂ monus) ⁂ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ id) ] ∘ distributeˡ⁻¹ ∘ (id ⁂ i₂) ∘ (now ∘ ⟨ id , z ∘ ! ⟩ ⁂ id)                   ≈⟨ refl⟩∘⟨ (pullˡ distributeˡ⁻¹-i₂) ⟩ 
      [ i₁ ∘ π₁ , [ i₂ ∘ (now ∘ (id ⁂ monus) ⁂ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ id) ] ∘ i₂ ∘ (now ∘ ⟨ id , z ∘ ! ⟩ ⁂ id)                                          ≈⟨ extendʳ inject₂ ⟩ 
      [ i₂ ∘ (now ∘ (id ⁂ monus) ⁂ id) , i₂ ] ∘ (distributeʳ⁻¹ ∘ (out ⁂ id)) ∘ (now ∘ ⟨ id , z ∘ ! ⟩ ⁂ id)                                                           ≈⟨ refl⟩∘⟨ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ (pullˡ unitlaw) refl ○ sym ⁂∘⁂)) ⟩ 
      [ i₂ ∘ (now ∘ (id ⁂ monus) ⁂ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (i₁ ⁂ id) ∘ (⟨ id , z ∘ ! ⟩ ⁂ id)                                                                    ≈⟨ refl⟩∘⟨ (pullˡ distributeʳ⁻¹-i₁) ⟩ 
      [ i₂ ∘ (now ∘ (id ⁂ monus) ⁂ id) , i₂ ] ∘ i₁ ∘ (⟨ id , z ∘ ! ⟩ ⁂ id)                                                                                           ≈⟨ extendʳ inject₁ ⟩ 
      i₂ ∘ (now ∘ (id ⁂ monus) ⁂ id) ∘ (⟨ id , z ∘ ! ⟩ ⁂ id)                                                                                                         ≈⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ (pullʳ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identity² (pullˡ monus-zero))) identity²) ⟩ 
      i₂ ∘ (now ∘ ⟨ id , z ∘ ! ⟩ ⁂ id)                                                                                                                               ∎

    u-succ : u ∘ (now ∘ (id ⁂ s) ⁂ later) ≈ i₂ ∘ (now ⁂ id)
    u-succ = begin 
      ([ i₁ ∘ π₁ , [ i₂ ∘ (now ∘ (id ⁂ monus) ⁂ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ id) ] ∘ distributeˡ⁻¹ ∘ (id ⁂ out)) ∘ (now ∘ (id ⁂ s) ⁂ later)             ≈˘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identityˡ identityʳ) ⟩
      ([ i₁ ∘ π₁ , [ i₂ ∘ (now ∘ (id ⁂ monus) ⁂ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ id) ] ∘ distributeˡ⁻¹ ∘ (id ⁂ out)) ∘ (id ⁂ later) ∘ (now ∘ (id ⁂ s) ⁂ id) ≈⟨ pullʳ (pullʳ (pullˡ (⁂∘⁂ ○ ⁂-cong₂ identity² laterlaw))) ⟩ 
      [ i₁ ∘ π₁ , [ i₂ ∘ (now ∘ (id ⁂ monus) ⁂ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ id) ] ∘ distributeˡ⁻¹ ∘ (id ⁂ i₂) ∘ (now ∘ (id ⁂ s) ⁂ id)                   ≈⟨ refl⟩∘⟨ (pullˡ distributeˡ⁻¹-i₂) ⟩ 
      [ i₁ ∘ π₁ , [ i₂ ∘ (now ∘ (id ⁂ monus) ⁂ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ id) ] ∘ i₂ ∘ (now ∘ (id ⁂ s) ⁂ id)                                          ≈⟨ extendʳ inject₂ ⟩ 
      [ i₂ ∘ (now ∘ (id ⁂ monus) ⁂ id) , i₂ ] ∘ (distributeʳ⁻¹ ∘ (out ⁂ id)) ∘ (now ∘ (id ⁂ s) ⁂ id)                                                           ≈⟨ refl⟩∘⟨ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ (pullˡ unitlaw) refl ○ sym ⁂∘⁂)) ⟩ 
      [ i₂ ∘ (now ∘ (id ⁂ monus) ⁂ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (i₁ ⁂ id) ∘ ((id ⁂ s) ⁂ id)                                                                    ≈⟨ refl⟩∘⟨ (pullˡ distributeʳ⁻¹-i₁) ⟩ 
      [ i₂ ∘ (now ∘ (id ⁂ monus) ⁂ id) , i₂ ] ∘ i₁ ∘ ((id ⁂ s) ⁂ id)                                                                                           ≈⟨ extendʳ inject₁ ⟩ 
      i₂ ∘ (now ∘ (id ⁂ monus) ⁂ id) ∘ ((id ⁂ s) ⁂ id)                                                                                                         ≈⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ (cancelʳ (⁂∘⁂ ○ ⁂-cong₂ identity² monus-succ ○ ⟨⟩-unique id-comm id-comm)) identity²) ⟩ 
      i₂ ∘ (now ⁂ id)                                                                                                                                          ∎

    coit-w-retract : coit w ∘ ⟨ D.μ.η X , D₁ ! ⟩ ≈ id
    coit-w-retract = begin 
      coit w ∘ ⟨ D.μ.η X , D₁ ! ⟩ ≈˘⟨ coit-unique out (coit w ∘ ⟨ D.μ.η X , D₁ ! ⟩) coit-helper ⟩ 
      coit out                    ≈⟨ coit-refl ⟩ 
      id                          ∎
      where
      coit-helper : out ∘ coit w ∘ ⟨ D.μ.η X , D₁ ! ⟩ ≈ (id +₁ coit w ∘ ⟨ D.μ.η X , D₁ ! ⟩) ∘ out
      coit-helper = begin 
        out ∘ coit w ∘ ⟨ D.μ.η X , D₁ ! ⟩                 ≈⟨ extendʳ (coit-commutes w) ⟩ 
        (id +₁ coit w) ∘ w ∘ ⟨ D.μ.η X , D₁ ! ⟩           ≈⟨ refl⟩∘⟨ (D-jointly-epic now-helper later-helper) ⟩ 
        (id +₁ coit w) ∘ (id +₁ ⟨ D.μ.η X , D₁ ! ⟩) ∘ out ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² refl) ⟩ 
        (id +₁ coit w ∘ ⟨ D.μ.η X , D₁ ! ⟩) ∘ out         ∎
        where
        now-helper : (w ∘ ⟨ D.μ.η X , D₁ ! ⟩) ∘ now ≈ ((id +₁ ⟨ D.μ.η X , D₁ ! ⟩) ∘ out) ∘ now
        now-helper = begin 
          (w ∘ ⟨ D.μ.η X , D₁ ! ⟩) ∘ now           ≈⟨ pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ D.identityʳ (sym (D.η.commute !))) ⟩ 
          w ∘ ⟨ id , now ∘ ! ⟩                     ≈˘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identity² refl) ⟩ 
          w ∘ (id ⁂ now) ∘ ⟨ id , ! ⟩              ≈⟨ extendʳ w-now ⟩
          i₁ ∘ π₁ ∘ ⟨ id , ! ⟩                     ≈⟨ elimʳ project₁ ⟩
          i₁                                       ≈˘⟨ inject₁ ○ identityʳ ⟩ 
          (id +₁ ⟨ D.μ.η X , D₁ ! ⟩) ∘ i₁          ≈˘⟨ pullʳ unitlaw ⟩ 
          ((id +₁ ⟨ D.μ.η X , D₁ ! ⟩) ∘ out) ∘ now ∎
        later-helper : (w ∘ ⟨ D.μ.η X , D₁ ! ⟩) ∘ later ≈ ((id +₁ ⟨ D.μ.η X , D₁ ! ⟩) ∘ out) ∘ later
        later-helper = begin 
          (w ∘ ⟨ D.μ.η X , D₁ ! ⟩) ∘ later                 ≈⟨ pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ (sym identityˡ) (sym (later-extend-comm (now ∘ !))) ○ sym ⁂∘⟨⟩) ⟩ 
          w ∘ (id ⁂ later) ∘ ⟨ D.μ.η X ∘ later , D₁ ! ⟩    ≈⟨ extendʳ w-later ⟩ 
          i₂ ∘ (earlier ⁂ id) ∘ ⟨ D.μ.η X ∘ later , D₁ ! ⟩ ≈⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ (∘-resp-≈ʳ (sym (later-extend-comm id)) ○ cancelˡ earlier∘later) identityˡ) ⟩ 
          i₂ ∘ ⟨ D.μ.η X , D₁ ! ⟩                          ≈˘⟨ inject₂ ⟩ 
          (id +₁ ⟨ D.μ.η X , D₁ ! ⟩) ∘ i₂                  ≈˘⟨ pullʳ laterlaw ⟩ 
          ((id +₁ ⟨ D.μ.η X , D₁ ! ⟩) ∘ out) ∘ later       ∎

    w-u-commute : ∀ (h : X × N ⇒ D₀ X) → h ∘ (id ⁂ monus) ≈ earlier ∘ h → w ∘ (extend h ⁂ id) ≈ (extend h +₁ (extend h ⁂ id)) ∘ u
    w-u-commute h earlier-monus = sym (D-jointly-epic-product case₁ case₂ case₃ case₄)
      where 
      case₁₂ : ((extend h +₁ (extend h ⁂ id)) ∘ u) ∘ (id ⁂ now) ≈ (w ∘ (extend h ⁂ id)) ∘ (id ⁂ now)
      case₁₂ = begin 
        ((extend h +₁ (extend h ⁂ id)) ∘ u) ∘ (id ⁂ now) ≈⟨ pullʳ u-now ⟩ 
        (extend h +₁ (extend h ⁂ id)) ∘ i₁ ∘ π₁          ≈⟨ extendʳ inject₁ ⟩ 
        i₁ ∘ extend h ∘ π₁                               ≈˘⟨ refl⟩∘⟨ project₁ ⟩ 
        i₁ ∘ π₁ ∘ (extend h ⁂ id)                        ≈˘⟨ extendʳ w-now ⟩ 
        w ∘ (id ⁂ now) ∘ (extend h ⁂ id)                 ≈˘⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ id-comm id-comm-sym ○ sym ⁂∘⁂) ⟩ 
        (w ∘ (extend h ⁂ id)) ∘ (id ⁂ now)               ∎
      case₁ : ((extend h +₁ (extend h ⁂ id)) ∘ u) ∘ (now ⁂ now) ≈ (w ∘ (extend h ⁂ id)) ∘ (now ⁂ now)
      case₁ = begin 
        ((extend h +₁ (extend h ⁂ id)) ∘ u) ∘ (now ⁂ now)             ≈˘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identityˡ identityʳ) ⟩ 
        ((extend h +₁ (extend h ⁂ id)) ∘ u) ∘ (id ⁂ now) ∘ (now ⁂ id) ≈⟨ extendʳ case₁₂ ⟩ 
        (w ∘ (extend h ⁂ id)) ∘ (id ⁂ now) ∘ (now ⁂ id)               ≈⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identityˡ identityʳ) ⟩ 
        (w ∘ (extend h ⁂ id)) ∘ (now ⁂ now)                           ∎
      case₂ : ((extend h +₁ (extend h ⁂ id)) ∘ u) ∘ (later ⁂ now) ≈ (w ∘ (extend h ⁂ id)) ∘ (later ⁂ now)
      case₂ = begin 
        ((extend h +₁ (extend h ⁂ id)) ∘ u) ∘ (later ⁂ now)             ≈˘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identityˡ identityʳ) ⟩ 
        ((extend h +₁ (extend h ⁂ id)) ∘ u) ∘ (id ⁂ now) ∘ (later ⁂ id) ≈⟨ extendʳ case₁₂ ⟩ 
        (w ∘ (extend h ⁂ id)) ∘ (id ⁂ now) ∘ (later ⁂ id)               ≈⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identityˡ identityʳ) ⟩ 
        (w ∘ (extend h ⁂ id)) ∘ (later ⁂ now)                           ∎
      case₃ : ((extend h +₁ (extend h ⁂ id)) ∘ u) ∘ (now ⁂ later) ≈ (w ∘ (extend h ⁂ id)) ∘ (now ⁂ later)
      case₃ = begin 
        ((extend h +₁ (extend h ⁂ id)) ∘ u) ∘ (now ⁂ later)                                                                                                             ≈˘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identityˡ identityʳ) ⟩ 
        ((extend h +₁ (extend h ⁂ id)) ∘ u) ∘ (id ⁂ later) ∘ (now ⁂ id)                                                                                                 ≈⟨ pullʳ (pullˡ (pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² laterlaw)))) ⟩ 
        (extend h +₁ (extend h ⁂ id)) ∘ ([ (i₁ ∘ π₁) , [ i₂ ∘ (now ∘ (id ⁂ monus) ⁂ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ id) ] ∘ distributeˡ⁻¹ ∘ (id ⁂ i₂)) ∘ (now ⁂ id) ≈⟨ refl⟩∘⟨ ((refl⟩∘⟨ distributeˡ⁻¹-i₂) ⟩∘⟨refl) ⟩ 
        (extend h +₁ (extend h ⁂ id)) ∘ ([ (i₁ ∘ π₁) , [ i₂ ∘ (now ∘ (id ⁂ monus) ⁂ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ id) ] ∘ i₂) ∘ (now ⁂ id)                        ≈⟨ refl⟩∘⟨ (∘-resp-≈ˡ inject₂ ○ assoc²βε) ⟩ 
        (extend h +₁ (extend h ⁂ id)) ∘ [ i₂ ∘ (now ∘ (id ⁂ monus) ⁂ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ id) ∘ (now ⁂ id)                                               ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ unitlaw identity²) ⟩ 
        (extend h +₁ (extend h ⁂ id)) ∘ [ i₂ ∘ (now ∘ (id ⁂ monus) ⁂ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (i₁ ⁂ id)                                                             ≈⟨ refl⟩∘⟨ refl⟩∘⟨ distributeʳ⁻¹-i₁ ⟩ 
        (extend h +₁ (extend h ⁂ id)) ∘ [ i₂ ∘ (now ∘ (id ⁂ monus) ⁂ id) , i₂ ] ∘ i₁                                                                                    ≈⟨ refl⟩∘⟨ inject₁ ⟩ 
        (extend h +₁ (extend h ⁂ id)) ∘ i₂ ∘ (now ∘ (id ⁂ monus) ⁂ id)                                                                                                  ≈⟨ extendʳ inject₂ ⟩ 
        i₂ ∘ (extend h ⁂ id) ∘ (now ∘ (id ⁂ monus) ⁂ id)                                                                                                                ≈⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ (pullˡ DK.identityʳ) identity²) ⟩ 
        i₂ ∘ (h ∘ (id ⁂ monus) ⁂ id)                                                                                                                                    ≈⟨ refl⟩∘⟨ ⁂-cong₂ earlier-monus refl ⟩ 
        i₂ ∘ (earlier ∘ h ⁂ id)                                                                                                                                         ≈˘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identity²) ⟩ 
        i₂ ∘ (earlier ⁂ id) ∘ (h ⁂ id)                                                                                                                                  ≈˘⟨ extendʳ w-later ⟩ 
        w ∘ (id ⁂ later) ∘ (h ⁂ id)                                                                                                                                     ≈˘⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ (DK.identityʳ ○ sym identityˡ) id-comm-sym ○ sym ⁂∘⁂) ⟩ 
        (w ∘ (extend h ⁂ id)) ∘ (now ⁂ later)                                                                                                                           ∎
      case₄ : ((extend h +₁ (extend h ⁂ id)) ∘ u) ∘ (later ⁂ later) ≈ (w ∘ (extend h ⁂ id)) ∘ (later ⁂ later)
      case₄ = begin 
        ((extend h +₁ (extend h ⁂ id)) ∘ u) ∘ (later ⁂ later) ≈⟨ pullʳ u-later ⟩ 
        (extend h +₁ (extend h ⁂ id)) ∘ i₂                    ≈⟨ inject₂ ⟩ 
        i₂ ∘ (extend h ⁂ id)                                  ≈˘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ (∘-resp-≈ʳ (sym (later-extend-comm h)) ○ cancelˡ earlier∘later) identity²) ⟩ 
        i₂ ∘ (earlier ⁂ id) ∘ (extend h ∘ later ⁂ id)         ≈˘⟨ extendʳ w-later ⟩ 
        w ∘ (id ⁂ later) ∘ (extend h ∘ later ⁂ id)            ≈˘⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ (sym identityˡ) id-comm-sym ○ sym ⁂∘⁂) ⟩ 
        (w ∘ (extend h ⁂ id)) ∘ (later ⁂ later)               ∎

    coit-w-u-commute-ι : coit w ∘ (extend ι ⁂ id) ≈ D₁ (extend ι) ∘ coit u
    coit-w-u-commute-ι = begin 
      coit w ∘ (extend ι ⁂ id)    ≈˘⟨ coit-unique ((extend ι +₁ id) ∘ u) (coit w ∘ (extend ι ⁂ id)) unique₁ ⟩ 
      coit ((extend ι +₁ id) ∘ u) ≈⟨ coit-unique ((extend ι +₁ id) ∘ u) (D₁ (extend ι) ∘ coit u) unique₂ ⟩ 
      D₁ (extend ι) ∘ coit u      ∎
      where
      earlier-monus : ι ∘ (id ⁂ monus) ≈ earlier ∘ ι {X}
      earlier-monus = begin 
        ι ∘ (id ⁂ monus) ≈⟨ PNNO-jointly-epic IB IS ⟩ 
        earlier ∘ ι {X} ∎
        where
        IB : (ι ∘ (id ⁂ monus)) ∘ ⟨ id , z ∘ ! ⟩ ≈ (earlier ∘ ι {X}) ∘ ⟨ id , z ∘ ! ⟩
        IB = begin 
          (ι ∘ (id ⁂ monus)) ∘ ⟨ id , z ∘ ! ⟩ ≈⟨ pullʳ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identity² (pullˡ monus-zero)) ⟩ 
          ι ∘ ⟨ id , z ∘ ! ⟩                  ≈⟨ ι-zero ⟩ 
          now                                 ≈˘⟨ inject₁ ⟩
          [ now , id ] ∘ i₁                   ≈˘⟨ pullʳ unitlaw ⟩ 
          ([ now , id ] ∘ out) ∘ now          ≈˘⟨ pullʳ ι-zero ⟩ 
          (earlier ∘ ι {X}) ∘ ⟨ id , z ∘ ! ⟩  ∎
        IS : (ι ∘ (id ⁂ monus)) ∘ (id ⁂ s) ≈ (earlier ∘ ι {X}) ∘ (id ⁂ s)
        IS = begin 
          (ι ∘ (id ⁂ monus)) ∘ (id ⁂ s) ≈⟨ cancelʳ (⁂∘⁂ ○ ⁂-cong₂ identity² monus-succ ○ ⟨⟩-unique id-comm id-comm) ⟩ 
          ι                             ≈˘⟨ cancelˡ earlier∘later ⟩
          earlier ∘ later ∘ ι           ≈˘⟨ pullʳ ι-succ ⟩
          (earlier ∘ ι) ∘ (id ⁂ s)      ∎
      unique₁ : out ∘ coit w ∘ (extend ι ⁂ id) ≈ (id +₁ coit w ∘ (extend ι ⁂ id)) ∘ (extend ι +₁ id) ∘ u
      unique₁ = begin 
        out ∘ coit w ∘ (extend ι ⁂ id)                          ≈⟨ extendʳ (coit-commutes w) ⟩ 
        (id +₁ coit w) ∘ w ∘ (extend ι ⁂ id)                    ≈⟨ refl⟩∘⟨ w-u-commute ι earlier-monus ⟩ 
        (id +₁ coit w) ∘ (extend ι +₁ (extend ι ⁂ id)) ∘ u      ≈⟨ extendʳ (+₁∘+₁ ○ +₁-cong₂ refl (sym identityʳ) ○ sym +₁∘+₁) ⟩ 
        (id +₁ coit w ∘ (extend ι ⁂ id)) ∘ (extend ι +₁ id) ∘ u ∎
      unique₂ : out ∘ D₁ (extend ι) ∘ coit u ≈ (id +₁ D₁ (extend ι) ∘ coit u) ∘ (extend ι +₁ id) ∘ u
      unique₂ = begin 
        out ∘ D₁ (extend ι) ∘ coit u                          ≈⟨ extendʳ (D₁-commutes (extend ι)) ⟩ 
        (extend ι +₁ D₁ (extend ι)) ∘ out ∘ coit u            ≈⟨ refl⟩∘⟨ (coit-commutes u) ⟩ 
        (extend ι +₁ D₁ (extend ι)) ∘ (id +₁ coit u) ∘ u      ≈⟨ extendʳ (+₁∘+₁ ○ +₁-cong₂ id-comm (sym identityʳ) ○ sym +₁∘+₁) ⟩ 
        (id +₁ D₁ (extend ι) ∘ coit u) ∘ (extend ι +₁ id) ∘ u ∎

    coit-w-u-commute-Dπ₁ : coit w ∘ (D₁ π₁ ⁂ id) ≈ D₁ (D₁ π₁) ∘ coit u
    coit-w-u-commute-Dπ₁ = begin 
      coit w ∘ (D₁ π₁ ⁂ id)    ≈˘⟨ coit-unique ((D₁ π₁ +₁ id) ∘ u) (coit w ∘ (D₁ π₁ ⁂ id)) unique₁ ⟩ 
      coit ((D₁ π₁ +₁ id) ∘ u) ≈⟨ coit-unique ((D₁ π₁ +₁ id) ∘ u) (D₁ (D₁ π₁) ∘ coit u) unique₂ ⟩ 
      D₁ (D₁ π₁) ∘ coit u      ∎
      where
      earlier-monus : (now ∘ π₁) ∘ (id ⁂ monus) ≈ earlier ∘ (now ∘ π₁)
      earlier-monus = begin 
        (now ∘ π₁) ∘ (id ⁂ monus) ≈⟨ pullʳ (project₁ ○ identityˡ) ⟩
        now ∘ π₁                  ≈˘⟨ pullˡ earlier∘now ⟩ 
        earlier ∘ (now ∘ π₁)      ∎
      unique₁ : out ∘ coit w ∘ (D₁ π₁ ⁂ id) ≈ (id +₁ coit w ∘ (D₁ π₁ ⁂ id)) ∘ (D₁ π₁ +₁ id) ∘ u
      unique₁ = begin 
        out ∘ coit w ∘ (D₁ π₁ ⁂ id)                       ≈⟨ extendʳ (coit-commutes w) ⟩ 
        (id +₁ coit w) ∘ w ∘ (D₁ π₁ ⁂ id)                 ≈⟨ refl⟩∘⟨ (w-u-commute (now ∘ π₁) earlier-monus) ⟩ 
        (id +₁ coit w) ∘ (D₁ π₁ +₁ (D₁ π₁ ⁂ id)) ∘ u      ≈⟨ extendʳ (+₁∘+₁ ○ +₁-cong₂ refl (sym identityʳ) ○ sym +₁∘+₁) ⟩ 
        (id +₁ coit w ∘ (D₁ π₁ ⁂ id)) ∘ (D₁ π₁ +₁ id) ∘ u ∎
      unique₂ : out ∘ D₁ (D₁ π₁) ∘ coit u ≈ (id +₁ D₁ (D₁ π₁) ∘ coit u) ∘ (D₁ π₁ +₁ id) ∘ u
      unique₂ = begin
        out ∘ D₁ (D₁ π₁) ∘ coit u                       ≈⟨ extendʳ (D₁-commutes (D₁ π₁)) ⟩ 
        (D₁ π₁ +₁ D₁ (D₁ π₁)) ∘ out ∘ coit u            ≈⟨ refl⟩∘⟨ (coit-commutes u) ⟩ 
        (D₁ π₁ +₁ D₁ (D₁ π₁)) ∘ (id +₁ coit u) ∘ u      ≈⟨ extendʳ (+₁∘+₁ ○ +₁-cong₂ id-comm (sym identityʳ) ○ sym +₁∘+₁) ⟩ 
        (id +₁ D₁ (D₁ π₁) ∘ coit u) ∘ (D₁ π₁ +₁ id) ∘ u ∎

    coit-w-ρ : D₁ ρ ∘ coit w ≈ D₁ π₁ ∘ τ ∘ (ρ ⁂ id)
    coit-w-ρ = begin 
      D₁ ρ ∘ coit w        ≈˘⟨ coit-unique ((ρ +₁ id) ∘ w) (D₁ ρ ∘ coit w) unique₁ ⟩ 
      coit ((ρ +₁ id) ∘ w) ≈⟨ coit-unique ((ρ +₁ id) ∘ w) (D₁ π₁ ∘ τ ∘ (ρ ⁂ id)) unique₂ ⟩ 
      D₁ π₁ ∘ τ ∘ (ρ ⁂ id) ∎
      where
      unique₁ : out ∘ D₁ ρ ∘ coit w ≈ (id +₁ D₁ ρ ∘ coit w) ∘ (ρ +₁ id) ∘ w
      unique₁ = begin 
        out ∘ D₁ ρ ∘ coit w ≈⟨ extendʳ (D₁-commutes ρ) ⟩ 
        (ρ +₁ D₁ ρ) ∘ out ∘ coit w            ≈⟨ refl⟩∘⟨ coit-commutes w ⟩ 
        (ρ +₁ D₁ ρ) ∘ (id +₁ coit w) ∘ w      ≈⟨ extendʳ (+₁∘+₁ ○ +₁-cong₂ id-comm (sym identityʳ) ○ sym +₁∘+₁) ⟩ 
        (id +₁ D₁ ρ ∘ coit w) ∘ (ρ +₁ id) ∘ w ∎
      unique₂ : out ∘ D₁ π₁ ∘ τ ∘ (ρ ⁂ id) ≈ (id +₁ D₁ π₁ ∘ τ ∘ (ρ ⁂ id)) ∘ (ρ +₁ id) ∘ w
      unique₂ = begin 
        out ∘ D₁ π₁ ∘ τ ∘ (ρ ⁂ id)                                               ≈⟨ extendʳ (D₁-commutes π₁) ⟩ 
        (π₁ +₁ D₁ π₁) ∘ out ∘ τ ∘ (ρ ⁂ id)                                       ≈⟨ refl⟩∘⟨ extendʳ τ-commutes ⟩ 
        (π₁ +₁ D₁ π₁) ∘ (id +₁ τ) ∘ (distributeˡ⁻¹ ∘ (id ⁂ out)) ∘ (ρ ⁂ id)      ≈⟨ extendʳ (+₁∘+₁ ○ +₁-cong₂ id-comm (sym identityʳ) ○ sym +₁∘+₁) ⟩ 
        (id +₁ D₁ π₁ ∘ τ) ∘ (π₁ +₁ id) ∘ (distributeˡ⁻¹ ∘ (id ⁂ out)) ∘ (ρ ⁂ id) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identityˡ identityʳ)) ⟩ 
        (id +₁ D₁ π₁ ∘ τ) ∘ (π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (ρ ⁂ out)               ≈⟨ refl⟩∘⟨ helper ⟩ 
        (id +₁ D₁ π₁ ∘ τ) ∘ (ρ +₁ (ρ ⁂ id)) ∘ w                                  ≈⟨ extendʳ (+₁∘+₁ ○ +₁-cong₂ refl (assoc ○ sym identityʳ) ○ sym +₁∘+₁) ⟩ 
        (id +₁ D₁ π₁ ∘ τ ∘ (ρ ⁂ id)) ∘ (ρ +₁ id) ∘ w                             ∎
        where
        helper : (π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (ρ ⁂ out) ≈ (ρ +₁ (ρ ⁂ id)) ∘ w
        helper = sym (begin 
          (ρ +₁ (ρ ⁂ id)) ∘ [ i₁ ∘ π₁ , i₂ ∘ (earlier ⁂ id) ] ∘ distributeˡ⁻¹ ∘ (id ⁂ out) ≈⟨ pullˡ (∘[] ○ []-cong₂ (extendʳ inject₁) (extendʳ inject₂ ○ ∘-resp-≈ʳ (⁂∘⁂ ○ ⁂-cong₂ refl identity²))) ⟩ 
          [ i₁ ∘ ρ ∘ π₁ , i₂ ∘ (ρ ∘ earlier ⁂ id) ] ∘ distributeˡ⁻¹ ∘ (id ⁂ out)           ≈˘⟨ ([]-cong₂ (∘-resp-≈ʳ project₁) (∘-resp-≈ʳ (⁂-cong₂ (sym ρ-earlier) refl))) ⟩∘⟨refl ⟩ 
          [ i₁ ∘ π₁ ∘ (ρ ⁂ id) , i₂ ∘ (ρ ⁂ id) ] ∘ distributeˡ⁻¹ ∘ (id ⁂ out)              ≈˘⟨ pullˡ ([]∘+₁ ○ []-cong₂ assoc refl) ⟩
          [ i₁ ∘ π₁ , i₂ ] ∘ (ρ ⁂ id +₁ ρ ⁂ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ out)               ≈⟨ refl⟩∘⟨ (extendʳ (distributeˡ⁻¹-natural ρ id id)) ⟩ 
          [ i₁ ∘ π₁ , i₂ ] ∘ distributeˡ⁻¹ ∘ (ρ ⁂ (id +₁ id)) ∘ (id ⁂ out)                 ≈⟨ ([]-cong₂ refl (sym identityʳ)) ⟩∘⟨ ∘-resp-≈ʳ (⁂∘⁂ ○ ⁂-cong₂ identityʳ (elimˡ ([]-unique id-comm-sym id-comm-sym))) ⟩ 
         (π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (ρ ⁂ out)                                           ∎)

  3⇒1 : (∀ X → cond-3 X) → cond-1
  3⇒1 c-3 X = record
    { equality = sym D.F.homomorphism ○ D.F.F-resp-≈ (Coequalizer.equality (coeqs X)) ○ D.F.homomorphism
    ; coequalize = b
    ; universal = λ {Z} {h} {eq} → universal' eq 
    ; unique = λ {Z} {h} {i} {eq} i-universal → epi-Dρ (Search-Algebra.search-algebra-on (Elgot⇒Search (record { A = Ď₀ X ; algebra = elgot }))) i (b eq) (sym i-universal ○ universal' eq)
    }
    where
      open cond-3 (c-3 X) using (elgot; ρ-algebra-morphism)
      open Search-Algebra (Elgot⇒Search (record { A = Ď₀ X ; algebra = elgot })) using (α)
      open import Monad.Instance.Delay.Quotient.Epis distributive DM PNNO DQ
      module CP = IsCoequalizer (coeq-productsˡ {X} {D₀ ⊤} (id))
      module _ {Y : Obj} {a : D₀ (D₀ X) ⇒ Y} (eq : a ∘ D₁ (extend ι) ≈ a ∘ D₁ (D₁ π₁)) where
        c : Ď₀ X × D₀ ⊤ ⇒ Y
        c = CP.coequalize (begin 
          (a ∘ coit w) ∘ (extend ι ⁂ id) ≈⟨ pullʳ coit-w-u-commute-ι ⟩ 
          a ∘ D₁ (extend ι) ∘ coit u    ≈⟨ extendʳ eq ⟩ 
          a ∘ D₁ (D₁ π₁) ∘ coit u       ≈˘⟨ pullʳ coit-w-u-commute-Dπ₁ ⟩ 
          (a ∘ coit w) ∘ (D₁ π₁ ⁂ id)   ∎)
        b : D₀ (Ď₀ X) ⇒ Y
        b = c ∘ ⟨ α , D₁ ! ⟩
        universal' : a ≈ b ∘ D₁ ρ
        universal' = sym (begin 
          b ∘ D₁ ρ                                             ≈⟨ introʳ coit-w-retract ⟩ 
          (b ∘ D₁ ρ) ∘ coit w ∘ ⟨ D.μ.η _ , D₁ ! ⟩             ≈⟨ pullʳ (extendʳ coit-w-ρ) ⟩ 
          b ∘ D₁ π₁ ∘ (τ ∘ (ρ ⁂ id)) ∘ ⟨ D.μ.η _ , D₁ ! ⟩      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullʳ upper-square ⟩ 
          (c ∘ ⟨ α , D₁ ! ⟩) ∘ D₁ π₁ ∘ τ ∘ ⟨ α , D₁ ! ⟩ ∘ D₁ ρ ≈⟨ refl⟩∘⟨ (sym-assoc ○ cancelˡ (assoc ○ retract-helper)) ⟩
          (c ∘ ⟨ α , D₁ ! ⟩) ∘ D₁ ρ                            ≈⟨ pullʳ (sym upper-square) ⟩ 
          c ∘ (ρ ⁂ id) ∘ ⟨ D.μ.η _ , D₁ ! ⟩                    ≈˘⟨ extendʳ CP.universal ⟩ 
          a ∘ coit w ∘ ⟨ D.μ.η _ , D₁ ! ⟩                      ≈⟨ elimʳ coit-w-retract ⟩ 
          a                                                    ∎)
          where
          open import Algebra.Search.Retraction distributive DM using (tau-retract)
          retract-helper : D₁ π₁ ∘ τ ∘ ⟨ α , D₁ ! ⟩ ≈ id
          retract-helper = begin 
            D₁ π₁ ∘ τ ∘ ⟨ α , D₁ ! ⟩                          ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ elimʳ (sym D.F.homomorphism ○ D.F.F-resp-≈ (Iso.isoʳ (_≅_.iso A×⊤≅A)) ○ D.F.identity) ⟩ 
            D₁ π₁ ∘ τ ∘ ⟨ α , D₁ ! ⟩ ∘ D₁ π₁ ∘ D₁ ⟨ id , ! ⟩  ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (⟨⟩∘ ○ ⟨⟩-cong₂ refl (sym D.F.homomorphism ○ D.F.F-resp-≈ !-unique₂)) ⟩ 
            D₁ π₁ ∘ τ ∘ ⟨ α ∘ D₁ π₁ , D₁ π₂ ⟩ ∘ D₁ ⟨ id , ! ⟩ ≈⟨ refl⟩∘⟨ (cancelˡ (Retract.is-retract (tau-retract ⊤ (Elgot⇒Search (record { A = Ď₀ X ; algebra = elgot }))))) ⟩ 
            D₁ π₁ ∘ D₁ ⟨ id , ! ⟩                             ≈⟨ sym D.F.homomorphism ○ D.F.F-resp-≈ (Iso.isoʳ (_≅_.iso A×⊤≅A)) ○ D.F.identity ⟩ 
            id                                                ∎
          upper-square : (ρ ⁂ id) ∘ ⟨ D.μ.η _ , D₁ ! ⟩ ≈ ⟨ α , D₁ ! ⟩ ∘ D₁ ρ
          upper-square = ⁂∘⟨⟩ ○ ⟨⟩-cong₂ ρ-algebra-morphism (identityˡ ○ D.F.F-resp-≈ (!-unique (! ∘ ρ)) ○ D.F.homomorphism) ○ sym ⟨⟩∘