open import Categories.Category.Core
open import Categories.Category.Distributive
open import Categories.Object.NaturalNumbers.Parametrized
open import Monad.Instance.Delay
open import Monad.Instance.Delay.Quotient
open import Categories.Object.Terminal
open import Categories.Functor.Properties using ([_]-resp-Iso)


import Categories.Morphism as M
import Categories.Morphism.Reasoning as MR
import Categories.Morphism.Properties as MP

module Monad.Instance.Delay.Quotient.Epis {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 HomReasoning
  open Equiv
  open import Category.Distributive.Helper distributive
  open M C
  open MR C
  open MP C
  
  open DelayM DM
  open D-Monad
  open DelayQ DQ
  open import Monad.Instance.Delay.Strong distributive DM
  open D-Strong
  open τ-mod
  open import Algebra.Search cocartesian DM
  open import Algebra.Search.Retraction distributive DM
  open Terminal terminal using (⊤)


  epi-Dρ : ∀ {X} → (s-alg-on : Search-Algebra-on (Ď₀ X)) → Epi (D₁ (ρ {X}))
  epi-Dρ {X} s-alg-on f g eq = epi₄ f g (epi₃ (f ∘ D₁ π₁) (g ∘ D₁ π₁) (pullʳ helper ○ extendʳ eq ○ pushʳ (sym helper)))
    where
      s-alg : Search-Algebra
      s-alg = record { A = Ď₀ X ; search-algebra-on = s-alg-on }
      open Search-Algebra-on s-alg-on
      helper : D₁ π₁ ∘ D₁ (ρ ⁂ id) ≈ D₁ ρ ∘ D₁ π₁
      helper = sym D.F.homomorphism ○ D.F.F-resp-≈ project₁ ○ D.F.homomorphism
      epi₁ : ∀ {Y} → Epi (ρ {X} ⁂ id {Y})
      epi₁ {Y} = IsCoequalizer⇒Epi (coeq-productsˡ (id {Y}))
      epi₂ : Epi (τ ∘ (ρ {X} ⁂ id {D₀ ⊤}))
      epi₂ f g eq = begin 
        f                             ≈⟨ introʳ (Retract.is-retract (tau-retract (⊤) s-alg)) ⟩ 
        f ∘ τ ∘ ⟨ α ∘ D₁ π₁ , D₁ π₂ ⟩ ≈⟨ extendʳ (epi₁ (f ∘ τ) (g ∘ τ) (assoc ○ eq ○ sym-assoc)) ⟩ 
        g ∘ τ ∘ ⟨ α ∘ D₁ π₁ , D₁ π₂ ⟩ ≈˘⟨ introʳ (Retract.is-retract (tau-retract (⊤) s-alg)) ⟩ 
        g                             ∎
      epi₃ : Epi (D₁ (ρ ⁂ id))
      epi₃ f g eq = epi₂ f g (begin 
        f ∘ τ ∘ (ρ ⁂ id)    ≈⟨ refl⟩∘⟨ epi₃-helper ⟩ 
        f ∘ D₁ (ρ ⁂ id) ∘ τ ≈⟨ extendʳ eq ⟩ 
        g ∘ D₁ (ρ ⁂ id) ∘ τ ≈˘⟨ refl⟩∘⟨ epi₃-helper ⟩ 
        g ∘ τ ∘ (ρ ⁂ id)    ∎)
        where
        epi₃-helper : τ ∘ (ρ ⁂ id) ≈ D₁ (ρ ⁂ id) ∘ τ
        epi₃-helper = begin 
          τ ∘ (ρ ⁂ id)    ≈⟨ refl⟩∘⟨ ⁂-cong₂ refl (sym D.F.identity) ⟩ 
          τ ∘ (ρ ⁂ D₁ id) ≈⟨ τ-natural ρ id ⟩ 
          D₁ (ρ ⁂ id) ∘ τ ∎
      epi₄ : Epi (D₁ (π₁ {Ď₀ X} {⊤}))
      epi₄ = Iso⇒Epi ([ D.F ]-resp-Iso (_≅_.iso A×⊤≅A))

