{-# OPTIONS --allow-unsolved-metas #-}

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 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

-- Lemmas concerning the zip function.
module Monad.Instance.Delay.Zip {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 Bundles
  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
  open D-Strong
  -- open Later∘Extend
  -- open import Algebra.Search cocartesian D
  open Terminal terminal using (! ; ⊤; !-unique)

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

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

  zip⁻¹ : ∀ {X Y} → D₀ (X × Y + (X × D₀ Y + D₀ X × Y)) ⇒ D₀ X × D₀ Y 
  zip⁻¹ = ⟨ zip₁⁻¹ , zip₂⁻¹ ⟩

  zip : ∀ {X Y} → D₀ X × D₀ Y ⇒ D₀ (X × Y + (X × D₀ Y + D₀ X × Y))
  zip =  Coit.coit (distr ∘ (out ⁂ out ))

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

  fst-eq : ∀ {X Y} → (f# : D₀ X × D₀ Y ⇒ D₀ X) → (out ∘ f# ≈ (π₁ +₁ [ π₁ , f# ] ∘ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ (out ⁂ out)) →  f# ≈ π₁
  fst-eq {X}{Y} f# eq = guarded-unique (out⁻¹ ∘ (i₁  +₁ id) ∘ f) f# π₁ (record { guard = f ; guard-eq = trans (introˡ out∘out⁻¹) assoc}) (fp-helper f# eq) fp  
    where
      f =  (π₁  +₁ [ (D₁ i₁) ∘ π₁ , now ∘ i₂ ] ∘ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ (out ⁂ out)

      fp-helper : (g : D₀ X × D₀ Y ⇒ D₀ X)
        → (out ∘ g ≈ (π₁ +₁ [ π₁ , g ] ∘ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ (out ⁂ out))
        → g ≈ extend [ now , g ] ∘ (out⁻¹ ∘ (i₁ +₁ id) ∘ f)
      fp-helper g eq = out-mono g (extend [ now , g ] ∘ out⁻¹ ∘ (i₁ +₁ id) ∘ f)
            (begin
              out ∘ g
                ≈⟨ eq ⟩
              [ i₁ ∘ π₁ , i₂ ∘ [ π₁ , g ] ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ out)
                ≈˘⟨ []-cong₂ refl (∘-resp-≈ʳ (∘-resp-≈ˡ ([]-cong₂ (elimˡ (extend-≈ inject₁ ○ DK.identityˡ)) inject₂))) ⟩∘⟨refl ⟩ 
              [ i₁ ∘ π₁ , i₂ ∘ [ extend ([ now , g ] ∘ i₁) ∘ π₁ , [ now , g ] ∘ i₂ ] ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ out)
                ≈˘⟨ []-cong₂ refl (∘-resp-≈ʳ (∘-resp-≈ˡ ([]-cong₂ (pullˡ (extend∘F₁' kleisli [ now , g ] i₁)) (pullˡ DK.identityʳ)))) ⟩∘⟨refl ⟩
              [ i₁ ∘ π₁ , i₂ ∘ [ extend [ now , g ] ∘ (D₁ i₁) ∘ π₁ , extend [ now , g ] ∘ now ∘ i₂ ] ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ out)
                ≈˘⟨ []-cong₂ refl (pullʳ (pullˡ ∘[]))  ⟩∘⟨refl ⟩
              [ i₁ ∘ π₁ , (i₂ ∘ extend [ now , g ]) ∘ [ (D₁ i₁) ∘ π₁ , now ∘ i₂ ] ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ out)
                ≈˘⟨ pullˡ []∘+₁ ⟩
              [ i₁ , i₂ ∘ extend [ now , g ] ] ∘ f
                ≈˘⟨ []-cong₂ unitlaw refl ⟩∘⟨refl ⟩ 
              [ out ∘ now , i₂ ∘ extend [ now , g ] ] ∘ f
                ≈˘⟨ []-cong₂ (pullʳ inject₁) identityʳ ⟩∘⟨refl ⟩ 
              [ (out ∘ [ now , g ]) ∘ i₁ , (i₂ ∘ extend [ now , g ]) ∘ id ] ∘ f
                ≈˘⟨ pullˡ []∘+₁ ⟩
              [ out ∘ [ now , g ] , i₂ ∘ extend [ now , g ] ] ∘ (i₁ +₁ id) ∘ f
                ≈˘⟨ pullˡ (cancelʳ out∘out⁻¹) ⟩
              ([ out ∘ [ now , g ] , i₂ ∘ extend [ now , g ] ] ∘ out) ∘ out⁻¹ ∘ (i₁ +₁ id) ∘ f
                ≈˘⟨ pullˡ (extend-commutes [ now , g ]) ⟩
              out ∘ extend [ now , g ] ∘ out⁻¹ ∘ (i₁ +₁ id) ∘ f
            ∎)

      fp = fp-helper π₁  
            (begin
              out ∘ π₁                                                               ≈⟨  sym project₁ ⟩
              π₁ ∘ (out ⁂ out)                                                      ≈˘⟨ pullˡ distributeʳ⁻¹-π₁ ⟩ 
              (π₁ +₁ π₁) ∘ distributeʳ⁻¹ ∘ (out ⁂ out)                              ≈⟨  +₁-cong₂ refl (sym distributeˡ⁻¹-π₁)  ⟩∘⟨refl ⟩ 
              (π₁ +₁ [ π₁ , π₁ ] ∘ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ (out ⁂ out) 
            ∎)

  snd-eq : ∀ {X Y} → (f# : D₀ X × D₀ Y ⇒ D₀ Y) → (out ∘ f# ≈ [ π₂  , (π₂ +₁ f#) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ out)) → f# ≈ π₂
  snd-eq {X}{Y} f# eq = guarded-unique (out⁻¹ ∘ (i₁ +₁ id) ∘ f) f# π₂ (record { guard = f ; guard-eq = trans (sym (elimˡ out∘out⁻¹)) assoc}) (fp-helper f# eq) fp
    where
      f = [ (id +₁ D₁ i₁) ∘ π₂ , (π₂ +₁ now ∘ i₂) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ out)

      fp-helper : (g : D₀ X × D₀ Y ⇒ D₀ Y)
        → (out ∘ g ≈ [ π₂  , (π₂ +₁ g) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ out))
        → g ≈ extend [ now , g ] ∘ out⁻¹ ∘ (i₁ +₁ id) ∘ f 
      fp-helper g eq = out-mono g (extend [ now , g ] ∘ out⁻¹ ∘ (i₁ +₁ id) ∘ f)
              (begin
              out ∘ g
                ≈⟨ eq ⟩
              [ π₂ , (π₂ +₁ g) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ out)  
                ≈˘⟨ []-cong₂ (elimˡ ([]-cong₂ identityʳ (elimʳ (extend∘F₁' kleisli [ now , g ] i₁ ○ extend-≈ inject₁ ○ DK.identityˡ)) ○ +-η)) refl ⟩∘⟨refl ⟩
              [ (id +₁ extend [ now , g ] ∘ D₁ i₁) ∘ π₂ , (π₂ +₁ g) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ out)  
                ≈˘⟨ []-cong₂ refl (∘-resp-≈ˡ (+₁-cong₂ identityˡ (pullˡ DK.identityʳ ○ inject₂))) ⟩∘⟨refl ⟩
              [ (id +₁ (extend [ now , g ]) ∘ D₁ i₁) ∘ π₂ , (id ∘ π₂ +₁ extend [ now , g ] ∘ now ∘ i₂) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ out)  
                ≈˘⟨ pullˡ (∘[] ○ []-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ refl)) (pullˡ +₁∘+₁)) ⟩ 
              (id +₁ extend [ now , g ]) ∘ f
                ≈˘⟨ []-cong₂ (trans unitlaw (sym identityʳ)) refl ⟩∘⟨refl ⟩ 
              [ out ∘ now , i₂ ∘ extend [ now , g ] ] ∘ f
                ≈˘⟨ []-cong₂ (pullʳ inject₁) identityʳ ⟩∘⟨refl ⟩ 
              [ (out ∘ [ now , g ]) ∘ i₁ , (i₂ ∘ extend [ now , g ]) ∘ id ] ∘ f
                ≈˘⟨ pullˡ []∘+₁ ⟩
              [ out ∘ [ now , g ] , i₂ ∘ extend [ now , g ] ] ∘ (i₁ +₁ id) ∘ f
                ≈˘⟨ pullˡ (cancelʳ out∘out⁻¹) ⟩
              ([ out ∘ [ now , g ] , i₂ ∘ extend [ now , g ] ] ∘ out) ∘ out⁻¹ ∘ (i₁ +₁ id) ∘ f  
                ≈˘⟨ pullˡ (extend-commutes [ now , g ]) ⟩
              out ∘ extend [ now , g ] ∘ out⁻¹ ∘ (i₁ +₁ id) ∘ f
            ∎)

      fp = fp-helper π₂  
            (begin
              out ∘ π₂                                                              ≈⟨  sym project₂ ⟩
              π₂ ∘ (out ⁂ out)                                                      ≈˘⟨ pullˡ distributeʳ⁻¹-π₂ ⟩  
              [ π₂ , π₂ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ out)                             ≈⟨ []-cong₂ refl (sym distributeˡ⁻¹-π₂)  ⟩∘⟨refl ⟩ 
              [ π₂ , (π₂ +₁ π₂) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ out)  
            ∎)

  zip⁻¹∘zip : ∀ {X Y} → zip⁻¹ {X}{Y} ∘ zip {X}{Y} ≈ id
  zip⁻¹∘zip = ⟨⟩-unique′
    (trans (fst-eq (π₁ ∘ zip⁻¹ ∘ zip) zip⁻¹∘zip-rec₁) (sym identityʳ))
    (trans (snd-eq (π₂ ∘ zip⁻¹ ∘ zip) zip⁻¹∘zip-rec₂) (sym identityʳ)) 
    where
      zip⁻¹∘zip-rec₁ : out ∘ π₁ ∘ zip⁻¹ ∘ zip ≈ (π₁ +₁ [ π₁ , π₁ ∘ zip⁻¹ ∘ zip ] ∘ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ (out ⁂ out)
      zip⁻¹∘zip-rec₁ =
        begin
        out ∘ π₁ ∘ zip⁻¹ ∘ zip
          ≈⟨ refl⟩∘⟨ pullˡ project₁ ⟩
        out ∘ zip₁⁻¹ ∘ zip
          ≈⟨ pullˡ (extend-commutes [ now ∘ π₁ , out⁻¹ ∘ (π₁ +₁ π₁) ]) ⟩
        ([ out ∘ [ now ∘ π₁ , out⁻¹ ∘ (π₁ +₁ π₁) ] , i₂ ∘ zip₁⁻¹ ] ∘ out) ∘ zip
          ≈⟨ []-cong₂ (∘[] ○ []-cong₂ (pullˡ unitlaw) (cancelˡ out∘out⁻¹)) refl ⟩∘⟨refl ⟩∘⟨refl ⟩
        ([ [ i₁ ∘ π₁ , π₁ +₁ π₁ ] , i₂ ∘ zip₁⁻¹ ] ∘ out) ∘ zip
          ≈⟨ pullʳ (Coit.coit-commutes (distr ∘ (out ⁂ out))) ⟩
        [ [ i₁ ∘ π₁ , π₁ +₁ π₁ ] , i₂ ∘ zip₁⁻¹ ] ∘ (id +₁ zip) ∘ distr ∘ (out ⁂ out)
          ≈⟨ pullˡ ([]∘+₁ ○ []-cong₂ identityʳ refl) ⟩ 
        [ [ i₁ ∘ π₁ , π₁ +₁ π₁ ] , (i₂ ∘ zip₁⁻¹) ∘ zip ] ∘ distr ∘ (out ⁂ out)
          ≈⟨ pullˡ (pullˡ (∘[] ○ []-cong₂ (pullˡ inject₁) (pullˡ ([]∘+₁ ○ []-cong₂ (pullˡ inject₂ ○ inject₂) identityʳ )))) ⟩ 
        ([ [ i₁ ∘ π₁ , π₁ +₁ π₁ ] ∘ (id +₁ i₁) ∘ distributeˡ⁻¹ , [ i₂ ∘ π₁ , (i₂ ∘ zip₁⁻¹) ∘ zip ] ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹) ∘ (out ⁂ out)
          ≈⟨ []-cong₂ (pullˡ ([]∘+₁ ○ []-cong₂ identityʳ inject₁)) refl ⟩∘⟨refl ⟩∘⟨refl ⟩
        ([ [ i₁ ∘ π₁ ,  i₁ ∘ π₁ ] ∘ distributeˡ⁻¹ , [ i₂ ∘ π₁ , (i₂ ∘ zip₁⁻¹) ∘ zip ] ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹) ∘ (out ⁂ out)
          ≈⟨ []-cong₂ ((∘-resp-≈ˡ (sym ∘[])) ○ pullʳ distributeˡ⁻¹-π₁) (∘-resp-≈ˡ ([]-cong₂ refl assoc ○ sym ∘[])) ⟩∘⟨refl ⟩∘⟨refl ⟩
        ([ i₁ ∘ π₁ , (i₂ ∘ [ π₁ , zip₁⁻¹ ∘ zip ]) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹) ∘ (out ⁂ out) 
          ≈⟨ []-cong₂ refl (pullʳ (∘-resp-≈ˡ ([]-cong₂ refl (pushˡ (sym project₁))))) ⟩∘⟨refl ⟩∘⟨refl ⟩
        ((π₁ +₁ [ π₁ , π₁ ∘ zip⁻¹ ∘ zip ] ∘ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ (out ⁂ out)
          ≈⟨ assoc ⟩
        (π₁ +₁ [ π₁ , π₁ ∘ zip⁻¹ ∘ zip ] ∘ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ (out ⁂ out)
        ∎
        
      zip⁻¹∘zip-rec₂ : out ∘ π₂ ∘ zip⁻¹ ∘ zip ≈ [ π₂ , (π₂ +₁ π₂ ∘ zip⁻¹ ∘ zip) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ out)
      zip⁻¹∘zip-rec₂ = 
        begin
        out ∘ π₂ ∘ zip⁻¹ ∘ zip
          ≈⟨ refl⟩∘⟨ pullˡ project₂ ⟩
        out ∘ zip₂⁻¹ ∘ zip
          ≈⟨ pullˡ (extend-commutes [ now ∘ π₂ , out⁻¹ ∘ [ i₂ ∘ π₂ , i₁ ∘ π₂ ] ])  ⟩
        ([ out ∘ [ now ∘ π₂ , out⁻¹ ∘ [ i₂ ∘ π₂ , i₁ ∘ π₂ ] ] , i₂ ∘ zip₂⁻¹ ] ∘ out) ∘ zip
          ≈⟨ []-cong₂ (∘[] ○ []-cong₂ (pullˡ unitlaw) (cancelˡ out∘out⁻¹)) refl  ⟩∘⟨refl ⟩∘⟨refl ⟩
        ([ [ i₁ ∘ π₂ , [ i₂ ∘ π₂ , i₁ ∘ π₂ ] ] , i₂ ∘ zip₂⁻¹ ] ∘ out) ∘ zip
          ≈⟨ pullʳ (Coit.coit-commutes (distr ∘ (out ⁂ out))) ⟩
        [ [ i₁ ∘ π₂ , [ i₂ ∘ π₂ , i₁ ∘ π₂ ] ] , i₂ ∘ zip₂⁻¹ ] ∘ (id +₁ zip) ∘ distr ∘ (out ⁂ out)
          ≈⟨ pullˡ ([]∘+₁ ○ []-cong₂ identityʳ refl) ⟩
        [ [ i₁ ∘ π₂ , [ i₂ ∘ π₂ , i₁ ∘ π₂ ] ] , (i₂ ∘ zip₂⁻¹) ∘ zip ] ∘ distr ∘ (out ⁂ out)
          ≈⟨ pullˡ (pullˡ (∘[] ○ []-cong₂ (pullˡ inject₁) (pullˡ ([]∘+₁ ○ []-cong₂ (pullˡ inject₂ ○ inject₂) identityʳ )))) ⟩
        ([ [ i₁ ∘ π₂ , [ i₂ ∘ π₂ , i₁ ∘ π₂ ] ] ∘ (id +₁ i₁) ∘ distributeˡ⁻¹ , [ i₁ ∘ π₂ , (i₂ ∘ zip₂⁻¹) ∘ zip ] ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹) ∘ (out ⁂ out)
          ≈⟨ assoc ⟩
        [ [ i₁ ∘ π₂ , [ i₂ ∘ π₂ , i₁ ∘ π₂ ] ] ∘ (id +₁ i₁) ∘ distributeˡ⁻¹ , [ i₁ ∘ π₂  , (i₂ ∘ zip₂⁻¹) ∘ zip ] ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ out)
          ≈⟨ []-cong₂ (pullˡ ([]∘+₁ ○ []-cong₂ identityʳ inject₁)) refl  ⟩∘⟨refl ⟩
        [ [ i₁ ∘ π₂ , i₂ ∘ π₂ ] ∘ distributeˡ⁻¹ , [ i₁ ∘ π₂  , (i₂ ∘ zip₂⁻¹) ∘ zip ] ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ out)
          ≈⟨ []-cong₂ ((∘-resp-≈ˡ (sym identityˡ)) ○ pullʳ distributeˡ⁻¹-π₂ ○ identityˡ) refl ⟩∘⟨refl ⟩
        [ π₂  , [ i₁ ∘ π₂  , (i₂ ∘ zip₂⁻¹) ∘ zip ] ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ out)
          ≈˘⟨ []-cong₂ refl (∘-resp-≈ˡ ([]-cong₂ refl (pushʳ (pullˡ project₂)))) ⟩∘⟨refl ⟩
        [ π₂ , (π₂ +₁ π₂ ∘ zip⁻¹ ∘ zip) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (out ⁂ out)
        ∎ 

  
  zip∘zip⁻¹ : ∀ {X Y} → zip{X}{Y} ∘ zip⁻¹{X}{Y} ≈ id
  zip∘zip⁻¹ = trans (sym (Coit.coit-unique out (zip ∘ zip⁻¹) zip∘zip⁻¹-rec)) Coit.coit-refl
    where
      zip∘zip⁻¹-rec =
        begin
          out ∘ zip ∘ zip⁻¹
            ≈⟨ pullˡ (Coit.coit-commutes (distr ∘ (out ⁂ out))) ⟩ 
          ((id +₁ zip) ∘ distr ∘ (out ⁂ out)) ∘ zip⁻¹
            ≈⟨ pullʳ (pullʳ ⁂∘⟨⟩) ⟩   
          (id +₁ zip) ∘ distr ∘ ⟨ out ∘ zip₁⁻¹ , out ∘ zip₂⁻¹ ⟩
            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ (extend-commutes _) (extend-commutes _) ⟩
          (id +₁ zip) ∘ distr ∘ ⟨ [ out ∘ [ now ∘ π₁ , out⁻¹ ∘ (π₁ +₁ π₁) ] , i₂ ∘ zip₁⁻¹ ] ∘ out ,  [ out ∘ [ now ∘ π₂ , out⁻¹ ∘ [ i₂ ∘ π₂ , i₁ ∘ π₂ ] ] , i₂ ∘ zip₂⁻¹ ] ∘ out  ⟩
            ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩∘ ⟩
          (id +₁ zip) ∘ distr ∘ ⟨ [ out ∘ [ now ∘ π₁ , out⁻¹ ∘ (π₁ +₁ π₁) ] , i₂ ∘ zip₁⁻¹ ] ,  [ out ∘ [ now ∘ π₂ , out⁻¹ ∘ [ i₂ ∘ π₂ , i₁ ∘ π₂ ] ] , i₂ ∘ zip₂⁻¹ ] ⟩ ∘ out
            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ ([]-cong₂ (∘[] ○ []-cong₂ (pullˡ (cancelˡ out∘out⁻¹)) (cancelˡ out∘out⁻¹)) refl) (([]-cong₂ (∘[] ○ []-cong₂ (pullˡ (cancelˡ out∘out⁻¹)) (cancelˡ out∘out⁻¹)) refl)) ⟩∘⟨refl ⟩
          (id +₁ zip) ∘ distr ∘ ⟨ [ [ i₁ ∘ π₁ , π₁ +₁ π₁ ] , i₂ ∘ zip₁⁻¹ ] ,  [ [ i₁ ∘ π₂ , [ i₂ ∘ π₂ , i₁ ∘ π₂ ] ] , i₂ ∘ zip₂⁻¹ ] ⟩ ∘ out
            ≈˘⟨ refl⟩∘⟨ pushˡ ([]-unique (trans zip∘zip⁻¹-rec' (sym identityʳ)) (pullʳ ⟨⟩∘ ○ ∘-resp-≈ʳ (⟨⟩-cong₂ inject₂ inject₂) ○  pushʳ (sym ⁂∘⟨⟩) ○ ∘-resp-≈ˡ distr-i₂+i₂)) ⟩
          (id +₁ zip) ∘ (id +₁ zip⁻¹) ∘ out
            ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ refl) ⟩
          (id +₁ zip ∘ zip⁻¹) ∘ out
        ∎
          where
            zip∘zip⁻¹-rec' =
              begin
                (distr ∘ ⟨ [ [ i₁ ∘ π₁ , π₁ +₁ π₁ ] , i₂ ∘ zip₁⁻¹ ] , [ [ i₁ ∘ π₂ , [ i₂ ∘ π₂ , i₁ ∘ π₂ ] ] , i₂ ∘ zip₂⁻¹ ] ⟩) ∘ i₁                ≈⟨ pullʳ ⟨⟩∘ ⟩
                distr ∘ ⟨ [ [ i₁ ∘ π₁ , π₁ +₁ π₁ ] , i₂ ∘ zip₁⁻¹ ] ∘ i₁ , [ [ i₁ ∘ π₂ , [ i₂ ∘ π₂ , i₁ ∘ π₂ ] ] , i₂ ∘ zip₂⁻¹ ] ∘ i₁ ⟩             ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ inject₁ inject₁ ⟩
                distr ∘ ⟨ [ i₁ ∘ π₁ , π₁ +₁ π₁ ] , [ i₁ ∘ π₂ , [ i₂ ∘ π₂ , i₁ ∘ π₂ ] ] ⟩                                                           ≈⟨ distr-helper ⟩ 
                i₁ 
              ∎
  
  zip-iso : ∀ X Y → IsIso (zip {X}{Y})
  zip-iso X Y .Mor.IsIso.inv = zip⁻¹
  zip-iso X Y .Mor.IsIso.iso .Mor.Iso.isoˡ = zip⁻¹∘zip {X = X}{Y = Y}
  zip-iso X Y .Mor.IsIso.iso .Mor.Iso.isoʳ = zip∘zip⁻¹ {X = X}{Y = Y}
      
  μchop : D.μ.η ⊤ ∘ chop ≈ π₁
  μchop = begin
          D.μ.η ⊤ ∘ chop              ≈⟨ pushˡ (extend⇒F₁ kleisli [ now ∘ π₁ , out⁻¹ ∘ (π₁ +₁ π₁) ]) ⟨   
          zip₁⁻¹ ∘ zip                ≈⟨ pullˡ project₁ ⟨ 
          π₁ ∘ zip⁻¹ ∘ zip            ≈⟨ elimʳ zip⁻¹∘zip ⟩ 
          π₁              
    ∎

  chopμD! : chop ∘ ⟨ D.μ.η ⊤ , D₁ ! ⟩ ≈ id
  chopμD! = begin
          chop ∘ ⟨ D.μ.η ⊤ , D₁ ! ⟩
              ≈⟨ refl⟩∘⟨ ⟨⟩-unique (pullˡ project₁ ○ help-eq₁) (pullˡ project₂ ○ help-eq₂) ⟩   
          chop ∘ zip⁻¹ ∘ D₁ (⟨ id , ! ⟩ +₁ i₂ ∘ ⟨ id , ! ⟩) ∘ D₁ out
              ≈⟨ pullˡ (pullʳ zip∘zip⁻¹ ○ identityʳ ) ⟩   
          (D₁ [ now ∘ π₁ , out⁻¹ ∘ (π₁ +₁ π₁) ]) ∘ D₁ (⟨ id , ! ⟩ +₁ i₂ ∘ ⟨ id , ! ⟩) ∘ D₁ out
              ≈⟨ pullˡ (sym D.F.homomorphism) ⟩   
          D₁ ([ now ∘ π₁ , out⁻¹ ∘ (π₁ +₁ π₁) ] ∘ (⟨ id , ! ⟩ +₁ i₂ ∘ ⟨ id , ! ⟩)) ∘ D₁ out
              ≈⟨ D.F.F-resp-≈ ([]∘+₁ ○ []-cong₂ (cancelʳ project₁) (pullˡ (pullʳ inject₂)) ) ⟩∘⟨refl ⟩   
          D₁ [ now ,   (out⁻¹ ∘ i₂ ∘ π₁) ∘ ⟨ id , ! ⟩ ] ∘ D₁ out
              ≈⟨ D.F.F-resp-≈ ([]-cong₂ refl (pullʳ (cancelʳ project₁))) ⟩∘⟨refl ⟩   
          D₁ [ now , later ] ∘ D₁ out
              ≈⟨ sym D.F.homomorphism ○ D.F.F-resp-≈ (∘-resp-≈ˡ (sym out⁻¹-now-later) ○ out⁻¹∘out) ○ D.F.identity ⟩   
          id              
    ∎
      where
        help-eq₁ : zip₁⁻¹ ∘ D₁ (⟨ id , ! ⟩ +₁ i₂ ∘ ⟨ id , ! ⟩) ∘ D₁ out ≈ D.μ.η ⊤  
        help-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 ⟩  
          D.μ.η ⊤  ∎

        help-eq₂ : zip₂⁻¹ ∘ D₁ (⟨ id , ! ⟩ +₁ i₂ ∘ ⟨ id , ! ⟩) ∘ D₁ out ≈ D₁ !
        help-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                                            ≈⟨ D.F.F-resp-≈ (!-unique (coproducts.[ ! , ! ] ∘ out)) ○ D.F.homomorphism ⟨ 
          D₁ !  ∎

  product-retract : ∀ X Y → Retract (D₀ (X × Y)) (D₀ X × D₀ Y)
  product-retract X Y .Mor.Retract.section = ⟨ D₁ π₁ , D₁ π₂ ⟩ 
  product-retract X Y .Mor.Retract.retract = extend [ now , [ τ , σ ] ] ∘ zip
  product-retract X Y .Mor.Retract.is-retract = assoc ○ 
     (begin
            extend [ now , [ τ , σ ] ] ∘ zip ∘ ⟨ D₁ π₁ , D₁ π₂ ⟩
              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ (extend∘F₁' kleisli _ _ ○ extend-≈ inject₁) (extend∘F₁' kleisli _ _ ○ extend-≈ inject₁) ) ⟨
            extend [ now , [ τ , σ ] ] ∘ zip ∘ zip⁻¹ ∘ D₁ i₁
              ≈⟨ refl⟩∘⟨ pullˡ zip∘zip⁻¹ ○ ∘-resp-≈ʳ identityˡ ⟩
            extend [ now , [ τ , σ ] ] ∘ D₁ i₁
              ≈⟨ extend∘F₁' kleisli _ _ ⟩
            extend ([ now , [ τ , σ ] ] ∘ i₁)
              ≈⟨ extend-≈ inject₁ ○  DK.identityˡ ⟩
            id              
     ∎)

  τ-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
    eq₁ : D₁ π₁ ∘ h₁ ≈ D₁ π₁ ∘ τ ∘ h₂
    eq₁ = ∘-resp-≈ˡ (D.F.F-resp-≈ (⟺ (project₁ ○ identityˡ))) ○ pushˡ D.F.homomorphism ○ ∘-resp-≈ʳ eq

    eq₂ : D₁ π₁ ∘ τ ∘ ⟨ π₁ ∘ h₂ , D₁ π₂ ∘ h₁ ⟩ ≈ D₁ π₁ ∘ τ ∘ h₂
    eq₂ = begin
            D₁ π₁ ∘ τ ∘ ⟨ π₁ ∘ h₂ , D₁ π₂ ∘ h₁ ⟩                ≈⟨ refl⟩∘⟨ (∘-resp-≈ʳ (⟨⟩-cong₂ (sym identityˡ) refl) ○ pushʳ (⟺ ⁂∘⟨⟩) ○ pushˡ (τ-natural id π₂)) ⟩
            D₁ π₁ ∘ D₁ (id ⁂ π₂) ∘        τ ∘ ⟨ π₁ ∘ h₂ , h₁ ⟩  ≈⟨ pullˡ (⟺ D.F.homomorphism ○ D.F.F-resp-≈ (project₁ ○ identityˡ)) ⟩
            D₁ π₁ ∘                        τ ∘ ⟨ π₁ ∘ h₂ , h₁ ⟩ ≈⟨ pushˡ (D.F.F-resp-≈ (sym (project₁ ○ identityˡ)) ○ D.F.homomorphism) ⟩
            D₁ π₁ ∘ D₁ (id ⁂ (id ⁂ f)) ∘ τ ∘ ⟨ π₁ ∘ h₂ , h₁ ⟩   ≈⟨ refl⟩∘⟨ ( pushʳ (⟨⟩-cong₂ (sym identityˡ) refl ○ ⟺ ⁂∘⟨⟩) ○ pushˡ (τ-natural id (id ⁂ f))) ⟨
            D₁ π₁ ∘ τ ∘ ⟨ π₁ ∘ h₂ , D₁ (id ⁂ f) ∘ h₁ ⟩          ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ refl eq ⟩
            D₁ π₁ ∘ τ ∘ ⟨ π₁ ∘ h₂ , τ ∘ h₂ ⟩                    ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl) ⟩
            D₁ π₁ ∘ τ ∘ (id ⁂ τ) ∘ ⟨ π₁ ∘ h₂ , h₂ ⟩             ≈⟨ sym-assoc ○ pullˡ (assoc ○ τ-assoc-helper) ○ assoc²βε ⟩
            D₁ π₁ ∘ τ ∘ (id ⁂ π₂) ∘ ⟨ π₁ ∘ h₂ , h₂ ⟩            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl) ⟩
            D₁ π₁ ∘ τ ∘ ⟨ π₁ ∘ h₂ , π₂ ∘ h₂ ⟩                   ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-g-η ⟩
            D₁ π₁ ∘ τ ∘ h₂                                      ∎
      where
      τ-assoc-helper : D₁ π₁ ∘ τ ∘ (id ⁂ τ) ≈ D₁ π₁ ∘ τ ∘ (id ⁂ π₂)
      τ-assoc-helper = begin 
        D₁ π₁ ∘ τ ∘ (id ⁂ τ) ≈˘⟨ pullˡ (sym D.F.homomorphism ○ D.F.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 ⁂ π₂) ∎

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