{-# OPTIONS --lossy-unification --safe #-}

open import Level
open import Data.Product using (_,_)
open import Categories.Category.Core
open import Categories.Functor hiding (id)
open import Categories.Functor.Algebra
open import Categories.Functor.Coalgebra
open import Categories.Monad.Strong
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 Category.Construction.ElgotAlgebras using (Elgot-Algebra-Morphism)
open import Categories.FreeObjects.Free
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.Condition3-4 {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.Instance.K 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 Algebra.Search cocartesian DM
  open import Algebra.Search.Properties cocartesian DM

  open import Monad.Instance.Delay.Quotient.Theorem.Conditions distributive DM PNNO DQ
  open import Monad.Instance.Delay.Quotient.Epis distributive DM PNNO DQ
  open Equiv
  open HomReasoning
  open M C
  open MR C
  open DelayM DM
  open Coit
  open D-Monad
  open DelayQ DQ
  open MonadK using (freealgebras; stable; μ-preserve)
  open import Monad.Instance.Delay.Strong distributive DM
  open D-Strong
  open τ-mod using () renaming (τ to D-τ)

  3⇒4 : (∀ X → cond-3 X) → cond-4
  3⇒4 c-3 = record 
    { extendsToStrongMonad = record
      { η = record { η = K.η.η ; commute = K-η-commute ; sym-commute = λ f → sym (K-η-commute f) }
      ; μ = record { η = K.μ.η ; commute = K-μ-commute ; sym-commute = λ f → sym (K-μ-commute f) }
      ; τ = record { η = τ.η ; commute = λ (f , g) → K-τ-commute f g ; sym-commute = λ (f , g) → sym (K-τ-commute f g) }
      ; assoc = K-assoc
      ; sym-assoc = sym K-assoc
      ; identityˡ = ∘-resp-≈ʳ (sym (F₁≈Ď₁ (K.η.η _))) ○ K.identityˡ
      ; identityʳ = K.identityʳ
      ; τ-identityˡ = ∘-resp-≈ˡ (sym (F₁≈Ď₁ π₂)) ○ KStrong.identityˡ
      ; τ-η-comm = KStrong.η-comm
      ; τ-μ-η-comm = ∘-resp-≈ʳ (∘-resp-≈ˡ (sym (F₁≈Ď₁ (τ.η _)))) ○ KStrong.μ-η-comm
      ; τ-strength-assoc = ∘-resp-≈ˡ (sym (F₁≈Ď₁ assocˡ)) ○ KStrong.strength-assoc
      } 
    ; ρ-strongMonadMorphism = record 
    { respects-η = refl 
    ; respects-μ = ρ-respects-μ 
    ; respects-τ = ρ-respects-τ 
    } 
    }
    where
    monadK : MonadK
    monadK .freealgebras X = freeElgot
      where open cond-3 (c-3 X)
    monadK .stable X = isStable
      where open cond-3 (c-3 X)

    open import Monad.Instance.K.Strong distributive monadK using (KStrong)
    module K = StrongMonad.M KStrong
    module τ = StrongMonad.strengthen KStrong
    module Ď = Functor Ď-Functor
    module KStrong = StrongMonad KStrong

    F₁≈Ď₁ : ∀ {X Y} (f : X ⇒ Y) → K.F.₁ f ≈ Ď.₁ f
    F₁≈Ď₁ {X} {Y} f = sym (*-uniq (K.η.η _ ∘ f) (record { h = Ď.₁ f ; preserves = Ď₁-preserves }) (begin 
      Ď.₁ f ∘ ρ ∘ now ≈˘⟨ extendʳ (NaturalTransformation.commute ρ-natural f) ⟩ 
      ρ ∘ D₁ f ∘ now  ≈˘⟨ pullʳ (D.η.commute f) ⟩
      (ρ ∘ now) ∘ f   ∎))
      where
      open cond-3 (c-3 X) using (isFO) renaming (elgot to elgotX; ρ-algebra-morphism to ρ-algebra-morphism-x)
      open cond-3 (c-3 Y) using () renaming (elgot to elgotY; ρ-algebra-morphism to ρ-algebra-morphism-y)
      open IsFreeObject isFO using (_*; *-uniq; *-lift)
      open FreeObject (IsFreeObject⇒FreeObject elgotForgetfulF X (record { A = Ď₀ X ; algebra = elgotX }) (ρ ∘ now) isFO) using (*-cong)
      open Elgot-Algebra-on elgotX using () renaming (_# to _#x; #-Uniformity to #x-Uniformity)
      open Elgot-Algebra-on elgotY using () renaming (_# to _#y; #-Uniformity to #y-Uniformity)
      Ď₁-preserves : ∀ {Z : Obj} {g : Z ⇒ Ď₀ X + Z} → Ď.₁ f ∘ g #x ≈ ((Ď.₁ f +₁ id) ∘ g) #y
      Ď₁-preserves {Z} {g} = begin 
        Ď.₁ f ∘ g #x                      ≈⟨ refl⟩∘⟨ #x-Uniformity (sym (coit-commutes g)) ⟩
        Ď.₁ f ∘ out #x ∘ coit g           ≈⟨ extendʳ commutes ⟩ 
        out #y ∘ D₁ (Ď.₁ f) ∘ coit g      ≈˘⟨ refl⟩∘⟨ coit-unique ((Ď.₁ f +₁ id) ∘ g) (D₁ (Ď.₁ f) ∘ coit g) unique-helper ⟩ 
        out #y ∘ coit ((Ď.₁ f +₁ id) ∘ g) ≈˘⟨ #y-Uniformity (sym (coit-commutes ((Ď.₁ f +₁ id) ∘ g))) ⟩ 
        ((Ď.₁ f +₁ id) ∘ g) #y            ∎
        where
        unique-helper : out ∘ D₁ (Ď.₁ f) ∘ coit g ≈ (id +₁ D₁ (Ď.₁ f) ∘ coit g) ∘ (Ď.₁ f +₁ id) ∘ g
        unique-helper = begin 
          out ∘ D₁ (Ď.₁ f) ∘ coit g                       ≈⟨ extendʳ (D₁-commutes (Ď.₁ f)) ⟩ 
          (Ď.₁ f +₁ D₁ (Ď.₁ f)) ∘ out ∘ coit g            ≈⟨ refl⟩∘⟨ (coit-commutes g) ⟩ 
          (Ď.₁ f +₁ D₁ (Ď.₁ f)) ∘ (id +₁ coit g) ∘ g      ≈⟨ extendʳ (+₁∘+₁ ○ +₁-cong₂ id-comm (sym identityʳ) ○ sym +₁∘+₁) ⟩ 
          (id +₁ D₁ (Ď.₁ f) ∘ coit g) ∘ (Ď.₁ f +₁ id) ∘ g ∎
        commutes : Ď.₁ f ∘ out #x ≈ out #y ∘ D₁ (Ď.₁ f)
        commutes = epi-Dρ search-algebra-on (Ď.₁ f ∘ out #x) (out #y ∘ D₁ (Ď.₁ f)) epi-helper
          where
          epi-helper : (Ď.₁ f ∘ out #x) ∘ D₁ ρ ≈ (out #y ∘ D₁ (Ď.₁ f)) ∘ D₁ ρ
          epi-helper = begin 
            (Ď.₁ f ∘ out #x) ∘ D₁ ρ      ≈˘⟨ pushʳ ρ-algebra-morphism-x ⟩ 
            Ď.₁ f ∘ ρ ∘ D.μ.η _          ≈˘⟨ extendʳ (NaturalTransformation.commute ρ-natural f) ⟩
            ρ ∘ D₁ f ∘ D.μ.η _           ≈˘⟨ refl⟩∘⟨ D.μ.commute f ⟩
            ρ ∘ D.μ.η _ ∘ D₁ (D₁ f)      ≈⟨ extendʳ ρ-algebra-morphism-y ⟩ 
            out #y ∘ D₁ ρ ∘ D₁ (D₁ f)    ≈⟨ pushʳ (sym D.F.homomorphism ○ D.F.F-resp-≈ (NaturalTransformation.commute ρ-natural f) ○ D.F.homomorphism) ⟩ 
            (out #y ∘ D₁ (Ď.₁ f)) ∘ D₁ ρ ∎
          open Search-Algebra (Elgot⇒Search (record { A = Ď₀ X ; algebra = elgotX })) using (search-algebra-on)

    K-η-commute : ∀ {X Y} (f : X ⇒ Y) → K.η.η Y ∘ f ≈ Ď.₁ f ∘ K.η.η X
    K-η-commute f = K.η.commute f ○ ∘-resp-≈ˡ (F₁≈Ď₁ f)

    K-μ-commute : ∀ {X Y} (f : X ⇒ Y) → K.μ.η Y ∘ Ď.₁ (Ď.₁ f) ≈ Ď.₁ f ∘ K.μ.η X
    K-μ-commute f = ∘-resp-≈ʳ (Ď.F-resp-≈ (sym (F₁≈Ď₁ f)) ○ sym (F₁≈Ď₁ (K.F.₁ f))) ○ K.μ.commute f ○ ∘-resp-≈ˡ (F₁≈Ď₁ f)

    K-assoc : ∀ {X} → K.μ.η X ∘ Ď.₁ (K.μ.η X) ≈ K.μ.η X ∘ K.μ.η (Ď₀ X)
    K-assoc {X} = (∘-resp-≈ʳ (sym (F₁≈Ď₁ (K.μ.η X)))) ○ K.assoc

    K-τ-commute : ∀ {X Y A B} (f : X ⇒ A) (g : Y ⇒ B) → τ.η (A , B) ∘ (f ⁂ Ď.₁ g) ≈ Ď.₁ (f ⁂ g) ∘ τ.η (X , Y)
    K-τ-commute {X} {Y} {A} {B} f g = ∘-resp-≈ʳ (⁂-cong₂ refl (sym (F₁≈Ď₁ g))) ○ τ.commute (f , g) ○ ∘-resp-≈ˡ (F₁≈Ď₁ (f ⁂ g))

    ρ-respects-μ : ∀ {X} → ρ ∘ D.μ.η X ≈ K.μ.η X ∘ ρ ∘ D.F.₁ ρ
    ρ-respects-μ {X} = begin 
      ρ ∘ D.μ.η X                                            ≈⟨ ρ-algebra-morphism-x ⟩ 
      out #x ∘ D.F.₁ ρ                                       ≈˘⟨ (#x-resp-≈ (cancelˡ (+₁∘+₁ ○ []-unique (id-comm-sym ○ ∘-resp-≈ʳ (sym K.identityʳ)) (id-comm-sym ○ ∘-resp-≈ʳ (sym identity²))))) ⟩∘⟨refl ⟩ 
      ((K.μ.η X +₁ id) ∘ (ρ ∘ now +₁ id) ∘ out) #x ∘ D.F.₁ ρ ≈˘⟨ pullˡ (μ-preserve monadK ((ρ ∘ now +₁ id) ∘ out)) ⟩ 
      K.μ.η X ∘ ((ρ ∘ now +₁ id) ∘ out) #Dx ∘ D.F.₁ ρ        ≈˘⟨ refl⟩∘⟨ (ρ-law ⟩∘⟨refl) ⟩ 
      K.μ.η X ∘ ρ ∘ D.F.₁ ρ                                  ∎
      where
      open cond-3 (c-3 X) using (freeElgot) renaming (ρ-algebra-morphism to ρ-algebra-morphism-x; elgot to elgotX)
      open cond-3 (c-3 (Ď₀ X)) using (ρ-law) renaming (elgot to elgotDX)
      open Elgot-Algebra-on elgotX using () renaming (_# to _#x; #-resp-≈ to #x-resp-≈)
      open Elgot-Algebra-on elgotDX using () renaming (_# to _#Dx)

    ρ-respects-τ : ∀ {X Y} → ρ ∘ D-τ ≈ τ.η (X , Y) ∘ (id ⁂ ρ)
    ρ-respects-τ {X} {Y} = sym (begin 
      τ.η _ ∘ (id ⁂ ρ)                                                           ≈⟨ refl⟩∘⟨ ⁂-cong₂ refl ρ-law-y ⟩ 
      τ.η _ ∘ (id ⁂ ((ρ ∘ now +₁ id) ∘ out) #y)                                  ≈⟨ τ-comm ((ρ ∘ now +₁ id) ∘ out) ⟩ 
      ((τ.η _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ (ρ ∘ now +₁ id) ∘ out)) #           ≈˘⟨ #xy-resp-≈ (∘-resp-≈ʳ (∘-resp-≈ʳ (⁂∘⁂ ○ ⁂-cong₂ identity² refl))) ⟩ 
      ((τ.η _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ (ρ ∘ now +₁ id)) ∘ (id ⁂ out)) #    ≈˘⟨ #xy-resp-≈ (∘-resp-≈ʳ (extendʳ (distributeˡ⁻¹-natural id (ρ ∘ now) id))) ⟩ 
      ((τ.η _ +₁ id) ∘ (id ⁂ ρ ∘ now +₁ id ⁂ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ out)) # ≈⟨ #xy-resp-≈ (pullˡ (+₁∘+₁ ○ +₁-cong₂ (τ-η (X , Y)) (elimʳ (⟨⟩-unique id-comm id-comm)))) ⟩ 
      ((ρ ∘ now +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ out)) #                           ≈⟨ #xy-Uniformity uni-helper ⟩ 
      ((ρ ∘ now +₁ id) ∘ out) # ∘ D-τ                                            ≈˘⟨ ρ-law-xy ⟩∘⟨refl ⟩ 
      ρ ∘ D-τ                                                                    ∎)
      where
      open MonadK monadK using (_#)
      open import Monad.Instance.K.Strong distributive monadK using (τ-comm; τ-η)
      open cond-3 (c-3 X) using () renaming (ρ-algebra-morphism to ρ-algebra-morphism-x; elgot to elgotX; ρ-law to ρ-law-x)
      open cond-3 (c-3 (X × Y)) using () renaming (ρ-law to ρ-law-xy; elgot to elgotXY)
      open cond-3 (c-3 Y) using () renaming (ρ-algebra-morphism to ρ-algebra-morphism-y; elgot to elgotY; ρ-law to ρ-law-y)
      open Elgot-Algebra-on elgotXY using () renaming (#-Uniformity to #xy-Uniformity; #-resp-≈ to #xy-resp-≈)
      open Elgot-Algebra-on elgotX using () renaming (_# to _#x; #-resp-≈ to #x-resp-≈)
      open Elgot-Algebra-on elgotY using () renaming (_# to _#y; #-resp-≈ to #y-resp-≈)
      uni-helper : (id +₁ D-τ) ∘ (ρ ∘ now +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ out) ≈ ((ρ ∘ now +₁ id) ∘ out) ∘ D-τ
      uni-helper = sym (begin 
        ((ρ ∘ now +₁ id) ∘ out) ∘ D-τ                              ≈⟨ pullʳ τ-mod.τ-commutes ⟩ 
        (ρ ∘ now +₁ id) ∘ (id +₁ D-τ) ∘ distributeˡ⁻¹ ∘ (id ⁂ out) ≈⟨ extendʳ (+₁∘+₁ ○ +₁-cong₂ id-comm id-comm-sym ○ sym +₁∘+₁) ⟩ 
        (id +₁ D-τ) ∘ (ρ ∘ now +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ out) ∎)