open import Cubical.Foundations.Prelude

module SignatureAlgebra.Examples.Coequalizer (ℓi : Level) where

open import Cubical.Foundations.Function
open import Cubical.Foundations.Structure

open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Sigma
open import Cubical.Data.Unit

open import Cubical.HITs.PropositionalTruncation as ∥₁

open import DCPO ℓi
open import DCPO.Constructions.BinaryProduct ℓi
open import DCPO.Constructions.Product ℓi

open import SignatureAlgebra.Initial ℓi as InitialΣAlg
open import SignatureAlgebra.Monomial ℓi
open import SignatureAlgebra.Signature ℓi
open import SignatureAlgebra.SignatureAlgebra ℓi

private
  variable
    ℓd ℓt ℓe ℓt' ℓx ℓt'' ℓf : Level

module _ {D : DCPO ℓd ℓt} {E : DCPO ℓe ℓt'} (f g : DCPOMorphism D E) where

  inclₘ : Monomial ℓ-zero ℓe ℓt'
  inclₘ = constantₘ E

  coeqPreΣ : PreSignature ℓ-zero ℓ-zero ℓe ℓt'
  coeqPreΣ = presignature Unit λ _ → inclₘ

  data InequalityName : Type ℓd where
    fd⊑gd : (d : ⟨ D ⟩) → InequalityName
    gd⊑fd : (d : ⟨ D ⟩) → InequalityName

  inclₜ : {V : Type} → ⟨ E ⟩ → Term coeqPreΣ V
  inclₜ = constr tt ⊥.rec

  coeqΣ : Signature ℓ-zero ℓ-zero ℓe ℓt' ℓd ℓ-zero
  coeqΣ =
      signature coeqPreΣ InequalityName
        λ { (fd⊑gd d) → inequality ⊥ (inclₜ (function f d)) (inclₜ (function g d))
          ; (gd⊑fd d) → inequality ⊥ (inclₜ (function g d)) (inclₜ (function f d)) }

  CoeqAlgebra : (ℓ ℓ' : Level) → Type (ℓ-max  (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) ℓd) ℓe) ℓt') (ℓ-suc ℓ)) (ℓ-suc ℓ'))
  CoeqAlgebra = SignatureAlgebra coeqΣ

  coeqalgebra : (X : DCPO ℓx ℓt'')
              → (incl : ⟨ E ⟩ → ⟨ X ⟩)
              → isContinuous E X incl
              → ((d : ⟨ D ⟩) → incl (function f d) ≡ incl (function g d))
              → CoeqAlgebra ℓx ℓt''
  coeqalgebra X incl inclCont p =
    signaturealgebra
      (presignaturealgebra X
        (λ _ → incl ∘ snd)
        (λ _ → isContinuous-∘ (⟦ inclₘ ⟧ₘ X) E X incl snd
                inclCont
                (sndIsContinuous (Πᵈᶜᵖᵒ ⊥ (λ _ → X)) E)))
      λ { (fd⊑gd d) ρ → ≡→⊑ X (p d)
        ; (gd⊑fd d) ρ → ≡→⊑ X (sym (p d)) }

  ⟦inclₜ⟧-≡ : {V : Type} (X : CoeqAlgebra ℓx ℓt'') {ρ : V → ⟨ X ⟩} {e : ⟨ E ⟩}
            → ⟦ inclₜ e ⟧ₜ (underlyingDCPO X) (interpretation X) ρ
            ≡ interpretation X tt (⊥.rec , e)
  ⟦inclₜ⟧-≡ X = cong (interpretation X tt) (≡-× (isContr→isProp isContr⊥→A _ _) refl)

  initialCoeqAlgebra : CoeqAlgebra (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) ℓd) ℓe) ℓt') (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) ℓd) ℓe) ℓt')
  initialCoeqAlgebra = initialSignatureAlgebra coeqΣ

  coeqDCPO : DCPO (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) ℓd) ℓe) ℓt') (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) ℓd) ℓe) ℓt')
  coeqDCPO = initialSignatureDCPO coeqΣ

  coeq : DCPOMorphism E coeqDCPO
  coeq =
    scottcontinuousmap
      (app tt ∘ pairing (const ⊥.rec) (λ e → e))
      (isContinuous-∘ E (⟦ inclₘ ⟧ₘ coeqDCPO) coeqDCPO
        (app tt) (pairing (const ⊥.rec) (λ e → e))
        (appIsContinuous tt)
        (pairingIsContinuous E (Πᵈᶜᵖᵒ ⊥ (λ _ → coeqDCPO)) E
          (const ⊥.rec) (λ e → e)
          (constIsContinuous E (Πᵈᶜᵖᵒ ⊥ (λ _ → coeqDCPO)))
          (idIsContinuous E)))

