open import Categories.Category.Core
open import Categories.Object.Product.Core using (Product)
open import Categories.Object.Terminal
open import Categories.Monad hiding (id)
open import Categories.Monad.Relative renaming (Monad to RMonad)
open import Categories.Functor.Core
open import Categories.Monad.Strong
open import Categories.Category.Distributive
open import Categories.Category.Cartesian using (Cartesian)
open import Categories.Category.Extensive using (Extensive)
open import Categories.Category.Extensive.Properties.Distributive
open import Categories.NaturalTransformation using (NaturalTransformation)
open import Categories.Functor using (_∘F_) renaming (id to Id)
open import Categories.Functor.Bifunctor using (reduce-×; overlap-×)
open import Categories.Object.NaturalNumbers.Parametrized

open import Data.Product using (_,_)

open import Monad.Instance.Delay
open import Monad.Helper

import Categories.Morphism as Mor
import Categories.Morphism.Reasoning as MR
import Categories.Morphism.Properties as MP
import Categories.Morphism.Regular.Properties as MRP
import Categories.Morphism.Regular as MRR

-- The N-indexed chopᴺ machinery (D₀Z × N ⇒ D₀Z × N, the prim-rec "strip n laters,
-- reset index"), built on top of Chop and Iota; plus chopᴺ-sat and ι-mono.
module Monad.Instance.Delay.ChopNat {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 import Categories.Diagram.Pullback C
  open import Monad.Instance.Delay.Commutative distributive D
  open τ-mod
  open σ-mod
  open HomReasoning
  open Equiv
  open Mor C
  open MRR C
  open MRP C
  open import Categories.Morphism.Properties C
  open MR C
  open MP C
  open DelayM D
  open import Monad.Instance.Delay.Guarded cocartesian D
  open D-Kleisli
  open D-Monad
  module F = D.F
  open F using (homomorphism; F-resp-≈; identity)
  open D.μ renaming (η to μ)
  open D-Strong
  open import Monad.Instance.Delay.Zip distributive D
  open import Monad.Instance.Delay.Chop distributive D
  open import Monad.Instance.Delay.Iota distributive D PNNO
  open ParametrizedNNO PNNO using (N; z; s)
  open import Object.NaturalNumbers.Parametrized.Primitive (Distributive.cartesian distributive) PNNO
       using (prec; prec-zero; prec-zero'; prec-succ; prec-unique; prec-natural; prec-uniform; prec-cong; prec-η
             ; min; sub; sub-zʳ; sub-Δ•; min-sum; sub-sʳ
             ; sum; sum-sʳ; sum-zʳ; sum-zˡ; sum-sˡ; sum-assoc•; sum-comm•; sgn; sgn-z; sgn-s
             ; cancel; sum-min-sub; z-or-s-≈•; z-or-s-≈)
  open import Object.NaturalNumbers.Parametrized cartesian
       (Categories.Object.NaturalNumbers.Parametrized.PNNO⇒NNO C cartesian PNNO) using (s⁻¹; s⁻¹-zero; s⁻¹-succ)

  -- the recursion step on the state (d, c): test d with `out`; on `now` keep
  -- the state, on `later d'` advance to d' and increment the count.
  chopᴺ-step : ∀ {Z} → D₀ Z × N ⇒ D₀ Z × N
  chopᴺ-step = [ π₂ , second (s ∘ π₂) ] ∘ distributeʳ⁻¹ ∘ ⟨ out ∘ π₁ , id ⟩

  chopᴺ : ∀ {Z} → D₀ Z × N ⇒ D₀ Z × N
  chopᴺ = prec ⟨ id , z ∘ ! ⟩ (chopᴺ-step ∘ π₁)

  -- chopᴺ-step on a `now` value: a no-op (now-values terminate immediately).
  chopᴺ-step-now : ∀ {Z} → chopᴺ-step {Z} ∘ (now ×₁ id) ≈ (now ×₁ id)
  chopᴺ-step-now = begin
    chopᴺ-step ∘ (now ×₁ id)                                                    ≈⟨ pullʳ (pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ π₁∘×₁ ○ pullˡ unitlaw) identityˡ)) ⟩
    [ π₂ , second (s ∘ π₂)  ] ∘ distributeʳ⁻¹ ∘ ⟨ i₁ ∘ π₁ , now ×₁ id ⟩         ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-congˡ identityˡ) ⟨
    [ π₂ , second (s ∘ π₂)  ] ∘ distributeʳ⁻¹ ∘ (i₁ ×₁ id) ∘ ⟨ π₁ , now ×₁ id ⟩ ≈⟨ refl⟩∘⟨ pullˡ distributeʳ⁻¹-i₁ ⟩
    [ π₂ , second (s ∘ π₂)  ] ∘ i₁ ∘ ⟨ π₁ , now ×₁ id ⟩                         ≈⟨ pullˡ inject₁ ○ project₂ ⟩
    (now ×₁ id)                                                                 ∎

  -- chopᴺ-step on a `later` value: strip the later, bump the count.
  chopᴺ-step-later : ∀ {Z} → chopᴺ-step {Z} ∘ (later ×₁ id) ≈ (id ×₁ s)
  chopᴺ-step-later = begin
    chopᴺ-step ∘ (later ×₁ id)                                                   ≈⟨ pullʳ (pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ π₁∘×₁ ○ pullˡ laterlaw) identityˡ)) ⟩ 
    [ π₂ , second (s ∘ π₂) ] ∘ distributeʳ⁻¹ ∘ ⟨ i₂ ∘ π₁ , later ×₁ id ⟩         ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-congˡ identityˡ) ⟨
    [ π₂ , second (s ∘ π₂) ] ∘ distributeʳ⁻¹ ∘ (i₂ ×₁ id) ∘ ⟨ π₁ , later ×₁ id ⟩ ≈⟨ refl⟩∘⟨ pullˡ distributeʳ⁻¹-i₂ ⟩
    [ π₂ , second (s ∘ π₂) ] ∘ i₂ ∘ ⟨ π₁ , later ×₁ id ⟩                         ≈⟨ pullˡ inject₂ ⟩
    second (s ∘ π₂) ∘ ⟨ π₁ , later ×₁ id ⟩                                       ≈⟨ second∘⟨⟩ ○ ⟨⟩-cong₂ (sym identityˡ) (pullʳ π₂∘first) ⟩ 
    (id ×₁ s)                                                                    ∎

  -- chopᴺ-step commutes with incrementing the count.
  chopᴺ-step-comm : ∀ {Z} → chopᴺ-step {Z} ∘ (id ×₁ s) ≈ (id ×₁ s) ∘ chopᴺ-step
  chopᴺ-step-comm = begin
    chopᴺ-step ∘ (id ×₁ s)                                                                                  ≈⟨ pullʳ (pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ π₁∘second) identityˡ)) ⟩
    [ π₂ , second (s ∘ π₂) ] ∘ distributeʳ⁻¹ ∘ ⟨ out ∘ π₁ , id ×₁ s ⟩                                       ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ identityʳ) ⟨
    [ π₂ , second (s ∘ π₂) ] ∘ distributeʳ⁻¹ ∘ (id ×₁ (id ×₁ s)) ∘ ⟨ out ∘ π₁ , id ⟩                        ≈⟨ refl⟩∘⟨ extendʳ (∘-resp-≈ʳ (×₁-cong₂ (sym id+₁id) refl)) ⟩
    [ π₂ , second (s ∘ π₂) ] ∘ distributeʳ⁻¹ ∘ ((id +₁ id) ×₁ id ×₁ s) ∘ ⟨ out ∘ π₁ , id ⟩                  ≈⟨ refl⟩∘⟨ extendʳ (distributeʳ⁻¹-natural (id ×₁ s) id id) ⟨ 
    [ π₂ , second (s ∘ π₂) ] ∘ ((id ×₁ (id ×₁ s)) +₁ (id ×₁ (id ×₁ s))) ∘ distributeʳ⁻¹ ∘ ⟨ out ∘ π₁ , id ⟩ ≈⟨ pullˡ ([]∘+₁ ○ []-cong₂ π₂∘×₁ second∘second) ⟩
    [ (id ×₁ s) ∘ π₂ , second ((s ∘ π₂) ∘ (id ×₁ s)) ] ∘ distributeʳ⁻¹ ∘ ⟨ out ∘ π₁ , id ⟩                  ≈⟨ extendʳ (∘-resp-≈ˡ ([]-congˡ (second-cong (pullʳ π₂∘×₁)))) ⟩ 
    [ (id ×₁ s) ∘ π₂ , second (s ∘ s ∘ π₂) ] ∘ distributeʳ⁻¹ ∘ ⟨ out ∘ π₁ , id ⟩                            ≈⟨ pullˡ (∘[] ○ []-congˡ second∘second) ⟨ 
    (id ×₁ s) ∘ chopᴺ-step                                                                                  ∎

  -- one extra `later` on the value with one extra fuel ⇒ one extra count.
  chopᴺ-later : ∀ {Z} → chopᴺ {Z} ∘ (later ×₁ s) ≈ (id ×₁ s) ∘ chopᴺ
  chopᴺ-later = prec-unique eq₁ eq₂ ○ sym (prec-uniform unif-hyp ○ prec-cong ids-z refl)
    where
      ids-z : (id ×₁ s) ∘ ⟨ id , z ∘ ! ⟩ ≈ ⟨ id , s ∘ z ∘ ! ⟩
      ids-z = ×₁∘⟨⟩ ○ ⟨⟩-congʳ identityˡ

      unif-hyp : (id ×₁ s) ∘ chopᴺ-step ∘ π₁ ≈ (chopᴺ-step ∘ π₁) ∘ ((id ×₁ s) ×₁ id)
      unif-hyp = pullˡ (sym chopᴺ-step-comm) ○ pullʳ (sym π₁∘×₁) ○ sym-assoc 

      chopᴺ-later-zero : chopᴺ ∘ ⟨ later , z ∘ ! ⟩ ≈ ⟨ later , z ∘ ! ⟩
      chopᴺ-later-zero = begin
        chopᴺ ∘ ⟨ later , z ∘ ! ⟩      ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ (pullʳ !-unique₂)) ⟨
        chopᴺ ∘ ⟨ id , z ∘ ! ⟩ ∘ later ≈⟨ pullˡ prec-zero ⟩
        ⟨ id , z ∘ ! ⟩ ∘ later         ≈⟨ ⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ (pullʳ !-unique₂) ⟩
        ⟨ later , z ∘ ! ⟩              ∎

      eq₁ : (chopᴺ ∘ (later ×₁ s)) ∘ ⟨ id , z ∘ ! ⟩ ≈ ⟨ id , s ∘ z ∘ ! ⟩
      eq₁ = begin
        (chopᴺ ∘ (later ×₁ s)) ∘ ⟨ id , z ∘ ! ⟩     ≈⟨ pullʳ (×₁∘⟨⟩ ○ ⟨⟩-congʳ identityʳ) ⟩
        chopᴺ ∘ ⟨ later , s ∘ z ∘ ! ⟩               ≈⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-congʳ identityˡ) ⟨
        chopᴺ ∘ (id ×₁ s) ∘ ⟨ later , z ∘ ! ⟩       ≈⟨ pullˡ (prec-succ ○ pullʳ project₁) ⟩
        (chopᴺ-step ∘ chopᴺ) ∘ ⟨ later , z ∘ ! ⟩    ≈⟨ pullʳ chopᴺ-later-zero ⟩
        chopᴺ-step ∘ ⟨ later , z ∘ ! ⟩              ≈⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟨
        chopᴺ-step ∘ (later ×₁ id) ∘ ⟨ id , z ∘ ! ⟩ ≈⟨ pullˡ chopᴺ-step-later ⟩
        (id ×₁ s) ∘ ⟨ id , z ∘ ! ⟩                  ≈⟨ ids-z ⟩
        ⟨ id , s ∘ z ∘ ! ⟩                          ∎

      eq₂ : (chopᴺ ∘ (later ×₁ s)) ∘ (id ×₁ s) ≈ (chopᴺ-step ∘ π₁) ∘ ⟨ chopᴺ ∘ (later ×₁ s) , id ⟩
      eq₂ = begin
        (chopᴺ ∘ (later ×₁ s)) ∘ (id ×₁ s)                ≈⟨ pullʳ (×₁∘×₁ ○ ×₁-cong₂ identityʳ refl) ⟩
        chopᴺ ∘ (later ×₁ s ∘ s)                          ≈⟨ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ identityˡ refl) ⟨
        chopᴺ ∘ (id ×₁ s) ∘ (later ×₁ s)                  ≈⟨ pullʳ project₁ ○ extendʳ (sym (prec-succ ○ pullʳ project₁)) ⟨
        (chopᴺ-step ∘ π₁) ∘ ⟨ chopᴺ ∘ (later ×₁ s) , id ⟩ ∎

  -- chopᴺ(laterⁿ now x, n) = (now x, n): the index is preserved.
  -- Both sides are prec ⟨ now , z ∘ ! ⟩ ((id ×₁ s) ∘ π₁).
  chopᴺ-Δ : ∀ {Z} → chopᴺ {Z} ∘ ⟨ ι , π₂ ⟩ ≈ ⟨ now ∘ π₁ , π₂ ⟩
  chopᴺ-Δ = prec-unique h-z h-s ○ sym (prec-unique g-z g-s)
    where
      h-z : (chopᴺ ∘ ⟨ ι , π₂ ⟩) ∘ ⟨ id , z ∘ ! ⟩ ≈ ⟨ now , z ∘ ! ⟩
      h-z = begin
        (chopᴺ ∘ ⟨ ι , π₂ ⟩) ∘ ⟨ id , z ∘ ! ⟩ ≈⟨ pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ ι-zero project₂) ⟩
        chopᴺ ∘ ⟨ now , z ∘ ! ⟩               ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ (pullʳ !-unique₂)) ⟨
        chopᴺ ∘ ⟨ id , z ∘ ! ⟩ ∘ now          ≈⟨ pullˡ prec-zero ⟩
        ⟨ id , z ∘ ! ⟩ ∘ now                  ≈⟨ ⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ (pullʳ !-unique₂) ⟩
        ⟨ now , z ∘ ! ⟩                       ∎

      h-s : (chopᴺ ∘ ⟨ ι , π₂ ⟩) ∘ (id ×₁ s) ≈ ((id ×₁ s) ∘ π₁) ∘ ⟨ chopᴺ ∘ ⟨ ι , π₂ ⟩ , id ⟩
      h-s = begin
        (chopᴺ ∘ ⟨ ι , π₂ ⟩) ∘ (id ×₁ s)               ≈⟨ pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ ι-succ π₂∘×₁) ⟩
        chopᴺ ∘ ⟨ later ∘ ι , s ∘ π₂ ⟩                 ≈⟨ refl⟩∘⟨ ×₁∘⟨⟩ ⟨
        chopᴺ ∘ (later ×₁ s) ∘ ⟨ ι , π₂ ⟩              ≈⟨ extendʳ chopᴺ-later ○ pushʳ (sym project₁) ⟩ 
        ((id ×₁ s) ∘ π₁) ∘ ⟨ chopᴺ ∘ ⟨ ι , π₂ ⟩ , id ⟩ ∎

      g-z : ⟨ now ∘ π₁ , π₂ ⟩ ∘ ⟨ id , z ∘ ! ⟩ ≈ ⟨ now , z ∘ ! ⟩
      g-z = ⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ project₁ ○ identityʳ) project₂

      g-s : ⟨ now ∘ π₁ , π₂ ⟩ ∘ (id ×₁ s) ≈ ((id ×₁ s) ∘ π₁) ∘ ⟨ ⟨ now ∘ π₁ , π₂ ⟩ , id ⟩
      g-s = (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ (π₁∘×₁ ○ identityˡ)) π₂∘×₁)
          ○ sym (pullʳ project₁ ○ ×₁∘⟨⟩ ○ ⟨⟩-congʳ identityˡ)

  -- chopᴺ on an ι-value with independent fuel k: strips min(m,k) laters (leaving the
  -- ι-value at count m∸k) and the index saturates at min(m,k).  Off-diagonal version
  -- of chopᴺ-Δ; both sides are prec ⟨ ι , z∘! ⟩ (chopᴺ-step∘π₁) (chopᴺ-side via prec-natural).
  chopᴺ-ι : ∀ {X} → chopᴺ ∘ (ι {X} ×₁ id) ≈ ⟨ ι ∘ ⟨ π₁ ∘ π₁ , sub ∘ (π₂ ×₁ id) ⟩ , min ∘ (π₂ ×₁ id) ⟩
  chopᴺ-ι {X} = prec-natural ○ sym (prec-unique G-z G-s)
    where
      G : (X × N) × N ⇒ D₀ X × N
      G = ⟨ ι ∘ ⟨ π₁ ∘ π₁ , sub ∘ (π₂ ×₁ id) ⟩ , min ∘ (π₂ ×₁ id) ⟩

      -- TODO: must be moved to Primitive.agda
      min-zʳ : ∀ {A} {f : A ⇒ N} → min ∘ ⟨ f , z ∘ ! ⟩ ≈ z ∘ !
      min-zʳ {_}{f} = begin
        min ∘ ⟨ f , z ∘ ! ⟩                ≈⟨ assoc ⟩
        sub ∘ ⟨ π₁ , sub ⟩ ∘ ⟨ f , z ∘ ! ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ project₁ sub-zʳ) ⟩
        sub ∘ ⟨ f , f ⟩                    ≈⟨ sub-Δ• ⟩
        z ∘ !                              ∎

      -- sgn(n) + pred(n) = n
      sgn-pred : sum ∘ ⟨ sgn , s⁻¹ ⟩ ≈ id
      sgn-pred = z-or-s-ť eqz eqs
        where
          eqz : (sum ∘ ⟨ sgn , s⁻¹ ⟩) ∘ z ∘ ! ≈ id ∘ z ∘ !
          eqz = assoc ○ ∘-resp-≈ʳ (⟨⟩∘ ○ ⟨⟩-cong₂ (pullˡ sgn-z) (pullˡ s⁻¹-zero)) ○ sum-zˡ ○ sym identityˡ
          eqs : (sum ∘ ⟨ sgn , s⁻¹ ⟩) ∘ s ≈ id ∘ s
          eqs = assoc ○ ∘-resp-≈ʳ (⟨⟩∘ ○ ⟨⟩-cong₂ sgn-s s⁻¹-succ)
              ○ ∘-resp-≈ʳ (sym (×₁∘⟨⟩ ○ ⟨⟩-congˡ identityˡ)) ○ pullˡ sum-sˡ
              ○ assoc ○ ∘-resp-≈ʳ sum-zˡ ○ identityʳ ○ sym identityˡ

      -- min(m, k+1) = min(m,k) + sgn(m∸k).  TODO: belongs in Primitive.agda.
      min-sʳ : min ∘ (id ×₁ s) ≈ sum ∘ ⟨ min , sgn ∘ sub ⟩
      min-sʳ = cancel (LHSeq ○ sym RHSeq)
        where
          sgn-sub-helper : sum ∘ ⟨ sgn ∘ sub , s⁻¹ ∘ sub ⟩ ≈ sub
          sgn-sub-helper = ∘-resp-≈ʳ (sym ⟨⟩∘) ○ sym-assoc ○ (sgn-pred ⟩∘⟨refl) ○ identityˡ

          LHSeq : sum ∘ ⟨ min ∘ (id ×₁ s) , sub ∘ (id ×₁ s) ⟩ ≈ π₁
          LHSeq = (refl⟩∘⟨ sym ⟨⟩∘) ○ pullˡ sum-min-sub ○ π₁∘×₁ ○ identityˡ

          RHSeq : sum ∘ ⟨ sum ∘ ⟨ min , sgn ∘ sub ⟩ , sub ∘ (id ×₁ s) ⟩ ≈ π₁
          RHSeq = (refl⟩∘⟨ ⟨⟩-congˡ sub-sʳ) ○ sum-assoc•
                ○ ∘-resp-≈ʳ (⟨⟩-congˡ sgn-sub-helper) ○ sum-min-sub

      G-z : G ∘ ⟨ id , z ∘ ! ⟩ ≈ ⟨ id , z ∘ ! ⟩ ∘ ι
      G-z = ⟨⟩∘ ○ ⟨⟩-cong₂
        (pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ project₁ ○ identityʳ)
                               (pullʳ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ○ sub-zʳ)
                     ○ ×₁-η) ○ identityʳ)
        (pullʳ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ○ min-zʳ)
        ○ sym (⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ (pullʳ !-unique₂))

      -- chopᴺ-step on an ι-value: strip one later from the value (count ↦ s⁻¹ count) and
      -- bump the index by sgn(count) (0 if the value was `now`, 1 if it was `later`).
      -- TODO: prove via ι-commutes + the from-iso coproduct split.
      chopᴺ-step-ι×₁ : chopᴺ-step ∘ (ι ×₁ id) ≈ ⟨ ι ∘ (id ×₁ s⁻¹) ∘ π₁ , sum ∘ ⟨ π₂ , sgn ∘ π₂ ∘ π₁ ⟩ ⟩
      chopᴺ-step-ι×₁ = formB ○ ⟨⟩-unique′ valpart idxpart
        where
          fr : (X × N) ⇒ X + X × N
          fr = _≅_.from nno-iso

          from-zero : fr ∘ ⟨ id , z ∘ ! ⟩ ≈ i₁
          from-zero = ∘-resp-≈ʳ (sym inject₁) ○ cancelˡ (_≅_.isoʳ nno-iso)

          from-succ : fr ∘ (id ×₁ s) ≈ i₂
          from-succ = ∘-resp-≈ʳ (sym inject₂) ○ cancelˡ (_≅_.isoʳ nno-iso)

          ι-decomp : ι ≈ [ now , later ∘ ι ] ∘ fr
          ι-decomp = begin
            ι                        ≈⟨ introˡ out⁻¹∘out ⟩
            (out⁻¹ ∘ out) ∘ ι        ≈⟨ assoc ⟩
            out⁻¹ ∘ out ∘ ι          ≈⟨ refl⟩∘⟨ ι-commutes ⟩
            out⁻¹ ∘ (id +₁ ι) ∘ fr   ≈⟨ pullˡ (∘-resp-≈ˡ out⁻¹-now-later ○ []∘+₁ ○ []-cong₂ identityʳ refl) ⟩
            [ now , later ∘ ι ] ∘ fr ∎

          ipred : [ now , ι ] ∘ fr ≈ ι ∘ (id ×₁ s⁻¹)
          ipred = z-or-s-≈ ipz ips
            where
              ipz : ([ now , ι ] ∘ fr) ∘ ⟨ id , z ∘ ! ⟩ ≈ (ι ∘ (id ×₁ s⁻¹)) ∘ ⟨ id , z ∘ ! ⟩
              ipz = begin
                ([ now , ι ] ∘ fr) ∘ ⟨ id , z ∘ ! ⟩ ≈⟨ pullʳ from-zero ⟩
                [ now , ι ] ∘ i₁                    ≈⟨ inject₁ ⟩
                now                                 ≈⟨ ι-zero ⟨
                ι ∘ ⟨ id , z ∘ ! ⟩                  ≈⟨ pullʳ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ (pullˡ s⁻¹-zero)) ⟨
                (ι ∘ (id ×₁ s⁻¹)) ∘ ⟨ id , z ∘ ! ⟩  ∎
              ips : ([ now , ι ] ∘ fr) ∘ (id ×₁ s) ≈ (ι ∘ (id ×₁ s⁻¹)) ∘ (id ×₁ s)
              ips = begin
                ([ now , ι ] ∘ fr) ∘ (id ×₁ s) ≈⟨ pullʳ from-succ ⟩
                [ now , ι ] ∘ i₂               ≈⟨ inject₂ ⟩
                ι                              ≈⟨ identityʳ ⟨
                ι ∘ id                         ≈⟨ pullʳ (×₁∘×₁ ○ ×₁-cong₂ identityˡ s⁻¹-succ ○ ⟨⟩-cong₂ identityˡ identityˡ ○ ×₁-η) ⟨
                (ι ∘ (id ×₁ s⁻¹)) ∘ (id ×₁ s)  ∎

          sgnfrom : [ z ∘ ! , s ∘ z ∘ ! ] ∘ fr ≈ sgn ∘ π₂
          sgnfrom = z-or-s-≈ sgz sgs
            where
              sgz : ([ z ∘ ! , s ∘ z ∘ ! ] ∘ fr) ∘ ⟨ id , z ∘ ! ⟩ ≈ (sgn ∘ π₂) ∘ ⟨ id , z ∘ ! ⟩
              sgz = begin
                ([ z ∘ ! , s ∘ z ∘ ! ] ∘ fr) ∘ ⟨ id , z ∘ ! ⟩ ≈⟨ pullʳ from-zero ⟩
                [ z ∘ ! , s ∘ z ∘ ! ] ∘ i₁                    ≈⟨ inject₁ ⟩
                z ∘ !                                         ≈⟨ pullˡ sgn-z ⟨
                sgn ∘ z ∘ !                                   ≈⟨ refl⟩∘⟨ project₂ ⟨
                sgn ∘ π₂ ∘ ⟨ id , z ∘ ! ⟩                     ≈⟨ sym-assoc ⟩
                (sgn ∘ π₂) ∘ ⟨ id , z ∘ ! ⟩                   ∎
              sgs : ([ z ∘ ! , s ∘ z ∘ ! ] ∘ fr) ∘ (id ×₁ s) ≈ (sgn ∘ π₂) ∘ (id ×₁ s)
              sgs = (pullʳ from-succ ○ inject₂) ○ sym sgs-rhs
                where
                  sgs-rhs : (sgn ∘ π₂) ∘ (id ×₁ s) ≈ s ∘ z ∘ !
                  sgs-rhs = begin
                    (sgn ∘ π₂) ∘ (id ×₁ s) ≈⟨ pullʳ π₂∘×₁ ⟩
                    sgn ∘ s ∘ π₂           ≈⟨ pullˡ sgn-s ⟩
                    (s ∘ z ∘ !) ∘ π₂       ≈⟨ pullʳ (pullʳ !-unique₂) ⟩
                    s ∘ z ∘ !              ∎

          dist-[] : [ now ×₁ id , (later ∘ ι) ×₁ id ] ∘ distributeʳ⁻¹ ≈ [ now , later ∘ ι ] ×₁ id
          dist-[] = sym (introʳ (IsIso.isoʳ isIsoʳ) ○ sym-assoc ○ (dr ⟩∘⟨refl))
            where
              dr : ([ now , later ∘ ι ] ×₁ id) ∘ distributeʳ ≈ [ now ×₁ id , (later ∘ ι) ×₁ id ]
              dr = ∘[] ○ []-cong₂ (×₁∘×₁ ○ ×₁-cong₂ inject₁ identityˡ) (×₁∘×₁ ○ ×₁-cong₂ inject₂ identityˡ)

          -- chopᴺ-step on the value decomposed over fr
          formB : chopᴺ-step ∘ (ι ×₁ id) ≈ [ now ×₁ id , ι ×₁ s ] ∘ distributeʳ⁻¹ ∘ (fr ×₁ id)
          formB = begin
            chopᴺ-step ∘ (ι ×₁ id)                                                                       ≈⟨ refl⟩∘⟨ (×₁-cong₂ ι-decomp refl ○ sym (×₁∘×₁ ○ ×₁-cong₂ refl identityˡ)) ⟩
            chopᴺ-step ∘ ([ now , later ∘ ι ] ×₁ id) ∘ (fr ×₁ id)                                        ≈⟨ refl⟩∘⟨ (sym dist-[] ⟩∘⟨refl) ⟩
            chopᴺ-step ∘ ([ now ×₁ id , (later ∘ ι) ×₁ id ] ∘ distributeʳ⁻¹) ∘ (fr ×₁ id)                ≈⟨ extendʳ (pullˡ ∘[]) ⟩
            [ chopᴺ-step ∘ (now ×₁ id) , chopᴺ-step ∘ ((later ∘ ι) ×₁ id) ] ∘ distributeʳ⁻¹ ∘ (fr ×₁ id) ≈⟨ ([]-cong₂ chopᴺ-step-now stepι) ⟩∘⟨refl ⟩
            [ now ×₁ id , ι ×₁ s ] ∘ distributeʳ⁻¹ ∘ (fr ×₁ id)                                          ∎
            where
              stepι : chopᴺ-step ∘ ((later ∘ ι) ×₁ id) ≈ ι ×₁ s
              stepι = ∘-resp-≈ʳ (sym (×₁∘×₁ ○ ×₁-cong₂ refl identityˡ)) ○ pullˡ chopᴺ-step-later
                    ○ ×₁∘×₁ ○ ×₁-cong₂ identityˡ identityʳ

          valpart : π₁ ∘ ([ now ×₁ id , ι ×₁ s ] ∘ distributeʳ⁻¹ ∘ (fr ×₁ id)) ≈ π₁ ∘ ⟨ ι ∘ (id ×₁ s⁻¹) ∘ π₁ , sum ∘ ⟨ π₂ , sgn ∘ π₂ ∘ π₁ ⟩ ⟩
          valpart = begin
            π₁ ∘ ([ now ×₁ id , ι ×₁ s ] ∘ distributeʳ⁻¹ ∘ (fr ×₁ id))   ≈⟨ sym-assoc ⟩
            (π₁ ∘ [ now ×₁ id , ι ×₁ s ]) ∘ distributeʳ⁻¹ ∘ (fr ×₁ id)   ≈⟨ (∘[] ○ []-cong₂ π₁∘×₁ π₁∘×₁) ⟩∘⟨refl ⟩
            [ now ∘ π₁ , ι ∘ π₁ ] ∘ distributeʳ⁻¹ ∘ (fr ×₁ id)           ≈⟨ (sym []∘+₁) ⟩∘⟨refl ⟩
            ([ now , ι ] ∘ (π₁ +₁ π₁)) ∘ distributeʳ⁻¹ ∘ (fr ×₁ id)      ≈⟨ assoc ○ refl⟩∘⟨ sym-assoc ⟩
            [ now , ι ] ∘ ((π₁ +₁ π₁) ∘ distributeʳ⁻¹) ∘ (fr ×₁ id)      ≈⟨ refl⟩∘⟨ (distributeʳ⁻¹-π₁ ⟩∘⟨refl) ⟩
            [ now , ι ] ∘ π₁ ∘ (fr ×₁ id)                                ≈⟨ refl⟩∘⟨ π₁∘×₁ ⟩
            [ now , ι ] ∘ fr ∘ π₁                                        ≈⟨ extendʳ ipred ⟩
            ι ∘ (id ×₁ s⁻¹) ∘ π₁                                         ≈⟨ project₁ ⟨
            π₁ ∘ ⟨ ι ∘ (id ×₁ s⁻¹) ∘ π₁ , sum ∘ ⟨ π₂ , sgn ∘ π₂ ∘ π₁ ⟩ ⟩ ∎

          idxpart : π₂ ∘ ([ now ×₁ id , ι ×₁ s ] ∘ distributeʳ⁻¹ ∘ (fr ×₁ id)) ≈ π₂ ∘ ⟨ ι ∘ (id ×₁ s⁻¹) ∘ π₁ , sum ∘ ⟨ π₂ , sgn ∘ π₂ ∘ π₁ ⟩ ⟩
          idxpart = begin
            π₂ ∘ ([ now ×₁ id , ι ×₁ s ] ∘ distributeʳ⁻¹ ∘ (fr ×₁ id))                                                  ≈⟨ sym-assoc ⟩
            (π₂ ∘ [ now ×₁ id , ι ×₁ s ]) ∘ distributeʳ⁻¹ ∘ (fr ×₁ id)                                                  ≈⟨ (∘[] ○ []-cong₂ (π₂∘×₁ ○ identityˡ) π₂∘×₁) ⟩∘⟨refl ⟩
            [ π₂ , s ∘ π₂ ] ∘ distributeʳ⁻¹ ∘ (fr ×₁ id)                                                                ≈⟨ br ⟩∘⟨refl ⟩
            (sum ∘ ⟨ [ π₂ , π₂ ] , [ z ∘ ! , s ∘ z ∘ ! ] ⟩) ∘ distributeʳ⁻¹ ∘ (fr ×₁ id)                                ≈⟨ assoc ⟩
            sum ∘ ⟨ [ π₂ , π₂ ] , [ z ∘ ! , s ∘ z ∘ ! ] ⟩ ∘ distributeʳ⁻¹ ∘ (fr ×₁ id)                                  ≈⟨ refl⟩∘⟨ ⟨⟩∘ ⟩
            sum ∘ ⟨ [ π₂ , π₂ ] ∘ (distributeʳ⁻¹ ∘ (fr ×₁ id)) , [ z ∘ ! , s ∘ z ∘ ! ] ∘ (distributeʳ⁻¹ ∘ (fr ×₁ id)) ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ p1 p2 ⟩
            sum ∘ ⟨ π₂ , sgn ∘ π₂ ∘ π₁ ⟩                                                                                ≈⟨ project₂ ⟨
            π₂ ∘ ⟨ ι ∘ (id ×₁ s⁻¹) ∘ π₁ , sum ∘ ⟨ π₂ , sgn ∘ π₂ ∘ π₁ ⟩ ⟩                                                ∎
            where
              br : [ π₂ , s ∘ π₂ ] ≈ sum ∘ ⟨ [ π₂ , π₂ ] , [ z ∘ ! , s ∘ z ∘ ! ] ⟩
              br = []-unique inj1 inj2
                where
                  sumsz : sum ∘ ⟨ π₂ , s ∘ z ∘ ! ⟩ ≈ s ∘ π₂
                  sumsz = ∘-resp-≈ʳ (sym (×₁∘⟨⟩ ○ ⟨⟩-congʳ identityˡ)) ○ pullˡ sum-sʳ ○ assoc ○ ∘-resp-≈ʳ sum-zʳ
                  
                  inj1 : (sum ∘ ⟨ [ π₂ , π₂ ] , [ z ∘ ! , s ∘ z ∘ ! ] ⟩) ∘ i₁ ≈ π₂
                  inj1 = pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ inject₁ inject₁) ○ sum-zʳ
                  
                  inj2 : (sum ∘ ⟨ [ π₂ , π₂ ] , [ z ∘ ! , s ∘ z ∘ ! ] ⟩) ∘ i₂ ≈ s ∘ π₂
                  inj2 = pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ inject₂ inject₂) ○ sumsz
              p1 : [ π₂ , π₂ ] ∘ (distributeʳ⁻¹ ∘ (fr ×₁ id)) ≈ π₂
              p1 = sym-assoc ○ (distributeʳ⁻¹-π₂ ⟩∘⟨refl) ○ π₂∘×₁ ○ identityˡ
              
              p2 : [ z ∘ ! , s ∘ z ∘ ! ] ∘ (distributeʳ⁻¹ ∘ (fr ×₁ id)) ≈ sgn ∘ π₂ ∘ π₁
              p2 = (bz ⟩∘⟨refl) ○ assoc
                 ○ ∘-resp-≈ʳ (sym-assoc ○ (distributeʳ⁻¹-π₁ ⟩∘⟨refl) ○ π₁∘×₁)
                 ○ sym-assoc ○ (sgnfrom ⟩∘⟨refl) ○ assoc
                where
                  bz : [ z ∘ ! , s ∘ z ∘ ! ] ≈ [ z ∘ ! , s ∘ z ∘ ! ] ∘ (π₁ +₁ π₁)
                  bz = sym ([]∘+₁ ○ []-cong₂ (pullʳ !-unique₂) (assoc ○ ∘-resp-≈ʳ (pullʳ !-unique₂)))

      -- the inductive step: advancing the fuel by one = one chopᴺ-step on the ι-value.
      -- chopᴺ-step's now/later split (value count zero vs positive, i.e. m ≤ k vs m > k)
      -- is exactly min's case split (carried branch-free by sgn).
      Gstep : G ∘ (id ×₁ s) ≈ chopᴺ-step ∘ G
      Gstep = begin
        G ∘ (id ×₁ s)                                                                                              ≈⟨ ⟨⟩∘ ⟩
        ⟨ (ι ∘ ⟨ π₁ ∘ π₁ , sub ∘ (π₂ ×₁ id) ⟩) ∘ (id ×₁ s) , (min ∘ (π₂ ×₁ id)) ∘ (id ×₁ s) ⟩                      ≈⟨ ⟨⟩-cong₂ valeq idxeq ⟩
        ⟨ ι ∘ (id ×₁ s⁻¹) ∘ ⟨ π₁ ∘ π₁ , sub ∘ (π₂ ×₁ id) ⟩ , sum ∘ ⟨ min ∘ (π₂ ×₁ id) , sgn ∘ sub ∘ (π₂ ×₁ id) ⟩ ⟩ ≈˘⟨ step-eq ⟩
        chopᴺ-step ∘ G                                                                                             ∎
        where
          ps : (π₂ ×₁ id) ∘ (id ×₁ s) ≈ (id ×₁ s) ∘ (π₂ ×₁ id)
          ps = ×₁∘×₁ ○ ×₁-cong₂ identityʳ identityˡ ○ ×₁-cong₂ (sym identityˡ) (sym identityʳ) ○ sym ×₁∘×₁

          valeq : (ι ∘ ⟨ π₁ ∘ π₁ , sub ∘ (π₂ ×₁ id) ⟩) ∘ (id ×₁ s)
                ≈ ι ∘ (id ×₁ s⁻¹) ∘ ⟨ π₁ ∘ π₁ , sub ∘ (π₂ ×₁ id) ⟩
          valeq = pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ π₁∘×₁ ○ ∘-resp-≈ʳ identityˡ)
                                         (assoc ○ (refl⟩∘⟨ ps) ○ pullˡ sub-sʳ ○ assoc)
                                ○ sym (×₁∘⟨⟩ ○ ⟨⟩-congʳ identityˡ))

          idxeq : (min ∘ (π₂ ×₁ id)) ∘ (id ×₁ s) ≈ sum ∘ ⟨ min ∘ (π₂ ×₁ id) , sgn ∘ sub ∘ (π₂ ×₁ id) ⟩
          idxeq = assoc ○ (refl⟩∘⟨ ps) ○ pullˡ min-sʳ ○ assoc ○ ∘-resp-≈ʳ (⟨⟩∘ ○ ⟨⟩-congˡ assoc)

          step-eq : chopᴺ-step ∘ G
                  ≈ ⟨ ι ∘ (id ×₁ s⁻¹) ∘ ⟨ π₁ ∘ π₁ , sub ∘ (π₂ ×₁ id) ⟩ , sum ∘ ⟨ min ∘ (π₂ ×₁ id) , sgn ∘ sub ∘ (π₂ ×₁ id) ⟩ ⟩
          step-eq = ∘-resp-≈ʳ (sym (×₁∘⟨⟩ ○ ⟨⟩-congˡ identityˡ))
                  ○ pullˡ chopᴺ-step-ι×₁
                  ○ ⟨⟩∘
                  ○ ⟨⟩-cong₂ (assoc ○ ∘-resp-≈ʳ (pullʳ project₁))
                             (assoc ○ ∘-resp-≈ʳ (⟨⟩∘ ○ ⟨⟩-cong₂ project₂
                                                     (assoc ○ (refl⟩∘⟨ (pullʳ project₁ ○ project₂)))))

      G-s : G ∘ (id ×₁ s) ≈ ((chopᴺ-step ∘ π₁) ∘ (id ×₁ ι ×₁ id)) ∘ ⟨ G , id ⟩
      G-s = Gstep ○ sym (assoc ○ (refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ identityʳ)) ○ pullʳ project₁)

  -- chopᴺ-step commutes with the functorial action D₁ f on the value.
  chopᴺ-step-natural : ∀ {Z W} (f : Z ⇒ W) → chopᴺ-step ∘ (D₁ f ×₁ id) ≈ (D₁ f ×₁ id) ∘ chopᴺ-step
  chopᴺ-step-natural f = begin
    chopᴺ-step ∘ (D₁ f ×₁ id)                                                                                        ≈⟨ pullʳ (pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ (assoc ○ (refl⟩∘⟨ π₁∘×₁) ○ sym-assoc ○ (D₁-commutes f ⟩∘⟨refl) ○ assoc) identityˡ)) ⟩
    [ π₂ , second (s ∘ π₂) ] ∘ distributeʳ⁻¹ ∘ ⟨ (f +₁ D₁ f) ∘ out ∘ π₁ , D₁ f ×₁ id ⟩                               ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-congˡ identityʳ) ⟨
    [ π₂ , second (s ∘ π₂) ] ∘ distributeʳ⁻¹ ∘ ((f +₁ D₁ f) ×₁ (D₁ f ×₁ id)) ∘ ⟨ out ∘ π₁ , id ⟩                     ≈⟨ refl⟩∘⟨ sym-assoc ⟩
    [ π₂ , second (s ∘ π₂) ] ∘ (distributeʳ⁻¹ ∘ ((f +₁ D₁ f) ×₁ (D₁ f ×₁ id))) ∘ ⟨ out ∘ π₁ , id ⟩                   ≈⟨ refl⟩∘⟨ (sym (distributeʳ⁻¹-natural (D₁ f ×₁ id) f (D₁ f)) ⟩∘⟨refl) ⟩
    [ π₂ , second (s ∘ π₂) ] ∘ (((f ×₁ (D₁ f ×₁ id)) +₁ (D₁ f ×₁ (D₁ f ×₁ id))) ∘ distributeʳ⁻¹) ∘ ⟨ out ∘ π₁ , id ⟩ ≈⟨ refl⟩∘⟨ assoc ⟩
    [ π₂ , second (s ∘ π₂) ] ∘ ((f ×₁ (D₁ f ×₁ id)) +₁ (D₁ f ×₁ (D₁ f ×₁ id))) ∘ distributeʳ⁻¹ ∘ ⟨ out ∘ π₁ , id ⟩   ≈⟨ pullˡ []∘+₁ ○ extendʳ (∘-resp-≈ˡ ([]-cong₂ π₂∘×₁ (second∘×₁ ○ ×₁-cong₂ refl (pullʳ π₂∘first)))) ⟩
    [ (D₁ f ×₁ id) ∘ π₂ , D₁ f ×₁ s ∘ π₂ ] ∘ distributeʳ⁻¹ ∘ ⟨ out ∘ π₁ , id ⟩                                       ≈⟨ pullˡ (∘[] ○ []-congˡ first∘second) ⟨
    (D₁ f ×₁ id) ∘ chopᴺ-step                                                                                        ∎

  -- chopᴺ is natural in the value.
  chopᴺ-natural : ∀ {Z W} (f : Z ⇒ W) → chopᴺ ∘ (D₁ f ×₁ id) ≈ (D₁ f ×₁ id) ∘ chopᴺ
  chopᴺ-natural f = prec-natural ○ prec-cong zero-eq succ-eq ○ sym (prec-uniform unif-hyp)
    where
      zero-eq : ⟨ id , z ∘ ! ⟩ ∘ D₁ f ≈ (D₁ f ×₁ id) ∘ ⟨ id , z ∘ ! ⟩
      zero-eq = ⟨⟩∘ ○ ⟨⟩-cong₂ (sym id-comm) (pullʳ !-unique₂) ○ sym first∘⟨⟩

      succ-eq : (chopᴺ-step ∘ π₁) ∘ (id ×₁ D₁ f ×₁ id) ≈ chopᴺ-step ∘ π₁
      succ-eq = pullʳ π₁∘second

      unif-hyp : (D₁ f ×₁ id) ∘ (chopᴺ-step ∘ π₁) ≈ (chopᴺ-step ∘ π₁) ∘ ((D₁ f ×₁ id) ×₁ id)
      unif-hyp = sym-assoc ○ (sym (chopᴺ-step-natural f) ⟩∘⟨refl) ○ assoc ○ (refl⟩∘⟨ sym π₁∘×₁) ○ sym-assoc

  -- "delay value by n":  dl(d, n) = laterⁿ d.  This is the value component of the
  -- section that chopᴺ retracts.
  dl : ∀ {Z} → D₀ Z × N ⇒ D₀ Z
  dl = prec id (later ∘ π₁)

  dl-zero : ∀ {Z} → dl {Z} ∘ ⟨ id , z ∘ ! ⟩ ≈ id
  dl-zero = prec-zero

  dl-succ : ∀ {Z} → dl {Z} ∘ (id ×₁ s) ≈ later ∘ dl
  dl-succ = prec-succ ○ pullʳ project₁

  -- chopᴺ-step does not change the delay encoded by dl (now: same; later: shift absorbed).
  dl-chopᴺ-step : ∀ {Z} → dl {Z} ∘ chopᴺ-step ≈ dl
  dl-chopᴺ-step = prec-unique zero-eq succ-eq
    where
      now-case : ((dl ∘ chopᴺ-step) ∘ ⟨ id , z ∘ ! ⟩) ∘ now ≈ id ∘ now
      now-case = begin
        ((dl ∘ chopᴺ-step) ∘ ⟨ id , z ∘ ! ⟩) ∘ now     ≈⟨ assoc ○ assoc ⟩
        dl ∘ chopᴺ-step ∘ ⟨ id , z ∘ ! ⟩ ∘ now         ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ (pullʳ !-unique₂)) ⟩
        dl ∘ chopᴺ-step ∘ ⟨ now , z ∘ ! ⟩              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟨
        dl ∘ chopᴺ-step ∘ (now ×₁ id) ∘ ⟨ id , z ∘ ! ⟩ ≈⟨ refl⟩∘⟨ pullˡ chopᴺ-step-now ⟩
        dl ∘ (now ×₁ id) ∘ ⟨ id , z ∘ ! ⟩              ≈⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟩
        dl ∘ ⟨ now , z ∘ ! ⟩                           ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ (pullʳ !-unique₂)) ⟨
        dl ∘ ⟨ id , z ∘ ! ⟩ ∘ now                      ≈⟨ pullˡ dl-zero ⟩
        id ∘ now                                       ∎

      later-case : ((dl ∘ chopᴺ-step) ∘ ⟨ id , z ∘ ! ⟩) ∘ later ≈ id ∘ later
      later-case = begin
        ((dl ∘ chopᴺ-step) ∘ ⟨ id , z ∘ ! ⟩) ∘ later     ≈⟨ assoc ○ assoc ⟩
        dl ∘ chopᴺ-step ∘ ⟨ id , z ∘ ! ⟩ ∘ later         ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ (pullʳ !-unique₂)) ⟩
        dl ∘ chopᴺ-step ∘ ⟨ later , z ∘ ! ⟩              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟨
        dl ∘ chopᴺ-step ∘ (later ×₁ id) ∘ ⟨ id , z ∘ ! ⟩ ≈⟨ refl⟩∘⟨ pullˡ chopᴺ-step-later ⟩
        dl ∘ (id ×₁ s) ∘ ⟨ id , z ∘ ! ⟩                  ≈⟨ pullˡ dl-succ ⟩
        (later ∘ dl) ∘ ⟨ id , z ∘ ! ⟩                    ≈⟨ pullʳ dl-zero ⟩
        later ∘ id                                       ≈⟨ id-comm ⟩
        id ∘ later                                       ∎

      zero-eq : (dl ∘ chopᴺ-step) ∘ ⟨ id , z ∘ ! ⟩ ≈ id
      zero-eq = D-jointly-epic now-case later-case

      succ-eq : (dl ∘ chopᴺ-step) ∘ (id ×₁ s) ≈ (later ∘ π₁) ∘ ⟨ dl ∘ chopᴺ-step , id ⟩
      succ-eq = assoc ○ (refl⟩∘⟨ chopᴺ-step-comm) ○ sym-assoc ○ (dl-succ ⟩∘⟨refl)
              ○ assoc ○ (refl⟩∘⟨ sym project₁) ○ sym-assoc

  -- chopᴺ left-inverts the delay map on the value: re-delaying recovers d.
  μchopᴺ : ∀ {Z} → dl {Z} ∘ chopᴺ ≈ π₁
  μchopᴺ = prec-unique zero-eq succ-eq ○ prec-η id ○ identityˡ
    where
      zero-eq : (dl ∘ chopᴺ) ∘ ⟨ id , z ∘ ! ⟩ ≈ id
      zero-eq = pullʳ prec-zero ○ dl-zero

      succ-eq : (dl ∘ chopᴺ) ∘ (id ×₁ s) ≈ π₁ ∘ ⟨ dl ∘ chopᴺ , id ⟩
      succ-eq = assoc ○ (refl⟩∘⟨ prec-succ ○ ∘-resp-≈ʳ (pullʳ project₁)) ○ sym-assoc ○ (dl-chopᴺ-step ⟩∘⟨refl) ○ sym project₁

  chopᴺ-section : ∀ {Z} → chopᴺ {Z} ∘ ⟨ dl , π₂ ⟩ ≈ id
  chopᴺ-section = prec-unique zero-eq succ-eq ○ sym (prec-unique identityˡ ids)
    where
      zero-eq : (chopᴺ ∘ ⟨ dl , π₂ ⟩) ∘ ⟨ id , z ∘ ! ⟩ ≈ ⟨ id , z ∘ ! ⟩
      zero-eq = begin
        (chopᴺ ∘ ⟨ dl , π₂ ⟩) ∘ ⟨ id , z ∘ ! ⟩ ≈⟨ pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ dl-zero project₂) ⟩
        chopᴺ ∘ ⟨ id , z ∘ ! ⟩                 ≈⟨ prec-zero ⟩
        ⟨ id , z ∘ ! ⟩                         ∎

      succ-eq : (chopᴺ ∘ ⟨ dl , π₂ ⟩) ∘ (id ×₁ s) ≈ ((id ×₁ s) ∘ π₁) ∘ ⟨ chopᴺ ∘ ⟨ dl , π₂ ⟩ , id ⟩
      succ-eq = begin
        (chopᴺ ∘ ⟨ dl , π₂ ⟩) ∘ (id ×₁ s)               ≈⟨ pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ dl-succ π₂∘×₁) ⟩
        chopᴺ ∘ ⟨ later ∘ dl , s ∘ π₂ ⟩                 ≈⟨ refl⟩∘⟨ ×₁∘⟨⟩ ⟨
        chopᴺ ∘ (later ×₁ s) ∘ ⟨ dl , π₂ ⟩              ≈⟨ pullˡ chopᴺ-later ⟩
        ((id ×₁ s) ∘ chopᴺ) ∘ ⟨ dl , π₂ ⟩               ≈⟨ assoc ⟩
        (id ×₁ s) ∘ chopᴺ ∘ ⟨ dl , π₂ ⟩                 ≈⟨ pullʳ project₁ ⟨
        ((id ×₁ s) ∘ π₁) ∘ ⟨ chopᴺ ∘ ⟨ dl , π₂ ⟩ , id ⟩ ∎

      ids : id ∘ (id ×₁ s) ≈ ((id ×₁ s) ∘ π₁) ∘ ⟨ id , id ⟩
      ids = identityˡ ○ sym (pullʳ project₁ ○ identityʳ)

  -- chopᴺ splits as an idempotent: D₀Z is a retract of D₀Z × N (the index-0 slice).
  chop-retractᴺ : ∀ Z → Retract (D₀ Z) (D₀ Z × N)
  chop-retractᴺ Z .Mor.Retract.section    = ⟨ id , z ∘ ! ⟩
  chop-retractᴺ Z .Mor.Retract.retract    = π₁ ∘ chopᴺ {Z}
  chop-retractᴺ Z .Mor.Retract.is-retract = pullʳ prec-zero ○ project₁

  -- pull-later transports ι's value-step to chopᴺ-step.  Both sides send (d,c) to
  -- laterᶜ (f d), where f peels one step of d to the outer level; so both
  -- equal prec f (later ∘ π₁).
  ψ-ι : ∀ {Z} → pull-later {Z} ∘ ι ≈ ι ∘ chopᴺ-step
  ψ-ι {Z} = prec-unique L-zero L-succ ○ sym (prec-unique R-zero R-succ)
    where
      f : D₀ Z ⇒ D₀ (D₀ Z)
      f = out⁻¹ ∘ (now +₁ now) ∘ out

      L-zero : (pull-later ∘ ι) ∘ ⟨ id , z ∘ ! ⟩ ≈ f
      L-zero = pullʳ ι-zero ○ DK.identityʳ

      L-succ : (pull-later ∘ ι) ∘ (id ×₁ s) ≈ (later ∘ π₁) ∘ ⟨ pull-later ∘ ι , id ⟩
      L-succ = pullʳ ι-succ ○ pullˡ (sym (Later∘Extend.later-extend-comm f)) ○ assoc ○ sym (pullʳ project₁)

      R-succ : (ι ∘ chopᴺ-step) ∘ (id ×₁ s) ≈ (later ∘ π₁) ∘ ⟨ ι ∘ chopᴺ-step , id ⟩
      R-succ = pullʳ chopᴺ-step-comm ○ pullˡ ι-succ ○ assoc ○ sym (pullʳ project₁)

      -- the two head-constructor branches of the value d: now and later.
      gnow : ((ι ∘ chopᴺ-step) ∘ ⟨ id , z ∘ ! ⟩) ∘ now ≈ now ∘ now
      gnow = begin
        ((ι ∘ chopᴺ-step) ∘ ⟨ id , z ∘ ! ⟩) ∘ now     ≈⟨ assoc ⟩
        (ι ∘ chopᴺ-step) ∘ ⟨ id , z ∘ ! ⟩ ∘ now       ≈⟨ assoc ⟩
        ι ∘ chopᴺ-step ∘ ⟨ id , z ∘ ! ⟩ ∘ now         ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ (pullʳ !-unique₂)) ⟩
        ι ∘ chopᴺ-step ∘ ⟨ now , z ∘ ! ⟩              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟨
        ι ∘ chopᴺ-step ∘ (now ×₁ id) ∘ ⟨ id , z ∘ ! ⟩ ≈⟨ refl⟩∘⟨ pullˡ chopᴺ-step-now ⟩
        ι ∘ (now ×₁ id) ∘ ⟨ id , z ∘ ! ⟩              ≈⟨ pullˡ (ι-natural now) ⟩
        (D₁ now ∘ ι) ∘ ⟨ id , z ∘ ! ⟩                 ≈⟨ pullʳ ι-zero ⟩
        D₁ now ∘ now                                  ≈⟨ sym (D.η.commute now) ⟩
        now ∘ now                                     ∎

      glater : ((ι ∘ chopᴺ-step) ∘ ⟨ id , z ∘ ! ⟩) ∘ later ≈ later ∘ now
      glater = begin
        ((ι ∘ chopᴺ-step) ∘ ⟨ id , z ∘ ! ⟩) ∘ later     ≈⟨ assoc ⟩
        (ι ∘ chopᴺ-step) ∘ ⟨ id , z ∘ ! ⟩ ∘ later       ≈⟨ assoc ⟩
        ι ∘ chopᴺ-step ∘ ⟨ id , z ∘ ! ⟩ ∘ later         ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ (pullʳ !-unique₂)) ⟩
        ι ∘ chopᴺ-step ∘ ⟨ later , z ∘ ! ⟩              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟨
        ι ∘ chopᴺ-step ∘ (later ×₁ id) ∘ ⟨ id , z ∘ ! ⟩ ≈⟨ refl⟩∘⟨ pullˡ chopᴺ-step-later ⟩
        ι ∘ (id ×₁ s) ∘ ⟨ id , z ∘ ! ⟩                  ≈⟨ pullˡ ι-succ ⟩
        (later ∘ ι) ∘ ⟨ id , z ∘ ! ⟩                    ≈⟨ pullʳ ι-zero ⟩
        later ∘ now                                     ∎

      -- d = [now,later]∘out, so split into the gnow/glater cases.
      R-zero : (ι ∘ chopᴺ-step) ∘ ⟨ id , z ∘ ! ⟩ ≈ f
      R-zero = begin
        (ι ∘ chopᴺ-step) ∘ ⟨ id , z ∘ ! ⟩                                                                 ≈⟨ introʳ out⁻¹∘out ⟩
        ((ι ∘ chopᴺ-step) ∘ ⟨ id , z ∘ ! ⟩) ∘ out⁻¹ ∘ out                                                 ≈⟨ sym-assoc ⟩
        (((ι ∘ chopᴺ-step) ∘ ⟨ id , z ∘ ! ⟩) ∘ out⁻¹) ∘ out                                               ≈⟨ (∘-resp-≈ʳ out⁻¹-now-later ○ ∘[]) ⟩∘⟨refl ⟩
        [ ((ι ∘ chopᴺ-step) ∘ ⟨ id , z ∘ ! ⟩) ∘ now , ((ι ∘ chopᴺ-step) ∘ ⟨ id , z ∘ ! ⟩) ∘ later ] ∘ out ≈⟨ ([]-cong₂ gnow glater) ⟩∘⟨refl ⟩
        [ now ∘ now , later ∘ now ] ∘ out                                                                 ≈⟨ (sym (∘-resp-≈ˡ out⁻¹-now-later ○ []∘+₁)) ⟩∘⟨refl ⟩
        (out⁻¹ ∘ (now +₁ now)) ∘ out                                                                      ≈⟨ assoc ⟩
        out⁻¹ ∘ (now +₁ now) ∘ out                                                                        ∎

  -- ι̂ recursion (now : ⊤ ⇒ D₀ ⊤)
  ι̂-zero : ι̂ ∘ z ≈ now
  ι̂-zero = begin
    ι̂ ∘ z                  ≈⟨ assoc ⟩
    ι ∘ ⟨ ! , id ⟩ ∘ z     ≈⟨ refl⟩∘⟨ ⟨⟩∘ ⟩
    ι ∘ ⟨ ! ∘ z , id ∘ z ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ !-unique₂ (identityˡ ○ sym (elimʳ !-unique₂)) ⟩
    ι ∘ ⟨ id , z ∘ ! ⟩     ≈⟨ ι-zero ⟩
    now                    ∎

  ι̂-succ : ι̂ ∘ s ≈ later ∘ ι̂
  ι̂-succ = begin
    ι̂ ∘ s                      ≈⟨ assoc ⟩
    ι ∘ ⟨ ! , id ⟩ ∘ s         ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ !-unique₂ identityˡ) ⟩
    ι ∘ ⟨ ! , s ⟩              ≈⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ identityʳ) ⟨
    ι ∘ (id ×₁ s) ∘ ⟨ ! , id ⟩ ≈⟨ pullˡ ι-succ ⟩
    (later ∘ ι) ∘ ⟨ ! , id ⟩   ≈⟨ assoc ⟩
    later ∘ ι̂                  ∎

  ι-chopᴺ : ∀ {Z} → ι ∘ chopᴺ {Z} ≈ chop ∘ (id ×₁ ι̂)
  ι-chopᴺ = lhs ○ sym rhs
    where
      lhs : ι ∘ chopᴺ ≈ prec now (pull-later ∘ π₁)
      lhs = prec-uniform unif ○ prec-cong ι-zero refl
        where
          unif : ι ∘ (chopᴺ-step ∘ π₁) ≈ (pull-later ∘ π₁) ∘ (ι ×₁ id)
          unif = sym-assoc ○ (sym ψ-ι ⟩∘⟨refl) ○ assoc ○ (refl⟩∘⟨ sym π₁∘×₁) ○ sym-assoc

      rhs : chop ∘ (id ×₁ ι̂) ≈ prec now (pull-later ∘ π₁)
      rhs = prec-unique zcase scase
        where
          zcase : (chop ∘ (id ×₁ ι̂)) ∘ ⟨ id , z ∘ ! ⟩ ≈ now
          zcase = begin
            (chop ∘ (id ×₁ ι̂)) ∘ ⟨ id , z ∘ ! ⟩ ≈⟨ pullʳ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ (sym-assoc ○ (ι̂-zero ⟩∘⟨refl))) ⟩
            chop ∘ ⟨ id , now ∘ ! ⟩             ≈⟨ chop-now' ⟩
            now                                 ∎

          scase : (chop ∘ (id ×₁ ι̂)) ∘ (id ×₁ s) ≈ (pull-later ∘ π₁) ∘ ⟨ chop ∘ (id ×₁ ι̂) , id ⟩
          scase = begin
            (chop ∘ (id ×₁ ι̂)) ∘ (id ×₁ s)                ≈⟨ pullʳ (×₁∘×₁ ○ ×₁-cong₂ identityʳ refl) ⟩
            chop ∘ (id ×₁ ι̂ ∘ s)                          ≈⟨ refl⟩∘⟨ ×₁-cong₂ refl ι̂-succ ⟩
            chop ∘ (id ×₁ later ∘ ι̂)                      ≈⟨ refl⟩∘⟨ (×₁-cong₂ (sym identityˡ) refl ○ sym ×₁∘×₁) ⟩
            chop ∘ (id ×₁ later) ∘ (id ×₁ ι̂)              ≈⟨ pullˡ chop-later ⟩
            (pull-later ∘ chop) ∘ (id ×₁ ι̂)               ≈⟨ assoc ⟩
            pull-later ∘ chop ∘ (id ×₁ ι̂)                 ≈⟨ refl⟩∘⟨ sym project₁ ⟩
            pull-later ∘ π₁ ∘ ⟨ chop ∘ (id ×₁ ι̂) , id ⟩   ≈⟨ sym-assoc ⟩
            (pull-later ∘ π₁) ∘ ⟨ chop ∘ (id ×₁ ι̂) , id ⟩ ∎


  -- saturation: running ι(x,m) for m+j steps reaches now x with count m (the true
  -- length), regardless of the extra fuel j.  Domain is (X × N) × N: ⟨⟨x,m⟩,j⟩, bound m+j.
  chopᴺ-sat : ∀ {X} → chopᴺ {X} ∘ ⟨ ι ∘ π₁ , sum ∘ first π₂ ⟩ ≈ (now ×₁ id) ∘ π₁
  chopᴺ-sat {X} = prec-unique lhs-z lhs-s ○ sym (prec-unique rhs-z rhs-s)
    where
      lhs-z : (chopᴺ {X} ∘ ⟨ ι ∘ π₁ , sum ∘ first π₂ ⟩) ∘ ⟨ id , z ∘ ! ⟩ ≈ ⟨ now ∘ π₁ , π₂ ⟩
      lhs-z = begin
        (chopᴺ {X} ∘ ⟨ ι ∘ π₁ , sum ∘ first π₂ ⟩) ∘ ⟨ id , z ∘ ! ⟩ ≈⟨ assoc ⟩
        chopᴺ {X} ∘ ⟨ ι ∘ π₁ , sum ∘ first π₂ ⟩ ∘ ⟨ id , z ∘ ! ⟩   ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ project₁ ○ identityʳ) (assoc ○ ∘-resp-≈ʳ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ○ sum-zʳ)) ⟩
        chopᴺ {X} ∘ ⟨ ι , π₂ ⟩                                     ≈⟨ chopᴺ-Δ ⟩
        ⟨ now ∘ π₁ , π₂ ⟩                                          ∎

      lhs-s : (chopᴺ {X} ∘ ⟨ ι ∘ π₁ , sum ∘ first π₂ ⟩) ∘ (id ×₁ s)
            ≈ (chopᴺ-step ∘ π₁) ∘ ⟨ chopᴺ {X} ∘ ⟨ ι ∘ π₁ , sum ∘ first π₂ ⟩ , id ⟩
      lhs-s = begin
        (chopᴺ {X} ∘ ⟨ ι ∘ π₁ , sum ∘ first π₂ ⟩) ∘ (id ×₁ s)                ≈⟨ assoc ⟩
        chopᴺ {X} ∘ ⟨ ι ∘ π₁ , sum ∘ first π₂ ⟩ ∘ (id ×₁ s)                  ≈⟨ refl⟩∘⟨ P-nat ⟩
        chopᴺ {X} ∘ (id ×₁ s) ∘ ⟨ ι ∘ π₁ , sum ∘ first π₂ ⟩                  ≈⟨ pullˡ (prec-succ ○ pullʳ project₁) ⟩
        (chopᴺ-step ∘ chopᴺ {X}) ∘ ⟨ ι ∘ π₁ , sum ∘ first π₂ ⟩               ≈⟨ assoc ⟩
        chopᴺ-step ∘ chopᴺ {X} ∘ ⟨ ι ∘ π₁ , sum ∘ first π₂ ⟩                 ≈⟨ sym (pullʳ project₁) ⟩
        (chopᴺ-step ∘ π₁) ∘ ⟨ chopᴺ {X} ∘ ⟨ ι ∘ π₁ , sum ∘ first π₂ ⟩ , id ⟩ ∎
        where
          -- the pairing is natural in the fuel j: bumping j bumps only the bound (s∘sum).
          P-nat : ⟨ ι ∘ π₁ , sum ∘ first π₂ ⟩ ∘ (id ×₁ s) ≈ (id ×₁ s) ∘ ⟨ ι ∘ π₁ , sum ∘ first π₂ ⟩
          P-nat = begin
            ⟨ ι ∘ π₁ , sum ∘ first π₂ ⟩ ∘ (id ×₁ s)                 ≈⟨ ⟨⟩∘ ⟩
            ⟨ (ι ∘ π₁) ∘ (id ×₁ s) , (sum ∘ first π₂) ∘ (id ×₁ s) ⟩ ≈⟨ ⟨⟩-cong₂ (pullʳ (π₁∘×₁ ○ identityˡ) ○ sym identityˡ) (assoc ○ ∘-resp-≈ʳ (×₁∘×₁ ○ ×₁-cong₂ identityʳ identityˡ ○ sym (×₁-cong₂ identityˡ identityʳ) ○ sym ×₁∘×₁) ○ pullˡ sum-sʳ ○ assoc) ⟩
            ⟨ id ∘ ι ∘ π₁ , s ∘ sum ∘ first π₂ ⟩                    ≈⟨ sym ×₁∘⟨⟩ ⟩
            (id ×₁ s) ∘ ⟨ ι ∘ π₁ , sum ∘ first π₂ ⟩                 ∎

      rhs-z : ((now ×₁ id) ∘ π₁) ∘ ⟨ id , z ∘ ! ⟩ ≈ ⟨ now ∘ π₁ , π₂ ⟩
      rhs-z = begin
        ((now ×₁ id) ∘ π₁) ∘ ⟨ id , z ∘ ! ⟩ ≈⟨ assoc ⟩
        (now ×₁ id) ∘ π₁ ∘ ⟨ id , z ∘ ! ⟩   ≈⟨ refl⟩∘⟨ project₁ ⟩
        (now ×₁ id) ∘ id                    ≈⟨ identityʳ ⟩
        now ×₁ id                           ≈⟨ ⟨⟩-congˡ identityˡ ⟩
        ⟨ now ∘ π₁ , π₂ ⟩                   ∎

      rhs-s : ((now ×₁ id) ∘ π₁) ∘ (id ×₁ s) ≈ (chopᴺ-step ∘ π₁) ∘ ⟨ (now ×₁ id) ∘ π₁ , id ⟩
      rhs-s = begin
        ((now ×₁ id) ∘ π₁) ∘ (id ×₁ s)                ≈⟨ assoc ⟩
        (now ×₁ id) ∘ π₁ ∘ (id ×₁ s)                  ≈⟨ refl⟩∘⟨ (π₁∘×₁ ○ identityˡ) ⟩
        (now ×₁ id) ∘ π₁                              ≈⟨ (sym chopᴺ-step-now ⟩∘⟨refl) ⟩
        (chopᴺ-step ∘ (now ×₁ id)) ∘ π₁               ≈⟨ assoc ⟩
        chopᴺ-step ∘ (now ×₁ id) ∘ π₁                 ≈⟨ sym (pullʳ project₁) ⟩
        (chopᴺ-step ∘ π₁) ∘ ⟨ (now ×₁ id) ∘ π₁ , id ⟩ ∎

  ι-mono : ∀ {X} → Mono (ι {X})
  ι-mono {X} f g ι∘f≈ι∘g = sym g-η ○ ⟨⟩-cong₂ val-eq idx-eq ○ g-η
    where
      -- now = out⁻¹ ∘ i₁ is mono since i₁ is mono in an extensive category.
      now-mono : ∀ {A} → Mono (now {A})
      now-mono a b eq = Extensive.pullback₁-is-mono extensive a b
        (∘-resp-≈ˡ (sym unitlaw) ○ extendˡ eq ○ ∘-resp-≈ˡ unitlaw) 

      -- run ι∘f for (n_f + n_g) steps: saturates at count n_f (sat-f), and symmetrically n_g (sat-g).
      sat-f : chopᴺ {X} ∘ ⟨ ι ∘ f , sum ∘ ⟨ π₂ ∘ f , π₂ ∘ g ⟩ ⟩ ≈ (now ×₁ id) ∘ f
      sat-f = begin
        chopᴺ {X} ∘ ⟨ ι ∘ f , sum ∘ ⟨ π₂ ∘ f , π₂ ∘ g ⟩ ⟩        ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ project₁) (pullʳ first∘⟨⟩)) ⟨  
        chopᴺ {X} ∘ ⟨ ι ∘ π₁ , sum ∘ first π₂ ⟩ ∘ ⟨ f , π₂ ∘ g ⟩ ≈⟨ pullˡ chopᴺ-sat ⟩
        ((now ×₁ id) ∘ π₁) ∘ ⟨ f , π₂ ∘ g ⟩                      ≈⟨ pullʳ project₁ ⟩
        (now ×₁ id) ∘ f                                          ∎

      sat-g : chopᴺ {X} ∘ ⟨ ι ∘ g , sum ∘ ⟨ π₂ ∘ g , π₂ ∘ f ⟩ ⟩ ≈ (now ×₁ id) ∘ g
      sat-g = begin
        chopᴺ {X} ∘ ⟨ ι ∘ g , sum ∘ ⟨ π₂ ∘ g , π₂ ∘ f ⟩ ⟩        ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ project₁) (pullʳ first∘⟨⟩)) ⟨
        chopᴺ {X} ∘ ⟨ ι ∘ π₁ , sum ∘ first π₂ ⟩ ∘ ⟨ g , π₂ ∘ f ⟩ ≈⟨ pullˡ chopᴺ-sat ⟩
        ((now ×₁ id) ∘ π₁) ∘ ⟨ g , π₂ ∘ f ⟩                      ≈⟨ pullʳ project₁ ⟩
        (now ×₁ id) ∘ g                                          ∎

      -- ι∘f≈ι∘g and sum's commutativity make the two saturating runs literally equal.
      chop-eq : (now ×₁ id) ∘ f ≈ (now ×₁ id) ∘ g
      chop-eq = sym sat-f ○ ∘-resp-≈ʳ (⟨⟩-cong₂ ι∘f≈ι∘g sum-comm•) ○ sat-g

      -- project: the count gives the index, the value (under mono now) gives the value.
      idx-eq : π₂ ∘ f ≈ π₂ ∘ g
      idx-eq = pushˡ (sym π₂∘first) ○ ∘-resp-≈ʳ chop-eq ○ pullˡ π₂∘first

      val-eq : π₁ ∘ f ≈ π₁ ∘ g
      val-eq = now-mono (π₁ ∘ f) (π₁ ∘ g) (extendʳ (sym π₁∘×₁) ○ ∘-resp-≈ʳ chop-eq ○ extendʳ π₁∘×₁ )


  ι̂-mono : Mono ι̂
  ι̂-mono f g ι̂∘f≈ι̂∘g = let eq = ι-mono _ _ (sym-assoc ○ ι̂∘f≈ι̂∘g ○ assoc)
      in insertˡ project₂ ○ ∘-resp-≈ʳ eq ○ cancelˡ project₂