  epi-DDρ : ∀ {X} → (s-alg-on : Search-Algebra-on (Ď₀ X)) → Epi (D₁ (D₁ (ρ {X})))
  epi-DDρ {X} s-alg-on f g eq = epi₄ f g (epi₃ (f ∘ D₁ (D₁ π₁)) (g ∘ D₁ (D₁ π₁)) (pullʳ helper ○ extendʳ eq ○ pushʳ (sym helper)))
        where
          s-alg : Search-Algebra
          s-alg = record { A = Ď₀ X ; search-algebra-on = s-alg-on }
          open Search-Algebra-on s-alg-on
          helper : D₁ (D₁ π₁) ∘ D₁ (D₁ (ρ ⁂ id)) ≈ D₁ (D₁ ρ) ∘ D₁ (D₁ π₁)
          helper = begin 
            D₁ (D₁ π₁) ∘ D₁ (D₁ (ρ ⁂ id)) ≈⟨ sym D.F.homomorphism ⟩ 
            D₁ (D₁ π₁ ∘ D₁ (ρ ⁂ id))      ≈⟨ D.F.F-resp-≈ (sym D.F.homomorphism) ⟩ 
            D₁ (D₁ (π₁ ∘ (ρ ⁂ id)))       ≈⟨ D.F.F-resp-≈ (D.F.F-resp-≈ project₁) ⟩ 
            D₁ (D₁ (ρ ∘ π₁))              ≈⟨ D.F.F-resp-≈ D.F.homomorphism ⟩ 
            D₁ (D₁ ρ ∘ D₁ π₁)             ≈⟨ D.F.homomorphism ⟩ 
            D₁ (D₁ ρ) ∘ D₁ (D₁ π₁)        ∎
          epi₁ : ∀ {Y} → Epi (ρ {X} ⁂ id {Y})
          epi₁ {Y} = IsCoequalizer⇒Epi (coeq-productsˡ (id {Y}))
          epi₂ : Epi (D₁ τ ∘ τ ∘ (ρ {X} ⁂ id {D₀ (D₀ (Terminal.⊤ terminal))}))
          epi₂ f g eq = begin 
            f                                                               ≈⟨ introʳ (D.F.F-resp-≈ (Retract.is-retract (tau-retract (Terminal.⊤ terminal) s-alg)) ○ D.F.identity) ⟩ 
            f ∘ D₁ (τ ∘ ⟨ α ∘ D₁ π₁ , D₁ π₂ ⟩)                              ≈⟨ refl⟩∘⟨ D.F.homomorphism ⟩ 
            f ∘ D₁ τ ∘ D₁ ⟨ α ∘ D₁ π₁ , D₁ π₂ ⟩                             ≈⟨ refl⟩∘⟨ refl⟩∘⟨ insertˡ (Retract.is-retract (tau-retract (D₀ (Terminal.⊤ terminal)) s-alg)) ⟩ 
            f ∘ D₁ τ ∘ τ ∘ ⟨ α ∘ D₁ π₁ , D₁ π₂ ⟩ ∘ D₁ ⟨ α ∘ D₁ π₁ , D₁ π₂ ⟩ ≈⟨ assoc²εβ ○ ∘-resp-≈ˡ (epi₁ (f ∘ D₁ τ ∘ τ) (g ∘ D₁ τ ∘ τ) (assoc²βε ○ eq ○ assoc²εβ)) ○ assoc²βε ⟩ 
            g ∘ D₁ τ ∘ τ ∘ ⟨ α ∘ D₁ π₁ , D₁ π₂ ⟩ ∘ D₁ ⟨ α ∘ D₁ π₁ , D₁ π₂ ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ insertˡ (Retract.is-retract (tau-retract (D₀ (Terminal.⊤ terminal)) s-alg)) ⟩ 
            g ∘ D₁ τ ∘ D₁ ⟨ α ∘ D₁ π₁ , D₁ π₂ ⟩                             ≈˘⟨ refl⟩∘⟨ D.F.homomorphism ⟩ 
            g ∘ D₁ (τ ∘ ⟨ α ∘ D₁ π₁ , D₁ π₂ ⟩)                              ≈˘⟨ introʳ (D.F.F-resp-≈ (Retract.is-retract (tau-retract (Terminal.⊤ terminal) s-alg)) ○ D.F.identity) ⟩ 
            g                                                               ∎
          epi₃ : Epi (D₁ (D₁ (ρ ⁂ id)))
          epi₃ f g eq = epi₂ f g (begin 
            f ∘ D₁ τ ∘ τ ∘ (ρ ⁂ id)         ≈⟨ refl⟩∘⟨ epi₃-helper ⟩ 
            f ∘ D₁ (D₁ (ρ ⁂ id)) ∘ D₁ τ ∘ τ ≈⟨ extendʳ eq ⟩ 
            g ∘ D₁ (D₁ (ρ ⁂ id)) ∘ D₁ τ ∘ τ ≈˘⟨ refl⟩∘⟨ epi₃-helper ⟩ 
            g ∘ D₁ τ ∘ τ ∘ (ρ ⁂ id)         ∎)
            where
            epi₃-helper : D₁ τ ∘ τ ∘ (ρ ⁂ id) ≈ D₁ (D₁ (ρ ⁂ id)) ∘ D₁ τ ∘ τ
            epi₃-helper = begin 
              D₁ τ ∘ τ ∘ (ρ ⁂ id)         ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ refl (sym D.F.identity) ⟩ 
              D₁ τ ∘ τ ∘ (ρ ⁂ D₁ id)      ≈⟨ refl⟩∘⟨ τ-natural ρ id ⟩ 
              D₁ τ ∘ D₁ (ρ ⁂ id) ∘ τ      ≈⟨ pullˡ (sym D.F.homomorphism) ⟩ 
              D₁ (τ ∘ (ρ ⁂ id)) ∘ τ       ≈⟨ (D.F.F-resp-≈ (∘-resp-≈ʳ (⁂-cong₂ refl (sym D.F.identity)))) ⟩∘⟨refl ⟩ 
              D₁ (τ ∘ (ρ ⁂ D₁ id)) ∘ τ    ≈⟨ (D.F.F-resp-≈ (τ-natural ρ id)) ⟩∘⟨refl ⟩ 
              D₁ (D₁ (ρ ⁂ id) ∘ τ) ∘ τ    ≈⟨ pushˡ D.F.homomorphism ⟩ 
              D₁ (D₁ (ρ ⁂ id)) ∘ D₁ τ ∘ τ ∎
          epi₄ : Epi (D₁ (D₁ (π₁ {Ď₀ X} {⊤})))
          epi₄ = Iso⇒Epi ([ D.F ]-resp-Iso ([ D.F ]-resp-Iso (_≅_.iso A×⊤≅A)))