open import Level
open import Categories.Category.Core
open import Categories.Object.NaturalNumbers.Parametrized
open import Categories.Category.Distributive
open import Categories.Object.Terminal
open import Monad.Instance.Delay
open import Monad.Instance.Delay.Quotient
import Categories.Morphism as M
import Categories.Morphism.Reasoning as MR
import Categories.Morphism.Properties as MP
module Monad.Instance.Delay.Quotient.KTheorem.Condition3-1 {o ℓ e} {C : Category o ℓ e}
(distributive : Distributive C) (DM : DelayM (Distributive.cocartesian distributive))
(PNNO : ParametrizedNNO C (Distributive.cartesian distributive))
(DQ : DelayQ distributive DM PNNO) where
open import Categories.Diagram.Coequalizer C
open Category C
open import Category.Distributive.Helper distributive renaming (η to η-prod)
open import Monad.Instance.K distributive
open import Monad.Strong.Helper cartesian
open Bundles
open import Algebra.Elgot cocartesian
open import Algebra.Search cocartesian DM
open import Algebra.Search.Properties cocartesian DM
open import Monad.Instance.Delay.Quotient.KTheorem.Conditions distributive DM PNNO DQ
open import Monad.Instance.Delay.Strong distributive DM
open Equiv
open HomReasoning
open M C
open MR C
open MP C
open DelayM DM
open Coit
open D-Monad
open D-Kleisli
open τ-mod
open DelayQ DQ
private
module PNNO = ParametrizedNNO PNNO
open PNNO using (s; z; N)
open import Monad.Instance.Delay.Iota distributive DM PNNO
open Later∘Extend
module _ {X : Obj} where
open import Object.NaturalNumbers.Parametrized cartesian (PNNO⇒NNO C cartesian PNNO)
w : D₀ X × D₀ ⊤ ⇒ D₀ X + D₀ X × D₀ ⊤
w = [ i₁ ∘ π₁ , i₂ ∘ (earlier ×₁ id) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ out)
w-now : w ∘ (id ×₁ now) ≈ i₁ ∘ π₁
w-now = begin
([ i₁ ∘ π₁ , i₂ ∘ (earlier ×₁ id) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ out)) ∘ (id ×₁ now) ≈⟨ pullʳ (pullʳ (×₁∘×₁ ○ ×₁-cong₂ identity² unitlaw)) ⟩
[ i₁ ∘ π₁ , i₂ ∘ (earlier ×₁ id) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ i₁) ≈⟨ refl⟩∘⟨ distributeˡ⁻¹-i₁ ⟩
[ i₁ ∘ π₁ , i₂ ∘ (earlier ×₁ id) ] ∘ i₁ ≈⟨ inject₁ ⟩
i₁ ∘ π₁ ∎
w-later : w ∘ (id ×₁ later) ≈ i₂ ∘ (earlier ×₁ id)
w-later = begin
([ i₁ ∘ π₁ , i₂ ∘ (earlier ×₁ id) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ out)) ∘ (id ×₁ later) ≈⟨ pullʳ (pullʳ (×₁∘×₁ ○ ×₁-cong₂ identity² laterlaw)) ⟩
[ i₁ ∘ π₁ , i₂ ∘ (earlier ×₁ id) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ i₂) ≈⟨ refl⟩∘⟨ distributeˡ⁻¹-i₂ ⟩
[ i₁ ∘ π₁ , i₂ ∘ (earlier ×₁ id) ] ∘ i₂ ≈⟨ inject₂ ⟩
i₂ ∘ (earlier ×₁ id) ∎
D-jointly-epic-product : ∀ {X Y Z} {f g : D₀ Z × D₀ X ⇒ Y} → (f ∘ (now ×₁ now) ≈ g ∘ (now ×₁ now)) → (f ∘ (later ×₁ now) ≈ g ∘ (later ×₁ now)) → (f ∘ (now ×₁ later) ≈ g ∘ (now ×₁ later)) → (f ∘ (later ×₁ later) ≈ g ∘ (later ×₁ later)) → f ≈ g
D-jointly-epic-product {X} {Y} {Z} {f} {g} now-now later-now now-later later-later = begin
f ≈⟨ introʳ (⟨⟩-unique (id-comm ○ ∘-resp-≈ˡ (sym out⁻¹∘out)) (id-comm ○ ∘-resp-≈ˡ (sym out⁻¹∘out))) ⟩
f ∘ (out⁻¹ ∘ out ×₁ out⁻¹ ∘ out) ≈˘⟨ refl⟩∘⟨ ×₁∘×₁ ⟩
f ∘ (out⁻¹ ×₁ out⁻¹) ∘ (out ×₁ out) ≈⟨ extendʳ (distribution ○ helper ○ sym distribution) ⟩
g ∘ (out⁻¹ ×₁ out⁻¹) ∘ (out ×₁ out) ≈⟨ refl⟩∘⟨ ×₁∘×₁ ⟩
g ∘ (out⁻¹ ∘ out ×₁ out⁻¹ ∘ out) ≈⟨ elimʳ (⟨⟩-unique (id-comm ○ ∘-resp-≈ˡ (sym out⁻¹∘out)) (id-comm ○ ∘-resp-≈ˡ (sym out⁻¹∘out))) ⟩
g ∎
where
distribution : ∀ {h : D₀ Z × D₀ X ⇒ Y} → h ∘ (out⁻¹ ×₁ out⁻¹) ≈ [ [ h ∘ (now ×₁ now) , h ∘ (later ×₁ now) ] , [ h ∘ (now ×₁ later) , h ∘ (later ×₁ later) ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹
distribution {h} = Iso⇒Epi (IsIso.iso isIsoˡ) (h ∘ (out⁻¹ ×₁ out⁻¹)) ([ [ h ∘ (now ×₁ now) , h ∘ (later ×₁ now) ] , [ h ∘ (now ×₁ later) , h ∘ (later ×₁ later) ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹) (begin
(h ∘ (out⁻¹ ×₁ out⁻¹)) ∘ distributeˡ ≈⟨ ∘[] ○ []-cong₂ (pullʳ (×₁∘×₁ ○ ×₁-cong₂ identityʳ refl)) (pullʳ (×₁∘×₁ ○ ×₁-cong₂ identityʳ refl)) ⟩
[ h ∘ (out⁻¹ ×₁ now) , h ∘ (out⁻¹ ×₁ later) ] ≈⟨ []-cong₂ distribution-helper₁ distribution-helper₂ ⟩
[ [ h ∘ (now ×₁ now) , h ∘ (later ×₁ now) ] ∘ distributeʳ⁻¹ , [ h ∘ (now ×₁ later) , h ∘ (later ×₁ later) ] ∘ distributeʳ⁻¹ ] ≈˘⟨ []∘+₁ ⟩
[ [ h ∘ (now ×₁ now) , h ∘ (later ×₁ now) ] , [ h ∘ (now ×₁ later) , h ∘ (later ×₁ later) ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ≈˘⟨ pullʳ (cancelʳ (IsIso.isoˡ isIsoˡ)) ⟩
([ [ h ∘ (now ×₁ now) , h ∘ (later ×₁ now) ] , [ h ∘ (now ×₁ later) , h ∘ (later ×₁ later) ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹) ∘ distributeˡ ∎)
where
distribution-helper₁ : h ∘ (out⁻¹ ×₁ now) ≈ [ h ∘ (now ×₁ now) , h ∘ (later ×₁ now) ] ∘ distributeʳ⁻¹
distribution-helper₁ = Iso⇒Epi (IsIso.iso isIsoʳ) (h ∘ (out⁻¹ ×₁ now)) ([ h ∘ (now ×₁ now) , h ∘ (later ×₁ now) ] ∘ distributeʳ⁻¹) (begin
(h ∘ (out⁻¹ ×₁ now)) ∘ distributeʳ ≈⟨ ∘[] ○ []-cong₂ (pullʳ (×₁∘×₁ ○ ×₁-cong₂ refl identityʳ)) (pullʳ (×₁∘×₁ ○ ×₁-cong₂ refl identityʳ)) ⟩
[ h ∘ (now ×₁ now) , h ∘ (later ×₁ now) ] ≈˘⟨ cancelʳ (IsIso.isoˡ isIsoʳ) ⟩
([ h ∘ (now ×₁ now) , h ∘ (later ×₁ now) ] ∘ distributeʳ⁻¹) ∘ distributeʳ ∎)
distribution-helper₂ : h ∘ (out⁻¹ ×₁ later) ≈ [ h ∘ (now ×₁ later) , h ∘ (later ×₁ later) ] ∘ distributeʳ⁻¹
distribution-helper₂ = Iso⇒Epi (IsIso.iso isIsoʳ) (h ∘ (out⁻¹ ×₁ later)) ([ h ∘ (now ×₁ later) , h ∘ (later ×₁ later) ] ∘ distributeʳ⁻¹) (begin
(h ∘ (out⁻¹ ×₁ later)) ∘ distributeʳ ≈⟨ ∘[] ○ []-cong₂ (pullʳ (×₁∘×₁ ○ ×₁-cong₂ refl identityʳ)) (pullʳ (×₁∘×₁ ○ ×₁-cong₂ refl identityʳ)) ⟩
[ h ∘ (now ×₁ later) , h ∘ (later ×₁ later) ] ≈˘⟨ cancelʳ (IsIso.isoˡ isIsoʳ) ⟩
([ h ∘ (now ×₁ later) , h ∘ (later ×₁ later) ] ∘ distributeʳ⁻¹) ∘ distributeʳ ∎)
helper : [ [ f ∘ (now ×₁ now) , f ∘ (later ×₁ now) ] , [ f ∘ (now ×₁ later) , f ∘ (later ×₁ later) ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ≈ [ [ g ∘ (now ×₁ now) , g ∘ (later ×₁ now) ] , [ g ∘ (now ×₁ later) , g ∘ (later ×₁ later) ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹
helper = ∘-resp-≈ˡ ([]-cong₂ ([]-cong₂ now-now later-now) ([]-cong₂ now-later later-later))
PNNO-jointly-epic : ∀ {X Y} {f g : X × N ⇒ Y} → (f ∘ ⟨ id , z ∘ ! ⟩ ≈ g ∘ ⟨ id , z ∘ ! ⟩) → (f ∘ (id ×₁ s) ≈ g ∘ (id ×₁ s)) → f ≈ g
PNNO-jointly-epic {X} {Y} {f} {g} IB IS = begin
f ≈⟨ introʳ (M._≅_.isoˡ nno-iso) ⟩
f ∘ [ ⟨ id , z ∘ ! ⟩ , (id ×₁ s) ] ∘ M._≅_.from nno-iso ≈⟨ pullˡ ∘[] ⟩
[ f ∘ ⟨ id , z ∘ ! ⟩ , f ∘ (id ×₁ s) ] ∘ M._≅_.from nno-iso ≈⟨ ([]-cong₂ IB IS) ⟩∘⟨refl ⟩
[ g ∘ ⟨ id , z ∘ ! ⟩ , g ∘ (id ×₁ s) ] ∘ M._≅_.from nno-iso ≈˘⟨ pullˡ ∘[] ⟩
g ∘ [ ⟨ id , z ∘ ! ⟩ , (id ×₁ s) ] ∘ M._≅_.from nno-iso ≈⟨ elimʳ (M._≅_.isoˡ nno-iso) ⟩
g ∎
u : D₀ (X × N) × D₀ ⊤ ⇒ D₀ (X × N) + D₀ (X × N) × D₀ ⊤
u = [ (i₁ ∘ π₁) , [ i₂ ∘ (now ∘ (id ×₁ s⁻¹) ×₁ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (out ×₁ id) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ out)
u-now : u ∘ (id ×₁ now) ≈ i₁ ∘ π₁
u-now = begin
u ∘ (id ×₁ now) ≈⟨ pullʳ (pullʳ (×₁∘×₁ ○ ×₁-cong₂ identity² unitlaw)) ⟩
[ i₁ ∘ π₁ , [ i₂ ∘ (now ∘ (id ×₁ s⁻¹) ×₁ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (out ×₁ id) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ i₁) ≈⟨ refl⟩∘⟨ distributeˡ⁻¹-i₁ ⟩
[ i₁ ∘ π₁ , [ i₂ ∘ (now ∘ (id ×₁ s⁻¹) ×₁ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (out ×₁ id) ] ∘ i₁ ≈⟨ inject₁ ⟩
i₁ ∘ π₁ ∎
u-later : u ∘ (later ×₁ later) ≈ i₂
u-later = begin
u ∘ (later ×₁ later) ≈˘⟨ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ identityˡ identityʳ) ⟩
u ∘ (id ×₁ later) ∘ (later ×₁ id) ≈⟨ pullʳ (pullʳ (pullˡ (×₁∘×₁ ○ ×₁-cong₂ identity² laterlaw))) ⟩
[ i₁ ∘ π₁ , [ i₂ ∘ (now ∘ (id ×₁ s⁻¹) ×₁ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (out ×₁ id) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ i₂) ∘ (later ×₁ id) ≈⟨ refl⟩∘⟨ (pullˡ distributeˡ⁻¹-i₂) ⟩
[ i₁ ∘ π₁ , [ i₂ ∘ (now ∘ (id ×₁ s⁻¹) ×₁ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (out ×₁ id) ] ∘ i₂ ∘ (later ×₁ id) ≈⟨ extendʳ inject₂ ⟩
[ i₂ ∘ (now ∘ (id ×₁ s⁻¹) ×₁ id) , i₂ ] ∘ (distributeʳ⁻¹ ∘ (out ×₁ id)) ∘ (later ×₁ id) ≈⟨ refl⟩∘⟨ (pullʳ (×₁∘×₁ ○ ×₁-cong₂ laterlaw identity²)) ⟩
[ i₂ ∘ (now ∘ (id ×₁ s⁻¹) ×₁ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (i₂ ×₁ id) ≈⟨ refl⟩∘⟨ distributeʳ⁻¹-i₂ ⟩
[ i₂ ∘ (now ∘ (id ×₁ s⁻¹) ×₁ id) , i₂ ] ∘ i₂ ≈⟨ inject₂ ⟩
i₂ ∎
u-zero : u ∘ (now ∘ ⟨ id , z ∘ ! ⟩ ×₁ later) ≈ i₂ ∘ (now ∘ ⟨ id , z ∘ ! ⟩ ×₁ id)
u-zero = begin
([ i₁ ∘ π₁ , [ i₂ ∘ (now ∘ (id ×₁ s⁻¹) ×₁ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (out ×₁ id) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ out)) ∘ (now ∘ ⟨ id , z ∘ ! ⟩ ×₁ later) ≈˘⟨ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ identityˡ identityʳ) ⟩
([ i₁ ∘ π₁ , [ i₂ ∘ (now ∘ (id ×₁ s⁻¹) ×₁ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (out ×₁ id) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ out)) ∘ (id ×₁ later) ∘ (now ∘ ⟨ id , z ∘ ! ⟩ ×₁ id) ≈⟨ pullʳ (pullʳ (pullˡ (×₁∘×₁ ○ ×₁-cong₂ identity² laterlaw))) ⟩
[ i₁ ∘ π₁ , [ i₂ ∘ (now ∘ (id ×₁ s⁻¹) ×₁ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (out ×₁ id) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ i₂) ∘ (now ∘ ⟨ id , z ∘ ! ⟩ ×₁ id) ≈⟨ refl⟩∘⟨ (pullˡ distributeˡ⁻¹-i₂) ⟩
[ i₁ ∘ π₁ , [ i₂ ∘ (now ∘ (id ×₁ s⁻¹) ×₁ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (out ×₁ id) ] ∘ i₂ ∘ (now ∘ ⟨ id , z ∘ ! ⟩ ×₁ id) ≈⟨ extendʳ inject₂ ⟩
[ i₂ ∘ (now ∘ (id ×₁ s⁻¹) ×₁ id) , i₂ ] ∘ (distributeʳ⁻¹ ∘ (out ×₁ id)) ∘ (now ∘ ⟨ id , z ∘ ! ⟩ ×₁ id) ≈⟨ refl⟩∘⟨ (pullʳ (×₁∘×₁ ○ ×₁-cong₂ (pullˡ unitlaw) refl ○ sym ×₁∘×₁)) ⟩
[ i₂ ∘ (now ∘ (id ×₁ s⁻¹) ×₁ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (i₁ ×₁ id) ∘ (⟨ id , z ∘ ! ⟩ ×₁ id) ≈⟨ refl⟩∘⟨ (pullˡ distributeʳ⁻¹-i₁) ⟩
[ i₂ ∘ (now ∘ (id ×₁ s⁻¹) ×₁ id) , i₂ ] ∘ i₁ ∘ (⟨ id , z ∘ ! ⟩ ×₁ id) ≈⟨ extendʳ inject₁ ⟩
i₂ ∘ (now ∘ (id ×₁ s⁻¹) ×₁ id) ∘ (⟨ id , z ∘ ! ⟩ ×₁ id) ≈⟨ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ (pullʳ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identity² (pullˡ s⁻¹-zero))) identity²) ⟩
i₂ ∘ (now ∘ ⟨ id , z ∘ ! ⟩ ×₁ id) ∎
u-succ : u ∘ (now ∘ (id ×₁ s) ×₁ later) ≈ i₂ ∘ (now ×₁ id)
u-succ = begin
([ i₁ ∘ π₁ , [ i₂ ∘ (now ∘ (id ×₁ s⁻¹) ×₁ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (out ×₁ id) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ out)) ∘ (now ∘ (id ×₁ s) ×₁ later) ≈˘⟨ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ identityˡ identityʳ) ⟩
([ i₁ ∘ π₁ , [ i₂ ∘ (now ∘ (id ×₁ s⁻¹) ×₁ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (out ×₁ id) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ out)) ∘ (id ×₁ later) ∘ (now ∘ (id ×₁ s) ×₁ id) ≈⟨ pullʳ (pullʳ (pullˡ (×₁∘×₁ ○ ×₁-cong₂ identity² laterlaw))) ⟩
[ i₁ ∘ π₁ , [ i₂ ∘ (now ∘ (id ×₁ s⁻¹) ×₁ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (out ×₁ id) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ i₂) ∘ (now ∘ (id ×₁ s) ×₁ id) ≈⟨ refl⟩∘⟨ (pullˡ distributeˡ⁻¹-i₂) ⟩
[ i₁ ∘ π₁ , [ i₂ ∘ (now ∘ (id ×₁ s⁻¹) ×₁ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (out ×₁ id) ] ∘ i₂ ∘ (now ∘ (id ×₁ s) ×₁ id) ≈⟨ extendʳ inject₂ ⟩
[ i₂ ∘ (now ∘ (id ×₁ s⁻¹) ×₁ id) , i₂ ] ∘ (distributeʳ⁻¹ ∘ (out ×₁ id)) ∘ (now ∘ (id ×₁ s) ×₁ id) ≈⟨ refl⟩∘⟨ (pullʳ (×₁∘×₁ ○ ×₁-cong₂ (pullˡ unitlaw) refl ○ sym ×₁∘×₁)) ⟩
[ i₂ ∘ (now ∘ (id ×₁ s⁻¹) ×₁ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (i₁ ×₁ id) ∘ ((id ×₁ s) ×₁ id) ≈⟨ refl⟩∘⟨ (pullˡ distributeʳ⁻¹-i₁) ⟩
[ i₂ ∘ (now ∘ (id ×₁ s⁻¹) ×₁ id) , i₂ ] ∘ i₁ ∘ ((id ×₁ s) ×₁ id) ≈⟨ extendʳ inject₁ ⟩
i₂ ∘ (now ∘ (id ×₁ s⁻¹) ×₁ id) ∘ ((id ×₁ s) ×₁ id) ≈⟨ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ (cancelʳ (×₁∘×₁ ○ ×₁-cong₂ identity² s⁻¹-succ ○ ⟨⟩-unique id-comm id-comm)) identity²) ⟩
i₂ ∘ (now ×₁ id) ∎
coit-w-retract : coit w ∘ ⟨ D.μ.η X , D₁ ! ⟩ ≈ id
coit-w-retract = begin
coit w ∘ ⟨ D.μ.η X , D₁ ! ⟩ ≈˘⟨ coit-unique out (coit w ∘ ⟨ D.μ.η X , D₁ ! ⟩) coit-helper ⟩
coit out ≈⟨ coit-refl ⟩
id ∎
where
coit-helper : out ∘ coit w ∘ ⟨ D.μ.η X , D₁ ! ⟩ ≈ (id +₁ coit w ∘ ⟨ D.μ.η X , D₁ ! ⟩) ∘ out
coit-helper = begin
out ∘ coit w ∘ ⟨ D.μ.η X , D₁ ! ⟩ ≈⟨ extendʳ (coit-commutes w) ⟩
(id +₁ coit w) ∘ w ∘ ⟨ D.μ.η X , D₁ ! ⟩ ≈⟨ refl⟩∘⟨ (D-jointly-epic now-helper later-helper) ⟩
(id +₁ coit w) ∘ (id +₁ ⟨ D.μ.η X , D₁ ! ⟩) ∘ out ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² refl) ⟩
(id +₁ coit w ∘ ⟨ D.μ.η X , D₁ ! ⟩) ∘ out ∎
where
now-helper : (w ∘ ⟨ D.μ.η X , D₁ ! ⟩) ∘ now ≈ ((id +₁ ⟨ D.μ.η X , D₁ ! ⟩) ∘ out) ∘ now
now-helper = begin
(w ∘ ⟨ D.μ.η X , D₁ ! ⟩) ∘ now ≈⟨ pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ D.identityʳ (sym (D.η.commute !))) ⟩
w ∘ ⟨ id , now ∘ ! ⟩ ≈˘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-congʳ identity²) ⟩
w ∘ (id ×₁ now) ∘ ⟨ id , ! ⟩ ≈⟨ extendʳ w-now ⟩
i₁ ∘ π₁ ∘ ⟨ id , ! ⟩ ≈⟨ elimʳ project₁ ⟩
i₁ ≈˘⟨ inject₁ ○ identityʳ ⟩
(id +₁ ⟨ D.μ.η X , D₁ ! ⟩) ∘ i₁ ≈˘⟨ pullʳ unitlaw ⟩
((id +₁ ⟨ D.μ.η X , D₁ ! ⟩) ∘ out) ∘ now ∎
later-helper : (w ∘ ⟨ D.μ.η X , D₁ ! ⟩) ∘ later ≈ ((id +₁ ⟨ D.μ.η X , D₁ ! ⟩) ∘ out) ∘ later
later-helper = begin
(w ∘ ⟨ D.μ.η X , D₁ ! ⟩) ∘ later ≈⟨ pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ (sym identityˡ) (sym (later-extend-comm (now ∘ !))) ○ sym ×₁∘⟨⟩) ⟩
w ∘ (id ×₁ later) ∘ ⟨ D.μ.η X ∘ later , D₁ ! ⟩ ≈⟨ extendʳ w-later ⟩
i₂ ∘ (earlier ×₁ id) ∘ ⟨ D.μ.η X ∘ later , D₁ ! ⟩ ≈⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ (∘-resp-≈ʳ (sym (later-extend-comm id)) ○ cancelˡ earlier∘later) identityˡ) ⟩
i₂ ∘ ⟨ D.μ.η X , D₁ ! ⟩ ≈˘⟨ inject₂ ⟩
(id +₁ ⟨ D.μ.η X , D₁ ! ⟩) ∘ i₂ ≈˘⟨ pullʳ laterlaw ⟩
((id +₁ ⟨ D.μ.η X , D₁ ! ⟩) ∘ out) ∘ later ∎
w-u-commute : ∀ (h : X × N ⇒ D₀ X) → h ∘ (id ×₁ s⁻¹) ≈ earlier ∘ h → w ∘ (extend h ×₁ id) ≈ (extend h +₁ (extend h ×₁ id)) ∘ u
w-u-commute h earlier-s⁻¹ = sym (D-jointly-epic-product case₁ case₂ case₃ case₄)
where
case₁₂ : ((extend h +₁ (extend h ×₁ id)) ∘ u) ∘ (id ×₁ now) ≈ (w ∘ (extend h ×₁ id)) ∘ (id ×₁ now)
case₁₂ = begin
((extend h +₁ (extend h ×₁ id)) ∘ u) ∘ (id ×₁ now) ≈⟨ pullʳ u-now ⟩
(extend h +₁ (extend h ×₁ id)) ∘ i₁ ∘ π₁ ≈⟨ extendʳ inject₁ ⟩
i₁ ∘ extend h ∘ π₁ ≈˘⟨ refl⟩∘⟨ project₁ ⟩
i₁ ∘ π₁ ∘ (extend h ×₁ id) ≈˘⟨ extendʳ w-now ⟩
w ∘ (id ×₁ now) ∘ (extend h ×₁ id) ≈˘⟨ pullʳ (×₁∘×₁ ○ ×₁-cong₂ id-comm id-comm-sym ○ sym ×₁∘×₁) ⟩
(w ∘ (extend h ×₁ id)) ∘ (id ×₁ now) ∎
case₁ : ((extend h +₁ (extend h ×₁ id)) ∘ u) ∘ (now ×₁ now) ≈ (w ∘ (extend h ×₁ id)) ∘ (now ×₁ now)
case₁ = begin
((extend h +₁ (extend h ×₁ id)) ∘ u) ∘ (now ×₁ now) ≈˘⟨ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ identityˡ identityʳ) ⟩
((extend h +₁ (extend h ×₁ id)) ∘ u) ∘ (id ×₁ now) ∘ (now ×₁ id) ≈⟨ extendʳ case₁₂ ⟩
(w ∘ (extend h ×₁ id)) ∘ (id ×₁ now) ∘ (now ×₁ id) ≈⟨ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ identityˡ identityʳ) ⟩
(w ∘ (extend h ×₁ id)) ∘ (now ×₁ now) ∎
case₂ : ((extend h +₁ (extend h ×₁ id)) ∘ u) ∘ (later ×₁ now) ≈ (w ∘ (extend h ×₁ id)) ∘ (later ×₁ now)
case₂ = begin
((extend h +₁ (extend h ×₁ id)) ∘ u) ∘ (later ×₁ now) ≈˘⟨ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ identityˡ identityʳ) ⟩
((extend h +₁ (extend h ×₁ id)) ∘ u) ∘ (id ×₁ now) ∘ (later ×₁ id) ≈⟨ extendʳ case₁₂ ⟩
(w ∘ (extend h ×₁ id)) ∘ (id ×₁ now) ∘ (later ×₁ id) ≈⟨ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ identityˡ identityʳ) ⟩
(w ∘ (extend h ×₁ id)) ∘ (later ×₁ now) ∎
case₃ : ((extend h +₁ (extend h ×₁ id)) ∘ u) ∘ (now ×₁ later) ≈ (w ∘ (extend h ×₁ id)) ∘ (now ×₁ later)
case₃ = begin
((extend h +₁ (extend h ×₁ id)) ∘ u) ∘ (now ×₁ later) ≈˘⟨ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ identityˡ identityʳ) ⟩
((extend h +₁ (extend h ×₁ id)) ∘ u) ∘ (id ×₁ later) ∘ (now ×₁ id) ≈⟨ pullʳ (pullˡ (pullʳ (pullʳ (×₁∘×₁ ○ ×₁-cong₂ identity² laterlaw)))) ⟩
(extend h +₁ (extend h ×₁ id)) ∘ ([ (i₁ ∘ π₁) , [ i₂ ∘ (now ∘ (id ×₁ s⁻¹) ×₁ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (out ×₁ id) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ i₂)) ∘ (now ×₁ id) ≈⟨ refl⟩∘⟨ ((refl⟩∘⟨ distributeˡ⁻¹-i₂) ⟩∘⟨refl) ⟩
(extend h +₁ (extend h ×₁ id)) ∘ ([ (i₁ ∘ π₁) , [ i₂ ∘ (now ∘ (id ×₁ s⁻¹) ×₁ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (out ×₁ id) ] ∘ i₂) ∘ (now ×₁ id) ≈⟨ refl⟩∘⟨ (∘-resp-≈ˡ inject₂ ○ assoc²βε) ⟩
(extend h +₁ (extend h ×₁ id)) ∘ [ i₂ ∘ (now ∘ (id ×₁ s⁻¹) ×₁ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (out ×₁ id) ∘ (now ×₁ id) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ unitlaw identity²) ⟩
(extend h +₁ (extend h ×₁ id)) ∘ [ i₂ ∘ (now ∘ (id ×₁ s⁻¹) ×₁ id) , i₂ ] ∘ distributeʳ⁻¹ ∘ (i₁ ×₁ id) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ distributeʳ⁻¹-i₁ ⟩
(extend h +₁ (extend h ×₁ id)) ∘ [ i₂ ∘ (now ∘ (id ×₁ s⁻¹) ×₁ id) , i₂ ] ∘ i₁ ≈⟨ refl⟩∘⟨ inject₁ ⟩
(extend h +₁ (extend h ×₁ id)) ∘ i₂ ∘ (now ∘ (id ×₁ s⁻¹) ×₁ id) ≈⟨ extendʳ inject₂ ⟩
i₂ ∘ (extend h ×₁ id) ∘ (now ∘ (id ×₁ s⁻¹) ×₁ id) ≈⟨ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ (pullˡ DK.identityʳ) identity²) ⟩
i₂ ∘ (h ∘ (id ×₁ s⁻¹) ×₁ id) ≈⟨ refl⟩∘⟨ ×₁-cong₂ earlier-s⁻¹ refl ⟩
i₂ ∘ (earlier ∘ h ×₁ id) ≈˘⟨ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ refl identity²) ⟩
i₂ ∘ (earlier ×₁ id) ∘ (h ×₁ id) ≈˘⟨ extendʳ w-later ⟩
w ∘ (id ×₁ later) ∘ (h ×₁ id) ≈˘⟨ pullʳ (×₁∘×₁ ○ ×₁-cong₂ (DK.identityʳ ○ sym identityˡ) id-comm-sym ○ sym ×₁∘×₁) ⟩
(w ∘ (extend h ×₁ id)) ∘ (now ×₁ later) ∎
case₄ : ((extend h +₁ (extend h ×₁ id)) ∘ u) ∘ (later ×₁ later) ≈ (w ∘ (extend h ×₁ id)) ∘ (later ×₁ later)
case₄ = begin
((extend h +₁ (extend h ×₁ id)) ∘ u) ∘ (later ×₁ later) ≈⟨ pullʳ u-later ⟩
(extend h +₁ (extend h ×₁ id)) ∘ i₂ ≈⟨ inject₂ ⟩
i₂ ∘ (extend h ×₁ id) ≈˘⟨ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ (∘-resp-≈ʳ (sym (later-extend-comm h)) ○ cancelˡ earlier∘later) identity²) ⟩
i₂ ∘ (earlier ×₁ id) ∘ (extend h ∘ later ×₁ id) ≈˘⟨ extendʳ w-later ⟩
w ∘ (id ×₁ later) ∘ (extend h ∘ later ×₁ id) ≈˘⟨ pullʳ (×₁∘×₁ ○ ×₁-cong₂ (sym identityˡ) id-comm-sym ○ sym ×₁∘×₁) ⟩
(w ∘ (extend h ×₁ id)) ∘ (later ×₁ later) ∎
coit-w-u-commute-ι : coit w ∘ (extend ι ×₁ id) ≈ D₁ (extend ι) ∘ coit u
coit-w-u-commute-ι = begin
coit w ∘ (extend ι ×₁ id) ≈˘⟨ coit-unique ((extend ι +₁ id) ∘ u) (coit w ∘ (extend ι ×₁ id)) unique₁ ⟩
coit ((extend ι +₁ id) ∘ u) ≈⟨ coit-unique ((extend ι +₁ id) ∘ u) (D₁ (extend ι) ∘ coit u) unique₂ ⟩
D₁ (extend ι) ∘ coit u ∎
where
earlier-s⁻¹ : ι ∘ (id ×₁ s⁻¹) ≈ earlier ∘ ι {X}
earlier-s⁻¹ = begin
ι ∘ (id ×₁ s⁻¹) ≈⟨ PNNO-jointly-epic IB IS ⟩
earlier ∘ ι {X} ∎
where
IB : (ι ∘ (id ×₁ s⁻¹)) ∘ ⟨ id , z ∘ ! ⟩ ≈ (earlier ∘ ι {X}) ∘ ⟨ id , z ∘ ! ⟩
IB = begin
(ι ∘ (id ×₁ s⁻¹)) ∘ ⟨ id , z ∘ ! ⟩ ≈⟨ pullʳ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identity² (pullˡ s⁻¹-zero)) ⟩
ι ∘ ⟨ id , z ∘ ! ⟩ ≈⟨ ι-zero ⟩
now ≈˘⟨ inject₁ ⟩
[ now , id ] ∘ i₁ ≈˘⟨ pullʳ unitlaw ⟩
([ now , id ] ∘ out) ∘ now ≈˘⟨ pullʳ ι-zero ⟩
(earlier ∘ ι {X}) ∘ ⟨ id , z ∘ ! ⟩ ∎
IS : (ι ∘ (id ×₁ s⁻¹)) ∘ (id ×₁ s) ≈ (earlier ∘ ι {X}) ∘ (id ×₁ s)
IS = begin
(ι ∘ (id ×₁ s⁻¹)) ∘ (id ×₁ s) ≈⟨ cancelʳ (×₁∘×₁ ○ ×₁-cong₂ identity² s⁻¹-succ ○ ⟨⟩-unique id-comm id-comm) ⟩
ι ≈˘⟨ cancelˡ earlier∘later ⟩
earlier ∘ later ∘ ι ≈˘⟨ pullʳ ι-succ ⟩
(earlier ∘ ι) ∘ (id ×₁ s) ∎
unique₁ : out ∘ coit w ∘ (extend ι ×₁ id) ≈ (id +₁ coit w ∘ (extend ι ×₁ id)) ∘ (extend ι +₁ id) ∘ u
unique₁ = begin
out ∘ coit w ∘ (extend ι ×₁ id) ≈⟨ extendʳ (coit-commutes w) ⟩
(id +₁ coit w) ∘ w ∘ (extend ι ×₁ id) ≈⟨ refl⟩∘⟨ w-u-commute ι earlier-s⁻¹ ⟩
(id +₁ coit w) ∘ (extend ι +₁ (extend ι ×₁ id)) ∘ u ≈⟨ extendʳ (+₁∘+₁ ○ +₁-cong₂ refl (sym identityʳ) ○ sym +₁∘+₁) ⟩
(id +₁ coit w ∘ (extend ι ×₁ id)) ∘ (extend ι +₁ id) ∘ u ∎
unique₂ : out ∘ D₁ (extend ι) ∘ coit u ≈ (id +₁ D₁ (extend ι) ∘ coit u) ∘ (extend ι +₁ id) ∘ u
unique₂ = begin
out ∘ D₁ (extend ι) ∘ coit u ≈⟨ extendʳ (D₁-commutes (extend ι)) ⟩
(extend ι +₁ D₁ (extend ι)) ∘ out ∘ coit u ≈⟨ refl⟩∘⟨ (coit-commutes u) ⟩
(extend ι +₁ D₁ (extend ι)) ∘ (id +₁ coit u) ∘ u ≈⟨ extendʳ (+₁∘+₁ ○ +₁-cong₂ id-comm (sym identityʳ) ○ sym +₁∘+₁) ⟩
(id +₁ D₁ (extend ι) ∘ coit u) ∘ (extend ι +₁ id) ∘ u ∎
coit-w-u-commute-Dπ₁ : coit w ∘ (D₁ π₁ ×₁ id) ≈ D₁ (D₁ π₁) ∘ coit u
coit-w-u-commute-Dπ₁ = begin
coit w ∘ (D₁ π₁ ×₁ id) ≈˘⟨ coit-unique ((D₁ π₁ +₁ id) ∘ u) (coit w ∘ (D₁ π₁ ×₁ id)) unique₁ ⟩
coit ((D₁ π₁ +₁ id) ∘ u) ≈⟨ coit-unique ((D₁ π₁ +₁ id) ∘ u) (D₁ (D₁ π₁) ∘ coit u) unique₂ ⟩
D₁ (D₁ π₁) ∘ coit u ∎
where
earlier-s⁻¹ : (now ∘ π₁) ∘ (id ×₁ s⁻¹) ≈ earlier ∘ (now ∘ π₁)
earlier-s⁻¹ = begin
(now ∘ π₁) ∘ (id ×₁ s⁻¹) ≈⟨ pullʳ (project₁ ○ identityˡ) ⟩
now ∘ π₁ ≈˘⟨ pullˡ earlier∘now ⟩
earlier ∘ (now ∘ π₁) ∎
unique₁ : out ∘ coit w ∘ (D₁ π₁ ×₁ id) ≈ (id +₁ coit w ∘ (D₁ π₁ ×₁ id)) ∘ (D₁ π₁ +₁ id) ∘ u
unique₁ = begin
out ∘ coit w ∘ (D₁ π₁ ×₁ id) ≈⟨ extendʳ (coit-commutes w) ⟩
(id +₁ coit w) ∘ w ∘ (D₁ π₁ ×₁ id) ≈⟨ refl⟩∘⟨ (w-u-commute (now ∘ π₁) earlier-s⁻¹) ⟩
(id +₁ coit w) ∘ (D₁ π₁ +₁ (D₁ π₁ ×₁ id)) ∘ u ≈⟨ extendʳ (+₁∘+₁ ○ +₁-cong₂ refl (sym identityʳ) ○ sym +₁∘+₁) ⟩
(id +₁ coit w ∘ (D₁ π₁ ×₁ id)) ∘ (D₁ π₁ +₁ id) ∘ u ∎
unique₂ : out ∘ D₁ (D₁ π₁) ∘ coit u ≈ (id +₁ D₁ (D₁ π₁) ∘ coit u) ∘ (D₁ π₁ +₁ id) ∘ u
unique₂ = begin
out ∘ D₁ (D₁ π₁) ∘ coit u ≈⟨ extendʳ (D₁-commutes (D₁ π₁)) ⟩
(D₁ π₁ +₁ D₁ (D₁ π₁)) ∘ out ∘ coit u ≈⟨ refl⟩∘⟨ (coit-commutes u) ⟩
(D₁ π₁ +₁ D₁ (D₁ π₁)) ∘ (id +₁ coit u) ∘ u ≈⟨ extendʳ (+₁∘+₁ ○ +₁-cong₂ id-comm (sym identityʳ) ○ sym +₁∘+₁) ⟩
(id +₁ D₁ (D₁ π₁) ∘ coit u) ∘ (D₁ π₁ +₁ id) ∘ u ∎
coit-w-ρ : D₁ ρ ∘ coit w ≈ D₁ π₁ ∘ τ ∘ (ρ ×₁ id)
coit-w-ρ = begin
D₁ ρ ∘ coit w ≈˘⟨ coit-unique ((ρ +₁ id) ∘ w) (D₁ ρ ∘ coit w) unique₁ ⟩
coit ((ρ +₁ id) ∘ w) ≈⟨ coit-unique ((ρ +₁ id) ∘ w) (D₁ π₁ ∘ τ ∘ (ρ ×₁ id)) unique₂ ⟩
D₁ π₁ ∘ τ ∘ (ρ ×₁ id) ∎
where
unique₁ : out ∘ D₁ ρ ∘ coit w ≈ (id +₁ D₁ ρ ∘ coit w) ∘ (ρ +₁ id) ∘ w
unique₁ = begin
out ∘ D₁ ρ ∘ coit w ≈⟨ extendʳ (D₁-commutes ρ) ⟩
(ρ +₁ D₁ ρ) ∘ out ∘ coit w ≈⟨ refl⟩∘⟨ coit-commutes w ⟩
(ρ +₁ D₁ ρ) ∘ (id +₁ coit w) ∘ w ≈⟨ extendʳ (+₁∘+₁ ○ +₁-cong₂ id-comm (sym identityʳ) ○ sym +₁∘+₁) ⟩
(id +₁ D₁ ρ ∘ coit w) ∘ (ρ +₁ id) ∘ w ∎
unique₂ : out ∘ D₁ π₁ ∘ τ ∘ (ρ ×₁ id) ≈ (id +₁ D₁ π₁ ∘ τ ∘ (ρ ×₁ id)) ∘ (ρ +₁ id) ∘ w
unique₂ = begin
out ∘ D₁ π₁ ∘ τ ∘ (ρ ×₁ id) ≈⟨ extendʳ (D₁-commutes π₁) ⟩
(π₁ +₁ D₁ π₁) ∘ out ∘ τ ∘ (ρ ×₁ id) ≈⟨ refl⟩∘⟨ extendʳ τ-commutes ⟩
(π₁ +₁ D₁ π₁) ∘ (id +₁ τ) ∘ (distributeˡ⁻¹ ∘ (id ×₁ out)) ∘ (ρ ×₁ id) ≈⟨ extendʳ (+₁∘+₁ ○ +₁-cong₂ id-comm (sym identityʳ) ○ sym +₁∘+₁) ⟩
(id +₁ D₁ π₁ ∘ τ) ∘ (π₁ +₁ id) ∘ (distributeˡ⁻¹ ∘ (id ×₁ out)) ∘ (ρ ×₁ id) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (pullʳ (×₁∘×₁ ○ ×₁-cong₂ identityˡ identityʳ)) ⟩
(id +₁ D₁ π₁ ∘ τ) ∘ (π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (ρ ×₁ out) ≈⟨ refl⟩∘⟨ helper ⟩
(id +₁ D₁ π₁ ∘ τ) ∘ (ρ +₁ (ρ ×₁ id)) ∘ w ≈⟨ extendʳ (+₁∘+₁ ○ +₁-cong₂ refl (assoc ○ sym identityʳ) ○ sym +₁∘+₁) ⟩
(id +₁ D₁ π₁ ∘ τ ∘ (ρ ×₁ id)) ∘ (ρ +₁ id) ∘ w ∎
where
helper : (π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (ρ ×₁ out) ≈ (ρ +₁ (ρ ×₁ id)) ∘ w
helper = sym (begin
(ρ +₁ (ρ ×₁ id)) ∘ [ i₁ ∘ π₁ , i₂ ∘ (earlier ×₁ id) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ out) ≈⟨ pullˡ (∘[] ○ []-cong₂ (extendʳ inject₁) (extendʳ inject₂ ○ ∘-resp-≈ʳ (×₁∘×₁ ○ ×₁-cong₂ refl identity²))) ⟩
[ i₁ ∘ ρ ∘ π₁ , i₂ ∘ (ρ ∘ earlier ×₁ id) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ out) ≈˘⟨ ([]-cong₂ (∘-resp-≈ʳ project₁) (∘-resp-≈ʳ (×₁-cong₂ (sym ρ-earlier) refl))) ⟩∘⟨refl ⟩
[ i₁ ∘ π₁ ∘ (ρ ×₁ id) , i₂ ∘ (ρ ×₁ id) ] ∘ distributeˡ⁻¹ ∘ (id ×₁ out) ≈˘⟨ pullˡ ([]∘+₁ ○ []-cong₂ assoc refl) ⟩
[ i₁ ∘ π₁ , i₂ ] ∘ (ρ ×₁ id +₁ ρ ×₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) ≈⟨ refl⟩∘⟨ (extendʳ (distributeˡ⁻¹-natural ρ id id)) ⟩
[ i₁ ∘ π₁ , i₂ ] ∘ distributeˡ⁻¹ ∘ (ρ ×₁ (id +₁ id)) ∘ (id ×₁ out) ≈⟨ ([]-cong₂ refl (sym identityʳ)) ⟩∘⟨ ∘-resp-≈ʳ (×₁∘×₁ ○ ×₁-cong₂ identityʳ (elimˡ ([]-unique id-comm-sym id-comm-sym))) ⟩
(π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (ρ ×₁ out) ∎)
3⇒1 : (∀ X → cond-3 X) → cond-1
3⇒1 c-3 X = record
{ equality = sym D.F.homomorphism ○ D.F.F-resp-≈ (Coequalizer.equality (coeqs X)) ○ D.F.homomorphism
; coequalize = b
; universal = λ {Z} {h} {eq} → universal' eq
; unique = λ {Z} {h} {i} {eq} i-universal → epi-Dρ (Search-Algebra.search-algebra-on (Elgot⇒Search (record { A = Ď₀ X ; algebra = elgot }))) i (b eq) (sym i-universal ○ universal' eq)
}
where
open cond-3 (c-3 X) using (elgot; ρ-algebra-morphism)
open Search-Algebra (Elgot⇒Search (record { A = Ď₀ X ; algebra = elgot })) using (α)
open import Monad.Instance.Delay.Quotient.Epis distributive DM PNNO DQ
module CP = IsCoequalizer (coeq-productsˡ {X} {D₀ ⊤} (id))
module _ {Y : Obj} {a : D₀ (D₀ X) ⇒ Y} (eq : a ∘ D₁ (extend ι) ≈ a ∘ D₁ (D₁ π₁)) where
c : Ď₀ X × D₀ ⊤ ⇒ Y
c = CP.coequalize (begin
(a ∘ coit w) ∘ (extend ι ×₁ id) ≈⟨ pullʳ coit-w-u-commute-ι ⟩
a ∘ D₁ (extend ι) ∘ coit u ≈⟨ extendʳ eq ⟩
a ∘ D₁ (D₁ π₁) ∘ coit u ≈˘⟨ pullʳ coit-w-u-commute-Dπ₁ ⟩
(a ∘ coit w) ∘ (D₁ π₁ ×₁ id) ∎)
b : D₀ (Ď₀ X) ⇒ Y
b = c ∘ ⟨ α , D₁ ! ⟩
universal' : a ≈ b ∘ D₁ ρ
universal' = sym (begin
b ∘ D₁ ρ ≈⟨ introʳ coit-w-retract ⟩
(b ∘ D₁ ρ) ∘ coit w ∘ ⟨ D.μ.η _ , D₁ ! ⟩ ≈⟨ pullʳ (extendʳ coit-w-ρ) ⟩
b ∘ D₁ π₁ ∘ (τ ∘ (ρ ×₁ id)) ∘ ⟨ D.μ.η _ , D₁ ! ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullʳ upper-square ⟩
(c ∘ ⟨ α , D₁ ! ⟩) ∘ D₁ π₁ ∘ τ ∘ ⟨ α , D₁ ! ⟩ ∘ D₁ ρ ≈⟨ refl⟩∘⟨ (sym-assoc ○ cancelˡ (assoc ○ retract-helper)) ⟩
(c ∘ ⟨ α , D₁ ! ⟩) ∘ D₁ ρ ≈⟨ pullʳ (sym upper-square) ⟩
c ∘ (ρ ×₁ id) ∘ ⟨ D.μ.η _ , D₁ ! ⟩ ≈˘⟨ extendʳ CP.universal ⟩
a ∘ coit w ∘ ⟨ D.μ.η _ , D₁ ! ⟩ ≈⟨ elimʳ coit-w-retract ⟩
a ∎)
where
open import Algebra.Search.Retraction distributive DM using (tau-retract)
retract-helper : D₁ π₁ ∘ τ ∘ ⟨ α , D₁ ! ⟩ ≈ id
retract-helper = begin
D₁ π₁ ∘ τ ∘ ⟨ α , D₁ ! ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ elimʳ (sym D.F.homomorphism ○ D.F.F-resp-≈ (Iso.isoʳ (_≅_.iso A×⊤≅A)) ○ D.F.identity) ⟩
D₁ π₁ ∘ τ ∘ ⟨ α , D₁ ! ⟩ ∘ D₁ π₁ ∘ D₁ ⟨ id , ! ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (⟨⟩∘ ○ ⟨⟩-congˡ (sym D.F.homomorphism ○ D.F.F-resp-≈ !-unique₂)) ⟩
D₁ π₁ ∘ τ ∘ ⟨ α ∘ D₁ π₁ , D₁ π₂ ⟩ ∘ D₁ ⟨ id , ! ⟩ ≈⟨ refl⟩∘⟨ (cancelˡ (Retract.is-retract (tau-retract ⊤ (Elgot⇒Search (record { A = Ď₀ X ; algebra = elgot }))))) ⟩
D₁ π₁ ∘ D₁ ⟨ id , ! ⟩ ≈⟨ sym D.F.homomorphism ○ D.F.F-resp-≈ (Iso.isoʳ (_≅_.iso A×⊤≅A)) ○ D.F.identity ⟩
id ∎
upper-square : (ρ ×₁ id) ∘ ⟨ D.μ.η _ , D₁ ! ⟩ ≈ ⟨ α , D₁ ! ⟩ ∘ D₁ ρ
upper-square = ×₁∘⟨⟩ ○ ⟨⟩-cong₂ ρ-algebra-morphism (identityˡ ○ D.F.F-resp-≈ (!-unique (! ∘ ρ)) ○ D.F.homomorphism) ○ sym ⟨⟩∘