open import Level
open import Categories.Category.Core
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 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.Conditions {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 import Monad.Strong.Helper cartesian
  open Bundles 
  open import Algebra.Elgot cocartesian
  open import Algebra.Elgot.Free cocartesian
  open import Algebra.Elgot.Stable distributive

  open DelayM DM
  open ParametrizedNNO PNNO

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

  cond-1 : Set (o ⊔ ℓ ⊔ e)
  cond-1 = ∀ X → IsCoequalizer (D₁ (extend (ι {X}))) (D₁ (D₁ π₁)) (D₁ (Coequalizer.arr (coeqs X)))

  record cond-2 (X : Obj) : Set (o ⊔ ℓ ⊔ e) where
    field
      s-alg-on : Search-Algebra-on (Ď₀ X)
      ρ-algebra-morphism : is-F-Algebra-Morphism {F = D.F} (record { A = D₀ X ; α = D.μ.η X }) (record { A = Ď₀ X ; α = Search-Algebra-on.α s-alg-on }) (ρ {X})

  record cond-3 (X : Obj) : Set (suc o ⊔ suc ℓ ⊔ suc e) where
    -- Ď₀ X is stable free elgot algebra
    field
      elgot : Elgot-Algebra-on (Ď₀ X)
    elgot-alg = record { A = Ď₀ X ; algebra = elgot }

    open Elgot-Algebra-on elgot
    field
      isFO : IsFreeObject elgotForgetfulF X elgot-alg (ρ ∘ now)
    freeobject = IsFreeObject⇒FreeObject elgotForgetfulF X elgot-alg (ρ ∘ now) isFO
    field
      isStable : IsStableFreeElgotAlgebra freeobject

    -- ρ is D-algebra morphism
    field
      ρ-algebra-morphism : is-F-Algebra-Morphism {F = D.F} (record { A = D₀ X ; α = D.μ.η X }) (record { A = Ď₀ X ; α = out # }) (ρ {X})
      ρ-law : ρ ≈ ((ρ ∘ now +₁ id) ∘ out) #

    freeElgot : FreeElgotAlgebra X
    freeElgot = record 
      { FX = record { A = Ď₀ X ; algebra = elgot } 
      ; η = ρ ∘ now 
      ; _* = F._* 
      ; *-lift = F.*-lift 
      ; *-uniq = F.*-uniq 
      }
      where module F = IsFreeObject isFO

  record cond-4 : Set (o ⊔ ℓ ⊔ e) where
    field
      extendsToStrongMonad : ExtendsToStrongMonad Ď-Functor
      ρ-strongMonadMorphism : IsStrongMonadMorphism D-Strong.strongMonad (ExtendsToStrongMonad⇒StrongMonad Ď-Functor extendsToStrongMonad) ρ-natural