open import Level
open import Categories.Category.Core
open import Categories.Object.NaturalNumbers.Parametrized
open import Categories.Category.Distributive
open import Categories.Functor hiding (id)
open import Categories.NaturalTransformation.Core using (NaturalTransformation; ntHelper)
open import Categories.Object.Exponential.Canonical using (Exponential)
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

-- Theorem:
-- When the coequalizer `ρ+1-coeq` of `Monad.Instance.Delay.Quotient` is preserved by (-)^N
-- (1) The equivalent conditions of `Monad.Instance.Delay.Quotient.KTheorem.Index` hold

module Monad.Instance.Delay.Quotient.ChoiceTheorem.KTheorem {o ℓ e} {C : Category o ℓ e} 
  (distributive : Distributive C) 
  (DM : DelayM (Distributive.cocartesian distributive)) 
  (PNNO : ParametrizedNNO C (Distributive.cartesian distributive)) 
  (ExpN : ∀ X → Exponential (Distributive.cartesian distributive) (ParametrizedNNO.N PNNO) X)
  (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
  open Functor
  open import Monad.Instance.Delay.Quotient.KTheorem.Conditions distributive DM PNNO DQ
  open import Monad.Instance.Delay.Retract distributive DM PNNO ExpN

  private
    module ExpN {X : Obj} = Exponential (ExpN X)
    open ExpN using (λg; β; eval; λ-cong; η-id; λ-unique′)

  coequalizer-preserved-by-retract :
    ∀ {F G : Endofunctor C}
      (section : NaturalTransformation F G)
      (retraction : NaturalTransformation G F)
      (is-retract : ∀ X → NaturalTransformation.η retraction X ∘
        NaturalTransformation.η section X ≈ id)
      {A B} {f g : A ⇒ B} (q : Coequalizer f g) →
      IsCoequalizer (Functor.₁ G f) (Functor.₁ G g)
        (Functor.₁ G (Coequalizer.arr q)) →
      IsCoequalizer (Functor.₁ F f) (Functor.₁ F g)
        (Functor.₁ F (Coequalizer.arr q))
  coequalizer-preserved-by-retract {F} {G} section retraction is-retract
    {A} {B} {f} {g} q Gq = record
    { equality = sym F.homomorphism ○ F.F-resp-≈ Q.equality ○ F.homomorphism
    ; coequalize = λ eq → GQ.coequalize (lift-equality eq) ∘ S.η Q.obj
    ; universal = universal′
    ; unique = retract-unique
    }
    where
      module F = Functor F
      module G = Functor G
      module S = NaturalTransformation section
      module R = NaturalTransformation retraction
      module Q = Coequalizer q
      module GQ = IsCoequalizer Gq

      lift-equality : ∀ {Z} {h : F.₀ B ⇒ Z} →
        h ∘ F.₁ f ≈ h ∘ F.₁ g →
        (h ∘ R.η B) ∘ G.₁ f ≈ (h ∘ R.η B) ∘ G.₁ g
      lift-equality {h = h} eq = begin
        (h ∘ R.η B) ∘ G.₁ f ≈⟨ assoc ⟩
        h ∘ R.η B ∘ G.₁ f   ≈⟨ refl⟩∘⟨ R.commute f ⟩
        h ∘ F.₁ f ∘ R.η A   ≈˘⟨ assoc ⟩
        (h ∘ F.₁ f) ∘ R.η A ≈⟨ eq ⟩∘⟨refl ⟩
        (h ∘ F.₁ g) ∘ R.η A ≈⟨ assoc ⟩
        h ∘ F.₁ g ∘ R.η A   ≈˘⟨ refl⟩∘⟨ R.commute g ⟩
        h ∘ R.η B ∘ G.₁ g   ≈˘⟨ assoc ⟩
        (h ∘ R.η B) ∘ G.₁ g ∎

      universal′ : ∀ {Z} {h : F.₀ B ⇒ Z}
        {eq : h ∘ F.₁ f ≈ h ∘ F.₁ g} →
        h ≈ (GQ.coequalize (lift-equality eq) ∘ S.η Q.obj) ∘ F.₁ Q.arr
      universal′ {h = h} {eq} = begin
        h ≈⟨ introʳ (is-retract B) ⟩
        h ∘ R.η B ∘ S.η B ≈⟨ extendʳ GQ.universal ⟩
        GQ.coequalize (lift-equality eq) ∘ G.₁ Q.arr ∘ S.η B
          ≈⟨ refl⟩∘⟨ sym (S.commute Q.arr) ⟩
        GQ.coequalize (lift-equality eq) ∘ S.η Q.obj ∘ F.₁ Q.arr
          ≈˘⟨ assoc ⟩
        (GQ.coequalize (lift-equality eq) ∘ S.η Q.obj) ∘ F.₁ Q.arr ∎

      retract-unique : ∀ {Z} {h : F.₀ B ⇒ Z} {i : F.₀ Q.obj ⇒ Z}
        {eq : h ∘ F.₁ f ≈ h ∘ F.₁ g} →
        h ≈ i ∘ F.₁ Q.arr →
        i ≈ GQ.coequalize (lift-equality eq) ∘ S.η Q.obj
      retract-unique {h = h} {i} {eq} factors = begin
        i ≈⟨ introʳ (is-retract Q.obj) ⟩
        i ∘ R.η Q.obj ∘ S.η Q.obj
          ≈˘⟨ assoc ⟩
        (i ∘ R.η Q.obj) ∘ S.η Q.obj
          ≈⟨ GQ.unique lifted-factors ⟩∘⟨refl ⟩
        GQ.coequalize (lift-equality eq) ∘ S.η Q.obj ∎
        where
          lifted-factors : h ∘ R.η B ≈
            (i ∘ R.η Q.obj) ∘ G.₁ Q.arr
          lifted-factors = begin
            h ∘ R.η B ≈⟨ factors ⟩∘⟨refl ⟩
            (i ∘ F.₁ Q.arr) ∘ R.η B ≈⟨ assoc ⟩
            i ∘ F.₁ Q.arr ∘ R.η B
              ≈˘⟨ refl⟩∘⟨ R.commute Q.arr ⟩
            i ∘ R.η Q.obj ∘ G.₁ Q.arr ≈˘⟨ assoc ⟩
            (i ∘ R.η Q.obj) ∘ G.₁ Q.arr ∎

  preserved-by-Streams : Set (o ⊔ ℓ ⊔ e)
  preserved-by-Streams = ∀ X → 
    IsCoequalizer (Stream-Functor.₁ (extend (ι {X}))) (Stream-Functor.₁ (D₁ π₁)) (Stream-Functor.₁ (Coequalizer.arr (coeqs X)))

  preserved-by-N⇒cond-1 : preserved-by-Streams → cond-1
  preserved-by-N⇒cond-1 pS X = coequalizer-preserved-by-retract
    D⇒Stream Stream⇒D Stream-D-retract (coeqs X) (pS X)