{-# OPTIONS --lossy-unification #-}
open import Level
open import Categories.Category.Core
open import Categories.Functor hiding (id)
open import Categories.Monad hiding (id)
open import Categories.Monad.Construction.Kleisli
open import Categories.Monad.Relative renaming (Monad to RMonad)
open import Data.Product using (_,_; Σ; Σ-syntax)
open import Categories.Functor.Algebra
open import Categories.Functor.Coalgebra
open import Categories.Object.Terminal
open import Categories.NaturalTransformation.Core hiding (id)
open import Object.FreeObject
open import Categories.Category.Distributive
open import Categories.Object.NaturalNumbers.Parametrized
open import Categories.Functor.Properties using ([_]-resp-Iso)
open import Categories.Category.Construction.EilenbergMoore using (Module)
open import Categories.Monad.Strong
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.Theorem.Condition2-3 {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
  open Bundles 
  open import Algebra.Elgot cocartesian
  open import Algebra.Elgot.Free cocartesian
  open import Algebra.Elgot.Stable distributive
  open F-Coalgebra-Morphism using () renaming (f to u; commutes to coalg-commutes)

  open DelayM DM
  open import Monad.Instance.Delay.Strong distributive DM
  open D-Kleisli
  open D-Monad
  open D-Strong
  open Coit
  open τ-mod
  open ParametrizedNNO PNNO hiding (η)

  open import Algebra.Search cocartesian DM
  open import Category.Construction.ElgotAlgebras cocartesian
  open import Algebra.Search.Retraction distributive DM

  open HomReasoning
  open M C
  open MR C
  open MP C using (Iso⇒Epi; Iso-swap; Iso⇒Mono)
  open Equiv
  open import Monad.Instance.Delay.Iota distributive DM PNNO
  open import Algebra.Search.Properties cocartesian
  open DelayQ DQ
  open import Monad.Instance.Delay.Quotient.Theorem.Conditions distributive DM PNNO DQ
  open import Monad.Helper
  open import Algebra.Elgot.MoreProperties distributive DM PNNO
  open IsFreeObject
  open Elgot-Algebra-Morphism using () renaming (h to EA-h; preserves to EA-preserves)
  open import Monad.Instance.Delay.Quotient.Epis distributive DM PNNO DQ

  open cond-3

  private
    elgot' : ∀ {X} → cond-2 X → Elgot-Algebra-on (Ď₀ X)
    elgot' {X} c-2 = D-Algebra+Search⇒Elgot DM (record 
      { A = Ď₀ X 
      ; action = α 
      ; commute = epi-DDρ s-alg-on (α ∘ D₁ α) (α ∘ extend (id)) (sym epi-helper)
      ; identity = identity₁ 
      }) (Search-Algebra-on⇒IsSearchAlgebra s-alg-on)
      where
      open cond-2 c-2 renaming (ρ-algebra-morphism to ρ-algebra-morphism-2)
      open Search-Algebra-on s-alg-on
      s-alg : Search-Algebra
      s-alg = record { A = Ď₀ X ; search-algebra-on = s-alg-on }
      μ∘Dμ : ∀ {X} → D.μ.η X ∘ D.μ.η (D₀ X) ≈ D.μ.η X ∘ D₁ (D.μ.η X)
      μ∘Dμ {X} = begin 
        D.μ.η X ∘ D.μ.η (D₀ X)                       ≈⟨ sym DK.assoc ⟩ 
        extend (extend id ∘ id)                ≈⟨ extend-≈ identityʳ ⟩ 
        extend (extend id)                      ≈⟨ extend-≈ (introˡ DK.identityʳ) ⟩ 
        extend ((extend id ∘ now) ∘ extend id) ≈⟨ extend-≈ assoc ⟩ 
        extend (extend id ∘ now ∘ extend id)   ≈⟨ DK.assoc ⟩ 
        D.μ.η X ∘ D₁ (D.μ.η X)                       ∎
      epi-helper : (α ∘ D.μ.η (Ď₀ X)) ∘ D₁ (D₁ ρ) ≈ (α ∘ D₁ α) ∘ D₁ (D₁ ρ)
      epi-helper = begin 
        (α ∘ D.μ.η (Ď₀ X)) ∘ D₁ (D₁ ρ) ≈⟨ pullʳ (D.μ.commute ρ) ⟩
        α ∘ D₁ ρ ∘ D.μ.η (D₀ X)        ≈⟨ pullˡ (sym ρ-algebra-morphism-2) ⟩
        (ρ ∘ D.μ.η X) ∘ D.μ.η (D₀ X)     ≈⟨ pullʳ μ∘Dμ ⟩
        ρ ∘ D.μ.η X ∘ D₁ (D.μ.η X)       ≈⟨ pullˡ ρ-algebra-morphism-2 ⟩
        (α ∘ D₁ ρ) ∘ D₁ (D.μ.η X)      ≈⟨ pullʳ (sym D.F.homomorphism) ⟩
        α ∘ D₁ (ρ ∘ D.μ.η X)           ≈⟨ (refl⟩∘⟨ (D.F.F-resp-≈ ρ-algebra-morphism-2)) ⟩
        α ∘ D₁ (α ∘ D₁ ρ)            ≈⟨ (refl⟩∘⟨ D.F.homomorphism) ⟩
        α ∘ D₁ α ∘ D₁ (D₁ ρ)         ≈⟨ sym-assoc ⟩
        (α ∘ D₁ α) ∘ D₁ (D₁ ρ)       ∎

    module Stable (X : Obj) (c-2 : ∀ Y → cond-2 Y) where
      open cond-2 (c-2 X) renaming (ρ-algebra-morphism to ρ-algebra-morphism-2)
      open Search-Algebra-on s-alg-on using (α)
      abstract
        ρ-law' : ρ ≈ α ∘ coit ((ρ ∘ now +₁ id) ∘ out)
        ρ-law' = begin 
          ρ                                ≈⟨ introʳ D.identityˡ ⟩ 
          ρ ∘ D.μ.η _ ∘ D₁ now               ≈⟨ extendʳ ρ-algebra-morphism-2 ⟩ 
          α ∘ D₁ ρ ∘ D₁ now                ≈˘⟨ refl⟩∘⟨ D.F.homomorphism ⟩ 
          α ∘ D₁ (ρ ∘ now)                 ≈˘⟨ refl⟩∘⟨ coit-unique ((ρ ∘ now +₁ id) ∘ out) (D₁ (ρ ∘ now)) coit-helper ⟩ 
          α ∘ coit ((ρ ∘ now +₁ id) ∘ out) ∎
          where
          coit-helper : out {Ď₀ X} ∘ D₁ {X} {Ď₀ X} (ρ ∘ now {X}) ≈ (id +₁ D₁ (ρ ∘ now)) ∘ (ρ ∘ now +₁ id) ∘ out
          coit-helper = begin 
            out {Ď₀ X} ∘ D₁ {X} {Ď₀ X} (ρ ∘ now)                           ≈⟨ D₁-commutes (ρ ∘ now) ⟩ 
            (ρ ∘ now +₁ D₁ (ρ ∘ now)) ∘ out              ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟩ 
            (id {Ď₀ X} +₁ D₁ (ρ ∘ now)) ∘ (ρ ∘ now +₁ id) ∘ out ∎
        module _ {Y : Obj} (EA : Elgot-Algebra) (f : Y × X ⇒ Elgot-Algebra.A EA) where
          open IsCoequalizer (coeq-productsʳ {X} {Y} (id {Y})) using () renaming (coequalize to prod-coequalize; universal to prod-universal)
          open Search-Algebra (Elgot⇒Search DM EA) using (A) renaming (α to a)
          open Module (Elgot⇒D-Algebra DM EA)
          abstract
            f-coequalize : (a ∘ D₁ f ∘ τ) ∘ (id ⁂ extend ι) ≈ (a ∘ D₁ f ∘ τ) ∘ (id ⁂ D₁ π₁)
            f-coequalize = begin 
              (a ∘ D₁ f ∘ τ) ∘ (id ⁂ extend ι)           ≈⟨ pullʳ (pullʳ help) ⟩ 
              a ∘ D₁ f ∘ extend ι ∘ D₁ assocʳ ∘ τ        ≈˘⟨ refl⟩∘⟨ extendʳ (extend∘F₁' kleisli ι (f ⁂ id) ○ extend-≈ (ι-natural f) ○ sym (F₁∘extend' kleisli f ι)) ⟩
              a ∘ extend ι ∘ D₁ (f ⁂ id) ∘ D₁ assocʳ ∘ τ ≈⟨ extendʳ (α-coequalize EA) ⟩
              a ∘ D₁ π₁ ∘ D₁ (f ⁂ id) ∘ D₁ assocʳ ∘ τ    ≈⟨ refl⟩∘⟨ extendʳ (sym D.F.homomorphism ○ D.F.F-resp-≈ project₁ ○ D.F.homomorphism) ⟩
              a ∘ D₁ f ∘ D₁ π₁ ∘ D₁ assocʳ ∘ τ           ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ D.F.homomorphism ⟩ 
              a ∘ D₁ f ∘ D₁ (π₁ ∘ assocʳ) ∘ τ            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ((D.F.F-resp-≈ (project₁ ○ ⟨⟩-cong₂ (sym identityˡ) refl)) ⟩∘⟨refl) ⟩ 
              a ∘ D₁ f ∘ D₁ (id ⁂ π₁) ∘ τ                ≈˘⟨ pullʳ (pullʳ (τ-natural id π₁)) ⟩ 
              (a ∘ D₁ f ∘ τ) ∘ (id ⁂ D₁ π₁)              ∎
              where
              τ-ι : ∀ {X Y} → τ {X} {Y} ∘ (id ⁂ ι {Y}) ≈ ι {X × Y} ∘ assocʳ
              τ-ι {X} {Y} = Iso⇒Epi (Iso-swap (_≅_.iso ×-assoc)) (τ ∘ (id ⁂ ι)) (ι ∘ assocʳ) (begin 
                (τ ∘ (id ⁂ ι)) ∘ assocˡ ≈⟨ pullʳ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl) ⟩ 
                τ ∘ ⟨ π₁ ∘ π₁ , ι ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈˘⟨ ι-unique (τ ∘ ⟨ π₁ ∘ π₁ , ι ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) IB₁ IS₁ ⟩ 
                ι ≈˘⟨ cancelʳ assocʳ∘assocˡ ⟩ 
                (ι ∘ assocʳ) ∘ assocˡ ∎)
                where
                IB₁ : (τ {X} {Y} ∘ ⟨ π₁ ∘ π₁ , ι ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ ⟨ id , z ∘ Terminal.! terminal ⟩ ≈ now
                IB₁ = begin 
                  (τ ∘ ⟨ π₁ ∘ π₁ , ι ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ ⟨ id , z ∘ Terminal.! terminal ⟩ ≈⟨ pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ (cancelʳ project₁) (pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ (cancelʳ project₁) project₂))) ⟩ 
                  τ ∘ ⟨ π₁ , ι ∘ ⟨ π₂ , z ∘ Terminal.! terminal ⟩ ⟩                           ≈˘⟨ refl⟩∘⟨ ⟨⟩-cong₂ refl (∘-resp-≈ʳ (⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ (pullʳ (sym (Terminal.!-unique terminal (Terminal.! terminal ∘ π₂)))))) ⟩ 
                  τ ∘ ⟨ π₁ , ι ∘ ⟨ id , z ∘ Terminal.! terminal ⟩ ∘ π₂ ⟩                      ≈⟨ (refl⟩∘⟨ (⟨⟩-cong₂ refl (pullˡ ι-zero))) ⟩ 
                  τ ∘ ⟨ π₁ , now ∘ π₂ ⟩                                                       ≈˘⟨ (refl⟩∘⟨ (⟨⟩-cong₂ identityˡ refl)) ⟩ 
                  τ ∘ (id ⁂ now)                                                              ≈⟨ τ-now ⟩ 
                  now                                                                         ∎
                IS₁ : (τ {X} {Y} ∘ ⟨ π₁ ∘ π₁ , ι ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (id ⁂ s) ≈ later ∘ τ ∘ ⟨ π₁ ∘ π₁ , ι ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩
                IS₁ = begin 
                  (τ ∘ ⟨ π₁ ∘ π₁ , ι ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (id ⁂ s)   ≈⟨ pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ (project₁ ○ identityˡ)) (pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ (project₁ ○ identityˡ)) project₂))) ⟩ 
                  τ ∘ ⟨ π₁ ∘ π₁ , ι ∘ ⟨ π₂ ∘ π₁ , s ∘ π₂ ⟩ ⟩            ≈˘⟨ (refl⟩∘⟨ (⟨⟩-cong₂ refl (refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl)))) ⟩ 
                  τ ∘ ⟨ π₁ ∘ π₁ , ι ∘ (id ⁂ s) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩     ≈⟨ (refl⟩∘⟨ (⟨⟩-cong₂ refl (extendʳ ι-succ))) ⟩ 
                  τ ∘ ⟨ π₁ ∘ π₁ , later ∘ ι ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩        ≈˘⟨ (refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl)) ⟩ 
                  τ ∘ (id ⁂ later) ∘ ⟨ π₁ ∘ π₁ , ι ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ extendʳ τ-later ⟩ 
                  later ∘ τ ∘ ⟨ π₁ ∘ π₁ , ι ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩        ∎
              help : τ {Y} {X} ∘ (id ⁂ extend ι) ≈ extend ι ∘ D₁ assocʳ ∘ τ
              help = begin 
                τ ∘ (id ⁂ extend ι)              ≈˘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identity² (sym (extend⇒F₁ kleisli ι))) ⟩
                τ ∘ (id ⁂ D.μ.η _) ∘ (id ⁂ D₁ ι)   ≈⟨ extendʳ (sym strength.μ-η-comm) ⟩
                D.μ.η _ ∘ (D₁ τ ∘ τ) ∘ (id ⁂ D₁ ι) ≈⟨ refl⟩∘⟨ pullʳ (τ-natural id ι) ⟩
                D.μ.η _ ∘ D₁ τ ∘ D₁ (id ⁂ ι) ∘ τ   ≈⟨ refl⟩∘⟨ (extendʳ (sym D.F.homomorphism ○ D.F.F-resp-≈ τ-ι ○ D.F.homomorphism)) ⟩
                D.μ.η _ ∘ D₁ ι ∘ D₁ assocʳ ∘ τ     ≈˘⟨ pushˡ (extend⇒F₁ kleisli ι) ⟩
                extend ι ∘ D₁ assocʳ ∘ τ         ∎

      abstract
        [_,_]♯' : ∀ {Y} (EA : Elgot-Algebra) → Y × X ⇒ Elgot-Algebra.A EA → Y × Ď₀ X ⇒ Elgot-Algebra.A EA
        [_,_]♯' {Y} EA f = prod-coequalize {h = a ∘ D₁ f ∘ τ} (f-coequalize EA f) 
          where
          open IsCoequalizer (coeq-productsʳ {X} {Y} (id {Y})) using () renaming (coequalize to prod-coequalize; universal to prod-universal)
          open Search-Algebra (Elgot⇒Search DM EA) using (A) renaming (α to a)
          open Module (Elgot⇒D-Algebra DM EA)

        ♯-law' : ∀ {Y} {EA : Elgot-Algebra} (f : Y × X ⇒ Elgot-Algebra.A EA) → f ≈ [ EA , f ]♯' ∘ (id ⁂ ρ ∘ now)
        ♯-law' {Y} {EA} f = begin 
          f                                                           ≈⟨ insertˡ identity₁ ⟩ 
          a ∘ now ∘ f                                                 ≈˘⟨ refl⟩∘⟨ DK.identityʳ ⟩ 
          a ∘ D₁ f ∘ now                                              ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ τ-now ⟩ 
          a ∘ D₁ f ∘ τ ∘ (id ⁂ now)                                   ≈˘⟨ (pullˡ (sym (prod-universal {eq = f-coequalize EA f})) ○ assoc²βε) ⟩ 
          prod-coequalize (f-coequalize EA f) ∘ (id ⁂ ρ) ∘ (id ⁂ now) ≈⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identity² refl) ⟩
          prod-coequalize (f-coequalize EA f) ∘ (id ⁂ ρ ∘ now)        ∎
          where
          open IsCoequalizer (coeq-productsʳ {X} {Y} (id {Y})) using () renaming (coequalize to prod-coequalize; universal to prod-universal)
          open Search-Algebra (Elgot⇒Search DM EA) using (A; identity₁) renaming (α to a)
          open Module (Elgot⇒D-Algebra DM EA)

        ♯-unique' : ∀ {Y} {EA : Elgot-Algebra} (f : Y × X ⇒ Elgot-Algebra.A EA) (g : Y × Ď₀ X ⇒ Elgot-Algebra.A EA) → f ≈ g ∘ (id ⁂ ρ ∘ now) → (∀ {Z} {h : Z ⇒ Ď₀ X + Z} → g ∘ (id ⁂ Search-Algebra-on.α s-alg-on ∘ coit h) ≈ Elgot-Algebra._# EA ((g +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h))) → g ≈ [ EA , f ]♯'
        ♯-unique' {Y} {EA} f g g-law g-preserving = prod-unique (sym (begin 
          g ∘ (id ⁂ ρ)                                                        ≈⟨ refl⟩∘⟨ (⁂-cong₂ refl ρ-law') ⟩ 
          g ∘ (id ⁂ α ∘ coit ((ρ ∘ now +₁ id) ∘ out))                         ≈⟨ g-preserving ⟩ 
          ((g +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ (ρ ∘ now +₁ id) ∘ out)) #        ≈˘⟨ #-resp-≈ (∘-resp-≈ʳ (∘-resp-≈ʳ (⁂∘⁂ ○ ⁂-cong₂ identity² refl))) ⟩ 
          ((g +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ (ρ ∘ now +₁ id)) ∘ (id ⁂ out)) # ≈⟨ #-resp-≈ (∘-resp-≈ʳ (extendʳ (sym (distributeˡ⁻¹-natural id (ρ ∘ now) id))) ○ pullˡ (+₁∘+₁ ○ +₁-cong₂ refl (elimʳ (⟨⟩-unique id-comm id-comm)))) ⟩ 
          ((g ∘ (id ⁂ ρ ∘ now) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ out)) #         ≈˘⟨ #-resp-≈ (∘-resp-≈ˡ (+₁-cong₂ g-law refl)) ⟩ 
          ((f +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ out)) #                          ≈⟨ #-Uniformity (sym (coit-commutes ((f +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ out)))) ⟩ 
          out # ∘ coit ((f +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ out))               ≈˘⟨ (refl⟩∘⟨ (D₁-coit (distributeˡ⁻¹ ∘ (id ⁂ out)) f)) ⟩ 
          a ∘ D₁ f ∘ coit (distributeˡ⁻¹ ∘ (id ⁂ out))                        ≈⟨ refl⟩∘⟨ refl⟩∘⟨ coit-unique (distributeˡ⁻¹ ∘ (id ⁂ out)) τ τ-commutes ⟩ 
          a ∘ D₁ f ∘ τ                                                        ∎))
          where
          open Elgot-Algebra EA using (_#; #-resp-≈; #-Uniformity)
          open IsCoequalizer (coeq-productsʳ {X} {Y} (id {Y})) using () renaming (coequalize to prod-coequalize; universal to prod-universal; unique to prod-unique)
          open Search-Algebra (Elgot⇒Search DM EA) using (A) renaming (α to a)
          open Module (Elgot⇒D-Algebra DM EA)

        ♯-preserving' : ∀ {Y} {EA : Elgot-Algebra} (f : Y × X ⇒ Elgot-Algebra.A EA) {Z} (g : Z ⇒ Ď₀ X + Z) → [ EA , f ]♯' ∘ (id ⁂ Search-Algebra-on.α s-alg-on ∘ coit g) ≈ Elgot-Algebra._# EA (([ EA , f ]♯' +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ g))
        ♯-preserving' {Y} {EA} f g = begin 
          [ EA , f ]♯' ∘ (id ⁂ α ∘ coit g)                               ≈˘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identity² refl) ⟩ 
          [ EA , f ]♯' ∘ (id ⁂ α) ∘ (id ⁂ coit g)                        ≈⟨ extendʳ (id⁂Dρ-epi ([ EA , f ]♯' ∘ (id ⁂ α)) (a ∘ D₁ ([ EA , f ]♯') ∘ τ) epi-helper) ○ ∘-resp-≈ʳ assoc ⟩ 
          a ∘ D₁ ([ EA , f ]♯') ∘ τ ∘ (id ⁂ coit g)                      ≈˘⟨ refl⟩∘⟨ coit-unique (([ EA , f ]♯' +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ g)) (D₁ ([ EA , f ]♯') ∘ τ ∘ (id ⁂ coit g)) unique-helper ⟩ 
          out # ∘ coit (([ EA , f ]♯' +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ g)) ≈˘⟨ #-Uniformity (sym (coit-commutes (([ EA , f ]♯' +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ g)))) ⟩ 
          (([ EA , f ]♯' +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ g)) #            ∎
          where
          open IsCoequalizer (coeq-productsʳ {X} {Y} (id {Y})) using () renaming (coequalize to prod-coequalize; universal to prod-universal)
          open Elgot-Algebra EA using (_#; #-Uniformity)
          open Search-Algebra (Elgot⇒Search DM EA) using (A; identity₁) renaming (α to a)
          open Module (Elgot⇒D-Algebra DM EA) using () renaming (commute to a-commute)

          id⁂Dρ-epi : ∀ {X Y} → Epi (id {X} ⁂ D₁ (ρ {Y}))
          id⁂Dρ-epi {X} {Y} {Z} f g eq = epi₁ f g (epi₂ (f ∘ (id ⁂ D₁ π₁)) (g ∘ (id ⁂ D₁ π₁)) (epi₃ ((f ∘ (id ⁂ D₁ π₁)) ∘ (id ⁂ τ)) ((g ∘ (id ⁂ D₁ π₁)) ∘ (id ⁂ τ)) (begin 
            ((f ∘ (id ⁂ D₁ π₁)) ∘ (id ⁂ τ)) ∘ (id ⁂ (ρ ⁂ id))  ≈⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ refl (∘-resp-≈ʳ (⁂-cong₂ refl (sym D.F.identity)) ○ τ-natural ρ id) ○ sym ⁂∘⁂) ⟩ 
            (f ∘ (id ⁂ D₁ π₁)) ∘ (id ⁂ D₁ (ρ ⁂ id)) ∘ (id ⁂ τ) ≈⟨ pullʳ (extendʳ (⁂∘⁂ ○ ⁂-cong₂ refl (sym D.F.homomorphism ○ D.F.F-resp-≈ project₁ ○ D.F.homomorphism) ○ sym ⁂∘⁂)) ⟩ 
            f ∘ (id ⁂ D₁ ρ) ∘ (id ⁂ D₁ π₁) ∘ (id ⁂ τ)          ≈⟨ extendʳ eq ⟩ 
            g ∘ (id ⁂ D₁ ρ) ∘ (id ⁂ D₁ π₁) ∘ (id ⁂ τ)          ≈˘⟨ pullʳ (extendʳ (⁂∘⁂ ○ ⁂-cong₂ refl (sym D.F.homomorphism ○ D.F.F-resp-≈ project₁ ○ D.F.homomorphism) ○ sym ⁂∘⁂)) ⟩ 
            (g ∘ (id ⁂ D₁ π₁)) ∘ (id ⁂ D₁ (ρ ⁂ id)) ∘ (id ⁂ τ) ≈˘⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ refl (∘-resp-≈ʳ (⁂-cong₂ refl (sym D.F.identity)) ○ τ-natural ρ id) ○ sym ⁂∘⁂) ⟩ 
            ((g ∘ (id ⁂ D₁ π₁)) ∘ (id ⁂ τ)) ∘ (id ⁂ (ρ ⁂ id))  ∎)))
            where
            open Terminal terminal using (⊤)
            open cond-2 (c-2 Y) using () renaming (s-alg-on to s-alg-on-Y)
            open Search-Algebra-on s-alg-on-Y using () renaming (α to y)
            s-alg-Y : Search-Algebra
            s-alg-Y = record { A = Ď₀ Y ; search-algebra-on = s-alg-on-Y }
            epi₁ : Epi (id {X} ⁂ D₁ ((π₁ {Ď₀ Y} {⊤})))
            epi₁ = Iso⇒Epi ([ X ×- ]-resp-Iso ([ D.F ]-resp-Iso (_≅_.iso A×⊤≅A)))
            epi₂ : Epi (id {X} ⁂ τ {Ď₀ Y} {⊤})
            epi₂ {G} h i eq' = begin 
              h                                           ≈˘⟨ elimʳ (⟨⟩-unique id-comm (id-comm ○ ∘-resp-≈ˡ (sym (Retract.is-retract (tau-retract ⊤ s-alg-Y))))) ⟩ 
              h ∘ (id ⁂ τ ∘ ⟨ y ∘ D₁ π₁ , D₁ π₂ ⟩)        ≈˘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identity² refl) ⟩ 
              h ∘ (id ⁂ τ) ∘ (id ⁂ ⟨ y ∘ D₁ π₁ , D₁ π₂ ⟩) ≈⟨ extendʳ eq' ⟩ 
              i ∘ (id ⁂ τ) ∘ (id ⁂ ⟨ y ∘ D₁ π₁ , D₁ π₂ ⟩) ≈⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identity² refl) ⟩ 
              i ∘ (id ⁂ τ ∘ ⟨ y ∘ D₁ π₁ , D₁ π₂ ⟩)        ≈⟨ elimʳ (⟨⟩-unique id-comm (id-comm ○ ∘-resp-≈ˡ (sym (Retract.is-retract (tau-retract ⊤ s-alg-Y))))) ⟩ 
              i                                           ∎
            epi₃ : Epi (id {X} ⁂ (ρ {Y} ⁂ id {D₀ ⊤}))
            epi₃ = IsCoequalizer⇒Epi coeq-productsᵐ

          unique-helper : out ∘ D₁ ([ EA , f ]♯') ∘ τ ∘ (id ⁂ coit g) ≈ (id +₁ D₁ ([ EA , f ]♯') ∘ τ ∘ (id ⁂ coit g)) ∘ ([ EA , f ]♯' +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ g)
          unique-helper = begin 
            out ∘ D₁ ([ EA , f ]♯') ∘ τ ∘ (id ⁂ coit g)                                                             ≈⟨ extendʳ (D₁-commutes [ EA , f ]♯') ⟩ 
            ([ EA , f ]♯' +₁ D₁ [ EA , f ]♯') ∘ out ∘ τ ∘ (id ⁂ coit g)                                             ≈⟨ refl⟩∘⟨ (extendʳ τ-commutes ○ ∘-resp-≈ʳ assoc) ⟩ 
            ([ EA , f ]♯' +₁ D₁ [ EA , f ]♯') ∘ (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ⁂ out) ∘ (id ⁂ coit g)              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl (coit-commutes g) ○ sym ⁂∘⁂) ⟩ 
            ([ EA , f ]♯' +₁ D₁ [ EA , f ]♯') ∘ (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ⁂ (id +₁ coit g)) ∘ (id ⁂ g)        ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (sym (distributeˡ⁻¹-natural id id (coit g))) ⟩ 
            ([ EA , f ]♯' +₁ D₁ [ EA , f ]♯') ∘ (id +₁ τ) ∘ ((id ⁂ id) +₁ (id ⁂ coit g)) ∘ distributeˡ⁻¹ ∘ (id ⁂ g) ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityʳ refl) ○ pullˡ (+₁∘+₁ ○ +₁-cong₂ (elimʳ (⟨⟩-unique id-comm id-comm)) assoc) ⟩ 
            ([ EA , f ]♯' +₁ D₁ [ EA , f ]♯' ∘ τ ∘ (id ⁂ coit g)) ∘ distributeˡ⁻¹ ∘ (id ⁂ g)                        ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟩ 
            (id +₁ D₁ ([ EA , f ]♯') ∘ τ ∘ (id ⁂ coit g)) ∘ ([ EA , f ]♯' +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ g)         ∎

          epi-helper : ([ EA , f ]♯' ∘ (id ⁂ α)) ∘ (id ⁂ D₁ ρ) ≈ (a ∘ D₁ ([ EA , f ]♯') ∘ τ) ∘ (id ⁂ D₁ ρ)
          epi-helper = begin 
            ([ EA , f ]♯' ∘ (id ⁂ α)) ∘ (id ⁂ D₁ ρ)   ≈⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ refl (sym ρ-algebra-morphism-2) ○ sym ⁂∘⁂) ⟩ 
            [ EA , f ]♯' ∘ (id ⁂ ρ) ∘ (id ⁂ D.μ.η _)    ≈⟨ (extendʳ (sym (prod-universal {eq = f-coequalize EA f}))) ○ ∘-resp-≈ʳ assoc ⟩ 
            a ∘ D₁ f ∘ τ ∘ (id ⁂ D.μ.η _)               ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym strength.μ-η-comm ⟩ 
            a ∘ D₁ f ∘ D.μ.η _ ∘ D₁ τ ∘ τ               ≈⟨ refl⟩∘⟨ (extendʳ (sym (D.μ.commute _))) ⟩ 
            a ∘ D.μ.η _ ∘ D₁ (D₁ f) ∘ D₁ τ ∘ τ          ≈⟨ extendʳ (sym a-commute) ⟩ 
            a ∘ D₁ a ∘ D₁ (D₁ f) ∘ D₁ τ ∘ τ           ≈⟨ refl⟩∘⟨ (sym-assoc ○ pullˡ (∘-resp-≈ˡ (sym D.F.homomorphism) ○ sym D.F.homomorphism ○ D.F.F-resp-≈ assoc)) ⟩ 
            a ∘ D₁ (a ∘ D₁ f ∘ τ) ∘ τ                 ≈⟨ refl⟩∘⟨ ((D.F.F-resp-≈ (prod-universal {eq = f-coequalize EA f}) ○ D.F.homomorphism) ⟩∘⟨refl) ⟩ 
            a ∘ (D₁ ([ EA , f ]♯') ∘ D₁ (id ⁂ ρ)) ∘ τ ≈⟨ (∘-resp-≈ʳ (pullʳ (sym (τ-natural id ρ))) ○ assoc²εβ) ⟩ 
            (a ∘ D₁ ([ EA , f ]♯') ∘ τ) ∘ (id ⁂ D₁ ρ) ∎

      *-h : ∀ {EA : Elgot-Algebra} (f : X ⇒ Elgot-Algebra.A EA) → Ď₀ X ⇒ Elgot-Algebra.A EA
      *-h {EA} f = [ EA , f ∘ π₂ ]♯' ∘ ⟨ ! , id ⟩
        where
        open Terminal terminal using (!)

      *-preserves : ∀ {EA : Elgot-Algebra} (f : X ⇒ Elgot-Algebra.A EA) {Z} {h : Z ⇒ Ď₀ X + Z} → ([ EA , f ∘ π₂ ]♯' ∘ ⟨ Terminal.! terminal , id ⟩) ∘ α ∘ coit h ≈ Elgot-Algebra._# EA (([ EA , f ∘ π₂ ]♯' ∘ ⟨ Terminal.! terminal , id ⟩ +₁ id) ∘ h)
      *-preserves {EA} f {Z} {h} = begin 
        ([ EA , f ∘ π₂ ]♯' ∘ ⟨ ! , id ⟩) ∘ α ∘ coit h                         ≈⟨ pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ (sym (!-unique (! ∘ α ∘ coit h))) identityˡ) ⟩ 
        [ EA , f ∘ π₂ ]♯' ∘ ⟨ ! , α ∘ coit h ⟩                                ≈˘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ identityʳ) ⟩ 
        [ EA , f ∘ π₂ ]♯' ∘ (id ⁂ α ∘ coit h) ∘ ⟨ ! , id ⟩                    ≈⟨ pullˡ (♯-preserving' (f ∘ π₂) h) ⟩ 
        (([ EA , f ∘ π₂ ]♯' +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) # ∘ ⟨ ! , id ⟩ ≈˘⟨ #-Uniformity uni-helper ⟩
        (([ EA , f ∘ π₂ ]♯' ∘ ⟨ ! , id ⟩ +₁ id) ∘ h) #                        ∎
        where
        open Terminal terminal using (!; !-unique)
        open Elgot-Algebra EA using (_#; #-Uniformity)
        uni-helper : (id +₁ ⟨ ! , id ⟩) ∘ ([ EA , f ∘ π₂ ]♯' ∘ ⟨ ! , id ⟩ +₁ id) ∘ h ≈ (([ EA , f ∘ π₂ ]♯' +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) ∘ ⟨ ! , id ⟩
        uni-helper = begin 
          (id +₁ ⟨ ! , id ⟩) ∘ ([ EA , f ∘ π₂ ]♯' ∘ ⟨ ! , id ⟩ +₁ id) ∘ h     ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟩ 
          ([ EA , f ∘ π₂ ]♯' ∘ ⟨ ! , id ⟩ +₁ ⟨ ! , id ⟩) ∘ h                  ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identityˡ) ⟩ 
          ([ EA , f ∘ π₂ ]♯' +₁ id) ∘ (⟨ ! , id ⟩ +₁ ⟨ ! , id ⟩) ∘ h          ≈⟨ refl⟩∘⟨ distrib-helper ⟩ 
          ([ EA , f ∘ π₂ ]♯' +₁ id) ∘ distributeˡ⁻¹ ∘ ⟨ ! , h ⟩               ≈˘⟨ pullʳ (pullʳ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ identityʳ)) ⟩ 
          (([ EA , f ∘ π₂ ]♯' +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) ∘ ⟨ ! , id ⟩ ∎
          where
          distrib-helper : (⟨ ! , id ⟩ +₁ ⟨ ! , id ⟩) ∘ h ≈ distributeˡ⁻¹ ∘ ⟨ ! , h ⟩
          distrib-helper = Iso⇒Mono (IsIso.iso isIsoˡ) ((⟨ ! , id ⟩ +₁ ⟨ ! , id ⟩) ∘ h) (distributeˡ⁻¹ ∘ ⟨ ! , h ⟩) (begin 
            distributeˡ ∘ (⟨ ! , id ⟩ +₁ ⟨ ! , id ⟩) ∘ h ≈⟨ pullˡ ([]∘+₁ ○ []-cong₂ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ identityʳ) (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ identityʳ)) ⟩ 
            [ ⟨ ! , i₁ ⟩ , ⟨ ! , i₂ ⟩ ] ∘ h              ≈⟨ []-unique (⟨⟩∘ ○ ⟨⟩-cong₂ (sym (!-unique (! ∘ i₁))) identityˡ) (⟨⟩∘ ○ ⟨⟩-cong₂ (sym (!-unique (! ∘ i₂))) identityˡ) ⟩∘⟨refl ⟩ 
            ⟨ ! , id ⟩ ∘ h                               ≈⟨ ⟨⟩∘ ○ ⟨⟩-cong₂ (sym (!-unique (! ∘ h))) identityˡ ⟩ 
            ⟨ ! , h ⟩                                    ≈˘⟨ cancelˡ (IsIso.isoʳ isIsoˡ) ⟩ 
            distributeˡ ∘ distributeˡ⁻¹ ∘ ⟨ ! , h ⟩      ∎)

      *-lift' : ∀ {EA : Elgot-Algebra} (f : X ⇒ Elgot-Algebra.A EA) → *-h {EA} f ∘ ρ ∘ now ≈ f
      *-lift' {EA} f = begin 
        ([ EA , f ∘ π₂ ]♯' ∘ ⟨ ! , id ⟩) ∘ ρ ∘ now      ≈⟨ pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ (sym (!-unique (! ∘ ρ ∘ now))) identityˡ) ⟩ 
        [ EA , f ∘ π₂ ]♯' ∘ ⟨ ! , ρ ∘ now ⟩             ≈˘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ identityʳ) ⟩ 
        [ EA , f ∘ π₂ ]♯' ∘ (id ⁂ ρ ∘ now) ∘ ⟨ ! , id ⟩ ≈˘⟨ extendʳ (♯-law' {⊤} {EA} (f ∘ π₂)) ⟩ 
        f ∘ π₂ ∘ ⟨ ! , id ⟩                             ≈⟨ elimʳ project₂ ⟩ 
        f                                               ∎
        where
        open Terminal terminal using (⊤; !; !-unique)

      *-uniq' : ∀ {EA : Elgot-Algebra} (f : X ⇒ Elgot-Algebra.A EA) (g : Elgot-Algebra-Morphism (record { A = Ď₀ X ; algebra = elgot' (c-2 X) }) EA) → EA-h g ∘ ρ ∘ now ≈ f → EA-h g ≈ *-h {EA} f
      *-uniq' {EA} f g g-lift = ρ-epi (EA-h g) (*-h {EA} f) (begin 
        EA-h g ∘ ρ                                     ≈⟨ refl⟩∘⟨ ρ-law' ⟩ 
        EA-h g ∘ α ∘ coit ((ρ ∘ now +₁ id) ∘ out)      ≈⟨ EA-preserves g ⟩ 
        ((EA-h g +₁ id) ∘ (ρ ∘ now +₁ id) ∘ out) #     ≈⟨ #-resp-≈ (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩ 
        ((EA-h g ∘ ρ ∘ now +₁ id) ∘ out) #             ≈⟨ #-resp-≈ (∘-resp-≈ˡ (+₁-cong₂ g-lift refl)) ⟩ 
        ((f +₁ id) ∘ out) #                            ≈˘⟨ #-resp-≈ (∘-resp-≈ˡ (+₁-cong₂ (*-lift' {EA} f) refl)) ⟩ 
        ((*-h {EA} f ∘ ρ ∘ now +₁ id) ∘ out) #         ≈˘⟨ #-resp-≈ (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩ 
        ((*-h {EA} f +₁ id) ∘ (ρ ∘ now +₁ id) ∘ out) # ≈˘⟨ *-preserves {EA} f ⟩ 
        *-h {EA} f ∘ α ∘ coit ((ρ ∘ now +₁ id) ∘ out)  ≈˘⟨ refl⟩∘⟨ ρ-law' ⟩ 
        *-h {EA} f ∘ ρ                                 ∎)
        where
        open Elgot-Algebra EA
        open Terminal terminal using (!; !-unique)


  2⇒3 : (∀ X → cond-2 X) → (∀ X → cond-3 X)
  2⇒3 c-2 X .elgot = elgot' (c-2 X)

  2⇒3 c-2 X .isFO = record 
    { _* = λ {EA} f → record { h = *-h {EA} f ; preserves = λ {Z} {h} → *-preserves {EA} f {Z} {h} }
    ; *-lift = λ {EA} f → *-lift' {EA} f 
    ; *-uniq = λ {EA} f g g-lift → *-uniq' {EA} f g g-lift 
    }
    where open Stable X c-2

  2⇒3 c-2 X .isStable = record 
    { [_,_]♯ = [_,_]♯' 
    ; ♯-law = λ {Y} {EA} f → ♯-law' {Y} {EA} f 
    ; ♯-preserving = λ {Y} {EA} f {Z} g → ♯-preserving' {Y} {EA} f {Z} g 
    ; ♯-unique = λ {Y} {EA} f g g-law g-preserving → ♯-unique' {Y} {EA} f g g-law (λ {Z} {h} → g-preserving {Z} h) 
    }
    where
    open Stable X c-2

  2⇒3 c-2 X .ρ-algebra-morphism = begin 
    ρ ∘ D.μ.η X           ≈⟨ ρ-algebra-morphism-2 ⟩ 
    α ∘ D₁ ρ              ≈˘⟨ ((elimʳ (coit-unique out id (id-comm ○ ∘-resp-≈ˡ (sym ([]-cong₂ identityʳ identityʳ ○ +-η))))) ⟩∘⟨refl) ⟩ 
    (α ∘ coit out) ∘ D₁ ρ ∎
    where
    open cond-2 (c-2 X) renaming (ρ-algebra-morphism to ρ-algebra-morphism-2)
    open Search-Algebra-on s-alg-on

  2⇒3 c-2 X .ρ-law = ρ-law'
    where
      open Stable X c-2 using (ρ-law')