module _ {D : DCPO ℓd ℓt} {E : DCPO ℓe ℓt'} {F : DCPO ℓf ℓt''}
         (f : DCPOMorphism D E) (g : DCPOMorphism D E) (h : DCPOMorphism E F)
         (p : (d : ⟨ D ⟩) → function h (function f d) ≡ function h (function g d)) where

  FasCoeqAlgebra : CoeqAlgebra f g ℓf ℓt''
  FasCoeqAlgebra =
    coeqalgebra f g F (function h) (continuity h) p

  universalArrow : DCPOMorphism (coeqDCPO f g) F
  universalArrow =
    scottcontinuousmap
      (InitialΣAlg.rec FasCoeqAlgebra)
      (InitialΣAlg.recIsContinuous FasCoeqAlgebra)

  universalArrowCommutes : function universalArrow ∘ function (coeq f g) ≡ function h
  universalArrowCommutes = refl

  universalArrowIsUnique : (k : DCPOMorphism (coeqDCPO f g) F)
                         → function k ∘ function (coeq f g) ≡ function h
                         → universalArrow ≡ k
  universalArrowIsUnique k p = DCPOMorphism≡ (funExt (ind (record { Args })))
    where module Args where
      Y : Initial (coeqΣ f g) → Type ℓf
      Y x = function universalArrow x ≡ function k x

      isPropY : (x : Initial (coeqΣ f g)) → isProp (Y x)
      isPropY x = sethood F _ _

      isSupPreservingY : {I : Type ℓi} (α : I → Initial (coeqΣ f g))
                       → (δ : isDirected (Leq (coeqΣ f g)) α)
                       → ((i : I) → Y (α i))
                       → Y (lub δ)
      isSupPreservingY α δ IH =
        function universalArrow (lub δ) ≡⟨ refl ⟩
        ∐ F δ₁ ≡⟨ congP (λ i → ∐ F) q ⟩
        ∐ F δ₂ ≡⟨ sym (supPreservation k δ) ⟩
        function k (lub δ) ∎
        where
          δ₁ : isDirected (order F) (function universalArrow ∘ α)
          δ₁ = recImageIsDirected FasCoeqAlgebra δ

          δ₂ : isDirected (order F) (function k ∘ α)
          δ₂ = imageIsDirected k δ

          q : PathP (λ i → isDirected (order F) (funExt IH i)) δ₁ δ₂
          q = isProp→PathP
                (λ i → isPropIsDirected (order F) (funExt IH i))
                δ₁ δ₂

      isAppPreservingY : (c : Unit)
                       → (args : ⟨ ⟦ constructors (coeqΣ f g) c ⟧ₘ (coeqDCPO f g) ⟩)
                       → ⟦ constructors (coeqΣ f g) c ⟧ₘᵈᵉᵖ (coeqDCPO f g) Y args
                       → Y (app c args)
      isAppPreservingY tt args IH =
        function universalArrow (app tt args)  ≡⟨ refl ⟩
        function h (snd args)                  ≡⟨ sym (funExt⁻ p (snd args)) ⟩
        function k (app tt (⊥.rec , snd args)) ≡⟨ cong (function k ∘ app tt) (≡-× (isContr→isProp isContr⊥→A _ _) refl) ⟩
        function k (app tt args) ∎