open import Cubical.Foundations.Prelude

module SignatureAlgebra.Initial.Base (ℓi : Level) where

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

open import Cubical.Relation.Binary.Order.Poset

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

open import SignatureAlgebra.Monomial ℓi
open import SignatureAlgebra.Signature ℓi
open import SignatureAlgebra.SignatureAlgebra ℓi

private
  variable
    ℓc ℓmb ℓmc ℓmct ℓe ℓv : Level

initialSignatureAlgebraLevel : (ℓc ℓmb ℓmc ℓmct ℓe ℓv : Level) → Level
initialSignatureAlgebraLevel ℓc ℓmb ℓmc ℓmct ℓe ℓv = ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) ℓc) ℓmb) ℓmc) ℓmct) ℓe) ℓv

data Initial (Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv)
  : Type (initialSignatureAlgebraLevel ℓc ℓmb ℓmc ℓmct ℓe ℓv)
data Leq (Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv)
  : Initial Σ → Initial Σ → Type (initialSignatureAlgebraLevel ℓc ℓmb ℓmc ℓmct ℓe ℓv)

syntax Leq Σ x y = x ⊑[ Σ ] y

leqIsPoset            : {Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv}
                      → IsPoset (Leq Σ)
leqIsDirectedComplete : {Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv}
                      → isDirectedComplete (Leq Σ)

initialSignatureDCPO : (Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv)
                  → DCPO (initialSignatureAlgebraLevel ℓc ℓmb ℓmc ℓmct ℓe ℓv)
                         (initialSignatureAlgebraLevel ℓc ℓmb ℓmc ℓmct ℓe ℓv)
initialSignatureDCPO Σ = dcpo (Initial Σ) (Leq Σ) leqIsPoset leqIsDirectedComplete

data Initial Σ where
  app          : (c : constructorNames Σ)
               → ⟨ ⟦ constructors Σ c ⟧ₘ (initialSignatureDCPO Σ) ⟩
               → Initial Σ
  lub          : {I : Type ℓi} {α : I → Initial Σ}
               → (δ : isDirected (Leq Σ) α)
               → Initial Σ
  leqAntiSym   : (x y : Initial Σ) → x ⊑[ Σ ] y → y ⊑[ Σ ] x → x ≡ y
  isSetInitial : isSet (Initial Σ)

data Leq Σ where
  appIsUpperbound :
      {I : Type ℓi} (c : constructorNames Σ)
      (α : I → ⟨ ⟦ constructors Σ c ⟧ₘ (initialSignatureDCPO Σ) ⟩)
      (δ : isDirected (order (⟦ constructors Σ c ⟧ₘ (initialSignatureDCPO Σ))) α)
    → let monomial B C = constructors Σ c in
      isUpperbound (Leq Σ)
        -- NOTE: This is definitionally equal to
        --   app c (∐ (⟦ constructors Σ c ⟧ₘ (initialSignatureDCPO Σ)) δ)
        -- but the strict positivity checker doesn't like that
        ((app c ((λ b → lub (pointwiseFamilyIsDirected' B (λ _ → initialSignatureDCPO Σ) (fstIsDirected' (Πᵈᶜᵖᵒ B (λ _ → initialSignatureDCPO Σ)) C δ) b)) ,
                ∐ C (sndIsDirected' (Πᵈᶜᵖᵒ B (λ _ → initialSignatureDCPO Σ)) C δ))))
        (app c ∘ α)
  appIsLowerboundOfUpperbounds :
      {I : Type ℓi} (c : constructorNames Σ)
      (α : I → ⟨ ⟦ constructors Σ c ⟧ₘ (initialSignatureDCPO Σ) ⟩)
      (δ : isDirected (order (⟦ constructors Σ c ⟧ₘ (initialSignatureDCPO Σ))) α)
    → let monomial B C = constructors Σ c in
      isLowerboundOfUpperbounds (Leq Σ)
        -- NOTE: This is definitionally equal to
        --   app c (∐ (⟦ constructors Σ c ⟧ₘ (initialSignatureDCPO Σ)) δ)
        -- but the strict positivity checker doesn't like that
        (app c ((λ b → lub (pointwiseFamilyIsDirected' B (λ _ → initialSignatureDCPO Σ) (fstIsDirected' (Πᵈᶜᵖᵒ B (λ _ → initialSignatureDCPO Σ)) C δ) b)) ,
                ∐ C (sndIsDirected' (Πᵈᶜᵖᵒ B (λ _ → initialSignatureDCPO Σ)) C δ)))
        (app c ∘ α)
  leqRefl           : (x : Initial Σ) → x ⊑[ Σ ] x
  leqTrans          : (x y z : Initial Σ) → x ⊑[ Σ ] y → y ⊑[ Σ ] z → x ⊑[ Σ ] z
  lubIsUpperbound   : {I : Type ℓi} {α : I → Initial Σ} (δ : isDirected (Leq Σ) α)
                    → isUpperbound (Leq Σ) (lub δ) α
  lubIsLowerboundOfUpperbounds
                    : {I : Type ℓi} {α : I → Initial Σ} (δ : isDirected (Leq Σ) α)
                    → isLowerboundOfUpperbounds (Leq Σ) (lub δ) α
  isPropLeq         : (x y : Initial Σ) → isProp (x ⊑[ Σ ] y)
  inequality        : (j : inequalityNames Σ)
                    → (ρ : (V (inequalities Σ j) → Initial Σ))
                    → ⟦ lhs (inequalities Σ j) ⟧ₜ (initialSignatureDCPO Σ) app ρ
                        ⊑[ Σ ]
                      ⟦ rhs (inequalities Σ j) ⟧ₜ (initialSignatureDCPO Σ) app ρ

lubIsSup : {Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv}
         → {I : Type ℓi} {α : I → Initial Σ} (δ : isDirected (Leq Σ) α)
         → isSup (Leq Σ) (lub δ) α
lubIsSup δ = lubIsUpperbound δ , lubIsLowerboundOfUpperbounds δ

leqIsPoset = isposet isSetInitial isPropLeq leqRefl leqTrans leqAntiSym
leqIsDirectedComplete δ = lub δ , lubIsSup δ

appIsContinuous : {Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv}
                → (c : constructorNames Σ)
                → isContinuous
                    (⟦ constructors Σ c ⟧ₘ (initialSignatureDCPO Σ))
                    (initialSignatureDCPO Σ)
                    (app c)
appIsContinuous c I α δ = appIsUpperbound c α δ , appIsLowerboundOfUpperbounds c α δ

initialSignatureAlgebra : (Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv)
                     → SignatureAlgebra Σ (initialSignatureAlgebraLevel ℓc ℓmb ℓmc ℓmct ℓe ℓv)
                                          (initialSignatureAlgebraLevel ℓc ℓmb ℓmc ℓmct ℓe ℓv)
initialSignatureAlgebra Σ =
  signaturealgebra
    (presignaturealgebra (initialSignatureDCPO Σ) app appIsContinuous)
    inequality