open import Cubical.Foundations.Prelude

module SignatureAlgebra.Examples.PointedDCPO (ℓ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 DCPO ℓi
open import DCPO.Constructions.Discrete ℓi

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

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

botₘ : Monomial ℓ-zero ℓ-zero ℓ-zero
botₘ = constantₘ (discreteDCPO Unit isSetUnit)

⊥preΣ : PreSignature ℓ-zero ℓ-zero ℓ-zero ℓ-zero
⊥preΣ = presignature Unit (λ _ → botₘ)

botₜ : {V : Type} → Term ⊥preΣ V
botₜ = constr tt ⊥.rec tt

botInequality : Inequality ⊥preΣ ℓ-zero
botInequality = inequality Unit botₜ (var tt)

⊥Σ : Signature ℓ-zero ℓ-zero ℓ-zero ℓ-zero ℓ-zero ℓ-zero
⊥Σ = signature ⊥preΣ Unit (λ _ → botInequality)

PointedDCPO : (ℓd ℓt : Level) → Type (ℓ-max (ℓ-max (ℓ-suc ℓi) (ℓ-suc ℓd)) (ℓ-suc ℓt))
PointedDCPO = SignatureAlgebra ⊥Σ

pointeddcpo : (D : DCPO ℓd ℓt)
            → (bot : ⟨ D ⟩)
            → isLeast (order D) bot
            → PointedDCPO ℓd ℓt
pointeddcpo D bot botIsLeast =
  signaturealgebra
    (presignaturealgebra D (λ _ _ → bot)
      λ c → constIsContinuous (⟦ botₘ ⟧ₘ D) D)
    λ _ ρ → botIsLeast (ρ tt)

infix  _⁻
_⁻ : PointedDCPO ℓd ℓt → DCPO ℓd ℓt
_⁻ = underlyingDCPO

least : (D : PointedDCPO ℓd ℓt) → ⟨ D ⟩
least D = interpretation D tt (⊥.rec , tt)

⟦botₜ⟧-≡ : (D : PointedDCPO ℓd ℓt)
         → {V : Type} {ρ : V → ⟨ D ⟩}
         → ⟦ botₜ ⟧ₜ (D ⁻) (interpretation D) ρ ≡ least D
⟦botₜ⟧-≡ D = cong (interpretation D tt) (≡-× (isContr→isProp isContr⊥→A _ _) refl)

leastIsLeast : (D : PointedDCPO ℓd ℓt) → isLeast (order (D ⁻)) (least D)
leastIsLeast D x =
  subst (λ - → order (D ⁻) - x)
    (⟦botₜ⟧-≡ D)
    (inequalityValidity D tt (λ _ → x))

StrictMorphism : (D : PointedDCPO ℓd ℓt) (E : PointedDCPO ℓe ℓt')
               → Type (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) ℓd) ℓt) ℓe) ℓt')
StrictMorphism = SignatureMorphism

strictmorphism : {D : PointedDCPO ℓd ℓt} {E : PointedDCPO ℓe ℓt'}
               → (f : ⟨ D ⟩ → ⟨ E ⟩)
               → isContinuous (D ⁻) (E ⁻) f
               → f (least D) ≡ least E
               → StrictMorphism D E
strictmorphism {D = D} {E = E} f fCont p =
  signaturemorphism (scottcontinuousmap f fCont)
    λ { tt args →
      interpretation E tt (f ∘ fst args , tt) ≡⟨ cong (interpretation E tt) (≡-× (isContr→isProp isContr⊥→A _ _) refl) ⟩
      least E                                 ≡⟨ sym p ⟩
      f (least D)                             ≡⟨ cong (f ∘ interpretation D tt) (≡-× (isContr→isProp isContr⊥→A _ _) (isPropUnit _ _)) ⟩
      f (interpretation D tt args) ∎}

StrictMorphism≡ : {D : PointedDCPO ℓd ℓt} {E : PointedDCPO ℓe ℓt'}
                → {f g : StrictMorphism D E}
                → function f ≡ function g
                → f ≡ g
StrictMorphism≡ = SignatureMorphism≡

strictMorphismIsStrict : {D : PointedDCPO ℓd ℓt} {E : PointedDCPO ℓe ℓt'}
                       → (f : StrictMorphism D E)
                       → function f (least D) ≡ least E
strictMorphismIsStrict {D = D} {E = E} f =
  sym (commutation f tt (rec , tt)) ∙
  cong (interpretation E tt) (≡-× (isContr→isProp isContr⊥→A _ _) refl)