open import Function.Base using (_$_)
open import Data.Fin using (Fin; zero) renaming (suc to nzero)

open import Categories.Object.NaturalNumbers.Parametrized

open import Categories.Category.Core using (Category)
open import Categories.Object.Terminal 
open import Categories.Monad hiding (id) 
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.Object.Exponential.Canonical using (Exponential)

open import Monad.Instance.Delay

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

module Monad.Instance.Delay.Pullbacks {o ℓ e} {C : Category o ℓ e}
    (extensive : Extensive C) (cartesian : Cartesian C)
    (D : DelayM (Extensive.cocartesian extensive)) where
    
  open Category C
  open import Monad.Instance.Delay.Cartesian extensive cartesian D using (η-nat-pullback)
  private distributive = Extensive×Cartesian⇒Distributive C extensive cartesian
  open import Category.Distributive.Helper distributive hiding (swap; η; cartesian)
  open import Categories.Diagram.Pullback C
  open import Monad.Instance.Delay.Commutative distributive D
  open τ-mod

  open HomReasoning
  open Equiv
  open Mor C
  open MRR C
  open MRP C
  open MR C hiding (glue; glue′)
  open DelayM D
  open D-Kleisli
  open D-Monad
  open import Monad.Helper using (extend⇒F₁)
  module F = D.F
  open F using (homomorphism; F-resp-≈; identity)
  open D.η using (η)
  open D.μ renaming (η to μ)
  open D-Strong
  private ı = ⊤
  open import Monad.Instance.Delay.Zip distributive D
  open import Monad.Instance.Delay.Chop distributive D
  open import Categories.Category.Extensive.Properties C as EP

  -- IMPORTANTLY: τ-nat-pullbackˡ is not valid
  τ-nat-pullbackʳ : ∀ {X Y Z} → (f : Y ⇒ Z) → IsPullback (τ {X}) (id ×₁ D₁ f) (D₁ (id ×₁ f)) τ
  τ-nat-pullbackʳ f .IsPullback.commute = sym (τ-natural id f)
  τ-nat-pullbackʳ f .IsPullback.universal {_}{h₁}{h₂} _ = ⟨ π₁ ∘ h₂ , D₁ π₂ ∘ h₁ ⟩
  τ-nat-pullbackʳ {X}{Y}{Z} f .IsPullback.p₁∘universal≈h₁ {_}{h₁}{h₂}{eq} = RegularMono⇒Mono
    (Section⇒RegularMono $ Mor.Retract.is-retract $ product-retract X Y) (τ ∘ ⟨ π₁ ∘ h₂ , D₁ π₂ ∘ h₁ ⟩) h₁ $
    begin
      ⟨ D₁ π₁ , D₁ π₂ ⟩ ∘ τ ∘ ⟨ π₁ ∘ h₂ , D₁ π₂ ∘ h₁ ⟩ ≈⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ (eq₂ ○ ⟺ eq₁) (pullˡ τ-identityˡ ○ project₂)) ⟩
      ⟨ D₁ π₁ ∘ h₁ , D₁ π₂ ∘ h₁ ⟩                      ≈⟨ ⟨⟩∘ ⟨
      ⟨ D₁ π₁ , D₁ π₂ ⟩ ∘ h₁                           ∎
      where
        τ-assoc-helper : D₁ π₁ ∘ τ ∘ (id ×₁ τ) ≈ D₁ π₁ ∘ τ ∘ (id ×₁ π₂)
        τ-assoc-helper = begin
          D₁ π₁ ∘ τ ∘ (id ×₁ τ)                 ≈⟨ pullˡ (sym homomorphism ○ F-resp-≈ (project₁ ○ identityˡ)) ⟨
          D₁ π₁ ∘ D₁ (id ×₁ π₂) ∘ τ ∘ (id ×₁ τ) ≈⟨ refl⟩∘⟨ (pullˡ (sym (τ-natural id π₂)) ○ pullʳ (×₁∘×₁ ○ ×₁-cong₂ identity² refl)) ⟩
          D₁ π₁ ∘ τ ∘ (id ×₁ (D₁ π₂ ∘ τ))       ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ×₁-cong₂ refl τ-identityˡ ⟩
          D₁ π₁ ∘ τ ∘ (id ×₁ π₂)                ∎ 

        eq₁ : D₁ π₁ ∘ h₁ ≈ D₁ π₁ ∘ τ ∘ h₂
        eq₁ = ∘-resp-≈ˡ (F-resp-≈ (⟺ (project₁ ○ identityˡ))) ○ pushˡ homomorphism ○ ∘-resp-≈ʳ eq

        eq₂ : D₁ π₁ ∘ τ ∘ ⟨ π₁ ∘ h₂ , D₁ π₂ ∘ h₁ ⟩ ≈ D₁ π₁ ∘ τ ∘ h₂
        eq₂ = begin
            D₁ π₁ ∘ τ ∘ ⟨ π₁ ∘ h₂ , D₁ π₂ ∘ h₁ ⟩                ≈⟨ refl⟩∘⟨ (∘-resp-≈ʳ (⟨⟩-congʳ (sym identityˡ)) ○ pushʳ (⟺ ×₁∘⟨⟩) ○ pushˡ (τ-natural id π₂)) ⟩
            D₁ π₁ ∘ D₁ (id ×₁ π₂) ∘ τ ∘ ⟨ π₁ ∘ h₂ , h₁ ⟩        ≈⟨ pullˡ (⟺ homomorphism ○ F-resp-≈ (project₁ ○ identityˡ)) ⟩
            D₁ π₁ ∘ τ ∘ ⟨ π₁ ∘ h₂ , h₁ ⟩                        ≈⟨ pushˡ (F-resp-≈ (sym (project₁ ○ identityˡ)) ○ homomorphism) ⟩
            D₁ π₁ ∘ D₁ (id ×₁ (id ×₁ f)) ∘ τ ∘ ⟨ π₁ ∘ h₂ , h₁ ⟩ ≈⟨ refl⟩∘⟨ (pushʳ (⟨⟩-congʳ (sym identityˡ) ○ ⟺ ×₁∘⟨⟩) ○ pushˡ (τ-natural id (id ×₁ f))) ⟨
            D₁ π₁ ∘ τ ∘ ⟨ π₁ ∘ h₂ , D₁ (id ×₁ f) ∘ h₁ ⟩         ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-congˡ eq ⟩
            D₁ π₁ ∘ τ ∘ ⟨ π₁ ∘ h₂ , τ ∘ h₂ ⟩                    ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-congʳ identityˡ) ⟨
            D₁ π₁ ∘ τ ∘ (id ×₁ τ) ∘ ⟨ π₁ ∘ h₂ , h₂ ⟩            ≈⟨ sym-assoc ○ pullˡ (assoc ○ τ-assoc-helper) ○ assoc²βε ⟩
            D₁ π₁ ∘ τ ∘ (id ×₁ π₂) ∘ ⟨ π₁ ∘ h₂ , h₂ ⟩           ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-congʳ identityˡ) ⟩
            D₁ π₁ ∘ τ ∘ ⟨ π₁ ∘ h₂ , π₂ ∘ h₂ ⟩                   ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ×₁-g-η ⟩
            D₁ π₁ ∘ τ ∘ h₂                                      ∎

  τ-nat-pullbackʳ f .IsPullback.p₂∘universal≈h₂ {_}{h₁}{h₂}{eq} =
    begin
      (id ×₁ D₁ f) ∘ ⟨ π₁ ∘ h₂ , D₁ π₂ ∘ h₁ ⟩ ≈⟨ ×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ (pullˡ (sym (F-resp-≈ project₂ ○ homomorphism))) ⟩
      ⟨ π₁ ∘ h₂ , D₁ (π₂ ∘ (id ×₁ f)) ∘ h₁ ⟩  ≈⟨ ⟨⟩-congˡ (∘-resp-≈ˡ homomorphism ○ pullʳ eq) ⟩
      ⟨ π₁ ∘ h₂ , D₁ π₂ ∘ τ ∘ h₂ ⟩            ≈⟨ ⟨⟩-congˡ (pullˡ τ-identityˡ) ○  ×₁-g-η ⟩
      h₂                                      ∎

  τ-nat-pullbackʳ f .IsPullback.unique-diagram {_}{i}{h} τ∘h≈τ∘i eq = ⟨⟩-unique′
    (pushˡ (sym π₁∘second) ○ ∘-resp-≈ʳ eq ○ pullˡ π₁∘second)
    (pushˡ (sym τ-identityˡ) ○ ∘-resp-≈ʳ τ∘h≈τ∘i ○ pullˡ τ-identityˡ)

  τ-μ-pullback : ∀ {X Y} → IsPullback (D₁ τ ∘ τ) (id ×₁ μ Y) (μ (X × Y)) τ
  τ-μ-pullback .IsPullback.commute = strength.μ-η-comm
  τ-μ-pullback .IsPullback.universal {_}{h₁}{h₂} _ = ⟨ π₁ ∘ h₂ ,  D₁ (D₁ π₂) ∘ h₁ ⟩
  τ-μ-pullback {X}{Y} .IsPullback.p₁∘universal≈h₁ {_}{h₁}{h₂}{eq} = begin
    (D₁ τ ∘ τ) ∘ ⟨ π₁ ∘ h₂ ,  D₁ (D₁ π₂) ∘ h₁ ⟩                                          ≈⟨ cancelˡ chopμD! ⟨
    chop ∘ ⟨ μ (X × Y) , D₁ ! ⟩ ∘ (D₁ τ ∘ τ) ∘ ⟨ π₁ ∘ h₂ ,  D₁ (D₁ π₂) ∘ h₁ ⟩            ≈⟨ refl⟩∘⟨ pullˡ (⟨⟩∘ ○ ⟨⟩-cong₂ strength.μ-η-comm (pullˡ (sym homomorphism ○ F-resp-≈ !-unique₂))) ⟩
    chop ∘ ⟨ τ ∘ (id ×₁ μ Y) , D₁ (! ∘ π₂) ∘ τ ⟩ ∘ ⟨ π₁ ∘ h₂ , D₁ (D₁ π₂) ∘ h₁ ⟩         ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ assoc (∘-resp-≈ˡ (pushˡ homomorphism ○ ∘-resp-≈ʳ τ-identityˡ) ○ pullʳ project₂)) ⟩
    chop ∘ ⟨ τ ∘ (id ×₁ μ Y) ∘ ⟨ π₁ ∘ h₂ , D₁ (D₁ π₂) ∘ h₁ ⟩ , D₁ ! ∘  D₁ (D₁ π₂) ∘ h₁ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ (∘-resp-≈ʳ (sym (×₁∘⟨⟩ ○ ⟨⟩-congʳ identityˡ))) ⟨
    chop ∘ ⟨ τ ∘ ⟨ π₁ ∘ h₂ , μ Y ∘ D₁ (D₁ π₂) ∘ h₁ ⟩ , D₁ ! ∘  D₁ (D₁ π₂) ∘ h₁ ⟩         ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (pushˡ (F-resp-≈ (!-unique _) ○ homomorphism)) ⟨
    chop ∘ ⟨ τ ∘ ⟨ π₁ ∘ h₂ , μ Y ∘ D₁ (D₁ π₂) ∘ h₁ ⟩ , D₁ ! ∘ h₁ ⟩                       ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ (∘-resp-≈ʳ (⟨⟩-congˡ (extendʳ (D.μ.commute π₂)))) ⟩
    chop ∘ ⟨ τ ∘ ⟨ π₁ ∘ h₂ , D₁ π₂ ∘ μ (X × Y) ∘ h₁ ⟩ , D₁ ! ∘ h₁ ⟩                      ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ (∘-resp-≈ʳ (⟨⟩-congˡ (∘-resp-≈ʳ eq))) ⟩
    chop ∘ ⟨ τ ∘ ⟨ π₁ ∘ h₂ , D₁ π₂ ∘ τ ∘ h₂ ⟩ , D₁ ! ∘ h₁ ⟩                              ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ (∘-resp-≈ʳ (⟨⟩-congˡ (pullˡ τ-identityˡ))) ⟩
    chop ∘ ⟨ τ ∘ ⟨ π₁ ∘ h₂ , π₂ ∘ h₂ ⟩ , D₁ ! ∘ h₁ ⟩                                     ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ (eq ○ ∘-resp-≈ʳ (sym ×₁-g-η)) ⟨
    chop ∘ ⟨ μ (X × Y) ∘ h₁ , D₁ ! ∘ h₁ ⟩                                                ≈⟨ refl⟩∘⟨ ⟨⟩∘ ⟨
    chop ∘ ⟨ μ (X × Y) , D₁ ! ⟩ ∘ h₁                                                     ≈⟨ cancelˡ chopμD! ⟩
    h₁                                                                                   ∎

  τ-μ-pullback {X}{Y} .IsPullback.p₂∘universal≈h₂ {_}{h₁}{h₂}{eq} = begin
    (id ×₁ μ Y) ∘  ⟨ π₁ ∘ h₂ ,  D₁ (D₁ π₂) ∘ h₁ ⟩ ≈⟨ ×₁∘⟨⟩ ⟩
    ⟨ id ∘ π₁ ∘ h₂ , μ Y ∘ D₁ (D₁ π₂) ∘ h₁ ⟩      ≈⟨ ⟨⟩-cong₂ identityˡ (extendʳ (D.μ.commute π₂)) ⟩
    ⟨ π₁ ∘ h₂ , D₁ π₂ ∘ μ (X × Y) ∘ h₁ ⟩          ≈⟨ ⟨⟩-congˡ (pushʳ eq ○ ∘-resp-≈ˡ τ-identityˡ ) ⟩
    ⟨ π₁ ∘ h₂ , π₂ ∘ h₂ ⟩                         ≈⟨ ×₁-g-η ⟩
    h₂                                            ∎

  τ-μ-pullback {X}{Y} .IsPullback.unique-diagram {_}{i}{h} Dτ∘τ∘h≈Dτ∘τ∘i eq = ⟨⟩-unique′
    (begin
      π₁ ∘ i               ≈⟨ pullˡ (project₁ ○ identityˡ) ⟨
      π₁ ∘ (id ×₁ μ Y) ∘ i ≈⟨ refl⟩∘⟨ eq ⟩
      π₁ ∘ (id ×₁ μ Y) ∘ h ≈⟨ pullˡ (project₁ ○ identityˡ) ⟩
      π₁ ∘ h               ∎)
    (begin
      π₂ ∘ i                      ≈⟨ pullˡ τ-identityˡ ⟨
      D₁ π₂ ∘ τ ∘ i               ≈⟨ F-resp-≈ τ-identityˡ ⟩∘⟨refl ⟨
      D₁ (D₁ π₂ ∘ τ) ∘ τ ∘ i      ≈⟨ extendʳ (pushˡ homomorphism) ⟩
      D₁ (D₁ π₂) ∘ (D₁ τ ∘ τ) ∘ i ≈⟨ refl⟩∘⟨ Dτ∘τ∘h≈Dτ∘τ∘i ⟩
      D₁ (D₁ π₂) ∘ (D₁ τ ∘ τ) ∘ h ≈⟨ extendʳ (pushˡ homomorphism) ⟨
      D₁ (D₁ π₂ ∘ τ) ∘ τ ∘ h      ≈⟨ F-resp-≈ τ-identityˡ ⟩∘⟨refl ⟩
      D₁ π₂ ∘ τ ∘ h               ≈⟨ pullˡ τ-identityˡ ⟩
      π₂ ∘ h                      ∎)

  module _ (PNNO : ParametrizedNNO C (Distributive.cartesian distributive)) where
    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 (sum; sum-zʳ; sum-sʳ; sub; sub-sum; min; min-sum; sum-min-sub; sum-comm•; prec; prec-zero; prec-zero'; prec-succ; prec-unique; prec-natural; prec-uniform; prec-cong)
    open import Monad.Instance.Delay.ChopNat extensive cartesian D PNNO

    -- ι-naturality square is a pullback 
    ι-nat-pullback : ∀ {X Y} (f : X ⇒ Y) → IsPullback ι (f ×₁ id) (D₁ f) ι
    ι-nat-pullback {X} {Y} f = record
      { commute         = sym (ι-natural f)
      ; universal       = λ eq → IsPullback.universal iPb₁ (thick eq)
      ; p₁∘universal≈h₁ = pushˡ (sym project₁) ○ (refl⟩∘⟨ IsPullback.p₁∘universal≈h₁ iPb₁) ○ project₁
      ; p₂∘universal≈h₂ = IsPullback.p₂∘universal≈h₂ iPb₁
      ; unique-diagram  = λ eq₁ eq₂ → IsPullback.unique-diagram iPb₁ (thick-uniq eq₁ eq₂) eq₂
      }
      where
        -- ι-nat-pullback is by simple reduction to iPb₁ below
        -- iPb₁ is obtained using unglue′. We then prove that the two involved square cells commute 

        top-comm : ⟨ ι , π₂ ⟩ ∘ (f ×₁ id) ≈ (D₁ f ×₁ id) ∘ ⟨ ι , π₂ ⟩
        top-comm = begin
          ⟨ ι , π₂ ⟩ ∘ (f ×₁ id)    ≈⟨ ⟨⟩∘ ○ ⟨⟩-cong₂ (ι-natural f) (π₂∘×₁ ○ identityˡ) ⟩
          ⟨ D₁ f ∘ ι , π₂ ⟩         ≈⟨ ×₁∘⟨⟩ ○ ⟨⟩-congˡ identityˡ ⟨
          (D₁ f ×₁ id) ∘ ⟨ ι , π₂ ⟩ ∎

        bottom-comm : chopᴺ ∘ (D₁ f ×₁ id) ≈ (D₁ f ×₁ id) ∘ chopᴺ
        bottom-comm = chopᴺ-natural f

        jm : JointMono₂ (D₁ f ×₁ id) chopᴺ
        jm g₁ g₂ 2fam = sym g-η ○ ⟨⟩-cong₂ π₁-eq π₂-eq ○ g-η
          where
            π₂-eq : π₂ ∘ g₁ ≈ π₂ ∘ g₂
            π₂-eq = begin
              π₂ ∘ g₁                ≈⟨ pullˡ (π₂∘×₁ ○ identityˡ) ⟨
              π₂ ∘ (D₁ f ×₁ id) ∘ g₁ ≈⟨ refl⟩∘⟨ 2fam zero ⟩
              π₂ ∘ (D₁ f ×₁ id) ∘ g₂ ≈⟨ pullˡ (π₂∘×₁ ○ identityˡ) ⟩
              π₂ ∘ g₂                ∎

            π₁-eq : π₁ ∘ g₁ ≈ π₁ ∘ g₂
            π₁-eq = begin
              π₁ ∘ g₁         ≈⟨ pullˡ μchopᴺ ⟨
              dl ∘ chopᴺ ∘ g₁ ≈⟨ refl⟩∘⟨ 2fam (nzero zero) ⟩
              dl ∘ chopᴺ ∘ g₂ ≈⟨ pullˡ μchopᴺ ⟩
              π₁ ∘ g₂         ∎

        -- After chopᴺ-Δ both legs are ⟨now∘π₁, z∘!⟩: the η-square in the value
        -- component (universal via η-nat-pullback), index carried by π₂.
        iPb₂ : IsPullback (f ×₁ id) (chopᴺ ∘ ⟨ ι , π₂ ⟩) (chopᴺ ∘ ⟨ ι , π₂ ⟩) (D₁ f ×₁ id)
        iPb₂ = record
          { commute         = pullʳ top-comm ○ extendʳ bottom-comm
          ; universal       = λ {A}{h₁}{h₂} eq → ⟨ IsPullback.universal (η-nat-pullback f) (val-eq eq) , π₂ ∘ h₁ ⟩
          ; p₁∘universal≈h₁ = first∘⟨⟩ ○ ⟨⟩-congʳ (IsPullback.p₂∘universal≈h₂ (η-nat-pullback f)) ○ g-η
          ; p₂∘universal≈h₂ = λ {_}{_}{_}{eq} → -- TODO: make into equational reasoning
              ∘-resp-≈ˡ chopᴺ-Δ
              ○ ⟨⟩∘
              ○ ⟨⟩-cong₂ (pullʳ project₁ ○ IsPullback.p₁∘universal≈h₁ (η-nat-pullback f)) project₂
              ○ ⟨⟩-congˡ (idx-eq eq)
              ○ g-η
          ; unique-diagram  = λ {_}{i}{j} eq₁ eq₂ → sym g-η ○ ⟨⟩-cong₂ (π₁-uniq eq₁ eq₂) (π₂-uniq eq₁) ○ g-η
          }
          where
            val-eq : ∀ {A} {h₁ : A ⇒ Y × N} {h₂ : A ⇒ D₀ X × N} → (chopᴺ ∘ ⟨ ι , π₂ ⟩) ∘ h₁ ≈ (D₁ f ×₁ id) ∘ h₂ → D₁ f ∘ (π₁ ∘ h₂) ≈ now ∘ (π₁ ∘ h₁)
            val-eq {A}{h₁}{h₂} eq = begin
              D₁ f ∘ π₁ ∘ h₂                 ≈⟨ extendʳ (sym π₁∘×₁) ⟩
              π₁ ∘ (D₁ f ×₁ id) ∘ h₂         ≈⟨ refl⟩∘⟨ eq ⟨
              π₁ ∘ (chopᴺ ∘ ⟨ ι , π₂ ⟩) ∘ h₁ ≈⟨ extendʳ (∘-resp-≈ʳ chopᴺ-Δ ○ project₁) ⟩
              now ∘ π₁ ∘ h₁                  ∎

            -- chopᴺ-Δ preserves the index, so the cone forces π₂∘h₁ ≈ π₂∘h₂
            idx-eq : ∀ {A} {h₁ : A ⇒ Y × N} {h₂ : A ⇒ D₀ X × N} → (chopᴺ ∘ ⟨ ι , π₂ ⟩) ∘ h₁ ≈ (D₁ f ×₁ id) ∘ h₂ → π₂ ∘ h₁ ≈ π₂ ∘ h₂
            idx-eq {A}{h₁}{h₂} eq = begin
              π₂ ∘ h₁                        ≈⟨ pullˡ (∘-resp-≈ʳ chopᴺ-Δ ○ project₂) ⟨
              π₂ ∘ (chopᴺ ∘ ⟨ ι , π₂ ⟩) ∘ h₁ ≈⟨ refl⟩∘⟨ eq ⟩
              π₂ ∘ (D₁ f ×₁ id) ∘ h₂         ≈⟨ pullˡ (π₂∘×₁ ○ identityˡ) ⟩
              π₂ ∘ h₂                        ∎

            π₂-uniq : ∀ {A} {i j : A ⇒ X × N} → (f ×₁ id) ∘ i ≈ (f ×₁ id) ∘ j → π₂ ∘ i ≈ π₂ ∘ j
            π₂-uniq {i = i}{j} eq₁ = begin
              π₂ ∘ i             ≈⟨ pullˡ (π₂∘×₁ ○ identityˡ) ⟨
              π₂ ∘ (f ×₁ id) ∘ i ≈⟨ refl⟩∘⟨ eq₁ ⟩
              π₂ ∘ (f ×₁ id) ∘ j ≈⟨ pullˡ (π₂∘×₁ ○ identityˡ) ⟩
              π₂ ∘ j             ∎

            -- the value leg is determined by η-nat-pullback's uniqueness
            π₁-uniq : ∀ {A} {i j : A ⇒ X × N} → (f ×₁ id) ∘ i ≈ (f ×₁ id) ∘ j → (chopᴺ ∘ ⟨ ι , π₂ ⟩) ∘ i ≈ (chopᴺ ∘ ⟨ ι , π₂ ⟩) ∘ j → π₁ ∘ i ≈ π₁ ∘ j
            π₁-uniq {i = i}{j} eq₁ eq₂ = IsPullback.unique-diagram (η-nat-pullback f) nval fval
              where
                nval = begin
                  now ∘ π₁ ∘ i                  ≈⟨ extendʳ (∘-resp-≈ʳ chopᴺ-Δ ○ project₁) ⟨
                  π₁ ∘ (chopᴺ ∘ ⟨ ι , π₂ ⟩) ∘ i ≈⟨ refl⟩∘⟨ eq₂ ⟩
                  π₁ ∘ (chopᴺ ∘ ⟨ ι , π₂ ⟩) ∘ j ≈⟨ extendʳ (∘-resp-≈ʳ chopᴺ-Δ ○ project₁) ⟩
                  now ∘ π₁ ∘ j                  ∎
                fval = begin
                  f ∘ π₁ ∘ i         ≈⟨ extendʳ π₁∘×₁ ⟨
                  π₁ ∘ (f ×₁ id) ∘ i ≈⟨ refl⟩∘⟨ eq₁ ⟩
                  π₁ ∘ (f ×₁ id) ∘ j ≈⟨ extendʳ π₁∘×₁ ⟩
                  f ∘ π₁ ∘ j         ∎

        -- the thickened ι-square is a pullback
        iPb₁ : IsPullback ⟨ ι , π₂ ⟩ (f ×₁ id) (D₁ f ×₁ id) ⟨ ι , π₂ ⟩
        iPb₁ = Pullback.isPullback $ swap $ record
          { p₁ = f ×₁ id ; p₂ = ⟨ ι , π₂ ⟩ ; isPullback = unglue′ bottom-comm top-comm jm iPb₂ }

        -- thicken a value-cone (h₁ : A → D₀X, h₂ : A → Y×N) to an iPb₁-cone
        thick : ∀ {A} {h₁ : A ⇒ D₀ X} {h₂ : A ⇒ Y × N} → D₁ f ∘ h₁ ≈ ι ∘ h₂ → (D₁ f ×₁ id) ∘ ⟨ h₁ , π₂ ∘ h₂ ⟩ ≈ ⟨ ι , π₂ ⟩ ∘ h₂
        thick eq = ×₁∘⟨⟩ ○ ⟨⟩-cong₂ eq identityˡ ○ sym ⟨⟩∘

        -- thicken the uniqueness data: the index leg agrees via p₂ = f ×₁ id
        thick-uniq : ∀ {A} {i j : A ⇒ X × N} → ι ∘ i ≈ ι ∘ j → (f ×₁ id) ∘ i ≈ (f ×₁ id) ∘ j → ⟨ ι , π₂ ⟩ ∘ i ≈ ⟨ ι , π₂ ⟩ ∘ j
        thick-uniq eq₁ eq₂ = ⟨⟩∘ ○ ⟨⟩-cong₂ eq₁ (pushˡ (sym π₂∘first) ○ ∘-resp-≈ʳ eq₂ ○ pullˡ π₂∘first) ○ sym ⟨⟩∘

    -- μ-ι square is a pullback (second square in eq:D_pb)
    ι-η-pullback : ∀ {X} → IsPullback id ⟨ id , ParametrizedNNO.z PNNO ∘ ! ⟩ (η X) ι
    ι-η-pullback .IsPullback.commute = identityʳ ○ sym ι-zero
    ι-η-pullback .IsPullback.universal {_}{h₁}{h₂} _ = h₁
    ι-η-pullback .IsPullback.p₁∘universal≈h₁ = identityˡ
    ι-η-pullback .IsPullback.p₂∘universal≈h₂ {_}{h₁}{h₂}{eq} = ι-mono (⟨ id , ParametrizedNNO.z PNNO ∘ ! ⟩ ∘ h₁) h₂ (pullˡ ι-zero ○ eq)
    ι-η-pullback .IsPullback.unique-diagram eq _ = sym identityˡ ○ eq ○ identityˡ

    -- "delays add": flattening a delay-of-delay sums the two step counts.  Both
    -- sides are the primitive recursion prec ι (later∘π₁) over the outer N.
    delays-add : ∀ {X} → μ X ∘ (D₁ ι ∘ ι) ≈ ι ∘ ⟨ π₁ ∘ π₁ , sum ∘ (π₂ ×₁ id) ⟩
    delays-add {X} = begin
      μ X ∘ D₁ ι ∘ ι                     ≈⟨ pushˡ (extend⇒F₁ kleisli ι) ⟨
      extend ι ∘ ι                       ≈⟨ prec-unique {zero = ι} {succ = later ∘ π₁} base₁ step₁ ⟩
      prec ι (later ∘ π₁)                ≈⟨ prec-unique {zero = ι} {succ = later ∘ π₁} base₂ step₂ ⟨
      ι ∘ ⟨ π₁ ∘ π₁ , sum ∘ (π₂ ×₁ id) ⟩ ∎
      where
        base₁ : (extend ι ∘ ι) ∘ ⟨ id , z ∘ ! ⟩ ≈ ι
        base₁ = pullʳ ι-zero ○ DK.identityʳ

        step₁ : (extend ι ∘ ι) ∘ (id ×₁ s) ≈ (later ∘ π₁) ∘ ⟨ extend ι ∘ ι , id ⟩
        step₁ = begin
          (extend ι ∘ ι) ∘ (id ×₁ s)           ≈⟨ pullʳ ι-succ ⟩
          extend ι ∘ later ∘ ι                 ≈⟨ extendʳ (Later∘Extend.later-extend-comm ι) ⟨ 
          later ∘ extend ι ∘ ι                 ≈⟨ pullʳ project₁ ⟨
          (later ∘ π₁) ∘ ⟨ extend ι ∘ ι , id ⟩ ∎

        base₂ : (ι ∘ ⟨ π₁ ∘ π₁ , sum ∘ (π₂ ×₁ id) ⟩) ∘ ⟨ id , z ∘ ! ⟩ ≈ ι
        base₂ = begin
          (ι ∘ ⟨ π₁ ∘ π₁ , sum ∘ (π₂ ×₁ id) ⟩) ∘ ⟨ id , z ∘ ! ⟩ ≈⟨ pullʳ (⟨⟩∘ ○ ⟨⟩-congʳ (pullʳ project₁ ○ identityʳ)) ⟩
          ι ∘ ⟨ π₁ , (sum ∘ (π₂ ×₁ id)) ∘ ⟨ id , z ∘ ! ⟩ ⟩      ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (pullʳ (first∘⟨⟩ ○ ⟨⟩-congʳ identityʳ) ○ sum-zʳ) ⟩   
          ι ∘ ⟨ π₁ , π₂ ⟩                                       ≈⟨ elimʳ ×₁-η ⟩
          ι                                                     ∎

        step₂ : (ι ∘ ⟨ π₁ ∘ π₁ , sum ∘ (π₂ ×₁ id) ⟩) ∘ (id ×₁ s) ≈ (later ∘ π₁) ∘ ⟨ ι ∘ ⟨ π₁ ∘ π₁ , sum ∘ (π₂ ×₁ id) ⟩ , id ⟩
        step₂ = begin
          (ι ∘ ⟨ π₁ ∘ π₁ , sum ∘ (π₂ ×₁ id) ⟩) ∘ (id ×₁ s)           ≈⟨ pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ π₁∘second) (pullʳ first↔second ○ extendʳ sum-sʳ)) ⟩
          ι ∘ ⟨ π₁ ∘ π₁ , s ∘ sum ∘ (π₂ ×₁ id) ⟩                     ≈⟨ refl⟩∘⟨ sym (×₁∘⟨⟩ ○ ⟨⟩-congʳ identityˡ) ⟩
          ι ∘ (id ×₁ s) ∘ ⟨ π₁ ∘ π₁ , sum ∘ (π₂ ×₁ id) ⟩             ≈⟨ extendʳ ι-succ ⟩
          later ∘ ι ∘ ⟨ π₁ ∘ π₁ , sum ∘ (π₂ ×₁ id) ⟩                 ≈⟨ pullʳ project₁ ⟨ 
          (later ∘ π₁) ∘ ⟨ ι ∘ ⟨ π₁ ∘ π₁ , sum ∘ (π₂ ×₁ id) ⟩ , id ⟩ ∎

    -- μ-ι square is a pullback : reduction to pb` construced below using unglue′
    ι-μ-pullback : ∀ {X} → IsPullback (D₁ ι ∘ ι) ⟨ π₁ ∘ π₁ , sum ∘ (π₂ ×₁ id)  ⟩ (μ X) ι
    ι-μ-pullback {X} = record
      { commute         = delays-add
      ; universal       = λ eq  → IsPullback.universal pb (cone eq)
      ; p₁∘universal≈h₁ = λ {_}{_}{_}{eq} → IsPullback.p₁∘universal≈h₁ pb {eq = cone eq}
      ; p₂∘universal≈h₂ = λ {_}{_}{_}{eq} → pushˡ (sym sumc-π₁) ○ ∘-resp-≈ʳ (IsPullback.p₂∘universal≈h₂ pb {eq = cone eq}) ○ project₁
      ; unique-diagram  = λ eq _  → IsPullback.unique-diagram pb eq (∘-resp-≈ʳ (sumc-eq _ _ eq))
      }
        where
          sumc : (X × N) × N ⇒ (X × N) × N
          sumc = ⟨ second sum , π₂ ∘ π₂ ⟩ ∘ assocˡ 

          subc : (X × N) × N ⇒ (X × N) × N
          subc = ⟨ second sub , min ∘ π₂ ⟩ ∘ assocˡ

          sumc-π₁ : π₁ ∘ sumc ≈ ⟨ π₁ ∘ π₁ , sum ∘ (π₂ ×₁ id) ⟩
          sumc-π₁ = begin
            π₁ ∘ sumc                                            ≈⟨ pullˡ project₁ ⟩
            second sum ∘ assocˡ                                  ≈⟨ refl⟩∘⟨ elimʳ (⟨⟩-congʳ ×₁-g-η ○ ×₁-η) ⟨
            second sum ∘ assocˡ ∘ ⟨ ⟨ π₁ ∘ π₁ , π₂ ∘ π₁ ⟩ , π₂ ⟩ ≈⟨ refl⟩∘⟨ assocˡ∘⟨⟩ ⟩ 
            second sum ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩          ≈⟨ second∘⟨⟩ ⟩
            ⟨ π₁ ∘ π₁ , sum ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩                 ≈⟨ ⟨⟩-congˡ (∘-resp-≈ʳ (⟨⟩-congˡ (sym identityˡ))) ⟩
            ⟨ π₁ ∘ π₁ , sum ∘ (π₂ ×₁ id) ⟩                       ∎

          sumc-π₂ : π₂ ∘ sumc ≈ π₂
          sumc-π₂ = begin
            π₂ ∘ sumc                                           ≈⟨ pullˡ project₂ ⟩
            (π₂ ∘ π₂) ∘ assocˡ                                  ≈⟨ refl⟩∘⟨ elimʳ (⟨⟩-congʳ ×₁-g-η ○ ×₁-η) ⟨
            (π₂ ∘ π₂) ∘ assocˡ ∘ ⟨ ⟨ π₁ ∘ π₁ , π₂ ∘ π₁ ⟩ , π₂ ⟩ ≈⟨ refl⟩∘⟨ assocˡ∘⟨⟩ ⟩ 
            (π₂ ∘ π₂) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩          ≈⟨ pullʳ project₂ ○ project₂ ⟩
            π₂                                                  ∎

          subc-π₁ : π₁ ∘ subc ≈ ⟨ π₁ ∘ π₁ , sub ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩
          subc-π₁ = begin
            π₁ ∘ subc                                            ≈⟨ pullˡ project₁ ⟩
            second sub ∘ assocˡ                                  ≈⟨ refl⟩∘⟨ elimʳ (⟨⟩-congʳ ×₁-g-η ○ ×₁-η) ⟨
            second sub ∘ assocˡ ∘ ⟨ ⟨ π₁ ∘ π₁ , π₂ ∘ π₁ ⟩ , π₂ ⟩ ≈⟨ refl⟩∘⟨ assocˡ∘⟨⟩ ⟩
            second sub ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩          ≈⟨ second∘⟨⟩ ⟩
            ⟨ π₁ ∘ π₁ , sub ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩                 ∎

          subc-π₂ : π₂ ∘ subc ≈ min ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩
          subc-π₂ = begin
            π₂ ∘ subc                                            ≈⟨ pullˡ project₂ ⟩
            (min ∘ π₂) ∘ assocˡ                                  ≈⟨ refl⟩∘⟨ elimʳ (⟨⟩-congʳ ×₁-g-η ○ ×₁-η) ⟨
            (min ∘ π₂) ∘ assocˡ ∘ ⟨ ⟨ π₁ ∘ π₁ , π₂ ∘ π₁ ⟩ , π₂ ⟩ ≈⟨ refl⟩∘⟨ assocˡ∘⟨⟩ ⟩
            (min ∘ π₂) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩          ≈⟨ pullʳ project₂ ⟩
            min ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩                               ∎

          -- reduction to (m + n) ∸ n = m (sub-sum)
          subc∘sumc : subc ∘ sumc ≈ id
          subc∘sumc = begin
            subc ∘ sumc                                                               ≈⟨ pullʳ (pullˡ assocˡ∘⟨⟩)  ⟩
            ⟨ second sub , min ∘ π₂ ⟩ ∘ ⟨ id ∘ π₁ , ⟨ sum ∘ π₂ , π₂ ∘ π₂ ⟩ ⟩ ∘ assocˡ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (sym ⟨⟩∘) ⟩∘⟨refl ⟩
            ⟨ second sub , min ∘ π₂ ⟩ ∘ (id ×₁ ⟨ sum  , π₂ ⟩ ) ∘ assocˡ               ≈⟨ pullˡ (⟨⟩∘ ○ ⟨⟩-congˡ (pullʳ π₂∘×₁  ○ pullˡ min-sum)) ⟩
            ⟨ second sub ∘ second ⟨ sum  , π₂ ⟩ , π₂ ∘ π₂ ⟩ ∘ assocˡ                  ≈⟨ (⟨⟩-congʳ (second∘second ○ second-cong sub-sum)) ⟩∘⟨refl ⟩
            ⟨ second π₁ , π₂ ∘ π₂ ⟩ ∘ assocˡ                                          ≈⟨ (⟨⟩-congʳ (⟨⟩-congʳ identityˡ)) ⟩∘⟨refl ○ assocʳ∘assocˡ ⟩
            id                                                                        ∎

          -- q for unglue′: thickened delays-add (paired with its D! shadow)
          thick-comm : ⟨ μ X , D₁ ! ⟩ ∘ (D₁ ι ∘ ι) ≈ (ι ×₁ ι̂) ∘ sumc
          thick-comm = begin
            ⟨ μ X , D₁ ! ⟩ ∘ (D₁ ι ∘ ι)                     ≈⟨ ⟨⟩∘ ○ ⟨⟩-congˡ (pullˡ (sym homomorphism  ○ F-resp-≈ !-unique₂)) ⟩
            ⟨ μ X ∘ (D₁ ι ∘ ι) , D₁ ! ∘ ι ⟩                 ≈⟨ ⟨⟩-congˡ (sym (ι-natural _) ○ pushʳ (⟨⟩-congʳ !-unique₂ ○ sym ⟨⟩∘)) ⟩
            ⟨ μ X ∘ (D₁ ι ∘ ι) , ι̂ ∘ π₂ ⟩                   ≈⟨ ⟨⟩-congʳ delays-add ⟩
            ⟨ ι ∘ ⟨ π₁ ∘ π₁ , sum ∘ (π₂ ×₁ id) ⟩ , ι̂ ∘ π₂ ⟩ ≈⟨ ⟨⟩-cong₂ (∘-resp-≈ʳ (sym sumc-π₁)) (∘-resp-≈ʳ (sym sumc-π₂)) ⟩
            ⟨ ι ∘ π₁ ∘ sumc , ι̂ ∘ π₂ ∘ sumc ⟩               ≈⟨ ⟨⟩∘ ○ ⟨⟩-cong₂ assoc assoc ⟨
            (ι ×₁ ι̂) ∘ sumc                                 ∎

          -- ι×₁ι̂ is monic, being a product of the monos ι and ι̂
          ι×₁ι̂-mono : Mono (ι ×₁ ι̂)
          ι×₁ι̂-mono g₁ g₂ eq = ⟨⟩-unique′
            (ι-mono (π₁ ∘ g₁) (π₁ ∘ g₂) (pullˡ (sym π₁∘×₁) ○ extendˡ eq ○ pushˡ π₁∘×₁))
            (ι̂-mono (π₂ ∘ g₁) (π₂ ∘ g₂) (pullˡ (sym π₂∘×₁) ○ extendˡ eq ○ pushˡ π₂∘×₁))

          -- TODO: refactor via Mono (D₁ ι)
          sumc-eq : Mono (D₁ ι ∘ ι)
          sumc-eq i j eq = begin
            i                 ≈⟨ introˡ subc∘sumc ⟩
            (subc ∘ sumc) ∘ i ≈⟨ assoc ⟩
            subc ∘ sumc ∘ i   ≈⟨ refl⟩∘⟨ ι×₁ι̂-mono (sumc ∘ i) (sumc ∘ j)
                                           ( pullˡ (sym thick-comm) ○ assoc ○ ∘-resp-≈ʳ eq
                                           ○ sym-assoc ○ ∘-resp-≈ˡ thick-comm ○ assoc ) ⟩
            subc ∘ sumc ∘ j   ≈⟨ sym-assoc ⟩
            (subc ∘ sumc) ∘ j ≈⟨ elimˡ subc∘sumc ⟩
            j                 ∎

          -- p for unglue′: right-cell commute, the subtraction dual of delays-add
          chop-comm : chop ∘ (ι ×₁ ι̂) ≈ (D₁ ι ∘ ι) ∘ subc
          chop-comm = begin
            chop ∘ (ι ×₁ ι̂)                                                                   ≈⟨ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ identityˡ identityʳ) ⟨ 
            chop ∘ (id ×₁ ι̂) ∘ (ι ×₁ id)                                                      ≈⟨ extendʳ ι-chopᴺ ⟨ 
            ι ∘ chopᴺ ∘ (ι ×₁ id)                                                             ≈⟨ refl⟩∘⟨ chopᴺ-ι ⟩
            ι ∘ ⟨ ι ∘ ⟨ π₁ ∘ π₁ , sub ∘ (π₂ ×₁ id) ⟩ , min ∘ (π₂ ×₁ id) ⟩                     ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (∘-resp-≈ʳ (⟨⟩-congˡ (∘-resp-≈ʳ (⟨⟩-congˡ identityˡ)))) (∘-resp-≈ʳ (⟨⟩-congˡ identityˡ)) ⟩
            ι ∘ ⟨ ι ∘ ⟨ π₁ ∘ π₁ , sub ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , min ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩         ≈⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-congˡ identityˡ) ⟨ 
            ι ∘ (ι ×₁ id) ∘ ⟨ ⟨ π₁ ∘ π₁ , sub ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , min ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ pullˡ (ι-natural ι) ⟩
            (D₁ ι ∘ ι) ∘ ⟨ ⟨ π₁ ∘ π₁ , sub ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , min ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩    ≈⟨ refl⟩∘⟨ ⟨⟩-unique subc-π₁ subc-π₂ ⟩
            (D₁ ι ∘ ι) ∘ subc                                                                 ∎

          -- jointly monic since ι×₁ι̂ is already monic (uses ι-mono)
          jm : JointMono₂ (ι ×₁ ι̂) subc
          jm g₁ g₂ 2fam = ⟨⟩-unique′
              (ι-mono (π₁ ∘ g₁) (π₁ ∘ g₂) (pullˡ (sym π₁∘×₁) ○ extendˡ (2fam zero) ○ pushˡ π₁∘×₁))   
             (ι̂-mono (π₂ ∘ g₁) (π₂ ∘ g₂) (pullˡ (sym π₂∘×₁) ○ extendˡ (2fam zero) ○ pushˡ π₂∘×₁))   

          -- the trivial identity rectangle (outer cell of the paper's 1st diagram)
          rect : IsPullback (D₁ ι ∘ ι) (subc ∘ sumc) (chop ∘ ⟨ μ X , D₁ ! ⟩) (D₁ ι ∘ ι)
          rect = record
            { commute         = elimˡ chopμD! ○ introʳ subc∘sumc
            ; universal       = λ {_}{h₁}{h₂} _ → h₂
            ; p₁∘universal≈h₁ = λ {_}{h₁}{h₂}{eq} → sym eq ○ elimˡ chopμD!
            ; p₂∘universal≈h₂ = λ {_}{h₁}{h₂}{eq} → elimˡ subc∘sumc
            ; unique-diagram  = λ {_}{h}{i} _ eq → introˡ subc∘sumc ○ eq ○ elimˡ subc∘sumc
            }

          pb : IsPullback (D₁ ι ∘ ι) sumc ⟨ μ X , D₁ ! ⟩ (ι ×₁ ι̂)
          pb = unglue′ chop-comm thick-comm jm rect

          -- lift an (μ,ι)-cone to a (⟨μ,D!⟩, ι×₁ι̂)-cone: augment h₂ with the count
          cone : ∀ {A} {h₁ : A ⇒ D₀ (D₀ X)} {h₂ : A ⇒ X × N} (eq : μ X ∘ h₁ ≈ ι ∘ h₂) → ⟨ μ X , D₁ ! ⟩ ∘ h₁ ≈ (ι ×₁ ι̂) ∘ ⟨ h₂ , π₂ ∘ chopᴺ ∘ ⟨ h₁ , π₂ ∘ h₂ ⟩ ⟩
          cone {h₁ = h₁} {h₂ = h₂} eq = ⟨⟩∘ ○ ⟨⟩-cong₂ eq shape-eq ○ sym ×₁∘⟨⟩
            where
              -- D₁! of an ι-value is ι̂ of its count (ι naturality at !).
              D!ι : ∀ {V} → D₁ ! ∘ ι {V} ≈ ι̂ ∘ π₂
              D!ι = sym (ι-natural !) ○ ∘-resp-≈ʳ (⟨⟩-congʳ !-unique₂ ○ sym ⟨⟩∘) ○ sym-assoc

              -- the clock = shape of the flattened value: D₁!∘μ∘h₁ = D₁!∘ι∘h₂ = ι̂∘π₂∘h₂.
              clock-eq : D₁ ! ∘ μ X ∘ h₁ ≈ ι̂ ∘ π₂ ∘ h₂
              clock-eq = ∘-resp-≈ʳ eq ○ sym-assoc ○ ∘-resp-≈ˡ D!ι ○ assoc

              -- the outer shape of h₁ = ι̂ of the count chopᴺ extracts (uses D!chop-μ + ι-chopᴺ).
              shape-eq : D₁ ! ∘ h₁ ≈ ι̂ ∘ π₂ ∘ chopᴺ ∘ ⟨ h₁ , π₂ ∘ h₂ ⟩
              shape-eq = begin
                D₁ ! ∘ h₁                                  ≈⟨ pushʳ sym-assoc ○ ∘-resp-≈ˡ D!chop-μ ⟨ 
                D₁ ! ∘ chop ∘ ⟨ id , D₁ ! ∘ μ X ⟩ ∘ h₁     ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ assoc) ⟩
                D₁ ! ∘ chop ∘ ⟨ h₁ , D₁ ! ∘ μ X ∘ h₁ ⟩     ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (second∘⟨⟩ ○ ⟨⟩-congˡ (sym clock-eq) ) ⟨ 
                D₁ ! ∘ chop ∘ (id ×₁ ι̂) ∘ ⟨ h₁ , π₂ ∘ h₂ ⟩ ≈⟨ refl⟩∘⟨ pullˡ (sym ι-chopᴺ) ⟩
                D₁ ! ∘ (ι ∘ chopᴺ) ∘ ⟨ h₁ , π₂ ∘ h₂ ⟩      ≈⟨ pullˡ (pullˡ D!ι) ○ assoc ○ assoc ⟩
                ι̂ ∘ π₂ ∘ chopᴺ ∘ ⟨ h₁ , π₂ ∘ h₂ ⟩          ∎