open import Level

open import Categories.Category.Core
open import Data.Product using (_,_; Σ; Σ-syntax)
open import Categories.Functor hiding (id)
open import Categories.Functor.Algebra
open import Categories.Functor.Coalgebra
open import Categories.Object.Terminal
open import Categories.NaturalTransformation.Core hiding (id)
open import Categories.Category.Distributive
open import Categories.Object.NaturalNumbers.Parametrized
open import Monad.Helper
open import Monad.Instance.Delay

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

module Monad.Instance.Delay.Quotient {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) (DM : DelayM (Distributive.cocartesian distributive)) (PNNO : ParametrizedNNO C (Distributive.cartesian distributive)) where
  open import Category.Distributive.Helper distributive
  open Bundles
  open Category C
  open import Categories.Diagram.Coequalizer C 
  open import Algebra.Search cocartesian
  open import Algebra.Elgot cocartesian
  open F-Coalgebra-Morphism using () renaming (f to u; commutes to coalg-commutes)

  -- preservation of coequalizers under functors
  preserves : ∀ {X Y} {f g : X ⇒ Y} → Endofunctor C → Coequalizer f g → Set (o ⊔ ℓ ⊔ e)
  preserves {X} {Y} {f} {g} F coeq = IsCoequalizer (Functor.₁ F f) (Functor.₁ F g) (Functor.₁ F (Coequalizer.arr coeq))

  open DelayM DM
  open import Monad.Instance.Delay.Iota distributive DM PNNO
  open ParametrizedNNO PNNO

  open D-Monad
  open D-Kleisli
  open Later∘Extend
  open Coit
  open HomReasoning
  open M C
  open MR C
  open Equiv

  record DelayQ : Set (o ⊔ ℓ ⊔ e) where
    field
      coeqs : ∀ X → Coequalizer (extend (ι {X})) (D₁ π₁)

    Ď₀ : Obj → Obj
    Ď₀ X = Coequalizer.obj (coeqs X)

    ρ : ∀ {X} → D₀ X ⇒ Ď₀ X
    ρ {X} = Coequalizer.arr (coeqs X)

    field
      coeq-productsˡ : ∀ {X Y} (f : Y ⇒ Y) → IsCoequalizer (extend (ι {X}) ×₁ f) (D₁ π₁ ×₁ f) (ρ {X} ×₁ f)
      coeq-productsᵐ : ∀ {X Y Z} → IsCoequalizer (id {X} ×₁ (extend (ι {Y}) ×₁ id {Z})) (id {X} ×₁ (D₁ (π₁ {Y} {N}) ×₁ id {Z})) (id {X} ×₁ (ρ {Y} ×₁ id {Z}))

    abstract
      coeq-productsʳ : ∀ {X Y} (f : Y ⇒ Y) → IsCoequalizer (f ×₁ extend (ι {X})) (f ×₁ D₁ π₁) (f ×₁ ρ {X})
      coeq-productsʳ {X} {Y} f = record
        { equality = begin 
          (f ×₁ ρ) ∘ (f ×₁ extend ι) ≈⟨ ×₁∘×₁ ⟩ 
          f ∘ f ×₁ ρ ∘ extend ι      ≈⟨ ×₁-cong₂ refl c-equality ⟩ 
          f ∘ f ×₁ ρ ∘ D₁ π₁         ≈˘⟨ ×₁∘×₁ ⟩  
          (f ×₁ ρ) ∘ (f ×₁ D₁ π₁)    ∎ 
        ; coequalize = λ {Z} {h} eq → p-coequalize {h = h ∘ swap} (eq-to-swap eq) ∘ swap 
        ; universal = λ {Z} {h} {eq} → begin 
          h                                                ≈⟨ introʳ swap∘swap ⟩ 
          h ∘ swap ∘ swap                                  ≈⟨ extendʳ (p-universal {h = h ∘ swap} {eq = eq-to-swap eq}) ⟩ 
          p-coequalize (eq-to-swap eq) ∘ (ρ ×₁ f) ∘ swap   ≈˘⟨ pullʳ swap∘×₁ ⟩ 
          (p-coequalize (eq-to-swap eq) ∘ swap) ∘ (f ×₁ ρ) ∎ 
        ; unique = λ {Z} {h} {i} {eqh} universal-i → begin 
          i                                    ≈⟨ introʳ swap∘swap ⟩ 
          i ∘ swap ∘ swap                      ≈⟨ pullˡ (p-unique (universal-swap universal-i)) ⟩ 
          p-coequalize (eq-to-swap eqh) ∘ swap ∎ 
        }
        where
          open Coequalizer (coeqs X) using () renaming (equality to c-equality)
          open IsCoequalizer (coeq-productsˡ {X} {Y} f) using () renaming (coequalize to p-coequalize; universal to p-universal; unique to p-unique)
          universal-swap : ∀ {Z} {h : Y × D₀ X ⇒ Z} {i : Y × Ď₀ X ⇒ Z} → h ≈ i ∘ (f ×₁ ρ) → h ∘ swap ≈ (i ∘ swap) ∘ (ρ ×₁ f)
          universal-swap {Z} {h} {i} eq = begin 
            h ∘ swap              ≈⟨ eq ⟩∘⟨refl ⟩ 
            (i ∘ (f ×₁ ρ)) ∘ swap ≈˘⟨ extendˡ swap∘×₁ ⟩ 
            (i ∘ swap) ∘ (ρ ×₁ f) ∎
          eq-to-swap : ∀ {Z} {h : Y × D₀ X ⇒ Z} → h ∘ (f ×₁ extend ι) ≈ h ∘ (f ×₁ D₁ π₁) → (h ∘ swap) ∘ (extend ι ×₁ f) ≈ (h ∘ swap) ∘ (D₁ π₁ ×₁ f)
          eq-to-swap {Z} {h} eq = begin 
            (h ∘ swap) ∘ (extend ι ×₁ f) ≈⟨ pullʳ swap∘×₁ ⟩ 
            h ∘ (f ×₁ extend ι) ∘ swap   ≈⟨ extendʳ eq ⟩ 
            h ∘ (f ×₁ D₁ π₁) ∘ swap      ≈˘⟨ pullʳ swap∘×₁ ⟩ 
            (h ∘ swap) ∘ (D₁ π₁ ×₁ f)    ∎
    
    ρ-epi : ∀ {X} → Epi (ρ {X})
    ρ-epi {X} = Coequalizer⇒Epi (coeqs X)

    ρ-later : ∀ {X} → ρ ∘ later ≈ ρ {X}
    ρ-later {X} = sym (begin 
      ρ                                                                  ≈⟨ introʳ intro-helper ⟩ 
      ρ ∘ D₁ π₁ ∘ D₁ ⟨ id , s ∘ z ∘ Terminal.! terminal ⟩                ≈⟨ pullˡ (sym equality) ⟩ 
      (ρ ∘ extend ι) ∘ D₁ ⟨ id , s ∘ z ∘ Terminal.! terminal ⟩           ≈⟨ pullʳ (sym DK.assoc) ⟩ 
      ρ ∘ extend (extend ι ∘ now ∘ ⟨ id , s ∘ z ∘ Terminal.! terminal ⟩) ≈⟨ (refl⟩∘⟨ extend-≈ (pullˡ DK.identityʳ)) ⟩ 
      ρ ∘ extend (ι ∘ ⟨ id , s ∘ z ∘ Terminal.! terminal ⟩)              ≈⟨ (refl⟩∘⟨ extend-≈ helper) ⟩ 
      ρ ∘ extend (later ∘ now)                                           ≈⟨ (refl⟩∘⟨ sym (extend∘later now)) ⟩ 
      ρ ∘ extend now ∘ later                                             ≈⟨ elim-center DK.identityˡ ⟩ 
      ρ ∘ later                                                          ∎)
      where
        open Coequalizer (coeqs X) using (equality; coequalize; id-coequalize; coequalize-resp-≈) renaming (universal to coeq-universal; unique to coeq-unique; unique′ to coeq-unique′)
        intro-helper : D₁ π₁ ∘ D₁ ⟨ id , s ∘ z ∘ Terminal.! terminal ⟩ ≈ id
        intro-helper = sym D.F.homomorphism ○ D.F.F-resp-≈ project₁ ○ D.F.identity
        helper : ι ∘ ⟨ id , s ∘ z ∘ Terminal.! terminal ⟩ ≈ later ∘ now
        helper = begin 
          ι ∘ ⟨ id , s ∘ z ∘ Terminal.! terminal ⟩                                                          ≈⟨ introˡ out⁻¹∘out ⟩ 
          (out⁻¹ ∘ out) ∘ ι ∘ ⟨ id , s ∘ z ∘ Terminal.! terminal ⟩                                          ≈⟨ pullʳ (pullˡ ι-commutes) ⟩
          out⁻¹ ∘ ((id +₁ ι) ∘ _≅_.from nno-iso) ∘ ⟨ id , s ∘ z ∘ Terminal.! terminal ⟩                     ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ sym (×₁∘⟨⟩ ○ ⟨⟩-congʳ identity²)) ⟩
          out⁻¹ ∘ ((id +₁ ι) ∘ _≅_.from nno-iso) ∘ (id ×₁ s) ∘ ⟨ id , z ∘ Terminal.! terminal ⟩             ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ sym inject₂ ⟩∘⟨refl) ⟩
          out⁻¹ ∘ ((id +₁ ι) ∘ _≅_.from nno-iso) ∘ (_≅_.to nno-iso ∘ i₂) ∘ ⟨ id , z ∘ Terminal.! terminal ⟩ ≈⟨ (refl⟩∘⟨ (pullʳ (pullˡ (cancelˡ (_≅_.isoʳ nno-iso))))) ⟩
          out⁻¹ ∘ (id +₁ ι) ∘ i₂ ∘ ⟨ id , z ∘ Terminal.! terminal ⟩                                         ≈⟨ (refl⟩∘⟨ pullˡ +₁∘i₂) ⟩
          out⁻¹ ∘ (i₂ ∘ ι) ∘ ⟨ id , z ∘ Terminal.! terminal ⟩                                               ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ sym inject₁) ⟩
          out⁻¹ ∘ (i₂ ∘ ι) ∘ _≅_.to nno-iso ∘ i₁                                                            ≈⟨ (refl⟩∘⟨ intro-center out⁻¹∘out ⟩∘⟨refl) ⟩
          out⁻¹ ∘ (i₂ ∘ (out⁻¹ ∘ out) ∘ ι) ∘ _≅_.to nno-iso ∘ i₁                                            ≈⟨ (refl⟩∘⟨ (refl⟩∘⟨ pullʳ ι-commutes) ⟩∘⟨refl) ⟩
          out⁻¹ ∘ (i₂ ∘ out⁻¹ ∘ (id +₁ ι) ∘ _≅_.from nno-iso) ∘ _≅_.to nno-iso ∘ i₁                         ≈⟨ (refl⟩∘⟨ (pullʳ (pullˡ (pullʳ (cancelʳ (_≅_.isoʳ nno-iso)))))) ⟩
          out⁻¹ ∘ i₂ ∘ (out⁻¹ ∘ (id +₁ ι)) ∘ i₁                                                             ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ pullʳ +₁∘i₁) ⟩
          out⁻¹ ∘ i₂ ∘ out⁻¹ ∘ i₁ ∘ id                                                                      ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ identityʳ) ⟩
          out⁻¹ ∘ i₂ ∘ out⁻¹ ∘ i₁                                                                           ≈⟨ ((refl⟩∘⟨ sym-assoc) ○ assoc²δγ) ⟩
          later ∘ now                                                                                       ∎

    ρ-earlier : ∀ {X} → ρ ∘ earlier ≈ ρ {X}
    ρ-earlier {X} = D-jointly-epic (pullʳ earlier∘now) (pullʳ earlier∘later ○ identityʳ ○ sym ρ-later)
        
    open IsCoequalizer
    open Coequalizer using (isCoequalizer)

    -- helper for showing the next coequalizer property
    private
      bisim-implies : ∀ {X Y} (h : D₀ X ⇒ Y) → (h ∘ extend ([ now , [ ι ∘ (id ×₁ s) , now ∘ π₁ ] ]) ≈ h ∘ extend ([ now , [ (now ∘ π₁) , (ι ∘ (id ×₁ s)) ] ])) → (h ∘ extend ι ≈ h ∘ D₁ π₁)
      bisim-implies {X} {Y} h eq = sym equality₁ ○ extendʳ (sym eq) ○ equality₂
        where
        h∘later≈h : h ≈ h ∘ later
        h∘later≈h = begin 
          h                                                                                                         ≈⟨ introʳ (extend∘F₁' kleisli _ _ ○ extend-≈ (pullˡ inject₂ ○ (extendʳ inject₂ ○ elimʳ project₁)) ○ DK.identityˡ) ⟩ 
          h ∘ extend ([ now , [ ι ∘ (id ×₁ s) , now ∘ π₁ ] ]) ∘ D₁ (i₂ ∘ i₂ ∘ ⟨ id , z ∘ Terminal.! terminal ⟩)     ≈⟨ extendʳ eq ⟩ 
          h ∘ extend ([ now , [ (now ∘ π₁) , (ι ∘ (id ×₁ s)) ] ]) ∘ D₁ (i₂ ∘ i₂ ∘ ⟨ id , z ∘ Terminal.! terminal ⟩) ≈⟨ refl⟩∘⟨ ((extend∘F₁' kleisli _ _) ○ extend-≈ (pullˡ inject₂ ○ (extendʳ inject₂))) ⟩ 
          h ∘ extend (ι ∘ (id ×₁ s) ∘ ⟨ id , z ∘ Terminal.! terminal ⟩)                                             ≈⟨ (refl⟩∘⟨ (extend-≈ (extendʳ ι-succ))) ⟩ 
          h ∘ extend (later ∘ ι ∘ ⟨ id , z ∘ Terminal.! terminal ⟩)                                                 ≈⟨ (refl⟩∘⟨ (extend-≈ (refl⟩∘⟨ ι-zero))) ⟩ 
          h ∘ extend (later ∘ now)                                                                                  ≈⟨ (refl⟩∘⟨ (sym (later∘extend now))) ⟩
          h ∘ later ∘ extend now                                                                                    ≈⟨ refl⟩∘⟨ elimʳ DK.identityˡ ⟩
          h ∘ later                                                                                                 ∎
        equality₁ : h ∘ extend ([ now , [ (now ∘ π₁) , (ι ∘ (id ×₁ s)) ] ]) ∘ D₁ (i₂ ∘ i₂) ≈ h ∘ extend ι
        equality₁ = begin 
          h ∘ extend ([ now , [ (now ∘ π₁) , (ι ∘ (id ×₁ s)) ] ]) ∘ D₁ (i₂ ∘ i₂) ≈⟨ (refl⟩∘⟨ (extend∘F₁' kleisli _ _)) ⟩ 
          h ∘ extend ([ now , [ (now ∘ π₁) , (ι ∘ (id ×₁ s)) ] ] ∘ i₂ ∘ i₂)      ≈⟨ (refl⟩∘⟨ (extend-≈ (pullˡ inject₂))) ⟩ 
          h ∘ extend ([ (now ∘ π₁) , (ι ∘ (id ×₁ s)) ] ∘ i₂)                     ≈⟨ (refl⟩∘⟨ (extend-≈ inject₂)) ⟩ 
          h ∘ extend (ι ∘ (id ×₁ s))                                             ≈⟨ (refl⟩∘⟨ (extend-≈ ι-succ)) ⟩ 
          h ∘ extend (later ∘ ι)                                                 ≈⟨ (refl⟩∘⟨ (sym (later∘extend ι))) ⟩
          h ∘ later ∘ extend ι                                                   ≈⟨ pullˡ (sym h∘later≈h) ⟩
          h ∘ extend ι                                                           ∎
        equality₂ : h ∘ extend ([ now , [ ι ∘ (id ×₁ s) , now ∘ π₁ ] ]) ∘ D₁ (i₂ ∘ i₂) ≈ h ∘ D₁ π₁
        equality₂ = begin 
          h ∘ extend ([ now , [ ι ∘ (id ×₁ s) , now ∘ π₁ ] ]) ∘ D₁ (i₂ ∘ i₂) ≈⟨ (refl⟩∘⟨ extend∘F₁' kleisli _ _) ⟩ 
          h ∘ extend ([ now , [ ι ∘ (id ×₁ s) , now ∘ π₁ ] ] ∘ i₂ ∘ i₂)      ≈⟨ (refl⟩∘⟨ (extend-≈ (pullˡ inject₂))) ⟩ 
          h ∘ extend ([ ι ∘ (id ×₁ s) , now ∘ π₁ ] ∘ i₂)                     ≈⟨ (refl⟩∘⟨ (extend-≈ inject₂)) ⟩ 
          h ∘ extend (now ∘ π₁)                                              ∎

    -- proposition 6.5
    bisimilarityCoeq : ∀ {X} → IsCoequalizer {A = D₀ (X + ((X × N) + (X × N)))} {B = D₀ X} {E = Ď₀ X} (extend ([ now , [ ι ∘ (id ×₁ s) , now ∘ π₁ ] ])) (extend ([ now , [ (now ∘ π₁) , (ι ∘ (id ×₁ s)) ] ])) ρ
    bisimilarityCoeq {X} .equality = equality₁ ○ sym equality₂
      where
      equality₁ : ρ ∘ extend ([ now , [ ι ∘ (id ×₁ s) , now ∘ π₁ ] ]) ≈ ρ ∘ extend ([ now , [ now ∘ π₁ , now ∘ π₁ ] ])
      equality₁ = begin 
        ρ ∘ extend ([ now , [ ι ∘ (id ×₁ s) , now ∘ π₁ ] ])                                                                      ≈˘⟨ (refl⟩∘⟨ (extend-≈ ([]-cong₂ ι-zero ([]-cong₂ refl (pullˡ ι-zero))))) ⟩ 
        ρ ∘ extend ([ ι ∘ ⟨ id , z ∘ ! ⟩ , [ ι ∘ (id ×₁ s) , ι ∘ ⟨ id , z ∘ ! ⟩ ∘ π₁ ] ])                                        ≈˘⟨ (refl⟩∘⟨ (extend-≈ ([]-cong₂ (pullˡ DK.identityʳ) ([]-cong₂ (pullˡ DK.identityʳ) (pullˡ DK.identityʳ))))) ⟩ 
        ρ ∘ extend ([ extend ι ∘ now ∘ ⟨ id , z ∘ ! ⟩ , [ extend ι ∘ now ∘ (id ×₁ s) , extend ι ∘ now ∘ ⟨ id , z ∘ ! ⟩ ∘ π₁ ] ]) ≈˘⟨ (refl⟩∘⟨ (extend-≈ (∘[] ○ []-cong₂ refl ∘[]))) ⟩ 
        ρ ∘ extend (extend ι ∘ [ now ∘ ⟨ id , z ∘ ! ⟩ , [ now ∘ (id ×₁ s) , now ∘ ⟨ id , z ∘ ! ⟩ ∘ π₁ ] ])                       ≈⟨ refl⟩∘⟨ DK.assoc ⟩ 
        ρ ∘ extend ι ∘ extend ([ now ∘ ⟨ id , z ∘ ! ⟩ , [ now ∘ (id ×₁ s) , now ∘ ⟨ id , z ∘ ! ⟩ ∘ π₁ ] ])                       ≈⟨ extendʳ (Coequalizer.equality (coeqs X)) ⟩ 
        ρ ∘ D₁ π₁ ∘ extend ([ now ∘ ⟨ id , z ∘ ! ⟩ , [ now ∘ (id ×₁ s) , now ∘ ⟨ id , z ∘ ! ⟩ ∘ π₁ ] ])                          ≈⟨ refl⟩∘⟨ F₁∘extend' kleisli π₁ _ ⟩ 
        ρ ∘ extend (D₁ π₁ ∘ [ now ∘ ⟨ id , z ∘ ! ⟩ , [ now ∘ (id ×₁ s) , now ∘ ⟨ id , z ∘ ! ⟩ ∘ π₁ ] ])                          ≈⟨ (refl⟩∘⟨ extend-≈ (∘[] ○ []-cong₂ refl ∘[])) ⟩ 
        ρ ∘ extend ([ D₁ π₁ ∘ now ∘ ⟨ id , z ∘ ! ⟩ , [ D₁ π₁ ∘ now ∘ (id ×₁ s) , D₁ π₁ ∘ now ∘ ⟨ id , z ∘ ! ⟩ ∘ π₁ ] ])          ≈⟨ (refl⟩∘⟨ extend-≈ ([]-cong₂ (extendʳ (sym (D.η.commute π₁))) ([]-cong₂ (extendʳ (sym (D.η.commute π₁))) (extendʳ (sym (D.η.commute π₁)))))) ⟩ 
        ρ ∘ extend ([ now ∘ π₁ ∘ ⟨ id , z ∘ ! ⟩ , [ now ∘ π₁ ∘ (id ×₁ s) , now ∘ π₁ ∘ ⟨ id , z ∘ ! ⟩ ∘ π₁ ] ])                   ≈⟨ (refl⟩∘⟨ (extend-≈ ([]-cong₂ (elimʳ project₁) ([]-cong₂ (refl⟩∘⟨ (project₁ ○ identityˡ)) (refl⟩∘⟨ (cancelˡ project₁)))))) ⟩ 
        ρ ∘ extend ([ now , [ now ∘ π₁ , now ∘ π₁ ] ])                                                                           ∎
      equality₂ : ρ ∘ extend ([ now , [ (now ∘ π₁) , (ι ∘ (id ×₁ s)) ] ]) ≈ ρ ∘ extend ([ now , [ now ∘ π₁ , now ∘ π₁ ] ])
      equality₂ = begin 
        ρ ∘ extend ([ now , [ (now ∘ π₁) , (ι ∘ (id ×₁ s)) ] ])                                                                      ≈˘⟨ (refl⟩∘⟨ (extend-≈ ([]-cong₂ ι-zero ([]-cong₂ (pullˡ ι-zero) refl)))) ⟩ 
        ρ ∘ extend ([ ι ∘ ⟨ id , z ∘ ! ⟩ , [ ι ∘ ⟨ id , z ∘ ! ⟩ ∘ π₁ , ι ∘ (id ×₁ s) ] ])                                            ≈˘⟨ (refl⟩∘⟨ (extend-≈ ([]-cong₂ (pullˡ DK.identityʳ) ([]-cong₂ (pullˡ DK.identityʳ) (pullˡ DK.identityʳ))))) ⟩ 
        ρ ∘ extend ([ extend ι ∘ (now ∘ ⟨ id , z ∘ ! ⟩) , [ extend ι ∘ (now ∘ ⟨ id , z ∘ ! ⟩ ∘ π₁) , extend ι ∘ now ∘ (id ×₁ s) ] ]) ≈˘⟨ (refl⟩∘⟨ (extend-≈ ([]-cong₂ refl ∘[]))) ⟩ 
        ρ ∘ extend ([ extend ι ∘ (now ∘ ⟨ id , z ∘ ! ⟩) , extend ι ∘ [ (now ∘ ⟨ id , z ∘ ! ⟩ ∘ π₁) , now ∘ (id ×₁ s) ] ])            ≈˘⟨ (refl⟩∘⟨ (extend-≈ ∘[])) ⟩ 
        ρ ∘ extend (extend ι ∘ [ now ∘ ⟨ id , z ∘ ! ⟩ , [ (now ∘ ⟨ id , z ∘ ! ⟩ ∘ π₁) , now ∘ (id ×₁ s) ] ])                         ≈⟨ refl⟩∘⟨ DK.assoc ⟩ 
        ρ ∘ extend ι ∘ extend ([ now ∘ ⟨ id , z ∘ ! ⟩ , [ (now ∘ ⟨ id , z ∘ ! ⟩ ∘ π₁) , now ∘ (id ×₁ s) ] ])                         ≈⟨ extendʳ (Coequalizer.equality (coeqs X)) ⟩ 
        ρ ∘ D₁ π₁ ∘ extend ([ now ∘ ⟨ id , z ∘ ! ⟩ , [ (now ∘ ⟨ id , z ∘ ! ⟩ ∘ π₁) , now ∘ (id ×₁ s) ] ])                            ≈⟨ (refl⟩∘⟨ F₁∘extend' kleisli π₁ _) ⟩ 
        ρ ∘ extend (D₁ π₁ ∘ [ now ∘ ⟨ id , z ∘ ! ⟩ , [ (now ∘ ⟨ id , z ∘ ! ⟩ ∘ π₁) , now ∘ (id ×₁ s) ] ])                            ≈⟨ (refl⟩∘⟨ (extend-≈ ∘[])) ⟩ 
        ρ ∘ extend ([ D₁ π₁ ∘ (now ∘ ⟨ id , z ∘ ! ⟩) , D₁ π₁ ∘ [ (now ∘ ⟨ id , z ∘ ! ⟩ ∘ π₁) , now ∘ (id ×₁ s) ] ])                  ≈⟨ (refl⟩∘⟨ (extend-≈ ([]-cong₂ refl ∘[]))) ⟩ 
        ρ ∘ extend ([ D₁ π₁ ∘ (now ∘ ⟨ id , z ∘ ! ⟩) , [ D₁ π₁ ∘ (now ∘ ⟨ id , z ∘ ! ⟩ ∘ π₁) , D₁ π₁ ∘ (now ∘ (id ×₁ s)) ] ])        ≈⟨ (refl⟩∘⟨ (extend-≈ ([]-cong₂ (pullˡ (sym (D.η.commute π₁))) ([]-cong₂ (pullˡ (sym (D.η.commute π₁))) (pullˡ (sym (D.η.commute π₁))))))) ⟩ 
        ρ ∘ extend ([ (now ∘ π₁) ∘ ⟨ id , z ∘ ! ⟩ , [ (now ∘ π₁) ∘ (⟨ id , z ∘ ! ⟩ ∘ π₁) , (now ∘ π₁) ∘ (id ×₁ s) ] ])               ≈⟨ (refl⟩∘⟨ (extend-≈ ([]-cong₂ (cancelʳ project₁) ([]-cong₂ (pullʳ (cancelˡ project₁)) (pullʳ (project₁ ○ identityˡ)))))) ⟩ 
        ρ ∘ extend ([ now , [ now ∘ π₁ , now ∘ π₁ ] ])                                                                               ∎
    bisimilarityCoeq {X} .coequalize {Y} {h} eq = coequalize (isCoequalizer (coeqs X)) {Y} {h} (bisim-implies h eq)
    bisimilarityCoeq {X} .universal {Y} {h} {h∘f≈h∘g} = universal (isCoequalizer (coeqs X))
    bisimilarityCoeq {X} .unique = unique (isCoequalizer (coeqs X))

    ρ+1-coeq : ∀ X → Coequalizer (extend (ι {X}) +₁ id {⊤}) (D₁ π₁ +₁ id {⊤})
    ρ+1-coeq X = record
      { arr = ρ +₁ id
      ; isCoequalizer = record
        { equality = +₁∘+₁ ○ +₁-cong₂ Q.equality refl ○ sym +₁∘+₁
        ; coequalize = coequalize'
        ; universal = universal′
        ; unique = coequalize'-unique
        }
      }
      where
        module Q = Coequalizer (coeqs X)

        left-equality : ∀ {Z} {h : D₀ X + ⊤ ⇒ Z} →
          h ∘ (extend ι +₁ id) ≈ h ∘ (D₁ π₁ +₁ id) →
          (h ∘ i₁) ∘ extend ι ≈ (h ∘ i₁) ∘ D₁ π₁
        left-equality {h = h} eq = begin
          (h ∘ i₁) ∘ extend ι         ≈⟨ assoc ⟩
          h ∘ i₁ ∘ extend ι           ≈˘⟨ refl⟩∘⟨ +₁∘i₁ ⟩
          h ∘ (extend ι +₁ id) ∘ i₁   ≈˘⟨ assoc ⟩
          (h ∘ (extend ι +₁ id)) ∘ i₁ ≈⟨ eq ⟩∘⟨refl ⟩
          (h ∘ (D₁ π₁ +₁ id)) ∘ i₁    ≈⟨ assoc ⟩
          h ∘ (D₁ π₁ +₁ id) ∘ i₁      ≈⟨ refl⟩∘⟨ +₁∘i₁ ⟩
          h ∘ i₁ ∘ D₁ π₁              ≈˘⟨ assoc ⟩
          (h ∘ i₁) ∘ D₁ π₁            ∎

        coequalize' : ∀ {Z} {h : D₀ X + ⊤ ⇒ Z} →
          h ∘ (extend ι +₁ id) ≈ h ∘ (D₁ π₁ +₁ id) →
          Ď₀ X + ⊤ ⇒ Z
        coequalize' {h = h} eq = [ Q.coequalize (left-equality eq) , h ∘ i₂ ]

        universal′ : ∀ {Z} {h : D₀ X + ⊤ ⇒ Z}
          {eq : h ∘ (extend ι +₁ id) ≈ h ∘ (D₁ π₁ +₁ id)} →
          h ≈ coequalize' eq ∘ (ρ +₁ id)
        universal′ = sym +-g-η ○ []-cong₂ Q.universal (sym identityʳ) ○ sym []∘+₁

        coequalize'-unique : ∀ {Z} {h : D₀ X + ⊤ ⇒ Z} {i : Ď₀ X + ⊤ ⇒ Z}
          {eq : h ∘ (extend ι +₁ id) ≈ h ∘ (D₁ π₁ +₁ id)} →
          h ≈ i ∘ (ρ +₁ id) → i ≈ coequalize' eq
        coequalize'-unique {h = h} {i} {eq} factors = sym ([]-unique left right)
          where
            left : i ∘ i₁ ≈ Q.coequalize (left-equality eq)
            left = Q.unique ((factors ⟩∘⟨refl) ○ assoc ○ (refl⟩∘⟨ +₁∘i₁) ○ sym-assoc)

            right : i ∘ i₂ ≈ h ∘ i₂
            right = sym ((factors ⟩∘⟨refl) ○ assoc ○ (refl⟩∘⟨ +₁∘i₂) ○ (refl⟩∘⟨ identityʳ))

    Ď-Functor : Endofunctor C
    Ď-Functor = record
      { F₀ = Ď₀
      ; F₁ = F₁'
      ; identity = λ {X} → Coequalizer.coequalize-resp-≈ (coeqs X) (elimʳ D.F.identity) ○ sym (Coequalizer.id-coequalize (coeqs X))
      ; homomorphism = λ {X} {Y} {Z} {f} {g} → sym (Coequalizer.unique (coeqs X) (sym (begin 
        (F₁' g ∘ F₁' f) ∘ ρ ≈⟨ pullʳ (sym (Coequalizer.universal (coeqs X))) ⟩ 
        F₁' g ∘ ρ ∘ D₁ f    ≈⟨ pullˡ (sym (Coequalizer.universal (coeqs Y))) ⟩
        (ρ ∘ D₁ g) ∘ D₁ f   ≈⟨ pullʳ (sym D.F.homomorphism) ⟩
        ρ ∘ D₁ (g ∘ f)      ∎)))
      ; F-resp-≈ = λ {X} {Y} {f} {g} eq → Coequalizer.coequalize-resp-≈ (coeqs X) (refl⟩∘⟨ (D.F.F-resp-≈ eq))
      }
      where
        F₁' : ∀ {X} {Y} (f : X ⇒ Y) → Ď₀ X ⇒ Ď₀ Y
        F₁' {X} {Y} f = Coequalizer.coequalize (coeqs X) {h = ρ ∘ D₁ f} (begin 
          (ρ ∘ D₁ f) ∘ extend ι                   ≈⟨ pullʳ (sym DK.assoc) ⟩ 
          ρ ∘ extend (D₁ f ∘ ι)                   ≈˘⟨ (refl⟩∘⟨ (DK.extend-≈ (ι-natural f))) ⟩
          ρ ∘ extend (ι ∘ (f ×₁ id))              ≈⟨ (refl⟩∘⟨ extend-≈ (pushˡ (sym DK.identityʳ))) ⟩
          ρ ∘ extend (extend ι ∘ now ∘ (f ×₁ id)) ≈⟨ pushʳ DK.assoc ⟩
          (ρ ∘ extend ι) ∘ D₁ (f ×₁ id)           ≈⟨ pushˡ (Coequalizer.equality (coeqs Y)) ⟩
          ρ ∘ D₁ π₁ ∘ D₁ (f ×₁ id)                ≈⟨ refl⟩∘⟨ sym D.F.homomorphism ⟩
          ρ ∘ D₁ (π₁ ∘ (f ×₁ id))                 ≈⟨ (refl⟩∘⟨ (D.F.F-resp-≈ project₁)) ⟩
          ρ ∘ D₁ (f ∘ π₁)                         ≈⟨ pushʳ D.F.homomorphism ⟩
          (ρ ∘ D₁ f) ∘ D₁ π₁                      ∎)

    ρ-natural : NaturalTransformation D.F Ď-Functor
    ρ-natural = ntHelper (record 
      { η = λ X → ρ {X} 
      ; commute = λ {X} {Y} f → Coequalizer.universal (coeqs X)
      })