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

-- 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
  module F = D.F
  open F using (homomorphism; F-resp-≈; identity)
  open D.μ renaming (η to μ)
  open D-Strong

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

  zip-natural : NaturalTransformation (reduce-× -×- D.F D.F) (D.F ∘F overlap-× -+- -×- (overlap-× -+- (reduce-× -×- Id D.F) (reduce-× -×- D.F Id))) 
  zip-natural .NaturalTransformation.η _ = zip
  zip-natural .NaturalTransformation.commute (f , g) = Coit.coit-unique'
    (((f ×₁ g +₁ f ×₁ D₁ g +₁ D₁ f ×₁ g) +₁ id) ∘ distr ∘ (out ×₁ out ))
    (zip ∘ (D₁ f ×₁ D₁ g))
    (D₁(f ×₁ g +₁ f ×₁ D₁ g +₁ D₁ f ×₁ g) ∘ zip)
    (begin
        out ∘ zip ∘ (D₁ f ×₁ D₁ g)
          ≈⟨ pullˡ (Coit.coit-commutes _) ⟩
        ((id +₁ zip) ∘ distr ∘ (out ×₁ out)) ∘ (D₁ f ×₁ D₁ g)
          ≈⟨ pullʳ (pullʳ (×₁∘×₁ ○ ×₁-cong₂ (D₁-commutes _) (D₁-commutes _))) ⟩
        (id +₁ zip) ∘ distr ∘ ((f +₁ D₁ f) ∘ out ×₁ (g +₁ D₁ g) ∘ out)
          ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ×₁∘×₁ ⟨
        (id +₁ zip) ∘ distr ∘ ((f +₁ D₁ f) ×₁ (g +₁ D₁ g)) ∘ (out ×₁ out)
          ≈⟨ refl⟩∘⟨ extendʳ (distr-natural f g (D₁ f) (D₁ g)) ⟩
        (id +₁ zip) ∘ ((f ×₁ g +₁ f ×₁ D₁ g +₁ D₁ f ×₁ g) +₁ D₁ f ×₁ D₁ g) ∘ distr ∘ (out ×₁ out)
          ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ refl) ⟩
        ((f ×₁ g +₁ f ×₁ D₁ g +₁ D₁ f ×₁ g) +₁ zip ∘ (D₁ f ×₁ D₁ g)) ∘ distr ∘ (out ×₁ out)
          ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟨
        (id +₁ zip ∘ (D₁ f ×₁ D₁ g)) ∘ ((f ×₁ g +₁ f ×₁ D₁ g +₁ D₁ f ×₁ g) +₁ id) ∘ distr ∘ (out ×₁ out)
      ∎)
    (begin
      out ∘ D₁ (f ×₁ g +₁ f ×₁ D₁ g +₁ D₁ f ×₁ g) ∘ zip ≈⟨ pullˡ (D₁-commutes _) ⟩
      (((f ×₁ g +₁ f ×₁ D₁ g +₁ D₁ f ×₁ g) +₁ D₁ (f ×₁ g +₁ f ×₁ D₁ g +₁ D₁ f ×₁ g)) ∘ out) ∘ zip                                  ≈⟨ pullʳ (Coit.coit-commutes _) ⟩
      ((f ×₁ g +₁ f ×₁ D₁ g +₁ D₁ f ×₁ g) +₁ D₁ (f ×₁ g +₁ f ×₁ D₁ g +₁ D₁ f ×₁ g)) ∘ (id +₁ zip) ∘ distr ∘ (out ×₁ out)           ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityʳ refl) ⟩
      ((f ×₁ g +₁ f ×₁ D₁ g +₁ D₁ f ×₁ g) +₁ D₁ (f ×₁ g +₁ f ×₁ D₁ g +₁ D₁ f ×₁ g) ∘ zip) ∘ distr ∘ (out ×₁ out)                   ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟨
      (id +₁ D₁ (f ×₁ g +₁ f ×₁ D₁ g +₁ D₁ f ×₁ g) ∘ zip) ∘ ((f ×₁ g +₁ f ×₁ D₁ g +₁ D₁ f ×₁ g) +₁ id) ∘ distr ∘ (out ×₁ out)      ∎)
     
  zip-natural .NaturalTransformation.sym-commute (f , g) = sym (zip-natural .NaturalTransformation.commute (f , g))

  fst-via-# : ∀ {X Y} → (f# : D₀ X × D₀ Y ⇒ D₀ X) → (out ∘ f# ≈ (π₁ +₁ [ π₁ , f# ] ∘ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ (out ×₁ out)) →  f# ≈ π₁
  fst-via-# {X}{Y} f# eq = guarded-unique (out⁻¹ ∘ (i₁  +₁ id) ∘ f) f# π₁ (record { guard = f ; guard-eq = 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-via-# : ∀ {X Y} → (f# : D₀ X × D₀ Y ⇒ D₀ Y) → (out ∘ f# ≈ [ π₂  , (π₂ +₁ f#) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (out ×₁ out)) → f# ≈ π₂
  snd-via-# {X}{Y} f# eq = guarded-unique (out⁻¹ ∘ (i₁ +₁ id) ∘ f) f# π₂ (record { guard = f ; guard-eq = sym (cancelˡ out∘out⁻¹)}) (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-via-# (π₁ ∘ zip⁻¹ ∘ zip) zip⁻¹∘zip-rec₁) (sym identityʳ))
    (trans (snd-via-# (π₂ ∘ 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ˡ unitlaw) (cancelˡ out∘out⁻¹)) refl) ([]-cong₂ (∘[] ○ []-cong₂ (pullˡ unitlaw) (cancelˡ out∘out⁻¹)) refl) ⟩∘⟨refl ⟩
          (id +₁ zip) ∘ distr ∘ ⟨ [ [ i₁ ∘ π₁ , π₁ +₁ π₁ ] , i₂ ∘ zip₁⁻¹ ] ,  [ [ i₁ ∘ π₂ , [ i₂ ∘ π₂ , i₁ ∘ π₂ ] ] , i₂ ∘ zip₂⁻¹ ] ⟩ ∘ out
            ≈˘⟨ refl⟩∘⟨ pushˡ ([]-unique (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}
      
  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              
     ∎)