open import Categories.Category.Core
open import Data.Product using (_,_)
open import Categories.Category.Distributive
open import Monad.Instance.Delay
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

import Categories.Morphism as Mor
import Categories.Morphism.Reasoning as MR
import Categories.Morphism.Properties as MP

-- Lemma A.11 and A.12
module Algebra.Search.Retraction {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 Bundles
  open import Monad.Instance.Delay.Commutative distributive D
  open τ-mod
  open σ-mod
  open HomReasoning
  open Equiv
  open Mor 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 Later∘Extend
  open import Algebra.Search cocartesian D

  -- needed for both lemmas
  private
    w : ∀ {X Y} → D₀ (X × Y) ⇒ D₀ (X × Y + D₀ (X × Y))
    w = [ now ∘ i₁ , later ∘ now ∘ out ] ∘ out
    w-guarded : ∀ {X Y} → IsGuarded (w {X} {Y})
    w-guarded = record 
      { guard = (id +₁ now ∘ out) ∘ out 
      ; guard-eq = sym (begin 
          out ∘ w                                            ≈⟨ pullˡ ∘[] ⟩ 
          [ out ∘ now ∘ i₁ , out ∘ later ∘ now ∘ out ] ∘ out ≈⟨ ([]-cong₂ (pullˡ unitlaw) (pullˡ laterlaw)) ⟩∘⟨refl ⟩ 
          (i₁ +₁ now ∘ out) ∘ out                            ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityʳ identityˡ) ⟩ 
          (i₁ +₁ id) ∘ (id +₁ now ∘ out) ∘ out               ∎)
      }

  -- Lemma A.11
  product-retract : ∀ X Y → Retract (D₀ (X × Y)) (D₀ X × D₀ Y)
  product-retract X Y = record 
    { section = ⟨ D₁ π₁ , D₁ π₂ ⟩ 
    ; retract = w #[ w-guarded ] ∘ extend σ ∘ τ 
    ; is-retract = assoc²βε ○ sym (guarded-uniformity v v-guarded u w w-guarded uniformity-helper) ○ guarded-unique v (v #[ v-guarded ]) id v-guarded (guarded-fixpoint v v-guarded) (sym id-fixpoint) 
    }
    where
    dst-eq : ∀ {X Y} → (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ Δ {X + Y} ≈ (i₁ ∘ Δ +₁ i₂ ∘ Δ)
    dst-eq = begin 
      (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ Δ                                          ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ elimʳ +-η ⟩ 
      (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ Δ ∘ [ i₁ , i₂ ]                            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ∘[] ⟩ 
      (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ [ Δ ∘ i₁ , Δ ∘ i₂ ]                        ≈⟨ refl⟩∘⟨ refl⟩∘⟨ []-cong₂ Δ∘ Δ∘ ⟩ 
      (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ [ ⟨ i₁ , i₁ ⟩ , ⟨ i₂ , i₂ ⟩ ]              ≈˘⟨ refl⟩∘⟨ (refl⟩∘⟨ ([]∘+₁ ○ []-cong₂ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ identityʳ) (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ identityʳ))) ⟩ 
      (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ distributeˡ ∘ (⟨ i₁ , id ⟩ +₁ ⟨ i₂ , id ⟩) ≈⟨ refl⟩∘⟨ (cancelˡ (IsIso.isoˡ isIsoˡ)) ⟩ 
      (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ (⟨ i₁ , id ⟩ +₁ ⟨ i₂ , id ⟩)                               ≈˘⟨ refl⟩∘⟨ (+₁-cong₂ ⁂∘Δ ⁂∘Δ) ⟩ 
      (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ ((i₁ ⁂ id) ∘ Δ +₁ (i₂ ⁂ id) ∘ Δ)                           ≈⟨ +₁∘+₁ ⟩
      (distributeʳ⁻¹ ∘ (i₁ ⁂ id) ∘ Δ +₁ distributeʳ⁻¹ ∘ (i₂ ⁂ id) ∘ Δ)                              ≈⟨ +₁-cong₂ (pullˡ distributeʳ⁻¹-i₁) (pullˡ distributeʳ⁻¹-i₂) ⟩ 
      (i₁ ∘ Δ +₁ i₂ ∘ Δ)                                                                            ∎

    u : D₀ (X × Y) ⇒ D₀ (X × Y)
    u = extend σ ∘ τ ∘ ⟨ D₁ π₁ , D₁ π₂ ⟩
    u-eq : out ∘ u ≈ (id +₁ later ∘ u) ∘ out
    u-eq = begin 
      out ∘ extend σ ∘ τ ∘ ⟨ D₁ π₁ , D₁ π₂ ⟩                                                                                                                                    ≈⟨ (refl⟩∘⟨ (extendʳ στ-comm)) ○ cancelˡ out∘out⁻¹ ⟩ 
      ([ id +₁ σ , i₂ ∘ [ τ , later ∘ extend σ ∘ τ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (out ⁂ out)) ∘ ⟨ D₁ π₁ , D₁ π₂ ⟩                                    ≈⟨ pullʳ (pullʳ (pullʳ ⁂∘⟨⟩)) ⟩ 
      [ id +₁ σ , i₂ ∘ [ τ , later ∘ extend σ ∘ τ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ ⟨ out ∘ D₁ π₁ , out ∘ D₁ π₂ ⟩                                        ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ (D₁-commutes π₁) (D₁-commutes π₂) ⟩ 
      [ id +₁ σ , i₂ ∘ [ τ , later ∘ extend σ ∘ τ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ ⟨ (π₁ +₁ D₁ π₁) ∘ out , (π₂ +₁ D₁ π₂) ∘ out ⟩                        ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩∘ ⟩ 
      [ id +₁ σ , i₂ ∘ [ τ , later ∘ extend σ ∘ τ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ ⟨ π₁ +₁ D₁ π₁ , π₂ +₁ D₁ π₂ ⟩ ∘ out                                  ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ ⁂∘Δ ⟩ 
      [ id +₁ σ , i₂ ∘ [ τ , later ∘ extend σ ∘ τ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ ((π₁ +₁ D₁ π₁) ⁂ (π₂ +₁ D₁ π₂)) ∘ Δ ∘ out                            ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (distributeˡ⁻¹-natural (π₁ +₁ D₁ π₁) π₂ (D₁ π₂)) ⟩ 
      [ id +₁ σ , i₂ ∘ [ τ , later ∘ extend σ ∘ τ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ (((π₁ +₁ D₁ π₁) ⁂ π₂) +₁ ((π₁ +₁ D₁ π₁) ⁂ D₁ π₂))  ∘ distributeˡ⁻¹ ∘ Δ ∘ out         ≈⟨ refl⟩∘⟨ pullˡ +₁∘+₁ ⟩ 
      [ id +₁ σ , i₂ ∘ [ τ , later ∘ extend σ ∘ τ ] ] ∘ (distributeʳ⁻¹ ∘ ((π₁ +₁ D₁ π₁) ⁂ π₂) +₁ distributeʳ⁻¹ ∘ ((π₁ +₁ D₁ π₁) ⁂ D₁ π₂)) ∘ distributeˡ⁻¹ ∘ Δ ∘ out             ≈˘⟨ refl⟩∘⟨ ((+₁-cong₂ (distributeʳ⁻¹-natural π₂ π₁ (D₁ π₁)) (distributeʳ⁻¹-natural (D₁ π₂) π₁ (D₁ π₁))) ⟩∘⟨refl) ⟩ 
      [ id +₁ σ , i₂ ∘ [ τ , later ∘ extend σ ∘ τ ] ] ∘ ((π₁ ⁂ π₂ +₁ D₁ π₁ ⁂ π₂) ∘ distributeʳ⁻¹ +₁ (π₁ ⁂ D₁ π₂ +₁ D₁ π₁ ⁂ D₁ π₂) ∘ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ Δ ∘ out    ≈˘⟨ refl⟩∘⟨ pullˡ +₁∘+₁ ⟩ 
      [ id +₁ σ , i₂ ∘ [ τ , later ∘ extend σ ∘ τ ] ] ∘ ((π₁ ⁂ π₂ +₁ D₁ π₁ ⁂ π₂) +₁ (π₁ ⁂ D₁ π₂ +₁ D₁ π₁ ⁂ D₁ π₂)) ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ Δ ∘ out ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (sym-assoc ○ pullˡ (assoc ○ dst-eq)) ⟩ 
      [ id +₁ σ , i₂ ∘ [ τ , later ∘ extend σ ∘ τ ] ] ∘ ((π₁ ⁂ π₂ +₁ D₁ π₁ ⁂ π₂) +₁ (π₁ ⁂ D₁ π₂ +₁ D₁ π₁ ⁂ D₁ π₂)) ∘ (i₁ ∘ Δ +₁ i₂ ∘ Δ) ∘ out                                   ≈⟨ refl⟩∘⟨ (pullˡ (+₁∘+₁ ○ +₁-cong₂ (extendʳ inject₁) (extendʳ inject₂))) ⟩ 
      [ id +₁ σ , i₂ ∘ [ τ , later ∘ extend σ ∘ τ ] ] ∘ ( i₁ ∘ (π₁ ⁂ π₂) ∘ Δ +₁ i₂ ∘ (D₁ π₁ ⁂ D₁ π₂) ∘ Δ) ∘ out                                                                 ≈⟨ pullˡ []∘+₁ ⟩
      [ (id +₁ σ) ∘ i₁ ∘ (π₁ ⁂ π₂) ∘ Δ , (i₂ ∘ [ τ , later ∘ extend σ ∘ τ ]) ∘ i₂ ∘ (D₁ π₁ ⁂ D₁ π₂) ∘ Δ ] ∘ out                                                                 ≈⟨ ([]-cong₂ (pullˡ (inject₁ ○ identityʳ)) (pullʳ (pullˡ inject₂))) ⟩∘⟨refl ⟩ 
      [ i₁ ∘ (π₁ ⁂ π₂) ∘ Δ , i₂ ∘ (later ∘ extend σ ∘ τ) ∘ (D₁ π₁ ⁂ D₁ π₂) ∘ Δ ] ∘ out                                                                                          ≈⟨ ([]-cong₂ (elimʳ (⁂∘Δ ○ ⁂-η)) (refl⟩∘⟨ refl⟩∘⟨ ⁂∘Δ)) ⟩∘⟨refl ⟩ 
      [ i₁ , i₂ ∘ (later ∘ extend σ ∘ τ) ∘ ⟨ D₁ π₁ , D₁ π₂ ⟩ ] ∘ out                                                                                                            ≈⟨ ([]-cong₂ (sym identityʳ) (refl⟩∘⟨ assoc²βε)) ⟩∘⟨refl ⟩ 
      (id +₁ later ∘ u) ∘ out                                                                                                                                                   ∎

    v : D₀ (X × Y) ⇒ D₀ (X × Y + D₀ (X × Y))
    v = [ now ∘ i₁ , later ∘ now ∘ i₂ ] ∘ out
    v-guarded : IsGuarded v
    v-guarded = record 
      { guard = (id +₁ now ∘ i₂) ∘ out 
      ; guard-eq = sym (begin 
          out ∘ v                                           ≈⟨ pullˡ ∘[] ⟩ 
          [ out ∘ now ∘ i₁ , out ∘ later ∘ now ∘ i₂ ] ∘ out ≈⟨ ([]-cong₂ (pullˡ unitlaw) (pullˡ laterlaw)) ⟩∘⟨refl ⟩ 
          [ i₁ ∘ i₁ , i₂ ∘ now ∘ i₂ ] ∘ out                 ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityʳ identityˡ) ⟩ 
          (i₁ +₁ id) ∘ (id +₁ now ∘ i₂) ∘ out               ∎)
      }

    uniformity-helper : w ∘ u ≈ D₁ (id +₁ u) ∘ v
    uniformity-helper = begin 
      ([ now ∘ i₁ , later ∘ now ∘ out ] ∘ out) ∘ u                       ≈⟨ pullʳ u-eq ⟩ 
      [ now ∘ i₁ , later ∘ now ∘ out ] ∘ (id +₁ later ∘ u) ∘ out         ≈⟨ pullˡ ([]∘+₁ ○ []-cong₂ identityʳ assoc²βε) ⟩ 
      [ now ∘ i₁ , later ∘ now ∘ out ∘ later ∘ u ] ∘ out                 ≈⟨ ([]-cong₂ refl (refl⟩∘⟨ (refl⟩∘⟨ (pullˡ laterlaw)))) ⟩∘⟨refl ⟩ 
      [ now ∘ i₁ , later ∘ now ∘ i₂ ∘ u ] ∘ out                          ≈˘⟨ ([]-cong₂ refl (refl⟩∘⟨ refl⟩∘⟨ inject₂)) ⟩∘⟨refl ⟩ 
      [ now ∘ i₁ , later ∘ now ∘ (id +₁ u) ∘ i₂ ] ∘ out                  ≈˘⟨ ([]-cong₂ (pullʳ (inject₁ ○ identityʳ)) (refl⟩∘⟨ (extendʳ DK.identityʳ))) ⟩∘⟨refl ⟩ 
      [ (now ∘ (id +₁ u)) ∘ i₁ , later ∘ D₁ (id +₁ u) ∘ now ∘ i₂ ] ∘ out ≈˘⟨ pullˡ (∘[] ○ []-cong₂ (pullˡ DK.identityʳ) (extendʳ (sym (later-extend-comm (now ∘ (id +₁ u)))))) ⟩ 
      D₁ (id +₁ u) ∘ [ now ∘ i₁ , later ∘ now ∘ i₂ ] ∘ out               ∎

    id-fixpoint : extend ([ now , id ]) ∘ [ now ∘ i₁ , later ∘ now ∘ i₂ ] ∘ out ≈ id
    id-fixpoint = begin 
      extend ([ now , id ]) ∘ [ now ∘ i₁ , later ∘ now ∘ i₂ ] ∘ out                         ≈⟨ pullˡ ∘[] ⟩ 
      [ extend ([ now , id ]) ∘ now ∘ i₁ , extend ([ now , id ]) ∘ later ∘ now ∘ i₂ ] ∘ out ≈⟨ ([]-cong₂ (pullˡ DK.identityʳ) (extendʳ (sym (later-extend-comm [ now , id ])))) ⟩∘⟨refl ⟩ 
      [ [ now , id ] ∘ i₁ , later ∘ extend ([ now , id ]) ∘ now ∘ i₂ ] ∘ out                ≈⟨ ([]-cong₂ inject₁ (elimʳ (pullˡ DK.identityʳ ○ inject₂))) ⟩∘⟨refl ⟩ 
      [ now , later ] ∘ out                                                                 ≈⟨ (sym ∘[] ○ elimʳ +-η) ⟩∘⟨refl ⟩ 
      out⁻¹ ∘ out                                                                           ≈⟨ out⁻¹∘out ⟩ 
      id                                                                                    ∎

  -- Lemma A.12
  tau-retract : ∀ X (algebra : Search-Algebra) → Retract (D₀ ((Search-Algebra.A algebra) × X)) (Search-Algebra.A algebra × D₀ X)
  tau-retract X algebra = record 
    { section = ⟨ α ∘ D₁ π₁ , D₁ π₂ ⟩
    ; retract = τ 
    ; is-retract = begin 
        τ ∘ ⟨ α ∘ D₁ π₁ , D₁ π₂ ⟩                                                           ≈⟨ introˡ product-is-retract ⟩
        ((w #[ w-guarded ] ∘ extend σ ∘ τ) ∘ ⟨ D₁ π₁ , D₁ π₂ ⟩) ∘ τ ∘ ⟨ α ∘ D₁ π₁ , D₁ π₂ ⟩ ≈⟨ pullʳ epi-helper ⟩
        (w #[ w-guarded ] ∘ extend σ ∘ τ) ∘ ⟨ D₁ π₁ , D₁ π₂ ⟩                               ≈⟨ product-is-retract ⟩
        id                                                                                  ∎ 
    } 
    where
    open Search-Algebra algebra using (A; α) renaming (identity₁ to s-identity₁; identity₂ to s-identity₂)
    open Retract (product-retract A X) using () renaming (is-retract to product-is-retract)
    top-square : ((now ⁂ id) +₁ ⟨ later ∘ D₁ π₁ , D₁ π₂ ⟩) ∘ out ≈ distributeˡ⁻¹ ∘ (id ⁂ out) ∘ ⟨ D₁ π₁ , D₁ π₂ ⟩
    top-square = out⁻¹-epi (((now ⁂ id) +₁ ⟨ later ∘ D₁ π₁ , D₁ π₂ ⟩) ∘ out) (distributeˡ⁻¹ ∘ (id ⁂ out) ∘ ⟨ D₁ π₁ , D₁ π₂ ⟩) (begin 
      (((now ⁂ id) +₁ ⟨ later ∘ D₁ π₁ , D₁ π₂ ⟩) ∘ out) ∘ out⁻¹ ≈⟨ cancelʳ out∘out⁻¹ ⟩ 
      (now ⁂ id) +₁ ⟨ later ∘ D₁ π₁ , D₁ π₂ ⟩                   ≈⟨ []-unique unique₁ unique₂ ⟩ 
      (distributeˡ⁻¹ ∘ (id ⁂ out) ∘ ⟨ D₁ π₁ , D₁ π₂ ⟩) ∘ out⁻¹  ∎)
      where
      unique₁ : ((distributeˡ⁻¹ ∘ (id ⁂ out) ∘ ⟨ D₁ π₁ , D₁ π₂ ⟩) ∘ out⁻¹) ∘ i₁ ≈ i₁ ∘ (now ⁂ id)
      unique₁ = begin 
        ((distributeˡ⁻¹ ∘ (id ⁂ out) ∘ ⟨ D₁ π₁ , D₁ π₂ ⟩) ∘ out⁻¹) ∘ i₁ ≈⟨ assoc ⟩ 
        (distributeˡ⁻¹ ∘ (id ⁂ out) ∘ ⟨ D₁ π₁ , D₁ π₂ ⟩) ∘ now          ≈⟨ pullʳ (pullʳ ⟨⟩∘) ⟩ 
        distributeˡ⁻¹ ∘ (id ⁂ out) ∘ ⟨ D₁ π₁ ∘ now , D₁ π₂ ∘ now ⟩      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ DK.identityʳ DK.identityʳ ⟩ 
        distributeˡ⁻¹ ∘ (id ⁂ out) ∘ ⟨ now ∘ π₁ , now ∘ π₂ ⟩            ≈⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ (pullˡ unitlaw)) ⟩ 
        distributeˡ⁻¹ ∘ ⟨ now ∘ π₁ , i₁ ∘ π₂ ⟩                          ≈˘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl) ⟩ 
        distributeˡ⁻¹ ∘ (id ⁂ i₁) ∘ ⟨ now ∘ π₁ , π₂ ⟩                   ≈⟨ pullˡ distributeˡ⁻¹-i₁ ⟩ 
        i₁ ∘ ⟨ now ∘ π₁ , π₂ ⟩                                          ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ refl (sym identityˡ)) ⟩ 
        i₁ ∘ (now ⁂ id)                                                 ∎
      unique₂ : ((distributeˡ⁻¹ ∘ (id ⁂ out) ∘ ⟨ D₁ π₁ , D₁ π₂ ⟩) ∘ out⁻¹) ∘ i₂ ≈ i₂ ∘ ⟨ later ∘ D₁ π₁ , D₁ π₂ ⟩
      unique₂ = begin 
        ((distributeˡ⁻¹ ∘ (id ⁂ out) ∘ ⟨ D₁ π₁ , D₁ π₂ ⟩) ∘ out⁻¹) ∘ i₂ ≈⟨ assoc ⟩ 
        (distributeˡ⁻¹ ∘ (id ⁂ out) ∘ ⟨ D₁ π₁ , D₁ π₂ ⟩) ∘ later        ≈⟨ pullʳ (pullʳ ⟨⟩∘) ⟩ 
        distributeˡ⁻¹ ∘ (id ⁂ out) ∘ ⟨ D₁ π₁ ∘ later , D₁ π₂ ∘ later ⟩  ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ (sym (later-extend-comm (now ∘ π₁))) (sym (later-extend-comm (now ∘ π₂))) ⟩ 
        distributeˡ⁻¹ ∘ (id ⁂ out) ∘ ⟨ later ∘ D₁ π₁ , later ∘ D₁ π₂ ⟩  ≈⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ (pullˡ laterlaw)) ⟩ 
        distributeˡ⁻¹ ∘ ⟨ later ∘ D₁ π₁ , i₂ ∘ D₁ π₂ ⟩                  ≈˘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl) ⟩ 
        distributeˡ⁻¹ ∘ (id ⁂ i₂) ∘ ⟨ later ∘ D₁ π₁ , D₁ π₂ ⟩           ≈⟨ pullˡ distributeˡ⁻¹-i₂ ⟩ 
        i₂ ∘ ⟨ later ∘ D₁ π₁ , D₁ π₂ ⟩                                  ∎
    eq : D₁ π₁ ≈ D₁ α ∘ D₁ π₁ ∘ τ ∘ ⟨ D₁ π₁ , D₁ π₂ ⟩
    eq = extend-unique (now ∘ π₁) (D₁ α ∘ D₁ π₁ ∘ τ ∘ ⟨ D₁ π₁ , D₁ π₂ ⟩) (begin 
      out ∘ D₁ α ∘ D₁ π₁ ∘ τ ∘ ⟨ D₁ π₁ , D₁ π₂ ⟩                                                 ≈⟨ extendʳ (D₁-commutes α) ⟩ 
      (α +₁ D₁ α) ∘ out ∘ D₁ π₁ ∘ τ ∘ ⟨ D₁ π₁ , D₁ π₂ ⟩                                          ≈⟨ refl⟩∘⟨ (extendʳ (D₁-commutes π₁)) ⟩ 
      (α +₁ D₁ α) ∘ (π₁ +₁ D₁ π₁) ∘ out ∘ τ ∘ ⟨ D₁ π₁ , D₁ π₂ ⟩                                  ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (extendʳ τ-commutes)) ⟩ 
      (α +₁ D₁ α) ∘ (π₁ +₁ D₁ π₁) ∘ (id +₁ τ) ∘ (distributeˡ⁻¹ ∘ (id ⁂ out)) ∘ ⟨ D₁ π₁ , D₁ π₂ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (assoc ○ sym top-square) ⟩ 
      (α +₁ D₁ α) ∘ (π₁ +₁ D₁ π₁) ∘ (id +₁ τ) ∘ ((now ⁂ id) +₁ ⟨ later ∘ D₁ π₁ , D₁ π₂ ⟩) ∘ out  ≈⟨ pullˡ +₁∘+₁ ○ pullˡ +₁∘+₁ ○ pullˡ +₁∘+₁ ⟩ 
      (((α ∘ π₁) ∘ id) ∘ (now ⁂ id) +₁ ((D₁ α ∘ D₁ π₁) ∘ τ) ∘ ⟨ later ∘ D₁ π₁ , D₁ π₂ ⟩) ∘ out   ≈⟨ (+₁-cong₂ (pullʳ identityˡ ○ pullʳ project₁) assoc²αε) ⟩∘⟨refl ⟩ 
      (α ∘ now ∘ π₁ +₁ D₁ α ∘ D₁ π₁ ∘ τ ∘ ⟨ later ∘ D₁ π₁ , D₁ π₂ ⟩) ∘ out                       ≈⟨ +₁-cong₂ (cancelˡ s-identity₁) (sym (refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ refl identityˡ))) ⟩∘⟨refl ⟩ 
      (π₁ +₁ D₁ α ∘ D₁ π₁ ∘ τ ∘ (later ⁂ id) ∘ ⟨ D₁ π₁ , D₁ π₂ ⟩) ∘ out                          ≈⟨ (+₁-cong₂ refl (refl⟩∘⟨ refl⟩∘⟨ extendʳ (refl⟩∘⟨ (⁂-cong₂ refl (sym D.F.identity)) ○ τ-natural later id))) ⟩∘⟨refl ⟩
      (π₁ +₁ D₁ α ∘ D₁ π₁ ∘ D₁ (later ⁂ id) ∘ τ ∘ ⟨ D₁ π₁ , D₁ π₂ ⟩) ∘ out                       ≈⟨ (+₁-cong₂ refl (refl⟩∘⟨ (extendʳ (sym D.F.homomorphism ○ D.F.F-resp-≈ project₁ ○ D.F.homomorphism)))) ⟩∘⟨refl ⟩ 
      (π₁ +₁ D₁ α ∘ D₁ later ∘ D₁ π₁ ∘ τ ∘ ⟨ D₁ π₁ , D₁ π₂ ⟩) ∘ out                              ≈⟨ ([]-cong₂ (pushˡ (sym unitlaw)) (refl⟩∘⟨ (pullˡ (sym D.F.homomorphism ○ D.F.F-resp-≈ s-identity₂)))) ⟩∘⟨refl ⟩ 
      [ out ∘ now ∘ π₁ , i₂ ∘ D₁ α ∘ D₁ π₁ ∘ τ ∘ ⟨ D₁ π₁ , D₁ π₂ ⟩ ] ∘ out                       ∎)
    epi-helper : ⟨ D₁ π₁ , D₁ π₂ ⟩ ∘ τ ∘ ⟨ α ∘ D₁ π₁ , D₁ π₂ ⟩ ≈ ⟨ D₁ π₁ , D₁ π₂ ⟩
    epi-helper = begin 
      ⟨ D₁ π₁ , D₁ π₂ ⟩ ∘ τ ∘ ⟨ α ∘ D₁ π₁ , D₁ π₂ ⟩                             ≈⟨ ⟨⟩∘ ⟩ 
      ⟨ D₁ π₁ ∘ τ ∘ ⟨ α ∘ D₁ π₁ , D₁ π₂ ⟩ , D₁ π₂ ∘ τ ∘ ⟨ α ∘ D₁ π₁ , D₁ π₂ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ (sym (refl⟩∘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ refl identityˡ))) (pullˡ τ-identityˡ) ⟩
      ⟨ D₁ π₁ ∘ τ ∘ (α ⁂ id) ∘ ⟨ D₁ π₁ , D₁ π₂ ⟩ , π₂ ∘ ⟨ α ∘ D₁ π₁ , D₁ π₂ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ (refl⟩∘⟨ (extendʳ (refl⟩∘⟨ (⁂-cong₂ refl (sym D.F.identity)) ○ τ-natural α id))) project₂ ⟩ 
      ⟨ D₁ π₁ ∘ D₁ (α ⁂ id) ∘ τ ∘ ⟨ D₁ π₁ , D₁ π₂ ⟩ , D₁ π₂ ⟩                   ≈⟨ ⟨⟩-cong₂ (extendʳ (sym D.F.homomorphism ○ D.F.F-resp-≈ project₁ ○ D.F.homomorphism)) refl ⟩
      ⟨ D₁ α ∘ D₁ π₁ ∘ τ ∘ ⟨ D₁ π₁ , D₁ π₂ ⟩ , D₁ π₂ ⟩                          ≈⟨ ⟨⟩-cong₂ (sym eq) refl ⟩
      ⟨ D₁ π₁ , D₁ π₂ ⟩                                                         ∎