open import Categories.Category
open import Monad.Instance.Delay
open import Categories.Category.Cartesian using (Cartesian)
open import Categories.Category.Extensive using (Extensive)
open import Categories.Category.Extensive.Properties.Distributive
open import Categories.Object.NaturalNumbers.Parametrized

open import Level using (_⊔_)
open import Data.Product using (Σ-syntax; _,_; proj₁; proj₂)

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

module Monad.Instance.Delay.LPO {o ℓ e} {C : Category o ℓ e}
    (extensive : Extensive C) (cartesian : Cartesian C)
    (D : DelayM (Extensive.cocartesian extensive))
    (PNNO : ParametrizedNNO C cartesian) where

    open Category C
    private distributive = Extensive×Cartesian⇒Distributive C extensive cartesian
    open import Category.Distributive.Helper distributive hiding (cartesian)
    open Bundles
    open DelayM D
    open HomReasoning
    open Equiv
    open D-Monad
    open D-Kleisli
    open Later∘Extend
    open Coit

    open M C
    open MR C
    open MP C

    open ParametrizedNNO PNNO renaming (unique to pnno-unique)

    open import Monad.Instance.Delay.Iota distributive D PNNO
    open import Monad.Instance.Delay.Pullbacks extensive cartesian D
    open import Monad.Instance.Delay.Cartesian extensive cartesian D using (D-preserves-pullback)
    open import Categories.Category.Cocartesian.Monoidal
    open CocartesianMonoidal cocartesian using (⊥+A≅A)

    open import Monad.Instance.Delay.Zip distributive D

    -- ∞ : the always-divergent computation (paper's ∞ : 1 → DX)
    ∞ : ∀ {X} → ⊤ ⇒ D₀ X
    ∞ = coit i₂

    ∞-commutes : ∀ {X} → out ∘ ∞ {X} ≈ (id +₁ ∞) ∘ i₂
    ∞-commutes = coit-commutes i₂

    ∞-later : ∀ {X} → ∞ {X} ≈ later ∘ ∞
    ∞-later = begin
      ∞                         ≈⟨ cancelˡ out⁻¹∘out ⟨
      out⁻¹ ∘ out ∘ ∞           ≈⟨ refl⟩∘⟨ ∞-commutes ⟩
      out⁻¹ ∘ (id +₁ ∞) ∘ i₂    ≈⟨ pushʳ inject₂ ⟩
      later ∘ ∞                 ∎

    -- ∞ is natural: D f ∘ ∞{X} = ∞{Y} (both (⊤,i₂)→(DY,out) coalgebra maps)
    ∞-natural : ∀ {X Y} (f : X ⇒ Y) → D.F.₁ f ∘ ∞ {X} ≈ ∞ {Y}
    ∞-natural f = sym (coit-unique i₂ (D.F.₁ f ∘ ∞) (begin
      out ∘ D.F.₁ f ∘ ∞                        ≈⟨ pullˡ (D₁-commutes f) ⟩
      ((f +₁ D.F.₁ f) ∘ out) ∘ ∞               ≈⟨ pullʳ ∞-commutes ⟩
      (f +₁ D.F.₁ f) ∘ (id +₁ ∞) ∘ i₂          ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityʳ refl) ⟩
      (f +₁ (D.F.₁ f ∘ ∞)) ∘ i₂                ≈⟨ inject₂ ○ sym inject₂ ⟩
      (id +₁ (D.F.₁ f ∘ ∞)) ∘ i₂               ∎))

    -- copairing, named to avoid the clash between the closed operator [_,_]
    -- and the postfix hom-notation _[_,_] when used as an argument.
    copair : ∀ {A B Z} → A ⇒ Z → B ⇒ Z → A + B ⇒ Z
    copair f g = [ f , g ]

    -- [ι,∞] : X×ℕ + 1 → DX
    [ι,∞] : ∀ {X} → (X × N) + ⊤ ⇒ D₀ X
    [ι,∞] = copair ι ∞

    -- coproduct of isos is an iso
    +₁-iso : ∀ {A B A' B'} {f : A ⇒ A'} {g : B ⇒ B'} → IsIso f → IsIso g → IsIso (f +₁ g)
    +₁-iso {f = f} {g = g} fi gi .M.IsIso.inv = IsIso.inv fi +₁ IsIso.inv gi
    +₁-iso {f = f} {g = g} fi gi .M.IsIso.iso .M.Iso.isoˡ = begin
            (IsIso.inv fi +₁ IsIso.inv gi) ∘ (f +₁ g)         ≈⟨ +₁∘+₁ ⟩
            (IsIso.inv fi ∘ f) +₁ (IsIso.inv gi ∘ g)          ≈⟨ +₁-cong₂ (Iso.isoˡ (IsIso.iso fi)) (Iso.isoˡ (IsIso.iso gi)) ⟩
            id +₁ id                                          ≈⟨ id+₁id ⟩
            id                                                ∎
    +₁-iso {f = f} {g = g} fi gi .M.IsIso.iso .M.Iso.isoʳ = begin
            (f +₁ g) ∘ (IsIso.inv fi +₁ IsIso.inv gi)         ≈⟨ +₁∘+₁ ⟩
            (f ∘ IsIso.inv fi) +₁ (g ∘ IsIso.inv gi)          ≈⟨ +₁-cong₂ (Iso.isoʳ (IsIso.iso fi)) (Iso.isoʳ (IsIso.iso gi)) ⟩
            id +₁ id                                          ≈⟨ id+₁id ⟩
            id                                                ∎

    open import Categories.Diagram.Pullback C using (IsPullback; Pullback)
    open import Categories.Object.Coproduct C using (IsCoproduct)
    open import Categories.Category.Extensive.Properties C as EP

    -- post-composing both legs of a cospan with a mono preserves pullbacks
    pb-post-mono : ∀ {P A B Q R} {p₁ : P ⇒ A} {p₂ : P ⇒ B} {f : A ⇒ Q} {g : B ⇒ Q} {m : Q ⇒ R}
      → Mono m → IsPullback p₁ p₂ f g → IsPullback p₁ p₂ (m ∘ f) (m ∘ g)
    pb-post-mono m-mono pb .IsPullback.commute           = extendˡ (IsPullback.commute pb)
    pb-post-mono m-mono pb .IsPullback.universal         = λ eq → IsPullback.universal pb (m-mono _ _ (sym-assoc ○ eq ○ assoc))
    pb-post-mono m-mono pb .IsPullback.p₁∘universal≈h₁   = IsPullback.p₁∘universal≈h₁ pb
    pb-post-mono m-mono pb .IsPullback.p₂∘universal≈h₂   = IsPullback.p₂∘universal≈h₂ pb
    pb-post-mono m-mono pb .IsPullback.unique-diagram    = IsPullback.unique-diagram pb

    IsPullback-resp-≈ : ∀ {P A B Q} {p₁ : P ⇒ A} {p₂ : P ⇒ B} {f f' : A ⇒ Q} {g g' : B ⇒ Q}
      → f ≈ f' → g ≈ g' → IsPullback p₁ p₂ f g → IsPullback p₁ p₂ f' g'
    IsPullback-resp-≈ ef eg pb .IsPullback.commute         = ∘-resp-≈ˡ (sym ef) ○ IsPullback.commute pb ○ ∘-resp-≈ˡ eg
    IsPullback-resp-≈ ef eg pb .IsPullback.universal       = λ eq → IsPullback.universal pb ( ∘-resp-≈ˡ ef ○ eq ○ (∘-resp-≈ˡ (sym eg)) ) 
    IsPullback-resp-≈ ef eg pb .IsPullback.p₁∘universal≈h₁ = IsPullback.p₁∘universal≈h₁ pb
    IsPullback-resp-≈ ef eg pb .IsPullback.p₂∘universal≈h₂ = IsPullback.p₂∘universal≈h₂ pb
    IsPullback-resp-≈ ef eg pb .IsPullback.unique-diagram  = IsPullback.unique-diagram pb

    -- transport a pullback along an iso on its vertex
    pb-vertex-iso : ∀ {V V' A B Q} {p₁ : V ⇒ A} {p₂ : V ⇒ B} {f : A ⇒ Q} {g : B ⇒ Q} {σ : V' ⇒ V}
      → IsIso σ → IsPullback p₁ p₂ f g → IsPullback (p₁ ∘ σ) (p₂ ∘ σ) f g
    pb-vertex-iso {p₁ = p₁} {p₂} {σ = σ} σiso pb .IsPullback.commute          = extendʳ (IsPullback.commute pb)
    pb-vertex-iso {p₁ = p₁} {p₂} {σ = σ} σiso pb .IsPullback.universal        = λ eq → IsIso.inv σiso ∘ IsPullback.universal pb eq
    pb-vertex-iso {p₁ = p₁} {p₂} {σ = σ} σiso pb .IsPullback.p₁∘universal≈h₁  = cancelInner (Iso.isoʳ (IsIso.iso σiso)) ○ IsPullback.p₁∘universal≈h₁ pb
    pb-vertex-iso {p₁ = p₁} {p₂} {σ = σ} σiso pb .IsPullback.p₂∘universal≈h₂  = cancelInner (Iso.isoʳ (IsIso.iso σiso)) ○ IsPullback.p₂∘universal≈h₂ pb
    pb-vertex-iso {p₁ = p₁} {p₂} {σ = σ} σiso pb .IsPullback.unique-diagram   = λ eq₁ eq₂ → Iso⇒Mono (IsIso.iso σiso) _ _
          (IsPullback.unique-diagram pb (sym-assoc ○ eq₁ ○ assoc) (sym-assoc ○ eq₂ ○ assoc))

    -- transport a pullback by precomposing one cospan leg with an iso
    pb-cospan-iso : ∀ {V A B B' Q} {p₁ : V ⇒ A} {p₂ : V ⇒ B} {f : A ⇒ Q} {g : B ⇒ Q} {m : B' ⇒ B}
      → (miso : IsIso m) → IsPullback p₁ p₂ f g → IsPullback p₁ (IsIso.inv miso ∘ p₂) f (g ∘ m)
    pb-cospan-iso {p₂ = p₂} {g = g} {m = m} miso pb .IsPullback.commute           = IsPullback.commute pb ○ sym (cancelInner (Iso.isoʳ (IsIso.iso miso)))
    pb-cospan-iso {p₂ = p₂} {g = g} {m = m} miso pb .IsPullback.universal         = λ eq → IsPullback.universal pb (eq ○ assoc)
    pb-cospan-iso {p₂ = p₂} {g = g} {m = m} miso pb .IsPullback.p₁∘universal≈h₁   = IsPullback.p₁∘universal≈h₁ pb
    pb-cospan-iso {p₂ = p₂} {g = g} {m = m} miso pb .IsPullback.p₂∘universal≈h₂   = pullʳ (IsPullback.p₂∘universal≈h₂ pb) ○ cancelˡ (Iso.isoˡ (IsIso.iso miso))
    pb-cospan-iso {p₂ = p₂} {g = g} {m = m} miso pb .IsPullback.unique-diagram    = λ eq₁ eq₂ → IsPullback.unique-diagram pb eq₁
          (Iso⇒Mono (Iso-swap (IsIso.iso miso)) _ _ (sym-assoc ○ eq₂ ○ assoc))

    -- one delay step on ι̂ increments the index
    later∘ι̂ : later ∘ ι̂ ≈ ι̂ ∘ s
    later∘ι̂ = begin
      later ∘ ι ∘ ⟨ ! , id ⟩          ≈⟨ pushˡ ι-succ ⟨ 
      (ι ∘ (id ×₁ s)) ∘ ⟨ ! , id ⟩    ≈⟨ extendˡ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ !-unique₂ id-comm ○ sym ⟨⟩∘) ⟩
      ι̂ ∘ s                          ∎

    -- now factors through ι̂ at index 0
    now∘! : ∀ {A} → now ∘ ! {A} ≈ ι̂ ∘ z ∘ !
    now∘! = begin
      now ∘ !                         ≈⟨ pullˡ ι-zero ⟨
      ι ∘ ⟨ id , z ∘ ! ⟩ ∘ !          ≈⟨ pushʳ (⟨⟩∘ ○ ⟨⟩-cong₂ !-unique₂ (pullʳ !-unique₂ ○ sym identityˡ) ○ sym ⟨⟩∘) ⟩
      ι̂ ∘ z ∘ !                      ∎

    -- any two maps out of an object isomorphic to ⊥ agree
    from-⊥-obj-unique : ∀ {A S} → A ≅ ⊥ → (p q : A ⇒ S) → p ≈ q
    from-⊥-obj-unique A≅⊥ p q = begin
      p                                           ≈⟨ introʳ (_≅_.isoˡ A≅⊥) ⟩
      p ∘ _≅_.to A≅⊥ ∘ _≅_.from A≅⊥            ≈⟨ pullˡ (¡-unique₂ _ _) ⟩
      ¡ ∘ _≅_.from A≅⊥                          ≈⟨ pullˡ (¡-unique₂ _ _) ⟨
      q ∘ _≅_.to A≅⊥ ∘ _≅_.from A≅⊥            ≈⟨ elimʳ (_≅_.isoˡ A≅⊥) ⟩
      q                                          ∎

    -- if one summand of a coproduct is ⊥, the other injection is an iso
    coproduct-inj₂-iso : ∀ {A B S} {f : A ⇒ S} {g : B ⇒ S}
      → IsCoproduct f g → A ≅ ⊥ → IsIso g
    coproduct-inj₂-iso {A}{B}{S}{f}{g} cp A≅⊥ = record
      { inv = CP.[ ¡ ∘ _≅_.from A≅⊥ , id ]
      ; iso = record
        { isoˡ = CP.inject₂
        ; isoʳ = sym (CP.unique eq-f eq-g) ○ CP.unique identityˡ identityˡ
        }
      }
      where
        module CP = IsCoproduct cp
        eq-f : (g ∘ CP.[ ¡ ∘ _≅_.from A≅⊥ , id ]) ∘ f ≈ f
        eq-f = pullʳ CP.inject₁ ○ from-⊥-obj-unique A≅⊥ _ _ 
        
        eq-g : (g ∘ CP.[ ¡ ∘ _≅_.from A≅⊥ , id ]) ∘ g ≈ g
        eq-g = pullʳ CP.inject₂ ○ identityʳ

    IsCoproduct-resp-≈ : ∀ {A B S} {f f' : A ⇒ S} {g g' : B ⇒ S} → f ≈ f' → g ≈ g' → IsCoproduct f g → IsCoproduct f' g'
    IsCoproduct-resp-≈ {f' = f'}{g' = g'} ef eg cp = record
      { [_,_]   = CP.[_,_]
      ; inject₁ = ∘-resp-≈ʳ (sym ef) ○ CP.inject₁
      ; inject₂ = ∘-resp-≈ʳ (sym eg) ○ CP.inject₂
      ; unique  = λ eq₁ eq₂ → CP.unique (∘-resp-≈ʳ ef ○ eq₁) (∘-resp-≈ʳ eg ○ eq₂)
      }
      where module CP = IsCoproduct cp

    IsCoproduct-precompose-iso : ∀ {A B S A' B'} {f : A ⇒ S} {g : B ⇒ S} (α : A' ⇒ A) (β : B' ⇒ B)
      → IsCoproduct f g → IsIso α → IsIso β → IsCoproduct (f ∘ α) (g ∘ β)
    IsCoproduct-precompose-iso {f = f}{g} α β cp αiso βiso = record
      { [_,_]   = λ p q → CP.[ p ∘ IsIso.inv αiso , q ∘ IsIso.inv βiso ]
      ; inject₁ = pullˡ CP.inject₁ ○ cancelʳ (Iso.isoˡ (IsIso.iso αiso))
      ; inject₂ = pullˡ CP.inject₂ ○ cancelʳ (Iso.isoˡ (IsIso.iso βiso))
      ; unique  = λ {_}{h}{p}{q} eq₁ eq₂ → CP.unique
          (pushʳ (sym (cancelʳ (Iso.isoʳ (IsIso.iso αiso)))) ○ ∘-resp-≈ˡ eq₁) 
          (pushʳ (sym (cancelʳ (Iso.isoʳ (IsIso.iso βiso)))) ○ ∘-resp-≈ˡ eq₂)
      }
      where module CP = IsCoproduct cp

    -- two pullbacks of one cospan: the comparison map is an iso (and commutes with p₁)
    two-pb-iso : ∀ {P P' A B Q} {p₁ : P ⇒ A} {p₂ : P ⇒ B} {p₁' : P' ⇒ A} {p₂' : P' ⇒ B} {f : A ⇒ Q} {g : B ⇒ Q}
      → (pb₁ : IsPullback p₁ p₂ f g) (pb₂ : IsPullback p₁' p₂' f g)
      → IsIso (IsPullback.universal pb₁ (IsPullback.commute pb₂))
    two-pb-iso pb₁ pb₂ .M.IsIso.inv = IsPullback.universal pb₂ (IsPullback.commute pb₁)
    two-pb-iso pb₁ pb₂ .M.IsIso.iso .M.Iso.isoˡ = IsPullback.unique-diagram pb₂
            (pullˡ (IsPullback.p₁∘universal≈h₁ pb₂) ○ IsPullback.p₁∘universal≈h₁ pb₁ ○ sym identityʳ)
            (pullˡ (IsPullback.p₂∘universal≈h₂ pb₂) ○ IsPullback.p₂∘universal≈h₂ pb₁ ○ sym identityʳ)      
    two-pb-iso pb₁ pb₂ .M.IsIso.iso .M.Iso.isoʳ = IsPullback.unique-diagram pb₁
            (pullˡ (IsPullback.p₁∘universal≈h₁ pb₁) ○ IsPullback.p₁∘universal≈h₁ pb₂ ○ sym identityʳ)
            (pullˡ (IsPullback.p₂∘universal≈h₂ pb₁) ○ IsPullback.p₂∘universal≈h₂ pb₂ ○ sym identityʳ)

    -- the copairing of a coproduct's injections against the standard coproduct is an iso
    IsCoproduct⇒iso : ∀ {A B S} {f : A ⇒ S} {g : B ⇒ S} → IsCoproduct f g → IsIso (copair f g)
    IsCoproduct⇒iso {f = f}{g = g} cp = record
      { inv = CP.[ i₁ , i₂ ]
      ; iso = record
        { isoˡ = sym ([]-unique (pullʳ inject₁ ○ CP.inject₁) (pullʳ inject₂ ○ CP.inject₂)) ○ +-η
        ; isoʳ = sym (CP.unique (pullʳ CP.inject₁ ○ inject₁) (pullʳ CP.inject₂ ○ inject₂)) ○ CP.unique identityˡ identityˡ
        }
      }
      where module CP = IsCoproduct cp

    -- conversely: if the copairing [f,g] is an iso, then S is a coproduct of A and B via f, g
    iso⇒IsCoproduct : ∀ {A B S} {f : A ⇒ S} {g : B ⇒ S} → IsIso (copair f g) → IsCoproduct f g
    iso⇒IsCoproduct {f = f}{g = g} miso = record
      { [_,_]   = λ h₁ h₂ → [ h₁ , h₂ ] ∘ m⁻¹
      ; inject₁ = pullʳ m⁻¹∘f≈i₁ ○ inject₁
      ; inject₂ = pullʳ m⁻¹∘g≈i₂ ○ inject₂
      ; unique  = λ {_}{u}{h₁}{h₂} u∘f≈h₁ u∘g≈h₂ → ∘-resp-≈ˡ ([]-unique (pullʳ inject₁ ○ u∘f≈h₁) (pullʳ inject₂ ○ u∘g≈h₂))
                  ○ cancelʳ (Iso.isoʳ (IsIso.iso miso)) 
      }
      where
        m⁻¹      = IsIso.inv miso
        m⁻¹∘f≈i₁ = pushʳ (sym inject₁) ○ elimˡ (Iso.isoˡ (IsIso.iso miso)) 
        m⁻¹∘g≈i₂ = pushʳ (sym inject₂) ○ elimˡ (Iso.isoˡ (IsIso.iso miso)) 

    -- a map whose pullback along i₁ is ⊥ factors through i₂
    i₂-factors : ∀ {Z A B} (k : Z ⇒ A + B) → (Pullback.P (Extensive.pullback₁ extensive k) ⇒ ⊥) → Σ[ w ∈ (Z ⇒ B) ] (k ≈ i₂ ∘ w)
    i₂-factors {Z}{A}{B} k P₁⇒⊥ = w , k≈i₂w
      where
        pb₂ = Extensive.pullback₂ extensive k
        
        cp : IsCoproduct (Pullback.p₁ (Extensive.pullback₁ extensive k)) (Pullback.p₁ pb₂)
        cp = Extensive.pullback-of-cp-is-cp extensive k

        P₁≅⊥ : Pullback.P (Extensive.pullback₁ extensive k) ≅ ⊥
        P₁≅⊥ = record { from = P₁⇒⊥ ; to = IsIso.inv f⊥ ; iso = IsIso.iso f⊥ }
          where f⊥ = EP.to-⊥-is-iso extensive P₁⇒⊥

        a₂-iso : IsIso (Pullback.p₁ pb₂)
        a₂-iso = coproduct-inj₂-iso cp P₁≅⊥
        
        w : Z ⇒ B
        w = Pullback.p₂ pb₂ ∘ IsIso.inv a₂-iso
        
        k≈i₂w : k ≈ i₂ ∘ w
        k≈i₂w = introʳ (Iso.isoʳ (IsIso.iso a₂-iso)) ○ extendʳ (Pullback.commute pb₂)

    -- LPO: ι̂ : ℕ ↣ D1 is complemented, i.e. a coproduct injection
    LPO : Set (o ⊔ ℓ ⊔ e)
    LPO = Σ[ I ∈ Obj ] Σ[ i ∈ (I ⇒ D.F.₀ ⊤) ] IsIso (copair ι̂ i)

    -- necessity: [ι,∞] iso (at X = 1) ⟹ ι̂ complemented
    -- take I = 1, i = ∞; then [ι̂,∞] = [ι,∞]{⊤} ∘ (⟨!,id⟩ +₁ id), a composite of isos.
    N×X+1⇒LPO : IsIso ([ι,∞] {⊤}) → LPO
    N×X+1⇒LPO given = ⊤ , ∞ , record { inv = (π₂ +₁ id) ∘ IsIso.inv given ; iso = iso[ι̂,∞] }
      where
        ⟨!,id⟩-iso : IsIso ⟨ ! , id ⟩
        ⟨!,id⟩-iso = record { inv = π₂ ; iso = Iso-swap (_≅_.iso ⊤×A≅A) }

        g₀-iso : IsIso (⟨ ! , id ⟩ +₁ id)
        g₀-iso = +₁-iso ⟨!,id⟩-iso id-is-iso

        eq : copair ι ∞ ∘ (⟨ ! , id ⟩ +₁ id) ≈ copair ι̂ ∞
        eq = []∘+₁ ○ []-cong₂ refl identityʳ

        iso[ι̂,∞] : Iso (copair ι̂ ∞) ((π₂ +₁ id) ∘ IsIso.inv given)
        iso[ι̂,∞] = Iso-resp-≈ (Iso-∘ (IsIso.iso g₀-iso) (IsIso.iso given)) eq refl

    -- ! : A → 1 is the (unique) morphism of (⊥+-)-coalgebras into (⊤, i₂):
    -- both legs are maps into ⊥+⊤ ≅ ⊤, which is terminal.
    !-coalg-morph : ∀ {A} (α : A ⇒ ⊥ + A) → i₂ ∘ ! ≈ (id +₁ !) ∘ α
    !-coalg-morph {A} α = Iso⇒Mono (_≅_.iso (⊥+A≅A {⊤})) (i₂ ∘ !) ((id +₁ !) ∘ α) !-unique₂

    -- D∅ ≅ 1 : the delay of the initial object is terminal.  D∅ is the final
    -- (⊥+-)-coalgebra (out); ⊤ is one too (from = !, to = ∞ = coit i₂), so they agree.
    D∅≅1 : D.F.₀ ⊥ ≅ ⊤
    D∅≅1 = record
      { from = !
      ; to   = ∞
      ; iso  = record
        { isoˡ = ∞∘!≈id
        ; isoʳ = sym (!-unique (! ∘ ∞)) ○ !-unique id
        }
      }
      where
        eq₁ : out ∘ (∞ ∘ !) ≈ (id +₁ (∞ ∘ !)) ∘ out
        eq₁ = begin
          out ∘ ∞ ∘ !                   ≈⟨ pullˡ ∞-commutes ⟩
          ((id +₁ ∞) ∘ i₂) ∘ !          ≈⟨ extendˡ (!-coalg-morph out) ⟩
          ((id +₁ ∞) ∘ (id +₁ !)) ∘ out ≈⟨ (+₁∘+₁ ○ +₁-cong₂ identity² refl) ⟩∘⟨refl ⟩
          (id +₁ (∞ ∘ !)) ∘ out         ∎
          
        eq₂ : out ∘ id ≈ (id +₁ id) ∘ out
        eq₂ = identityʳ ○ sym (elimˡ id+₁id)

        ∞∘!≈id : ∞ ∘ ! ≈ id
        ∞∘!≈id = sym (coit-unique out (∞ ∘ !) eq₁) ○ coit-unique out id eq₂

    -- sufficiency: ι̂ complemented ⟹ [ι,∞] iso (for every X)
    LPO⇒N×X+1 : LPO → ∀ {X} → IsIso ([ι,∞] {X})
    LPO⇒N×X+1 (I , i , iso) {X} = IsCoproduct⇒iso IsCop-ι∞
      where
        μ : N + I ⇒ D.F.₀ ⊤
        μ = copair ι̂ i

        μ-mono : Mono μ
        μ-mono = Iso⇒Mono (IsIso.iso iso)

        -- disjointness of the injections ι̂, i : from Extensive.disjoint through the iso μ
        ι̂-i-disjoint : IsPullback (¡ {N}) (¡ {I}) ι̂ i
        ι̂-i-disjoint = IsPullback-resp-≈ inject₁ inject₂ (pb-post-mono μ-mono (Extensive.disjoint extensive))

        μ⁻¹ : D₀ ⊤ ⇒ N + I
        μ⁻¹ = IsIso.inv iso

        pb₁-out = Extensive.pullback₁ extensive (out ∘ i)
        
        clash-out : Pullback.P pb₁-out ⇒ ⊥
        clash-out = IsPullback.universal ι̂-i-disjoint cone-out
          where
            a₁ = Pullback.p₁ pb₁-out
            b₁ = Pullback.p₂ pb₁-out
            
            cone-out : ι̂ ∘ z ∘ ! ≈ i ∘ a₁
            cone-out = begin
              ι̂ ∘ z ∘ !                ≈⟨ now∘! ⟨
              now ∘ !                  ≈⟨ refl⟩∘⟨ !-unique₂ ⟩
              now ∘ b₁                 ≈⟨ pushʳ (sym-assoc ○ Pullback.commute pb₁-out) ⟨  
              out⁻¹ ∘ out ∘ i ∘ a₁     ≈⟨ cancelˡ out⁻¹∘out ⟩
              i ∘ a₁                   ∎

        w : I ⇒ D.F.₀ ⊤
        w = proj₁ (i₂-factors (out ∘ i) clash-out)
        
        out∘i≈i₂w : out ∘ i ≈ i₂ ∘ w
        out∘i≈i₂w = proj₂ (i₂-factors (out ∘ i) clash-out)

        i≈later∘w : i ≈ later ∘ w
        i≈later∘w = sym (cancelˡ out⁻¹∘out) ○ pushʳ out∘i≈i₂w

        μ⁻¹-mono : Mono μ⁻¹
        μ⁻¹-mono = Iso⇒Mono (Iso-swap (IsIso.iso iso))

        μ⁻¹∘ι̂ : μ⁻¹ ∘ ι̂ ≈ i₁
        μ⁻¹∘ι̂ = (refl⟩∘⟨ sym inject₁) ○ cancelˡ (Iso.isoˡ (IsIso.iso iso))

        pb₁-w = Extensive.pullback₁ extensive (μ⁻¹ ∘ w)
        clash-w : Pullback.P pb₁-w ⇒ ⊥
        clash-w = IsPullback.universal ι̂-i-disjoint cone-w
          where
            a = Pullback.p₁ pb₁-w
            b = Pullback.p₂ pb₁-w
            w∘a≈ι̂∘b : w ∘ a ≈ ι̂ ∘ b
            w∘a≈ι̂∘b = μ⁻¹-mono (w ∘ a) (ι̂ ∘ b) (begin
              μ⁻¹ ∘ w ∘ a   ≈⟨ sym-assoc ○ Pullback.commute pb₁-w ⟩
              i₁ ∘ b        ≈⟨ pullˡ μ⁻¹∘ι̂ ⟨
              μ⁻¹ ∘ ι̂ ∘ b   ∎)
            cone-w : ι̂ ∘ s ∘ b ≈ i ∘ a
            cone-w = begin
              ι̂ ∘ s ∘ b     ≈⟨ extendʳ later∘ι̂ ⟨
              later ∘ ι̂ ∘ b ≈⟨ refl⟩∘⟨ w∘a≈ι̂∘b ⟨
              later ∘ w ∘ a ≈⟨ pushˡ i≈later∘w ⟨
              i ∘ a         ∎

        v : I ⇒ I
        v = proj₁ (i₂-factors (μ⁻¹ ∘ w) clash-w)
        
        μ⁻¹w≈i₂v : μ⁻¹ ∘ w ≈ i₂ ∘ v
        μ⁻¹w≈i₂v = proj₂ (i₂-factors (μ⁻¹ ∘ w) clash-w)

        w≈i∘v : w ≈ i ∘ v
        w≈i∘v = introˡ (Iso.isoʳ (IsIso.iso iso)) ○ pullʳ μ⁻¹w≈i₂v ○ pullˡ inject₂

        -- i is a (⊤+-)-coalgebra map (I, i₂∘v) → (D⊤, out)
        out∘i≈i₂iv : out ∘ i ≈ (id +₁ i) ∘ (i₂ ∘ v)
        out∘i≈i₂iv = begin
          out ∘ i              ≈⟨ out∘i≈i₂w ⟩
          i₂ ∘ w               ≈⟨ refl⟩∘⟨ w≈i∘v ⟩
          i₂ ∘ i ∘ v           ≈⟨ extendʳ inject₂ ⟨
          (id +₁ i) ∘ i₂ ∘ v   ∎

        i≈∞! : i ≈ ∞ ∘ !
        i≈∞! = sym (coit-unique (i₂ ∘ v) i out∘i≈i₂iv) ○ coit-unique (i₂ ∘ v) (∞ ∘ !) eq∞
          where
            eq∞ : out ∘ (∞ ∘ !) ≈ (id +₁ (∞ ∘ !)) ∘ (i₂ ∘ v)
            eq∞ = begin
              out ∘ ∞ ∘ !                ≈⟨ extendʳ (∞-commutes ○ inject₂) ⟩
              i₂ ∘ ∞ ∘ !                 ≈⟨ refl⟩∘⟨ refl⟩∘⟨ !-unique₂ ⟩
              i₂ ∘ ∞ ∘ ! ∘ v             ≈⟨ refl⟩∘⟨ sym-assoc ⟩
              i₂ ∘ (∞ ∘ !) ∘ v           ≈⟨ extendʳ inject₂ ⟨
              (id +₁ (∞ ∘ !)) ∘ i₂ ∘ v   ∎

        -- i is mono (μ iso, i₂ mono), hence I is subterminal (i = ∞∘! collapses through ⊤)
        i-mono : Mono i
        i-mono g h eq = Extensive.pullback₂-is-mono extensive g h
          (μ-mono (i₂ ∘ g) (i₂ ∘ h) (pullˡ inject₂ ○ eq ○ sym (pullˡ inject₂)))

        I-subterminal : ∀ {A} (g h : A ⇒ I) → g ≈ h
        I-subterminal g h = i-mono g h (begin
          i ∘ g        ≈⟨ pushˡ i≈∞! ⟩
          ∞ ∘ ! ∘ g    ≈⟨ refl⟩∘⟨ !-unique₂ ⟩
          ∞ ∘ ! ∘ h    ≈⟨ pushˡ i≈∞! ⟨
          i ∘ h        ∎)

        -- the point ⊤ → I : ∞{⊤} lands in the I-summand (its ℕ-part ≅ ∅ by ι-nat-pullback at ⊥)
        pb∞ = Extensive.pullback₁ extensive (μ⁻¹ ∘ ∞ {⊤})
        clash∞ : Pullback.P pb∞ ⇒ ⊥
        clash∞ = π₁ ∘ IsPullback.universal (ι-nat-pullback PNNO !) cone∞
          where
            a = Pullback.p₁ pb∞
            b = Pullback.p₂ pb∞
            
            ∞∘a≈ι̂∘b : ∞ {⊤} ∘ a ≈ ι̂ ∘ b
            ∞∘a≈ι̂∘b = μ⁻¹-mono (∞ ∘ a) (ι̂ ∘ b) (begin
              μ⁻¹ ∘ ∞ ∘ a ≈⟨ sym-assoc ○ Pullback.commute pb∞ ⟩
              i₁ ∘ b      ≈⟨ pullˡ μ⁻¹∘ι̂ ⟨
              μ⁻¹ ∘ ι̂ ∘ b ∎)
              
            cone∞ : D.F.₁ ! ∘ (∞ {⊥} ∘ a) ≈ ι ∘ (⟨ ! , id ⟩ ∘ b)
            cone∞ = pullˡ (∞-natural !) ○ ∞∘a≈ι̂∘b ○ assoc

        point : ⊤ ⇒ I
        point = proj₁ (i₂-factors (μ⁻¹ ∘ ∞ {⊤}) clash∞)

        I≅⊤ : I ≅ ⊤
        I≅⊤ = record
          { from = !
          ; to   = point
          ; iso  = record { isoˡ = I-subterminal (point ∘ !) id ; isoʳ = !-unique₂ }
          }

        -- ν = [ι̂, ∞] : N+⊤ ≅ D⊤ (base case, using I ≅ ⊤ so that i corresponds to ∞)
        point-iso : IsIso point
        point-iso = record { inv = ! ; iso = Iso-swap (_≅_.iso I≅⊤) }

        i∘point≈∞ : i ∘ point ≈ ∞ {⊤}
        i∘point≈∞ = pushˡ (sym inject₂) ○ (refl⟩∘⟨ sym (proj₂ (i₂-factors (μ⁻¹ ∘ ∞ {⊤}) clash∞)))
                  ○ cancelˡ (Iso.isoʳ (IsIso.iso iso))

        ν-iso : IsIso (copair ι̂ (∞ {⊤}))
        ν-iso = record
          { inv = IsIso.inv (+₁-iso id-is-iso point-iso) ∘ μ⁻¹
          ; iso = Iso-resp-≈ (Iso-∘ (IsIso.iso (+₁-iso id-is-iso point-iso)) (IsIso.iso iso))
                    ([]∘+₁ ○ []-cong₂ identityʳ i∘point≈∞) refl
          }

        -- D⊤ is a coproduct of ℕ and 1, with injections ι̂ and ∞
        D⊤-coproduct : IsCoproduct ι̂ (∞ {⊤})
        D⊤-coproduct = iso⇒IsCoproduct ν-iso

        νinv = IsIso.inv ν-iso
        Dfun = D₁ (! {X})

        pb₁ = Extensive.pullback₁ extensive (νinv ∘ Dfun)
        pb₂ = Extensive.pullback₂ extensive (νinv ∘ Dfun)

        q₁ = Pullback.p₁ pb₁
        q₂ = Pullback.p₁ pb₂

        -- pulling the coproduct D⊤ = ℕ + 1 back along D! : DX → D⊤ decomposes DX
        DX-coproduct : IsCoproduct q₁ q₂
        DX-coproduct = Extensive.pullback-of-cp-is-cp extensive (νinv ∘ Dfun)
        
        ν-mono = Iso⇒Mono (IsIso.iso ν-iso)
        νk≈D : copair ι̂ (∞ {⊤}) ∘ νinv ∘ Dfun ≈ Dfun
        νk≈D = cancelˡ (Iso.isoʳ (IsIso.iso ν-iso))

        -- Q₁ = pullback(Dfun, ι̂); ιpb = same pullback with vertex X×N, leg ι
        Q₁-pb : IsPullback q₁ (Pullback.p₂ pb₁) Dfun ι̂
        Q₁-pb = IsPullback-resp-≈ νk≈D inject₁ (pb-post-mono ν-mono (Pullback.isPullback pb₁))
        
        ⟨!,id⟩-iso : IsIso (⟨ ! , id {N} ⟩)
        ⟨!,id⟩-iso = record { inv = π₂ ; iso = Iso-swap (_≅_.iso ⊤×A≅A) }

        ιpb : IsPullback ι (IsIso.inv ⟨!,id⟩-iso ∘ (! ×₁ id)) Dfun ι̂
        ιpb = pb-cospan-iso ⟨!,id⟩-iso (ι-nat-pullback PNNO !)
        α₁-iso = two-pb-iso Q₁-pb ιpb

         -- Q₂ = pullback(Dfun, ∞{⊤}); ∞pb = same pullback with vertex ⊤ (via D∅≅1), leg ∞{X}
        Q₂-pb : IsPullback q₂ (Pullback.p₂ pb₂) Dfun (∞ {⊤})
        Q₂-pb = IsPullback-resp-≈ νk≈D inject₂ (pb-post-mono ν-mono (Pullback.isPullback pb₂))
        
        -- ---- α₂ : ⊤ ≅ Q₂, mirroring the I ≅ ⊤ argument (complement of ι̂ in D⊤), now for
        -- the complement Q₂ of q₁ in DX.  Q₂ is the ∞{⊤}-fibre of D!, hence closed under
        -- "tail" (via its own pullback universal property), so coit-unique gives q₂ ≈ ∞{X}∘!
        -- directly — no exponentials.

        Q₂ = Pullback.P pb₂

        q₂-mono : Mono q₂
        q₂-mono g h eq = Extensive.pullback₂-is-mono extensive g h
          (Iso⇒Mono (IsIso.iso (IsCoproduct⇒iso DX-coproduct)) (i₂ ∘ g) (i₂ ∘ h)
            (pullˡ inject₂ ○ eq ○ sym (pullˡ inject₂)))

        -- q₂ lies in the ∞-fibre of D!
        D!q₂≈∞! : Dfun ∘ q₂ ≈ ∞ {⊤} ∘ !
        D!q₂≈∞! = IsPullback.commute Q₂-pb ○ (refl⟩∘⟨ !-unique₂)

        -- the "shape" identity: (!+₁D!) ∘ out ∘ q₂ lands in the divergent summand
        gid : (! +₁ Dfun) ∘ out ∘ q₂ ≈ i₂ ∘ ∞ {⊤} ∘ !
        gid = begin
          (! +₁ Dfun) ∘ out ∘ q₂    ≈⟨ extendʳ (D₁-commutes !) ⟨
          out ∘ Dfun ∘ q₂           ≈⟨ refl⟩∘⟨ D!q₂≈∞! ⟩
          out ∘ ∞ {⊤} ∘ !           ≈⟨ extendʳ (∞-commutes ○ inject₂) ⟩
          i₂ ∘ ∞ ∘ !                ∎

        -- q₂ never returns "now": out ∘ q₂ factors through i₂ (else it would meet ∞{⊤})
        pb₁-q₂ = Extensive.pullback₁ extensive (out ∘ q₂)
        clash-q₂ : Pullback.P pb₁-q₂ ⇒ ⊥
        clash-q₂ = IsPullback.universal (Extensive.disjoint extensive) cone-q₂
          where
            a = Pullback.p₁ pb₁-q₂
            b = Pullback.p₂ pb₁-q₂
            
            +i₁ : (! +₁ Dfun) ∘ i₁ {X} {D₀ X} ≈ i₁ {⊤} {D₀ ⊤} ∘ ! {X}
            +i₁ = +₁∘i₁
            
            cone-q₂ : i₁ {⊤} {D₀ ⊤} ∘ ! ≈ i₂ ∘ (∞ {⊤} ∘ ! ∘ a)
            cone-q₂ = ⟺ (begin
              i₂ ∘ (∞ {⊤} ∘ ! ∘ a)          ≈⟨ refl⟩∘⟨ sym-assoc ⟩
              i₂ ∘ (∞ {⊤} ∘ !) ∘ a          ≈⟨ extendʳ gid ⟨
              (! +₁ Dfun) ∘ (out ∘ q₂) ∘ a  ≈⟨ refl⟩∘⟨ Pullback.commute pb₁-q₂ ⟩
              (! +₁ Dfun) ∘ i₁ ∘ b          ≈⟨ extendʳ +i₁ ⟩
              i₁ ∘ ! ∘ b                    ≈⟨ refl⟩∘⟨ !-unique₂ ⟨
              i₁ {⊤} {D₀ ⊤} ∘ !             ∎)

        w₂ : Q₂ ⇒ D₀ X
        w₂ = proj₁ (i₂-factors (out ∘ q₂) clash-q₂)
        out∘q₂≈i₂w₂ : out ∘ q₂ ≈ i₂ ∘ w₂
        out∘q₂≈i₂w₂ = proj₂ (i₂-factors (out ∘ q₂) clash-q₂)

        -- w₂ is again in the ∞-fibre, so — Q₂ being that fibre — it factors through q₂: w₂ = q₂ ∘ τ
        D!w₂≈∞! : Dfun ∘ w₂ ≈ ∞ {⊤} ∘ !
        D!w₂≈∞! = Extensive.pullback₂-is-mono extensive _ _ (⟺ (begin
          i₂ ∘ ∞ {⊤} ∘ !         ≈⟨ gid ⟨
          (! +₁ Dfun) ∘ out ∘ q₂ ≈⟨ refl⟩∘⟨ out∘q₂≈i₂w₂ ⟩
          (! +₁ Dfun) ∘ i₂ ∘ w₂  ≈⟨ extendʳ +i₂ ⟩
          i₂ ∘ Dfun ∘ w₂         ∎))
          where
            +i₂ : (! +₁ Dfun) ∘ i₂ {X} {D₀ X} ≈ i₂ {⊤} {D₀ ⊤} ∘ Dfun
            +i₂ = +₁∘i₂

        τ : Q₂ ⇒ Q₂
        τ = IsPullback.universal Q₂-pb D!w₂≈∞!
        
        w₂≈q₂τ : w₂ ≈ q₂ ∘ τ
        w₂≈q₂τ = sym (IsPullback.p₁∘universal≈h₁ Q₂-pb {eq = D!w₂≈∞!})

        out∘q₂≈i₂q₂τ : out ∘ q₂ ≈ (id +₁ q₂) ∘ (i₂ ∘ τ)
        out∘q₂≈i₂q₂τ = begin
          out ∘ q₂            ≈⟨ out∘q₂≈i₂w₂ ⟩
          i₂ ∘ w₂             ≈⟨ refl⟩∘⟨ w₂≈q₂τ ⟩
          i₂ ∘ q₂ ∘ τ         ≈⟨ extendʳ (sym inject₂) ⟩
          (id +₁ q₂) ∘ i₂ ∘ τ ∎

        -- crux: the complement injection q₂ is the point at infinity
        q₂≈∞! : q₂ ≈ ∞ {X} ∘ !
        q₂≈∞! = sym (coit-unique (i₂ ∘ τ) q₂ out∘q₂≈i₂q₂τ) ○ coit-unique (i₂ ∘ τ) (∞ ∘ !) eq∞
          where
            eq∞ : out ∘ (∞ ∘ !) ≈ (id +₁ (∞ ∘ !)) ∘ (i₂ ∘ τ)
            eq∞ = begin
              out ∘ ∞ ∘ !                ≈⟨ extendʳ (∞-commutes ○ inject₂) ⟩
              i₂ ∘ ∞ ∘ !                 ≈⟨ refl⟩∘⟨ refl⟩∘⟨ !-unique₂ ⟩
              i₂ ∘ ∞ ∘ ! ∘ τ             ≈⟨ refl⟩∘⟨ sym-assoc ⟩
              i₂ ∘ (∞ ∘ !) ∘ τ           ≈⟨ extendʳ inject₂ ⟨
              (id +₁ (∞ ∘ !)) ∘ i₂ ∘ τ   ∎

        Q₂-subterminal : ∀ {A} (g h : A ⇒ Q₂) → g ≈ h
        Q₂-subterminal g h = q₂-mono g h (begin
          q₂ ∘ g     ≈⟨ pushˡ q₂≈∞! ⟩
          ∞ ∘ ! ∘ g  ≈⟨ refl⟩∘⟨ !-unique₂ ⟩
          ∞ ∘ ! ∘ h  ≈⟨ pushˡ q₂≈∞! ⟨
          q₂ ∘ h     ∎)

        -- the point ⊤ → Q₂ : ∞{X} lands in the Q₂-summand (D!∘∞{X} = ∞{⊤})
        point₂ : ⊤ ⇒ Q₂
        point₂ = IsPullback.universal Q₂-pb (∞-natural ! ○ sym identityʳ)

        Q₂≅⊤ : Q₂ ≅ ⊤
        Q₂≅⊤ = record
          { from = !
          ; to   = point₂
          ; iso  = record { isoˡ = Q₂-subterminal (point₂ ∘ !) id ; isoʳ = !-unique₂ }
          }

        α₂-iso : IsIso point₂
        α₂-iso = record { inv = ! ; iso = Iso-swap (_≅_.iso Q₂≅⊤) }

        IsCop-ι∞ : IsCoproduct ι (∞ {X})
        IsCop-ι∞ = IsCoproduct-resp-≈ (IsPullback.p₁∘universal≈h₁ Q₁-pb)
                                      (IsPullback.p₁∘universal≈h₁ Q₂-pb {eq = ∞-natural ! ○ sym identityʳ})
                                      (IsCoproduct-precompose-iso _ _ DX-coproduct α₁-iso α₂-iso)