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

-- The Delay monad D is cartesian: D preserves pullbacks, and the unit (η) and
-- multiplication (μ) naturality squares are pullbacks (prop:D-cart).  These
-- proofs are independent of the τ/ι machinery in Monad.Instance.Delay.Pullbacks
-- (which imports this module for η-nat-pullback).
module Monad.Instance.Delay.Cartesian {o ℓ e} {C : Category o ℓ e}
    (extensive : Extensive C) (cartesian : Cartesian C)
    (D : DelayM (Extensive.cocartesian extensive)) where

  open Category C
  private distributive = Extensive×Cartesian⇒Distributive C extensive cartesian
  open import Category.Distributive.Helper distributive hiding (swap; η)
  open import Categories.Diagram.Pullback C
  open import Categories.Object.Coproduct C using (IsCoproduct; Coproduct; IsCoproduct⇒Coproduct)
  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-Monad
  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.Chop distributive D
  open import Categories.Category.Extensive.Properties C as EP

  -- D preserves pullbacks (prop:D-cart)
  -- The proof requires D₀ X to be a retract of a stream type; we scope the
  -- extra assumptions (PNNO + exponentials) to just this block.
  module _
      (pnno : ParametrizedNNO C (Distributive.cartesian distributive))
      (Expℕ : ∀ X → Exponential (Distributive.cartesian distributive) (ParametrizedNNO.N pnno) X) where

    open import Monad.Instance.Delay.Retract distributive D pnno Expℕ
    open ParametrizedNNO pnno using (N)

    -- the function-space object Aᴺ = N ⇒ A, carrier of the exponential Expℕ A
    infix  _^ℕ
    _^ℕ : Obj → Obj
    X ^ℕ = Exponential.B^A (Expℕ X)

    -- the exponential structure at an (implicit) object, so its combinators
    -- read as Exp.eval, Exp.λg, Exp.β, ... with the object inferred from the goal
    module Exp {X} = Exponential (Expℕ X)

    -- functorial action of the exponential endofunctor (-)^ℕ on morphisms: a
    -- map h : A ⇒ B is sent to post-composition with h
    ^ℕ-map : ∀ {A B} → A ⇒ B → A ^ℕ ⇒ B ^ℕ
    ^ℕ-map h = Exp.λg (h ∘ Exp.eval)

    D₁-via-Stream : ∀ {X Y} (f : X ⇒ Y) → D₁ f ≈ stream-to-D ∘ Stream-Functor.₁ f ∘ D-to-stream
    D₁-via-Stream f = begin
      D₁ f                                       ≈⟨ introʳ (Mor.Retract.is-retract D-retract) ⟩
      D₁ f ∘ stream-to-D ∘ D-to-stream           ≈⟨ extendʳ (stream-to-D-natural f) ⟩
      stream-to-D ∘ Stream-Functor.₁ f ∘ D-to-stream     ∎

    -- ^ℕ-map is functorial
    ^ℕ-map-eval : ∀ {A B} (h : A ⇒ B) → Exp.eval ∘ (^ℕ-map h ×₁ id) ≈ h ∘ Exp.eval
    ^ℕ-map-eval h = Exp.β

    ^ℕ-map-cong : ∀ {A B} {h k : A ⇒ B} → h ≈ k → ^ℕ-map h ≈ ^ℕ-map k
    ^ℕ-map-cong eq = Exp.λ-cong (∘-resp-≈ˡ eq)

    ^ℕ-map-id : ∀ {A} → ^ℕ-map (id {A}) ≈ id
    ^ℕ-map-id = Exp.λ-cong identityˡ ○ Exp.η-id

    ^ℕ-map-∘ : ∀ {A B C} (k : B ⇒ C) (h : A ⇒ B) → ^ℕ-map (k ∘ h) ≈ ^ℕ-map k ∘ ^ℕ-map h
    ^ℕ-map-∘ k h = Exp.λ-unique′ $ begin
        Exp.eval ∘ (^ℕ-map (k ∘ h) ×₁ id)              ≈⟨ ^ℕ-map-eval (k ∘ h) ○ assoc  ⟩
        k ∘ h ∘ Exp.eval                              ≈⟨ refl⟩∘⟨ (^ℕ-map-eval h) ⟨ 
        k ∘ Exp.eval ∘ (^ℕ-map h ×₁ id)                ≈⟨ extendʳ (^ℕ-map-eval k) ⟨
        Exp.eval ∘ (^ℕ-map k ×₁ id) ∘ (^ℕ-map h ×₁ id)  ≈⟨ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ refl identity²) ⟩
        Exp.eval ∘ ((^ℕ-map k ∘ ^ℕ-map h) ×₁ id)       ∎

    -- (-)^ℕ preserves pullbacks
    ^ℕ-preserves-pullback : ∀ {P X Y Z} {p₁ : P ⇒ X} {p₂ : P ⇒ Y} {f : X ⇒ Z} {g : Y ⇒ Z}
      → IsPullback p₁ p₂ f g → IsPullback (^ℕ-map p₁) (^ℕ-map p₂) (^ℕ-map f) (^ℕ-map g)
      
    ^ℕ-preserves-pullback {P}{X}{Y}{Z}{p₁}{p₂}{f}{g} pb = record
       { commute         = ⟺ (^ℕ-map-∘ f p₁) ○ ^ℕ-map-cong (IsPullback.commute pb) ○ ^ℕ-map-∘ g p₂
       ; universal       = λ {A}{h₁}{h₂} eq → Exp.λg (u eq)
       ; p₁∘universal≈h₁ = λ {A}{h₁}{h₂}{eq} → Exp.λ-unique′ $ begin
           Exp.eval ∘ (^ℕ-map p₁ ∘ Exp.λg (u eq) ×₁ id)             ≈⟨ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ refl identityˡ) ⟨
           Exp.eval ∘ (^ℕ-map p₁ ×₁ id) ∘ (Exp.λg (u eq) ×₁ id)      ≈⟨ extendʳ (^ℕ-map-eval p₁)  ⟩
           p₁ ∘ Exp.eval ∘ (Exp.λg (u eq) ×₁ id)                    ≈⟨ refl⟩∘⟨ Exp.β ⟩
           p₁ ∘ u eq                                               ≈⟨ IsPullback.p₁∘universal≈h₁ pb ⟩
           Exp.eval ∘ (h₁ ×₁ id)                                    ∎
       ; p₂∘universal≈h₂ = λ {A}{h₁}{h₂}{eq} → Exp.λ-unique′ $ begin
           Exp.eval ∘ ((^ℕ-map p₂ ∘ Exp.λg (u eq)) ×₁ id)           ≈⟨ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ refl identityˡ) ⟨
           Exp.eval ∘ (^ℕ-map p₂ ×₁ id) ∘ (Exp.λg (u eq) ×₁ id)      ≈⟨ extendʳ (^ℕ-map-eval p₂) ⟩
           p₂ ∘ Exp.eval ∘ (Exp.λg (u eq) ×₁ id)                    ≈⟨ refl⟩∘⟨ Exp.β ⟩
           p₂ ∘ u eq                                               ≈⟨ IsPullback.p₂∘universal≈h₂ pb ⟩
           Exp.eval ∘ (h₂ ×₁ id)                                    ∎
       ; unique-diagram  = λ {A}{i}{h} eq₁ eq₂ → Exp.λ-unique′
           (IsPullback.unique-diagram pb
             (evalP i p₁ ○ ∘-resp-≈ʳ (×₁-cong₂ eq₁ refl) ○ sym (evalP h p₁))
             (evalP i p₂ ○ ∘-resp-≈ʳ (×₁-cong₂ eq₂ refl) ○ sym (evalP h p₂)))
       }
       where
         -- evaluating the cone (h₁, h₂) pointwise lands in the original square
         eqPB : ∀ {A}{h₁ : A ⇒ X ^ℕ}{h₂ : A ⇒ Y ^ℕ} → ^ℕ-map f ∘ h₁ ≈ ^ℕ-map g ∘ h₂
              → f ∘ Exp.eval ∘ (h₁ ×₁ id) ≈ g ∘ Exp.eval ∘ (h₂ ×₁ id)
              
         eqPB {_}{h₁}{h₂} eq = begin
           f ∘ Exp.eval ∘ (h₁ ×₁ id)                  ≈⟨ extendʳ (^ℕ-map-eval f) ⟨
           Exp.eval ∘ (^ℕ-map f ×₁ id) ∘ (h₁ ×₁ id)    ≈⟨ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ refl identityˡ) ⟩
           Exp.eval ∘ ((^ℕ-map f ∘ h₁) ×₁ id)         ≈⟨ refl⟩∘⟨ ×₁-cong₂ eq refl ⟩
           Exp.eval ∘ ((^ℕ-map g ∘ h₂) ×₁ id)         ≈⟨ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ refl identityˡ) ⟨
           Exp.eval ∘ (^ℕ-map g ×₁ id) ∘ (h₂ ×₁ id)    ≈⟨ extendʳ (^ℕ-map-eval g) ⟩
           g ∘ Exp.eval ∘ (h₂ ×₁ id)                  ∎

         u : ∀ {A}{h₁ : A ⇒ X ^ℕ}{h₂ : A ⇒ Y ^ℕ} → ^ℕ-map f ∘ h₁ ≈ ^ℕ-map g ∘ h₂ → A × N ⇒ P
         u eq = IsPullback.universal pb (eqPB eq)

         -- push evaluation past a projection q : P ⇒ W (used for joint monicity)
         evalP : ∀ {A W}(w : A ⇒ P ^ℕ)(q : P ⇒ W) → q ∘ Exp.eval ∘ (w ×₁ id) ≈ Exp.eval ∘ (^ℕ-map q ∘ w ×₁ id)
         evalP w q = begin
           q ∘ Exp.eval ∘ (w ×₁ id)                    ≈⟨ extendʳ (^ℕ-map-eval q) ⟨
           Exp.eval ∘ (^ℕ-map q ×₁ id) ∘ (w ×₁ id)      ≈⟨ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ refl identityˡ) ⟩
           Exp.eval ∘ (^ℕ-map q ∘ w ×₁ id)             ∎

    -- (- + 1) preserves pullbacks
    +1-preserves-pullback : ∀ {P X Y Z} {p₁ : P ⇒ X} {p₂ : P ⇒ Y} {f : X ⇒ Z} {g : Y ⇒ Z}
      → IsPullback p₁ p₂ f g → IsPullback (p₁ +₁ ! {ı}) (p₂ +₁ !) (f +₁ !) (g +₁ !)
      
    +1-preserves-pullback {P = P} {X = X} {Y = Y} {p₁ = p₁} {p₂ = p₂} {f = f} {g = g} pb = record
       { commute = begin
           (f +₁ !) ∘ (p₁ +₁ !)    ≈⟨ +₁∘+₁ ○ +₁-cong₂ refl !-unique₂  ⟩ 
           f ∘ p₁ +₁ !             ≈⟨ +₁-cong₂ (IsPullback.commute pb) refl ⟩
           g ∘ p₂ +₁ !             ≈⟨ +₁-cong₂ refl !-unique₂ ○ sym +₁∘+₁ ⟩
           (g +₁ !) ∘ (p₂ +₁ !)    ∎
       ; universal        = λ {A}{h₁}{h₂} eq → Cone.u eq
       ; p₁∘universal≈h₁  = λ {A}{h₁}{h₂}{eq} → Cone.p₁-ver eq
       ; p₂∘universal≈h₂  = λ {A}{h₁}{h₂}{eq} → Cone.p₂-ver eq
       ; unique-diagram   = λ {A}{i}{j} eqA eqB → Uniq.i≈j eqA eqB
       }
         where
          -- a map into Y+ı whose (g+₁!)-image lands in the ı-summand is itself i₂∘!
          i₂-factor : ∀ {A} (h : A ⇒ Y + ı) → (g +₁ !) ∘ h ≈ i₂ ∘ ! → h ≈ i₂ ∘ !
          i₂-factor h eq = sym (IsPullback.p₂∘universal≈h₂ (EP.i₂-cartesian extensive g !) {eq = sym eq})
            ○ ∘-resp-≈ʳ !-unique₂

          -- the P+ı analogue of i₂-factor, used for the ı-summand in unique-diagram
          i₂-factorP : ∀ {A} (h : A ⇒ P + ı) → (p₁ +₁ !) ∘ h ≈ i₂ ∘ ! → h ≈ i₂ ∘ !
          i₂-factorP h eq = sym (IsPullback.p₂∘universal≈h₂ (EP.i₂-cartesian extensive p₁ !) {eq = sym eq})
            ○ ∘-resp-≈ʳ !-unique₂

          -- decompose the test object A ≅ Q₁ + Q₂ along h₁ (h₁ lands in X vs. ı);
          -- on Q₁ build a P-mediator, on Q₂ the mediator is i₂∘!
          module Cone {A} {h₁ : A ⇒ X + ı} {h₂ : A ⇒ Y + ı} (eq : (f +₁ !) ∘ h₁ ≈ (g +₁ !) ∘ h₂) where
            pb₁ = Extensive.pullback₁ extensive h₁
            pb₂ = Extensive.pullback₂ extensive h₁
            module CP = Coproduct (IsCoproduct⇒Coproduct (Extensive.pullback-of-cp-is-cp extensive h₁))

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

            -- on Q₁, h₂∘q₁ also lands in i₁ (its image equals i₁∘(f∘x₁))
            eq₁ : i₁ ∘ f ∘ x₁ ≈ (g +₁ !) ∘ h₂ ∘ q₁
            eq₁ = extendʳ (sym +₁∘i₁) ○ (refl⟩∘⟨ sym (Pullback.commute pb₁)) ○ extendʳ eq

            y₁ = IsPullback.universal (EP.i₁-cartesian extensive g !) eq₁

            fx₁≈gy₁ : f ∘ x₁ ≈ g ∘ y₁
            fx₁≈gy₁ = sym (IsPullback.p₁∘universal≈h₁ (EP.i₁-cartesian extensive g !) {eq = eq₁})

            m₁ = IsPullback.universal pb fx₁≈gy₁

            u = CP.[ i₁ ∘ m₁ , i₂ ∘ ! ]

            -- q₁, q₂ are jointly epic, so equalities into P+ı are checked on each summand
            jointly-epi : JointEpi₂ q₁ q₂
            jointly-epi w w′ 2fam = sym CP.g-η ○ CP.[]-cong₂ (2fam zero) (2fam (nzero zero)) ○ CP.g-η

            p₁-ver : (p₁ +₁ !) ∘ u ≈ h₁
            p₁-ver = jointly-epi _ _ λ
              { zero →
                begin ((p₁ +₁ !) ∘ u) ∘ q₁  ≈⟨ pullʳ CP.inject₁ ⟩
                      (p₁ +₁ !) ∘ i₁ ∘ m₁    ≈⟨ pullˡ +₁∘i₁ ⟩
                      (i₁ ∘ p₁) ∘ m₁         ≈⟨ pullʳ (IsPullback.p₁∘universal≈h₁ pb) ⟩
                      i₁ ∘ x₁                ≈⟨ Pullback.commute pb₁ ⟨
                      h₁ ∘ q₁                ∎
              ; (nzero _) →
                begin ((p₁ +₁ !) ∘ u) ∘ q₂  ≈⟨ pullʳ CP.inject₂ ⟩
                      (p₁ +₁ !) ∘ i₂ ∘ !     ≈⟨ pullˡ +₁∘i₂ ⟩
                      (i₂ ∘ !) ∘ !           ≈⟨ pullʳ !-unique₂ ⟩
                      i₂ ∘ !                 ≈⟨ Pullback.commute pb₂ ○ ∘-resp-≈ʳ !-unique₂ ⟨
                      h₁ ∘ q₂                ∎
              }

            p₂-ver : (p₂ +₁ !) ∘ u ≈ h₂
            p₂-ver = jointly-epi _ _ λ
              { zero →
                begin ((p₂ +₁ !) ∘ u) ∘ q₁  ≈⟨ pullʳ CP.inject₁ ⟩
                      (p₂ +₁ !) ∘ i₁ ∘ m₁    ≈⟨ pullˡ +₁∘i₁ ⟩
                      (i₁ ∘ p₂) ∘ m₁         ≈⟨ pullʳ (IsPullback.p₂∘universal≈h₂ pb) ⟩
                      i₁ ∘ y₁                ≈⟨ IsPullback.p₂∘universal≈h₂ (EP.i₁-cartesian extensive g !) {eq = eq₁} ⟩
                      h₂ ∘ q₁                ∎
              ; (nzero _) →
                begin ((p₂ +₁ !) ∘ u) ∘ q₂  ≈⟨ pullʳ CP.inject₂ ⟩
                      (p₂ +₁ !) ∘ i₂ ∘ !     ≈⟨ pullˡ +₁∘i₂ ⟩
                      (i₂ ∘ !) ∘ !           ≈⟨ pullʳ !-unique₂ ⟩
                      i₂ ∘ !                 ≈⟨ i₂-factor (h₂ ∘ q₂) h₂q₂-i₂ ⟨
                      h₂ ∘ q₂                ∎
              }
              where
                h₂q₂-i₂ : (g +₁ !) ∘ h₂ ∘ q₂ ≈ i₂ ∘ !
                h₂q₂-i₂ = begin
                  (g +₁ !) ∘ h₂ ∘ q₂   ≈⟨ extendʳ eq ⟨
                  (f +₁ !) ∘ h₁ ∘ q₂   ≈⟨ refl⟩∘⟨ (Pullback.commute pb₂ ○ ∘-resp-≈ʳ !-unique₂) ⟩
                  (f +₁ !) ∘ i₂ ∘ !    ≈⟨ pullˡ +₁∘i₂ ⟩
                  (i₂ ∘ !) ∘ !         ≈⟨ pullʳ !-unique₂ ⟩
                  i₂ ∘ !               ∎

          -- joint monicity of (p₁+₁!, p₂+₁!): decompose A ≅ B₁ + B₂ along i
          module Uniq {A} {i j : A ⇒ P + ı} (eqA : (p₁ +₁ !) ∘ i ≈ (p₁ +₁ !) ∘ j) (eqB : (p₂ +₁ !) ∘ i ≈ (p₂ +₁ !) ∘ j) where
            ub₁ = Extensive.pullback₁ extensive i
            ub₂ = Extensive.pullback₂ extensive i
            module CPi = Coproduct (IsCoproduct⇒Coproduct (Extensive.pullback-of-cp-is-cp extensive i))

            r₁ = Pullback.p₁ ub₁
            b  = Pullback.p₂ ub₁
            r₂ = Pullback.p₁ ub₂

            jointly-epi : JointEpi₂ r₁ r₂
            jointly-epi w w′ 2fam = sym CPi.g-η ○ CPi.[]-cong₂ (2fam zero) (2fam (nzero zero)) ○ CPi.g-η

            -- on B₁ (where i = i₁∘b), j∘r₁ also factors through i₁ as i₁∘b′
            eqj₁ : i₁ ∘ p₁ ∘ b ≈ (p₁ +₁ !) ∘ j ∘ r₁
            eqj₁ = extendʳ (sym +₁∘i₁) ○ (refl⟩∘⟨ sym (Pullback.commute ub₁)) ○ extendʳ eqA

            b′ = IsPullback.universal (EP.i₁-cartesian extensive p₁ !) eqj₁

            i₁b′≈jr₁ : i₁ ∘ b′ ≈ j ∘ r₁
            i₁b′≈jr₁ = IsPullback.p₂∘universal≈h₂ (EP.i₁-cartesian extensive p₁ !) {eq = eqj₁}

            b′≈b : b′ ≈ b
            b′≈b = IsPullback.unique-diagram pb
                (IsPullback.p₁∘universal≈h₁ (EP.i₁-cartesian extensive p₁ !) {eq = eqj₁})
                (Extensive.pullback₁-is-mono extensive (p₂ ∘ b′) (p₂ ∘ b)
                (begin i₁ ∘ p₂ ∘ b′       ≈⟨ extendʳ +₁∘i₁ ⟨
                       (p₂ +₁ !) ∘ i₁ ∘ b′ ≈⟨ refl⟩∘⟨ i₁b′≈jr₁ ⟩
                       (p₂ +₁ !) ∘ j ∘ r₁  ≈⟨ extendʳ eqB ⟨
                       (p₂ +₁ !) ∘ i ∘ r₁  ≈⟨ refl⟩∘⟨ Pullback.commute ub₁ ⟩
                       (p₂ +₁ !) ∘ i₁ ∘ b  ≈⟨ extendʳ +₁∘i₁ ⟩
                       i₁ ∘ p₂ ∘ b         ∎))

            i≈j : i ≈ j
            i≈j = jointly-epi _ _ λ
              { zero →
                begin i ∘ r₁  ≈⟨ Pullback.commute ub₁ ⟩
                      i₁ ∘ b   ≈⟨ refl⟩∘⟨ sym b′≈b ⟩
                      i₁ ∘ b′  ≈⟨ i₁b′≈jr₁ ⟩
                      j ∘ r₁   ∎
              ; (nzero _) →
                begin i ∘ r₂  ≈⟨ Pullback.commute ub₂ ○ ∘-resp-≈ʳ !-unique₂ ⟩
                      i₂ ∘ !   ≈⟨ i₂-factorP (j ∘ r₂) jr₂-i₂ ⟨
                      j ∘ r₂   ∎
              }
              where
                jr₂-i₂ : (p₁ +₁ !) ∘ j ∘ r₂ ≈ i₂ ∘ !
                jr₂-i₂ = begin
                  (p₁ +₁ !) ∘ j ∘ r₂  ≈⟨ extendʳ eqA ⟨
                  (p₁ +₁ !) ∘ i ∘ r₂  ≈⟨ refl⟩∘⟨ (Pullback.commute ub₂ ○ ∘-resp-≈ʳ !-unique₂) ⟩
                  (p₁ +₁ !) ∘ i₂ ∘ !  ≈⟨ pullˡ +₁∘i₂ ⟩
                  (i₂ ∘ !) ∘ !        ≈⟨ pullʳ !-unique₂ ⟩
                  i₂ ∘ !              ∎

    -- (- + 1)^ℕ preserves pullbacks (third step; follows from the previous two)
    Stream-preserves-pullback : ∀ {P X Y Z} {p₁ : P ⇒ X} {p₂ : P ⇒ Y} {f : X ⇒ Z} {g : Y ⇒ Z}
      → IsPullback p₁ p₂ f g → IsPullback (Stream-Functor.₁ p₁) (Stream-Functor.₁ p₂) (Stream-Functor.₁ f) (Stream-Functor.₁ g)
    Stream-preserves-pullback pb = ^ℕ-preserves-pullback (+1-preserves-pullback pb)

    -- D preserves by reduction to that (-+1)^ℕ preserves pullbacks
    D-preserves-pullback : ∀ {P X Y Z} {p₁ : P ⇒ X} {p₂ : P ⇒ Y} {f : X ⇒ Z} {g : Y ⇒ Z}

      → IsPullback p₁ p₂ f g → IsPullback (D₁ p₁) (D₁ p₂) (D₁ f) (D₁ g)
    D-preserves-pullback {P = P} {X = X} {Y = Y} {p₁ = p₁} {p₂ = p₂} {f = f} {g = g} pb = record
      { commute = sym homomorphism ○ F-resp-≈ (IsPullback.commute pb) ○ homomorphism
      ; universal = λ {_}{h₁}{h₂} eq → stream-to-D ∘ univ eq
      ; p₁∘universal≈h₁ = λ {_}{h₁}{h₂}{eq} →
          begin
            D₁ p₁ ∘ stream-to-D ∘ univ eq           ≈⟨ extendʳ (stream-to-D-natural p₁) ⟩
            stream-to-D ∘ Stream-Functor.₁ p₁ ∘ univ eq     ≈⟨ refl⟩∘⟨ IsPullback.p₁∘universal≈h₁ (Stream-preserves-pullback pb) {eq = cone eq} ⟩
            stream-to-D ∘ D-to-stream ∘ h₁          ≈⟨ cancelˡ (Mor.Retract.is-retract D-retract) ⟩
            h₁                                      ∎
      ; p₂∘universal≈h₂ = λ {_}{h₁}{h₂}{eq} →
          begin
            D₁ p₂ ∘ stream-to-D ∘ univ eq           ≈⟨ extendʳ (stream-to-D-natural p₂) ⟩
            stream-to-D ∘ Stream-Functor.₁ p₂ ∘ univ eq     ≈⟨ refl⟩∘⟨ IsPullback.p₂∘universal≈h₂ (Stream-preserves-pullback pb) {eq = cone eq} ⟩
            stream-to-D ∘ D-to-stream ∘ h₂          ≈⟨ cancelˡ (Mor.Retract.is-retract D-retract) ⟩
            h₂                                      ∎
      ; unique-diagram = λ {_}{i}{h} eq₁ eq₂ →
          begin
            i                                       ≈⟨ cancelˡ (Mor.Retract.is-retract D-retract) ⟨
            stream-to-D ∘ D-to-stream ∘ i           ≈⟨ refl⟩∘⟨ IsPullback.unique-diagram (Stream-preserves-pullback pb)
                                                               (extendʳ (D-to-stream-natural p₁) ○ (∘-resp-≈ʳ eq₁) ○ sym (extendʳ (D-to-stream-natural p₁)))
                                                               (extendʳ (D-to-stream-natural p₂) ○ (∘-resp-≈ʳ eq₂) ○ sym (extendʳ (D-to-stream-natural p₂))) ⟩
            stream-to-D ∘ D-to-stream ∘ h           ≈⟨ cancelˡ (Mor.Retract.is-retract D-retract) ⟩
            h                                       ∎
      }
      where
        -- the test cone, transported along the retraction to the stream side
        cone : ∀ {A} {h₁ : A ⇒ D₀ X} {h₂ : A ⇒ D₀ Y} → D₁ f ∘ h₁ ≈ D₁ g ∘ h₂ → Stream-Functor.₁ f ∘ D-to-stream ∘ h₁ ≈ Stream-Functor.₁ g ∘ D-to-stream ∘ h₂
        cone {_}{h₁}{h₂} eq = begin
            Stream-Functor.₁ f ∘ D-to-stream ∘ h₁     ≈⟨ extendʳ (D-to-stream-natural f) ⟩
            D-to-stream ∘ D₁ f ∘ h₁           ≈⟨ refl⟩∘⟨ eq ⟩
            D-to-stream ∘ D₁ g ∘ h₂           ≈⟨ extendʳ (D-to-stream-natural g) ⟨
            Stream-Functor.₁ g ∘ D-to-stream ∘ h₂     ∎

        univ : ∀ {A} {h₁ : A ⇒ D₀ X} {h₂ : A ⇒ D₀ Y} → D₁ f ∘ h₁ ≈ D₁ g ∘ h₂ → A ⇒ (P + ı) ^ℕ
        univ eq = IsPullback.universal (Stream-preserves-pullback pb) (cone eq)

  -- η-naturality square is a pullback (first pullback in prop:D-cart)
  η-nat-pullback : ∀ {X Y} (f : X ⇒ Y) → IsPullback (η _) f (D₁ f) (η _)
  η-nat-pullback f = Pullback.isPullback
    (swap (record { p₁ = f
                  ; p₂ = η _
                  ; isPullback = unglue′ (D₁-commutes f) (D.η.commute f) jm rect }))
    where
      jm : JointMono₂ (D₁ f) out
      jm g₁ g₂ 2fam = out-mono g₁ g₂ (2fam (nzero zero))

      rect : IsPullback f (out ∘ η _) (out ∘ η _) (f +₁ D₁ f)
      rect = record
        { commute         = ∘-resp-≈ˡ unitlaw ○ IsPullback.commute pb ○ ∘-resp-≈ʳ (sym unitlaw)
        ; universal       = λ eq → IsPullback.universal pb (∘-resp-≈ˡ (sym unitlaw) ○ eq)
        ; p₁∘universal≈h₁ = IsPullback.p₁∘universal≈h₁ pb
        ; p₂∘universal≈h₂ = ∘-resp-≈ˡ unitlaw ○ IsPullback.p₂∘universal≈h₂ pb
        ; unique-diagram  = λ eq₁ eq₂ → IsPullback.unique-diagram pb eq₁ (∘-resp-≈ˡ (sym unitlaw) ○ eq₂ ○ ∘-resp-≈ˡ unitlaw)
        } where pb = EP.i₁-cartesian extensive f (D₁ f)

  -- μ-naturality square is a pullback (second pullback in prop:D-cart)
  μ-nat-pullback : ∀ {X Y} (f : X ⇒ Y) → IsPullback (μ X) (D₁ (D₁ f)) (D₁ f) (μ Y)
  μ-nat-pullback f .IsPullback.commute = sym (D.μ.commute f)
  μ-nat-pullback f .IsPullback.universal {_}{h₁}{h₂} _ = chop ∘ ⟨ h₁ , D₁ ! ∘ h₂ ⟩

  μ-nat-pullback f .IsPullback.p₁∘universal≈h₁ {_}{h₁}{h₂} =
    begin
      μ _ ∘ chop ∘ ⟨ h₁ , D₁ ! ∘ h₂ ⟩           ≈⟨ pullˡ μchop ⟩
      π₁ ∘ ⟨ h₁ , D₁ ! ∘ h₂ ⟩                   ≈⟨ project₁ ⟩
      h₁                                        ∎

  μ-nat-pullback f .IsPullback.p₂∘universal≈h₂ {_}{h₁}{h₂}{eq} =
    begin
      D₁ (D₁ f) ∘ chop ∘ ⟨ h₁ , D₁ ! ∘ h₂ ⟩    ≈⟨ extendʳ (chop-natural f) ⟩
      chop ∘ (D₁ f ×₁ id) ∘ ⟨ h₁ , D₁ ! ∘ h₂ ⟩  ≈⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-congˡ identityˡ) ⟩
      chop ∘ ⟨ D₁ f ∘ h₁ , D₁ ! ∘ h₂ ⟩         ≈⟨ refl⟩∘⟨ (⟨⟩-congʳ eq ○ sym ⟨⟩∘) ⟩
      chop ∘ ⟨ μ _ , D₁ ! ⟩ ∘ h₂               ≈⟨ cancelˡ chopμD! ⟩
      h₂                                       ∎

  μ-nat-pullback f .IsPullback.unique-diagram {_}{i}{h} p₁ p₂ =
    RegularMono⇒Mono (Section⇒RegularMono $ Mor.Retract.is-retract $ chop-retract _) i h $
      ⟨⟩-unique′ (pullˡ project₁ ○ p₁ ○ sym (pullˡ project₁))
                 (pullˡ project₂ ○ D!-eq ○ sym (pullˡ project₂))
    where
      D!-eq : D₁ ! ∘ i ≈ D₁ ! ∘ h
      D!-eq =
        begin
          D₁ ! ∘ i                      ≈⟨ pushˡ (F-resp-≈ (!-unique _) ○ homomorphism) ⟩
          D₁ ! ∘ D₁ (D₁ f) ∘ i          ≈⟨ refl⟩∘⟨ p₂ ⟩
          D₁ ! ∘ D₁ (D₁ f) ∘ h          ≈⟨ pushˡ (F-resp-≈ (!-unique _) ○ homomorphism) ⟨
          D₁ ! ∘ h
        ∎