open import Level
open import Categories.Category.Core
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 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.Condition1-2 {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) (D : DelayM (Distributive.cocartesian distributive)) (PNNO : ParametrizedNNO C (Distributive.cartesian distributive)) (DQ : DelayQ distributive D 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 D
  open D-Kleisli
  open D-Monad
  open Later∘Extend
  open ParametrizedNNO PNNO

  open import Algebra.Search cocartesian D
  open import Algebra.Search.Retraction distributive D
  open HomReasoning
  open M C
  open MR C
  open MP C using (Iso⇒Epi)
  open Equiv
  open import Monad.Instance.Delay.Iota distributive D PNNO
  open import Monad.Instance.Delay.Strong distributive D
  open τ-mod
  open import Algebra.Search.Properties cocartesian
  open DelayQ DQ
  open import Monad.Instance.Delay.Quotient.KTheorem.Conditions distributive D PNNO DQ

  1⇒2 : cond-1 → (∀ X → cond-2 X)
  1⇒2 c-1 X = record { s-alg-on = s-alg-on ; ρ-algebra-morphism = D-universal }
    where
      open Coequalizer (coeqs X) renaming (universal to coeq-universal)
      open IsCoequalizer (c-1 X) using () renaming (equality to D-equality; coequalize to D-coequalize; universal to D-universal; unique to D-unique)
      s-alg-on : Search-Algebra-on (Ď₀ X)
      s-alg-on = record 
        { α = α'
        ; identity₁ = ρ-epi (α' ∘ now) id (begin 
          (α' ∘ now) ∘ ρ      ≈⟨ pullʳ (D.η.commute ρ) ⟩ 
          α' ∘ D₁ ρ ∘ now     ≈⟨ pullˡ (sym D-universal) ⟩
          (ρ ∘ D.μ.η X) ∘ now ≈⟨ cancelʳ D.identityʳ ⟩
          ρ                   ≈⟨ sym identityˡ ⟩
          id ∘ ρ              ∎) 
        ; identity₂ = IsCoequalizer⇒Epi (c-1 X) (α' ∘ later) α' (begin 
          (α' ∘ later) ∘ D₁ ρ   ≈⟨ pullʳ (later-extend-comm (now ∘ ρ)) ⟩ 
          α' ∘ D₁ ρ ∘ later     ≈⟨ pullˡ (sym D-universal) ⟩
          (ρ ∘ D.μ.η X) ∘ later ≈⟨ pullʳ (sym (later-extend-comm id)) ⟩
          ρ ∘ later ∘ extend id ≈⟨ pullˡ ρ-later ⟩
          ρ ∘ extend id         ≈⟨ D-universal ⟩
          α' ∘ D₁ ρ             ∎) 
        }
        where
          μ∘Dι : D.μ.η X ∘ D₁ ι ≈ extend ι
          μ∘Dι = sym DK.assoc ○ extend-≈ (cancelˡ DK.identityʳ)
          eq₁ : D₁ (extend ι) ≈ D₁ (D.μ.η X) ∘ D₁ (D₁ ι)
          eq₁ = sym (begin 
            D₁ (D.μ.η X) ∘ D₁ (D₁ ι) ≈⟨ sym D.F.homomorphism ⟩ 
            D₁ (D.μ.η X ∘ D₁ ι)      ≈⟨ D.F.F-resp-≈ μ∘Dι ⟩
            D₁ (extend ι)            ∎)
          α' = D-coequalize {h = ρ {X} ∘ D.μ.η X} (begin 
            (ρ ∘ D.μ.η X) ∘ D₁ (extend ι)            ≈⟨ (refl⟩∘⟨ eq₁) ⟩ 
            (ρ ∘ D.μ.η X) ∘ D₁ (D.μ.η X) ∘ D₁ (D₁ ι) ≈⟨ pullʳ (pullˡ D.assoc) ⟩
            ρ ∘ (D.μ.η X ∘ D.μ.η (D₀ X)) ∘ D₁ (D₁ ι) ≈⟨ (refl⟩∘⟨ pullʳ (D.μ.commute ι)) ⟩
            ρ ∘ D.μ.η X ∘ (D₁ ι) ∘ D.μ.η (X × N)     ≈⟨ (refl⟩∘⟨ pullˡ μ∘Dι) ⟩
            ρ ∘ extend ι ∘ D.μ.η (X × N)             ≈⟨ pullˡ equality ⟩
            (ρ ∘ D₁ π₁) ∘ D.μ.η (X × N)              ≈⟨ (pullʳ (sym (D.μ.commute π₁)) ○ sym-assoc) ⟩
            (ρ ∘ D.μ.η X) ∘ D₁ (D₁ π₁)               ∎)