{-# OPTIONS --safe #-}

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.Condition4-2 {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 import Monad.Instance.Delay.Quotient.Theorem.Conditions distributive DM PNNO DQ
  open Equiv
  open HomReasoning
  open MR C
  open DelayM DM
  open D-Monad
  open DelayQ DQ

  4⇒2 : cond-4 → (∀ X → cond-2 X)
  4⇒2 c-4 X = record 
    { s-alg-on = record 
      { α = E.μ.η X ∘ ρ 
      ; identity₁ = begin 
        (E.μ.η X ∘ ρ) ∘ now ≈⟨ coeq-unique (sym coeq-helper) ⟩ 
        coequalize equality ≈˘⟨ id-coequalize ⟩ 
        id                  ∎ 
      ; identity₂ = pullʳ ρ-later 
      } 
    ; ρ-algebra-morphism = begin 
      ρ ∘ D.μ.η X          ≈⟨ respects-μ ○ sym-assoc ⟩ 
      (E.μ.η X ∘ ρ) ∘ D₁ ρ ∎ 
    }
    where
    open cond-4 c-4
    module E = ExtendsToStrongMonad extendsToStrongMonad
    open IsStrongMonadMorphism ρ-strongMonadMorphism
    open Coequalizer (coeqs X) using (coequalize; equality; id-coequalize) renaming (unique to coeq-unique)
    coeq-helper : ((E.μ.η X ∘ ρ) ∘ now) ∘ ρ ≈ ρ
    coeq-helper = begin 
      ((E.μ.η X ∘ ρ) ∘ now) ∘ ρ    ≈⟨ (pullʳ respects-η) ⟩∘⟨refl ⟩ 
      (E.μ.η X ∘ E.η.η (Ď₀ X)) ∘ ρ ≈⟨ elimˡ E.identityʳ ⟩  
      ρ                            ∎