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.NaturalTransformation using (NaturalTransformation)
open import Categories.Functor using (_∘F_) renaming (id to Id)
open import Categories.Functor.Bifunctor using (reduce-×; overlap-×)

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 chop functions: chop (D₀X × D₀⊤ ⇒ D₀(D₀X), a retraction of ⟨μ,D₁!⟩) and the
-- N-indexed chopᴺ (D₀Z × N ⇒ D₀Z × N, the prim-rec "strip n laters, reset index").
module Monad.Instance.Delay.Chop {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) (D : DelayM (Distributive.cocartesian distributive)) where
  open Category C
  open import Category.Distributive.Helper distributive
  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

  chop : ∀ {X} → D₀ X × D₀ ⊤ ⇒ D₀ (D₀ X)
  chop = D₁ [ now ∘ π₁ , out⁻¹ ∘ (π₁ +₁ π₁) ] ∘ zip

  -- chop is the anamorphism for the coalgebra that ticks both clocks together:
  -- timing now → emit the value; timing later → peel a shared `later` or emit at
  -- the value head.  It is just zip's coalgebra with chop's D₁-argument applied
  -- to the terminating cells.
  chop-coalg : ∀ {X} → D₀ X × D₀ ⊤ ⇒ D₀ X + (D₀ X × D₀ ⊤)
  chop-coalg = ([ now ∘ π₁ , out⁻¹ ∘ (π₁ +₁ π₁) ] +₁ id) ∘ distr ∘ (out ×₁ out)

  out-chop : ∀ {X} → out ∘ chop {X} ≈ (id +₁ chop) ∘ chop-coalg
  out-chop = begin
    out ∘ chop                                       ≈⟨ pullˡ (D₁-commutes h) ⟩
    ((h +₁ D₁ h) ∘ out) ∘ zip                        ≈⟨ pullʳ (Coit.coit-commutes (distr ∘ (out ×₁ out))) ⟩
    (h +₁ D₁ h) ∘ (id +₁ zip) ∘ distr ∘ (out ×₁ out) ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityʳ refl) ⟩
    (h +₁ chop) ∘ distr ∘ (out ×₁ out)               ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟨
    (id +₁ chop) ∘ (h +₁ id) ∘ distr ∘ (out ×₁ out)  ∎
       where h = [ now ∘ π₁ , out⁻¹ ∘ (π₁ +₁ π₁) ]

  chop-corec : ∀ {X} → chop {X} ≈ Coit.coit chop-coalg
  chop-corec = sym (Coit.coit-unique chop-coalg chop out-chop)

  μchop : ∀ {X} → μ X ∘ chop ≈ π₁
  μchop {X} = begin
          μ X ∘ chop       ≈⟨ pushˡ (extend⇒F₁ kleisli [ now ∘ π₁ , out⁻¹ ∘ (π₁ +₁ π₁) ]) ⟨
          zip₁⁻¹ ∘ zip     ≈⟨ pullˡ project₁ ⟨
          π₁ ∘ zip⁻¹ ∘ zip ≈⟨ elimʳ zip⁻¹∘zip ⟩
          π₁               ∎

  chopμD! : ∀ {X} → chop ∘ ⟨ μ X , D₁ ! ⟩ ≈ id
  chopμD! {X} = begin
    chop ∘ ⟨ μ X , D₁ ! ⟩                                                             ≈⟨ refl⟩∘⟨ ⟨⟩-unique (pullˡ project₁ ○ eq₁) (pullˡ project₂ ○ eq₂) ⟩
    chop ∘ zip⁻¹ ∘ D₁ (⟨ id , ! ⟩ +₁ i₂ ∘ ⟨ id , ! ⟩) ∘ D₁ out                        ≈⟨ pullˡ (cancelʳ zip∘zip⁻¹) ○ pullˡ (sym homomorphism) ⟩
    D₁ ([ now ∘ π₁ , out⁻¹ ∘ (π₁ +₁ π₁) ] ∘ (⟨ id , ! ⟩ +₁ i₂ ∘ ⟨ id , ! ⟩)) ∘ D₁ out ≈⟨ F-resp-≈ ([]∘+₁ ○ []-cong₂ (cancelʳ project₁) (pullˡ (pullʳ inject₂))) ⟩∘⟨refl ⟩
    D₁ [ now ,  (out⁻¹ ∘ i₂ ∘ π₁) ∘ ⟨ id , ! ⟩ ] ∘ D₁ out                             ≈⟨ F-resp-≈ ([]-congˡ (pullʳ (cancelʳ project₁))) ⟩∘⟨refl ⟩
    D₁ [ now , later ] ∘ D₁ out                                                       ≈⟨ sym homomorphism ○ F-resp-≈ (∘-resp-≈ˡ (sym out⁻¹-now-later) ○ out⁻¹∘out) ○ identity ⟩
    id                                                                                ∎
      where
        eq₁ : zip₁⁻¹ ∘ D₁ (⟨ id , ! ⟩ +₁ i₂ ∘ ⟨ id , ! ⟩) ∘ D₁ out ≈ μ X
        eq₁ = begin
          zip₁⁻¹ ∘ D₁ (⟨ id , ! ⟩ +₁ i₂ ∘ ⟨ id , ! ⟩) ∘ D₁ out              ≈⟨ pullˡ (extend∘F₁' kleisli _ _ ○ extend-≈ ([]∘+₁ ○ []-cong₂ (pullʳ project₁) (pullˡ (pullʳ +₁∘i₂)))) ⟩
          extend [ now ∘ id , (out⁻¹ ∘ i₂ ∘ π₁) ∘ ⟨ id , ! ⟩ ] ∘ D₁ out     ≈⟨ extend-≈ ([]-cong₂ identityʳ (pullʳ (pullʳ project₁ ○ identityʳ))) ⟩∘⟨refl ⟩
          extend [ now  , out⁻¹ ∘ i₂  ] ∘ D₁ out                            ≈⟨ extend-≈ (sym out⁻¹-now-later) ⟩∘⟨refl ⟩
          extend out⁻¹ ∘ D₁ out                                             ≈⟨ extend∘F₁' kleisli _ _ ○ extend-≈ out⁻¹∘out ⟩
          μ X                                                               ∎

        eq₂ : zip₂⁻¹ ∘ D₁ (⟨ id , ! ⟩ +₁ i₂ ∘ ⟨ id , ! ⟩) ∘ D₁ out ≈ D₁ !
        eq₂  = begin
          zip₂⁻¹ ∘ D₁ (⟨ id , ! ⟩ +₁ i₂ ∘ ⟨ id , ! ⟩) ∘ D₁ out         ≈⟨ pullˡ (extend∘F₁' kleisli _ _ ○ extend-≈ ([]∘+₁ ○ []-cong₂ (pullʳ project₂) (pullˡ (pullʳ inject₂)))) ⟩
          extend [ now ∘ ! , (out⁻¹ ∘ i₁ ∘ π₂) ∘ ⟨ id , ! ⟩ ] ∘ D₁ out ≈⟨ extend-≈ ([]-cong₂ assoc (pullʳ (pullʳ project₂))) ⟩∘⟨refl ⟩
          extend [ out⁻¹ ∘ i₁ ∘ ! , out⁻¹ ∘ i₁ ∘ ! ] ∘ D₁ out          ≈⟨ extend-≈ ([]-unique (pullʳ inject₁ ○ assoc) (pullʳ inject₂ ○ assoc)) ⟩∘⟨refl ⟩ 
          D₁ [ ! , !  ] ∘ D₁ out                                       ≈⟨ F-resp-≈ (!-unique ([ ! , ! ] ∘ out)) ○ homomorphism ⟨
          D₁ !                                                         ∎

  chop-retract : ∀ X → Retract (D₀ (D₀ X)) (D₀ X × D₀ ⊤)
  chop-retract X .Mor.Retract.section =  ⟨ μ X , D₁ ! ⟩
  chop-retract X .Mor.Retract.retract = chop
  chop-retract X .Mor.Retract.is-retract = chopμD!

  -- chop-coalg is a coalgebra morphism for D₁ f: the finite (non-recursive) cell.
  chop-coalg-natural : ∀ {X Y} (f : X ⇒ Y) → chop-coalg ∘ (D₁ f ×₁ id) ≈ (D₁ f +₁ (D₁ f ×₁ id)) ∘ chop-coalg
  chop-coalg-natural {X} {Y} f = begin
    chop-coalg ∘ (D₁ f ×₁ id)                                                                      ≈⟨ pullʳ assoc ⟩ 
    ([ now ∘ π₁ , out⁻¹ ∘ (π₁ +₁ π₁) ] +₁ id) ∘ distr ∘ (out ×₁ out) ∘ (D₁ f ×₁ id)                ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ refl identityʳ) ⟩
    ([ now ∘ π₁ , out⁻¹ ∘ (π₁ +₁ π₁) ] +₁ id) ∘ distr ∘ (out ∘ D₁ f ×₁ out)                        ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ (sym (D₁-commutes f)) (elimˡ id+₁id)) ⟨ 
    ([ now ∘ π₁ , out⁻¹ ∘ (π₁ +₁ π₁) ] +₁ id) ∘ distr ∘ ((f +₁ D₁ f) ×₁ (id +₁ id)) ∘ (out ×₁ out) ≈⟨ pushʳ (pullˡ (distr-natural _ _ _ _)) ○ pushˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ eq identityˡ)) ⟩
    (D₁ f ∘ [ now ∘ π₁ , out⁻¹ ∘ (π₁ +₁ π₁) ] +₁ (D₁ f ×₁ id)) ∘ distr ∘ (out ×₁ out)              ≈⟨ pushˡ (sym (+₁∘+₁ ○ +₁-cong₂ refl identityʳ)) ⟩
    (D₁ f +₁ (D₁ f ×₁ id)) ∘ chop-coalg                                                            ∎
      where
        eq₁ : (now ∘ π₁) ∘ (f ×₁ id) ≈ D₁ f ∘ now ∘ π₁
        eq₁ = extendˡ π₁∘×₁ ○ pushˡ (D.η.commute f) 

        eq₂ : (out⁻¹ ∘ (π₁ +₁ π₁)) ∘ (f ×₁ id +₁ D₁ f ×₁ id) ≈ D₁ f ∘ out⁻¹ ∘ (π₁ +₁ π₁)
        eq₂ = pullʳ (+₁∘+₁ ○ +₁-cong₂ π₁∘×₁ π₁∘×₁ ○ sym +₁∘+₁) ○ extendʳ (sym (D₁out⁻¹ f))

        eq : [ now ∘ π₁ , out⁻¹ ∘ (π₁ +₁ π₁) ] ∘ (f ×₁ id +₁ f ×₁ id +₁ D₁ f ×₁ id) ≈ D₁ f ∘ [ now ∘ π₁ , out⁻¹ ∘ (π₁ +₁ π₁) ]
        eq = []∘+₁ ○ []-cong₂ eq₁ eq₂ ○ sym ∘[]

  chop-natural : ∀ {X Y} (f : X ⇒ Y) → D₁ (D₁ f) ∘ chop ≈ chop ∘ (D₁ f ×₁ id)
  chop-natural {X} {Y} f = Coit.coit-unique' h (D₁ (D₁ f) ∘ chop) (chop ∘ (D₁ f ×₁ id)) eq₁ eq₂
    where
      h : D₀ X × D₀ ⊤ ⇒ D₀ Y + (D₀ X × D₀ ⊤)
      h = (D₁ f +₁ id) ∘ chop-coalg

      eq₁ : out ∘ (D₁ (D₁ f) ∘ chop) ≈ (id +₁ (D₁ (D₁ f) ∘ chop)) ∘ h
      eq₁ = begin
        out ∘ D₁ (D₁ f) ∘ chop                  ≈⟨ extendʳ (D₁-commutes (D₁ f)) ⟩
        (D₁ f +₁ D₁ (D₁ f)) ∘ out ∘ chop        ≈⟨ pushʳ out-chop ○ extendʳ (∘-resp-≈ˡ (+₁∘+₁ ○ +₁-cong₂ identityʳ refl )) ⟩
        (D₁ f +₁ D₁ (D₁ f) ∘ chop) ∘ chop-coalg ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟨ 
        (id +₁ D₁ (D₁ f) ∘ chop) ∘ h            ∎

      eq₂ : out ∘ (chop ∘ (D₁ f ×₁ id)) ≈ (id +₁ (chop ∘ (D₁ f ×₁ id))) ∘ h
      eq₂ = begin
        out ∘ chop ∘ (D₁ f ×₁ id)                  ≈⟨ extendʳ out-chop ⟩ 
        (id +₁ chop) ∘ chop-coalg ∘ (D₁ f ×₁ id)   ≈⟨ pushʳ (chop-coalg-natural f) ○ extendʳ (∘-resp-≈ˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ refl )) ⟩
        (D₁ f +₁ chop ∘ (D₁ f ×₁ id)) ∘ chop-coalg ≈⟨ pushˡ (sym (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ)) ⟩
        (id +₁ chop ∘ (D₁ f ×₁ id)) ∘ h            ∎

  chop-now : ∀ {Z} → chop {Z} ∘ (id ×₁ now) ≈ now ∘ π₁
  chop-now {Z} = begin
    chop ∘ (id ×₁ now)                          ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ identityˡ (∘-resp-≈ʳ !-unique₂) ⟩
    chop ∘ ⟨ π₁ , now ∘ ! ⟩                     ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (insertˡ D.identityʳ) (pushʳ (!-unique _) ○ pushˡ (D.η.commute !)) ⟩
    chop ∘ ⟨ μ Z ∘ now ∘ π₁ , D₁ ! ∘ now ∘ π₁ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩∘ ⟨  
    chop ∘ ⟨ μ Z , D₁ ! ⟩ ∘ now ∘ π₁            ≈⟨ cancelˡ chopμD! ⟩  
    now ∘ π₁                                    ∎

  chop-now' : ∀ {Z} → chop {Z} ∘ ⟨ id , now ∘ ! ⟩ ≈ now
  chop-now' = begin
    chop ∘ ⟨ id , now ∘ ! ⟩         ≈⟨ refl⟩∘⟨ sym (×₁∘⟨⟩ ○ ⟨⟩-congʳ identityˡ) ⟩
    chop ∘ (id ×₁ now) ∘ ⟨ id , ! ⟩ ≈⟨ pullˡ chop-now ⟩
    (now ∘ π₁) ∘ ⟨ id , ! ⟩         ≈⟨ pullʳ project₁ ⟩
    now ∘ id                        ≈⟨ identityʳ ⟩
    now                             ∎

  -- value head is `now` (clock arbitrary): chop-coalg terminates, emitting now(value) into i₁.
  chop-coalg-nowˡ : ∀ {Z} → chop-coalg {Z} ∘ (now ×₁ id) ≈ i₁ ∘ now ∘ π₁
  chop-coalg-nowˡ = begin
    chop-coalg ∘ (now ×₁ id)                                                                    ≈⟨ pullʳ assoc ⟩
    ([ now ∘ π₁ , out⁻¹ ∘ (π₁ +₁ π₁) ] +₁ id) ∘ distr ∘ (out ×₁ out) ∘ (now ×₁ id)              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ unitlaw identityʳ ○ sym first∘second ) ⟩
    ([ now ∘ π₁ , out⁻¹ ∘ (π₁ +₁ π₁) ] +₁ id) ∘ distr ∘ (i₁ ×₁ id) ∘ (id ×₁ out)                ≈⟨ refl⟩∘⟨ pullˡ (pullʳ distributeʳ⁻¹-i₁ ○ inject₁) ⟩
    ([ now ∘ π₁ , out⁻¹ ∘ (π₁ +₁ π₁) ] +₁ id) ∘ (i₁ ∘ (id +₁ i₁) ∘ distributeˡ⁻¹) ∘ (id ×₁ out) ≈⟨ pullˡ (pullˡ +₁∘i₁ ○ pullʳ eq) ⟩
    (i₁ ∘ now ∘ π₁) ∘ (id ×₁ out)                                                               ≈⟨ pullʳ (pullʳ (π₁∘×₁ ○ identityˡ)) ⟩
    i₁ ∘ now ∘ π₁                                                                               ∎
      where
        eq : [ now ∘ π₁ , out⁻¹ ∘ (π₁ +₁ π₁) ] ∘ (id +₁ i₁) ∘ distributeˡ⁻¹ ≈ now ∘ π₁
        eq = pullˡ ([]∘+₁ ○ []-cong₂ identityʳ (pullʳ +₁∘i₁ ○ sym-assoc) ○ sym ∘[]) ○ pullʳ distributeˡ⁻¹-π₁ 

  chop-coalg-now : ∀ {Z} → chop-coalg {Z} ∘ (id ×₁ now) ≈ i₁ ∘ π₁
  chop-coalg-now = begin
    chop-coalg ∘ (id ×₁ now)                                               ≈⟨ pullʳ assoc ⟩
    (h +₁ id) ∘ distr ∘ (out ×₁ out) ∘ (id ×₁ now)                         ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ identityʳ unitlaw) ⟩
    (h +₁ id) ∘ distr ∘ (out ×₁ i₁)                                        ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym (×₁∘×₁ ○ ×₁-cong₂ identityˡ identityʳ) ⟩
    (h +₁ id) ∘ distr ∘ (id ×₁ i₁) ∘ (out ×₁ id)                           ≈⟨ refl⟩∘⟨ pullˡ eq₁ ⟩
    (h +₁ id) ∘ ([ i₁ ∘ i₁ , i₁ ∘ i₂ ∘ i₂ ] ∘ distributeʳ⁻¹) ∘ (out ×₁ id) ≈⟨ extendʳ (pullˡ (∘[] ○ []-cong₂ eq₂ eq₃)) ⟩
    [ i₁ ∘ now ∘ π₁ , i₁ ∘ out⁻¹ ∘ i₂ ∘ π₁ ] ∘ distributeʳ⁻¹ ∘ (out ×₁ id) ≈⟨ pullˡ red ⟩
    (i₁ ∘ out⁻¹ ∘ π₁) ∘ (out ×₁ id)                                        ≈⟨ pullʳ (pullʳ π₁∘×₁) ⟩
    i₁ ∘ out⁻¹ ∘ out ∘ π₁                                                  ≈⟨ refl⟩∘⟨ cancelˡ out⁻¹∘out ⟩
    i₁ ∘ π₁                                                                ∎
      where
        h = [ now ∘ π₁ , out⁻¹ ∘ (π₁ +₁ π₁) ]

        eq₁ : distr ∘ (id ×₁ i₁) ≈ [ i₁ ∘ i₁ , i₁ ∘ i₂ ∘ i₂ ] ∘ distributeʳ⁻¹
        eq₁ = begin
          distr ∘ (id ×₁ i₁)                                                                                                  ≈⟨ pullʳ (∘-resp-≈ʳ (×₁-cong₂ (sym id+₁id) refl)) ⟩
          [ i₁ ∘ (id +₁ i₁) ∘ distributeˡ⁻¹ , (i₂ ∘ i₂ +₁ id) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ ((id +₁ id) ×₁ i₁)          ≈⟨ ∘-resp-≈ˡ (sym []∘+₁) ○ pullʳ (distributeʳ⁻¹-natural _ _ _) ⟨
          [ (i₁ ∘ (id +₁ i₁) ∘ distributeˡ⁻¹) ∘ (id ×₁ i₁) , ((i₂ ∘ i₂ +₁ id) ∘ distributeˡ⁻¹) ∘ (id ×₁ i₁) ] ∘ distributeʳ⁻¹ ≈⟨ []-cong₂ (pullʳ (pullʳ distributeˡ⁻¹-i₁)) (pullʳ distributeˡ⁻¹-i₁) ⟩∘⟨refl ⟩
          [ i₁ ∘ (id +₁ i₁) ∘ i₁ , (i₂ ∘ i₂ +₁ id) ∘ i₁ ] ∘ distributeʳ⁻¹                                                     ≈⟨ []-cong₂ (∘-resp-≈ʳ (+₁∘i₁ ○ identityʳ)) +₁∘i₁ ⟩∘⟨refl ⟩
          [ i₁ ∘ i₁ , i₁ ∘ i₂ ∘ i₂ ] ∘ distributeʳ⁻¹                                                                          ∎

        -- (h +₁ id) applied to the two terminating cells of distr.
        eq₂ : (h +₁ id) ∘ i₁ ∘ i₁ ≈ i₁ ∘ now ∘ π₁
        eq₂ = extendʳ +₁∘i₁ ○ (refl⟩∘⟨ inject₁)

        eq₃ : (h +₁ id) ∘ i₁ ∘ i₂ ∘ i₂ ≈ i₁ ∘ out⁻¹ ∘ i₂ ∘ π₁
        eq₃ = begin
          (h +₁ id) ∘ i₁ ∘ i₂ ∘ i₂     ≈⟨ extendʳ +₁∘i₁ ⟩
          i₁ ∘ h ∘ i₂ ∘ i₂             ≈⟨ refl⟩∘⟨ extendʳ inject₂ ⟩
          i₁ ∘ out⁻¹ ∘ (π₁ +₁ π₁) ∘ i₂ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ +₁∘i₂ ⟩
          i₁ ∘ out⁻¹ ∘ i₂ ∘ π₁         ∎

        -- both branches emit i₁: timing `now` means chop-coalg terminates, returning
        -- the whole value π₁ (= out⁻¹ ∘ out ∘ π₁) reassembled from its `out`-split halves.
        red : [ i₁ ∘ now ∘ π₁ , i₁ ∘ out⁻¹ ∘ i₂ ∘ π₁ ] ∘ distributeʳ⁻¹ ≈ i₁ ∘ out⁻¹ ∘ π₁
        red = begin
          [ i₁ ∘ now ∘ π₁ , i₁ ∘ out⁻¹ ∘ i₂ ∘ π₁ ] ∘ distributeʳ⁻¹ ≈⟨ (sym ∘[]) ⟩∘⟨refl ⟩
          (i₁ ∘ [ now ∘ π₁ , out⁻¹ ∘ i₂ ∘ π₁ ]) ∘ distributeʳ⁻¹    ≈⟨ assoc ⟩
          i₁ ∘ [ now ∘ π₁ , out⁻¹ ∘ i₂ ∘ π₁ ] ∘ distributeʳ⁻¹      ≈⟨ refl⟩∘⟨ inner ⟩
          i₁ ∘ out⁻¹ ∘ π₁                                          ∎
            where
              inner : [ now ∘ π₁ , out⁻¹ ∘ i₂ ∘ π₁ ] ∘ distributeʳ⁻¹ ≈ out⁻¹ ∘ π₁
              inner = begin
                [ now ∘ π₁ , out⁻¹ ∘ i₂ ∘ π₁ ] ∘ distributeʳ⁻¹      ≈⟨ ([]-cong₂ refl sym-assoc) ⟩∘⟨refl ⟩
                [ now ∘ π₁ , (out⁻¹ ∘ i₂) ∘ π₁ ] ∘ distributeʳ⁻¹    ≈⟨ (sym []∘+₁) ⟩∘⟨refl ⟩
                ([ now , out⁻¹ ∘ i₂ ] ∘ (π₁ +₁ π₁)) ∘ distributeʳ⁻¹ ≈⟨ (sym out⁻¹-now-later ⟩∘⟨refl) ⟩∘⟨refl ⟩
                (out⁻¹ ∘ (π₁ +₁ π₁)) ∘ distributeʳ⁻¹                ≈⟨ pullʳ distributeʳ⁻¹-π₁ ⟩
                out⁻¹ ∘ π₁                                          ∎

  chop-coalg-later : ∀ {Z} → chop-coalg {Z} ∘ (id ×₁ later) ≈ (now ∘ π₁ +₁ id) ∘ distributeʳ⁻¹ ∘ (out ×₁ id)
  chop-coalg-later = begin
    chop-coalg ∘ (id ×₁ later)                                        ≈⟨ pullʳ assoc ⟩
    (h +₁ id) ∘ distr ∘ (out ×₁ out) ∘ (id ×₁ later)                  ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ identityʳ laterlaw) ⟩
    (h +₁ id) ∘ distr ∘ (out ×₁ i₂)                                   ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym (×₁∘×₁ ○ ×₁-cong₂ identityˡ identityʳ) ⟩
    (h +₁ id) ∘ distr ∘ (id ×₁ i₂) ∘ (out ×₁ id)                      ≈⟨ refl⟩∘⟨ pullˡ eq₁ ⟩                                                                  
    (h +₁ id) ∘ ([ i₁ ∘ i₂ ∘ i₁ , i₂ ] ∘ distributeʳ⁻¹) ∘ (out ×₁ id) ≈⟨ extendʳ (pullˡ (∘[] ○ []-cong₂ eq₂ (+₁∘i₂ ○ identityʳ))) ⟩
    [ i₁ ∘ now ∘ π₁ , i₂ ] ∘ distributeʳ⁻¹ ∘ (out ×₁ id)              ≈⟨ []-congˡ identityʳ ⟩∘⟨refl ⟨  
    (now ∘ π₁ +₁ id) ∘ distributeʳ⁻¹ ∘ (out ×₁ id)                    ∎
      where
        h = [ now ∘ π₁ , out⁻¹ ∘ (π₁ +₁ π₁) ]

        -- distr on a `later`-only timing: drop to the single value-distribution.
        eq₁ : distr ∘ (id ×₁ i₂) ≈ [ i₁ ∘ i₂ ∘ i₁ , i₂ ] ∘ distributeʳ⁻¹
        eq₁ = begin
          distr ∘ (id ×₁ i₂)                                                                                                  ≈⟨ pullʳ (∘-resp-≈ʳ (×₁-cong₂ (sym id+₁id) refl)) ⟩
          [ i₁ ∘ (id +₁ i₁) ∘ distributeˡ⁻¹ , (i₂ ∘ i₂ +₁ id) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ ((id +₁ id) ×₁ i₂)          ≈⟨ ∘-resp-≈ˡ (sym []∘+₁) ○ pullʳ (distributeʳ⁻¹-natural _ _ _) ⟨ 
          [ (i₁ ∘ (id +₁ i₁) ∘ distributeˡ⁻¹) ∘ (id ×₁ i₂) , ((i₂ ∘ i₂ +₁ id) ∘ distributeˡ⁻¹) ∘ (id ×₁ i₂) ] ∘ distributeʳ⁻¹ ≈⟨ []-cong₂ (pullʳ (pullʳ distributeˡ⁻¹-i₂)) (pullʳ distributeˡ⁻¹-i₂) ⟩∘⟨refl ⟩
          [ i₁ ∘ (id +₁ i₁) ∘ i₂ , (i₂ ∘ i₂ +₁ id) ∘ i₂ ] ∘ distributeʳ⁻¹                                                     ≈⟨ []-cong₂ (∘-resp-≈ʳ inject₂) (inject₂ ○ identityʳ) ⟩∘⟨refl ⟩
          [ i₁ ∘ i₂ ∘ i₁ , i₂ ] ∘ distributeʳ⁻¹                                                                               ∎

        -- the value head: project the now-cell out of the parked i₁∘i₂∘i₁ summand.
        eq₂ : (h +₁ id) ∘ i₁ ∘ i₂ ∘ i₁ ≈ i₁ ∘ now ∘ π₁
        eq₂ = begin
          (h +₁ id) ∘ i₁ ∘ i₂ ∘ i₁     ≈⟨ extendʳ +₁∘i₁ ⟩
          i₁ ∘ h ∘ i₂ ∘ i₁             ≈⟨ refl⟩∘⟨ extendʳ inject₂ ⟩
          i₁ ∘ out⁻¹ ∘ (π₁ +₁ π₁) ∘ i₁ ≈⟨ refl⟩∘⟨ pushʳ inject₁ ⟩ 
          i₁ ∘ now ∘ π₁                ∎

  -- pull-later(laterᶜ now (later e')) = laterᶜ⁺¹ now e'
  -- pull-later(laterᶜ now (now z))    = laterᶜ now (now z)
  pull-later : ∀ {Z} → D₀ (D₀ Z) ⇒ D₀ (D₀ Z)
  pull-later = extend (out⁻¹ ∘ (now +₁ now) ∘ out)

  -- one-step unfolding of pull-later: out∘p collapses to (now+₁now)∘out.
  pull-later-commutes : ∀ {Z} → out ∘ pull-later {Z} ≈ [ (now +₁ now) ∘ out , i₂ ∘ pull-later ] ∘ out
  pull-later-commutes = extend-commutes (out⁻¹ ∘ (now +₁ now) ∘ out) ○ ∘-resp-≈ˡ ([]-congʳ (cancelˡ out∘out⁻¹))

  -- chop∘(id×₁later) is not an anamorphism over D Z × D ⊤, but it is over the
  -- enlarged state S = D Z × D ⊤ + D(D Z)
  -- 
  -- chop∘(id×₁later) = viaLater∘i₁ and pull-later∘chop = viaPull∘i₁; both viaLater and
  -- viaPull are γ-coalgebra morphisms on S, hence equal by coit-unique'.
  -- Restricting that equality along i₁ gives the result.
  chop-later : ∀ {Z} → chop {Z} ∘ (id ×₁ later) ≈ pull-later ∘ chop
  chop-later {Z} = sym inject₁ ○ ∘-resp-≈ˡ (Coit.coit-unique' γ viaLater viaPull (coalg-mor eq-later) (coalg-mor eq-pull)) ○ inject₁
    where
      -- value already running (d'); split on the timing clock:
      --   timing done   → park now d' in the D₀(D₀Z) summand (i₂∘i₂)
      --   timing running → recurse on (d',t') in the D₀Z×D₀⊤ summand (i₂∘i₁)
      δ : D₀ Z × D₀ ⊤ ⇒ D₀ Z × D₀ ⊤ + D₀ (D₀ Z)
      δ = [ i₂ ∘ now ∘ π₁ , i₁ ] ∘ distributeˡ⁻¹ ∘ (id ×₁ out)

      γ : D₀ Z × D₀ ⊤ + D₀ (D₀ Z) ⇒ D₀ Z + (D₀ Z × D₀ ⊤ + D₀ (D₀ Z))
      γ = [ (now ∘ π₁ +₁ δ ) ∘ distributeʳ⁻¹ ∘ (out ×₁ id) , (id +₁ i₂) ∘ out ]

      viaLater viaPull : D₀ Z × D₀ ⊤ + D₀ (D₀ Z) ⇒ D₀ (D₀ Z)
      
      viaLater = [ chop ∘ (id ×₁ later) , id ]
      viaPull  = [ pull-later ∘ chop , id ]

      -- assemble a γ-coalgebra morphism from the running-branch law; the parked branch
      -- collapses since [ k , id ] ∘ i₂ = id.
      coalg-mor : ∀ {k : D₀ Z × D₀ ⊤ ⇒ D₀ (D₀ Z)}
                → out ∘ k ≈ (id +₁ [ k , id ]) ∘ (now ∘ π₁ +₁ δ) ∘ distributeʳ⁻¹ ∘ (out ×₁ id)
                → out ∘ [ k , id ] ≈ (id +₁ [ k , id ]) ∘ γ
      coalg-mor run = ∘[] ○ []-cong₂ run (identityʳ ○ insertˡ (+-second∘+-second ○ +₁-cong₂ refl inject₂ ○ id+₁id)) ○ sym ∘[]

      eq-later : out ∘ chop ∘ (id ×₁ later) ≈ (id +₁ viaLater) ∘ (now ∘ π₁ +₁ δ) ∘ distributeʳ⁻¹ ∘ (out ×₁ id)
      eq-later = begin
        out ∘ chop ∘ (id ×₁ later)                                         ≈⟨ extendʳ out-chop ⟩
        (id +₁ chop) ∘ chop-coalg ∘ (id ×₁ later)                          ≈⟨ pushʳ chop-coalg-later ○ ∘-resp-≈ˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟩
        (now ∘ π₁ +₁ chop) ∘ distributeʳ⁻¹ ∘ (out ×₁ id)                   ≈⟨ (∘[] ○ []-cong₂ (pullˡ (inject₁ ○ identityʳ)) (pullˡ +₁∘i₂ ○ pullʳ δ-eq)) ⟩∘⟨refl ⟨ 
        ((id +₁ viaLater) ∘ (now ∘ π₁ +₁ δ)) ∘ distributeʳ⁻¹ ∘ (out ×₁ id) ≈⟨ assoc ⟩ 
        (id +₁ viaLater) ∘ (now ∘ π₁ +₁ δ) ∘ distributeʳ⁻¹ ∘ (out ×₁ id)   ∎
          where
            δ-eq : viaLater ∘ δ ≈ chop
            δ-eq = begin
              viaLater ∘ δ                                                                           ≈⟨ pullˡ ∘[] ⟩
              [ viaLater ∘ i₂ ∘ now ∘ π₁ , viaLater ∘ i₁ ] ∘ distributeˡ⁻¹ ∘ (id ×₁ out)             ≈⟨ []-cong₂ (pullˡ inject₂ ○ identityˡ ○ sym chop-now) inject₁ ⟩∘⟨refl ⟩
              [ chop ∘ (id ×₁ now) , chop ∘ (id ×₁ later) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ out)            ≈⟨ pullˡ ∘[] ⟨
              chop ∘ [ id ×₁ now , id ×₁ later ] ∘ distributeˡ⁻¹ ∘ (id ×₁ out)                       ≈⟨ refl⟩∘⟨ pullˡ (∘[] ○ []-cong₂ (second∘second ○ second-cong inject₁)
                                                                                                                                      (second∘second ○ second-cong inject₂)) ⟨  
              chop ∘ (id ×₁ [ now , later ]) ∘ [ id ×₁ i₁ , id ×₁ i₂ ] ∘ distributeˡ⁻¹ ∘ (id ×₁ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ cancelˡ (IsIso.isoʳ isIsoˡ) ⟩  
              chop ∘ (id ×₁ [ now , later ]) ∘ (id ×₁ out)                                           ≈⟨ refl⟩∘⟨ second-cong out⁻¹-now-later ⟩∘⟨refl ⟨
              chop ∘ (id ×₁ out⁻¹) ∘ (id ×₁ out)                                                     ≈⟨ elimʳ (second∘second ○ second-cong out⁻¹∘out ○ id×₁id) ⟩
              chop                                                                                   ∎
      
      eq-pull : out ∘ pull-later ∘ chop ≈ (id +₁ viaPull) ∘ (now ∘ π₁ +₁ δ) ∘ distributeʳ⁻¹ ∘ (out ×₁ id)
      eq-pull = begin
        out ∘ pull-later ∘ chop                                           ≈⟨ out-pull-chop ⟩
        (now ∘ π₁ +₁ valpull) ∘ distributeʳ⁻¹ ∘ (out ×₁ out)              ≈⟨ distr-push-out ⟩
        (now ∘ π₁ +₁ valpull ∘ (id ×₁ out)) ∘ distributeʳ⁻¹ ∘ (out ×₁ id) ≈⟨ sym-assoc ○ extendʳ (∘-resp-≈ˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ δ-eq)) ⟨ 
        (id +₁ viaPull) ∘ (now ∘ π₁ +₁ δ) ∘ distributeʳ⁻¹ ∘ (out ×₁ id)   ∎
          where
            -- the value branch: park-now on done-timing, recurse on running-timing
            valpull = [ now ∘ π₁ , pull-later ∘ chop ] ∘ distributeˡ⁻¹

            out-pull-chop = begin
              out ∘ pull-later ∘ chop                                                                                                                       ≈⟨ extendʳ pull-later-commutes ⟩
              [ (now +₁ now) ∘ out , i₂ ∘ pull-later ] ∘ out ∘ chop                                                                                         ≈⟨ refl⟩∘⟨ out-chop ⟩
              [ (now +₁ now) ∘ out , i₂ ∘ pull-later ] ∘ (id +₁ chop) ∘ chop-coalg                                                                          ≈⟨ pullˡ ([]∘+₁ ○ []-cong₂ identityʳ assoc) ⟩
              [ (now +₁ now) ∘ out , i₂ ∘ pull-later ∘ chop ] ∘ chop-coalg                                                                                  ≈⟨ pullˡ ([]∘+₁ ○ []-cong₂ assoc identityʳ) ⟩
              [ (now +₁ now) ∘ out ∘ [ now ∘ π₁ , out⁻¹ ∘ (π₁ +₁ π₁) ] , i₂ ∘ pull-later ∘ chop ] ∘ distr ∘ (out ×₁ out)                                    ≈⟨ []-congʳ (∘-resp-≈ʳ (∘[] ○ []-cong₂ (pullˡ unitlaw) (cancelˡ out∘out⁻¹))) ⟩∘⟨refl ⟩
              [ (now +₁ now) ∘ [ i₁ ∘ π₁ , (π₁ +₁ π₁) ] , i₂ ∘ pull-later ∘ chop ] ∘ distr ∘ (out ×₁ out)                                                   ≈⟨ []-congʳ (∘[] ○ []-cong₂ (extendʳ +₁∘i₁) +₁∘+₁) ⟩∘⟨refl ⟩ 
              [ [ i₁ ∘ now ∘ π₁ , now ∘ π₁ +₁ now ∘ π₁ ] , i₂ ∘ pull-later ∘ chop ]  ∘ distr ∘ (out ×₁ out)                                                 ≈⟨ extendʳ (pullˡ (∘[] ○ []-cong₂ (pullˡ inject₁) (extendʳ ([]∘+-first ○ []-congʳ (pullˡ inject₂ ○ +₁∘i₂) ○ sym ∘[])))) ⟩
              [ [ i₁ ∘ now ∘ π₁ , now ∘ π₁ +₁ now ∘ π₁ ] ∘ (id +₁ i₁) ∘ distributeˡ⁻¹ , i₂ ∘ [ now ∘ π₁ , pull-later ∘ chop ] ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (out ×₁ out)
                                                                                                                                                            ≈⟨ []-cong₂ (pullˡ ([]∘+₁ ○ []-cong₂ identityʳ inject₁)) refl ⟩∘⟨refl ⟩
              [ [ i₁ ∘ now ∘ π₁ , i₁ ∘ now ∘ π₁ ] ∘ distributeˡ⁻¹ , i₂ ∘ [ now ∘ π₁ , pull-later ∘ chop ] ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (out ×₁ out)  ≈⟨ []-congʳ (pullˡ ∘[]) ⟩∘⟨refl ⟨ 
              ([ now ∘ π₁ , now ∘ π₁ ] ∘ distributeˡ⁻¹ +₁ [ now ∘ π₁ , pull-later ∘ chop ] ∘ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ (out ×₁ out)                  ≈⟨ extendʳ (∘-resp-≈ˡ (+₁-cong₂ (∘-resp-≈ˡ (sym ∘[]) ○ pullʳ distributeˡ⁻¹-π₁) refl)) ⟩ 
              (now ∘ π₁ +₁ valpull) ∘ distributeʳ⁻¹ ∘ (out ×₁ out)                                                                                          ∎
 
            -- move (id×₁out) through distributeʳ⁻¹: (out×₁out) becomes (out×₁id), with the
            -- timing-out pushed into the value branch.
            distr-push-out = begin
                (now ∘ π₁ +₁ valpull) ∘ distributeʳ⁻¹ ∘ (out ×₁ out)                               ≈⟨ refl⟩∘⟨ refl⟩∘⟨ second∘first ⟨ 
                (now ∘ π₁ +₁ valpull) ∘ distributeʳ⁻¹ ∘ (id ×₁ out) ∘ (out ×₁ id)                  ≈⟨ refl⟩∘⟨ extendʳ (distributeʳ⁻¹-natural _ _ _ ○ ∘-resp-≈ʳ (×₁-cong₂ id+₁id refl)) ⟨ 
                (now ∘ π₁ +₁ valpull) ∘ ((id ×₁ out) +₁ (id ×₁ out)) ∘ distributeʳ⁻¹ ∘ (out ×₁ id) ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ (pullʳ π₁∘second) refl) ⟩
                (now ∘ π₁ +₁ valpull ∘ (id ×₁ out)) ∘ distributeʳ⁻¹ ∘ (out ×₁ id)                  ∎

            -- viaPull collapses δ's bracket back to the value branch (parked-now / recurse)
            δ-eq : viaPull ∘ δ ≈ valpull ∘ (id ×₁ out)
            δ-eq = pullˡ (∘[] ○ []-cong₂ (pullˡ inject₂ ○ identityˡ) inject₁) ○ sym assoc

  D!chop-μ : ∀ {Y} → D₁ ! ∘ chop {D₀ Y} ∘ ⟨ id , D₁ ! ∘ μ Y ⟩ ≈ D₁ !
  D!chop-μ {Y} = Coit.coit-unique' γ Φ (D₁ !) eqΦ eqD!
    where
      Φ : D₀ (D₀ Y) ⇒ D₀ ⊤
      Φ = D₁ ! ∘ chop ∘ ⟨ id , D₁ ! ∘ μ Y ⟩

      γ : D₀ (D₀ Y) ⇒ ⊤ + D₀ (D₀ Y)
      γ = (! +₁ id) ∘ out

      -- clock-dominance: the self-clock D₁!∘μ peels a `later` exactly when the value does,
      -- so chop-coalg always takes the now-emit / recurse branch, never the truncating one.
      clock-dom : chop-coalg {D₀ Y} ∘ ⟨ id , D₁ ! ∘ μ Y ⟩ ≈ (now +₁ ⟨ id , D₁ ! ∘ μ Y ⟩) ∘ out
      clock-dom = D-jointly-epic now-case later-case
        where
          -- later is natural for D₁ (later = out⁻¹∘i₂, via D₁out⁻¹) and for μ (μ = extend id).
          D₁later : ∀ {A B} (f : A ⇒ B) → D₁ f ∘ later ≈ later ∘ D₁ f
          D₁later f = pullˡ (D₁out⁻¹ f) ○ assoc ○ ∘-resp-≈ʳ +₁∘i₂ ○ sym-assoc

          μlater : μ Y ∘ later ≈ later ∘ μ Y
          μlater = sym (Later∘Extend.later-extend-comm id)

          -- inner value now: ⟨now∘now, now∘!⟩ = (now×₁id)∘⟨now, now∘!⟩; emit via chop-coalg-now.
          emit-now : (chop-coalg ∘ ⟨ now , D₁ ! ⟩) ∘ now ≈ (i₁ ∘ now) ∘ now
          emit-now = begin
            (chop-coalg ∘ ⟨ now , D₁ ! ⟩) ∘ now          ≈⟨ pullʳ (⟨⟩∘ ○ ⟨⟩-congˡ (sym (D.η.commute !))) ⟩
            chop-coalg ∘ ⟨ now ∘ now , now ∘ ! ⟩         ≈⟨ refl⟩∘⟨ sym (×₁∘⟨⟩ ○ ⟨⟩-congˡ identityˡ) ⟩
            chop-coalg ∘ (now ×₁ id) ∘ ⟨ now , now ∘ ! ⟩ ≈⟨ pullˡ chop-coalg-nowˡ ⟩
            (i₁ ∘ now ∘ π₁) ∘ ⟨ now , now ∘ ! ⟩          ≈⟨ pullʳ (pullʳ project₁) ⟩
            i₁ ∘ now ∘ now                               ≈⟨ sym-assoc ⟩
            (i₁ ∘ now) ∘ now                             ∎

          -- inner value later: ⟨now∘later, later∘D₁!⟩ = (now×₁id)∘⟨later, later∘D₁!⟩; emit via chop-coalg-now.
          emit-later : (chop-coalg ∘ ⟨ now , D₁ ! ⟩) ∘ later ≈ (i₁ ∘ now) ∘ later
          emit-later = begin
            (chop-coalg ∘ ⟨ now , D₁ ! ⟩) ∘ later               ≈⟨ pullʳ (⟨⟩∘ ○ ⟨⟩-congˡ (D₁later !)) ⟩
            chop-coalg ∘ ⟨ now ∘ later , later ∘ D₁ ! ⟩         ≈⟨ refl⟩∘⟨ sym (×₁∘⟨⟩ ○ ⟨⟩-congˡ identityˡ) ⟩
            chop-coalg ∘ (now ×₁ id) ∘ ⟨ later , later ∘ D₁ ! ⟩ ≈⟨ pullˡ chop-coalg-nowˡ ⟩
            (i₁ ∘ now ∘ π₁) ∘ ⟨ later , later ∘ D₁ ! ⟩          ≈⟨ pullʳ (pullʳ project₁) ⟩
            i₁ ∘ now ∘ later                                    ≈⟨ sym-assoc ⟩
            (i₁ ∘ now) ∘ later                                  ∎


          now-case : (chop-coalg {D₀ Y} ∘ ⟨ id , D₁ ! ∘ μ Y ⟩) ∘ now ≈ ((now +₁ ⟨ id , D₁ ! ∘ μ Y ⟩) ∘ out) ∘ now
          now-case = begin
            (chop-coalg ∘ ⟨ id , D₁ ! ∘ μ Y ⟩) ∘ now   ≈⟨ assoc ⟩
            chop-coalg ∘ ⟨ id , D₁ ! ∘ μ Y ⟩ ∘ now     ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ (cancelʳ D.identityʳ)) ⟩
            chop-coalg ∘ ⟨ now , D₁ ! ⟩                ≈⟨ D-jointly-epic emit-now emit-later ⟩
            i₁ ∘ now                                   ≈⟨ +₁∘i₁ ⟨
            (now +₁ ⟨ id , D₁ ! ∘ μ Y ⟩) ∘ i₁          ≈⟨ refl⟩∘⟨ unitlaw ⟨
            (now +₁ ⟨ id , D₁ ! ∘ μ Y ⟩) ∘ out ∘ now   ≈⟨ sym-assoc ⟩
            ((now +₁ ⟨ id , D₁ ! ∘ μ Y ⟩) ∘ out) ∘ now ∎

          -- the self-clock peels a `later` exactly when the value does
          clater : ⟨ id , D₁ ! ∘ μ Y ⟩ ∘ later ≈ (later ×₁ later) ∘ ⟨ id , D₁ ! ∘ μ Y ⟩
          clater = ⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ cl ○ sym (×₁∘⟨⟩ ○ ⟨⟩-congʳ identityʳ)
            where
              cl : (D₁ ! ∘ μ Y) ∘ later ≈ later ∘ D₁ ! ∘ μ Y
              cl = assoc ○ ∘-resp-≈ʳ μlater ○ sym-assoc ○ ∘-resp-≈ˡ (D₁later !) ○ assoc

          -- both values running: chop-coalg recurses (i₂), via chop-coalg-later.
          cc-ll : chop-coalg {D₀ Y} ∘ (later ×₁ later) ≈ i₂
          cc-ll = begin
            chop-coalg ∘ (later ×₁ later)                                    ≈⟨ refl⟩∘⟨ sym (×₁∘×₁ ○ ×₁-cong₂ identityˡ identityʳ) ⟩
            chop-coalg ∘ (id ×₁ later) ∘ (later ×₁ id)                       ≈⟨ pullˡ chop-coalg-later ⟩
            ((now ∘ π₁ +₁ id) ∘ distributeʳ⁻¹ ∘ (out ×₁ id)) ∘ (later ×₁ id) ≈⟨ assoc ○ ∘-resp-≈ʳ assoc ⟩
            (now ∘ π₁ +₁ id) ∘ distributeʳ⁻¹ ∘ (out ×₁ id) ∘ (later ×₁ id)   ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ laterlaw identity²) ⟩
            (now ∘ π₁ +₁ id) ∘ distributeʳ⁻¹ ∘ (i₂ ×₁ id)                    ≈⟨ refl⟩∘⟨ distributeʳ⁻¹-i₂ ⟩
            (now ∘ π₁ +₁ id) ∘ i₂                                            ≈⟨ +₁∘i₂ ○ identityʳ ⟩
            i₂                                                               ∎

          later-case = begin
            (chop-coalg ∘ ⟨ id , D₁ ! ∘ μ Y ⟩) ∘ later          ≈⟨ pullʳ clater ⟩
            chop-coalg ∘ (later ×₁ later) ∘ ⟨ id , D₁ ! ∘ μ Y ⟩ ≈⟨ pullˡ cc-ll ⟩
            i₂ ∘ ⟨ id , D₁ ! ∘ μ Y ⟩                            ≈⟨ +₁∘i₂ ⟨
            (now +₁ ⟨ id , D₁ ! ∘ μ Y ⟩) ∘ i₂                   ≈⟨ refl⟩∘⟨ laterlaw ⟨
            (now +₁ ⟨ id , D₁ ! ∘ μ Y ⟩) ∘ out ∘ later          ≈⟨ sym-assoc ⟩
            ((now +₁ ⟨ id , D₁ ! ∘ μ Y ⟩) ∘ out) ∘ later        ∎

      eqΦ : out ∘ Φ ≈ (id +₁ Φ) ∘ γ
      eqΦ = begin
        out ∘ D₁ ! ∘ chop ∘ ⟨ id , D₁ ! ∘ μ Y ⟩                 ≈⟨ extendʳ (D₁-commutes !) ⟩
        (! +₁ D₁ !) ∘ out ∘ chop ∘ ⟨ id , D₁ ! ∘ μ Y ⟩          ≈⟨ ∘-resp-≈ʳ (extendʳ out-chop) ○ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityʳ refl) ⟩
        (! +₁ D₁ ! ∘ chop) ∘ chop-coalg ∘ ⟨ id , D₁ ! ∘ μ Y ⟩   ≈⟨ refl⟩∘⟨ clock-dom ⟩
        (! +₁ D₁ ! ∘ chop) ∘ (now +₁ ⟨ id , D₁ ! ∘ μ Y ⟩) ∘ out ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ !-unique₂ assoc) ⟩
        (! +₁ Φ) ∘ out                                          ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟨
        (id +₁ Φ) ∘ γ                                           ∎

      eqD! : out ∘ D₁ ! ≈ (id +₁ D₁ !) ∘ γ
      eqD! = D₁-commutes ! ○ sym (pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ))