DCPO.Base

open import Cubical.Foundations.Prelude

module DCPO.Base (ℓi : Level) where

open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Transport

open import Cubical.Data.Bool
open import Cubical.Data.Sigma

open import Cubical.HITs.PropositionalTruncation as ∥₁

open import Cubical.Relation.Binary.Base
open import Cubical.Relation.Binary.Order.Poset

open import Cubical.Reflection.RecordEquiv

open BinaryRelation

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

module _ {D : Type ℓd} (_⊑_ : D → D → Type ℓt) where

  isSemidirected : {I : Type ℓi} (α : I → D) → Type (ℓ-max ℓi ℓt)
  isSemidirected {I = I} α = (i j : I) → ∃[ k ∈ I ] (α i ⊑ α k) × (α j ⊑ α k)

  isPropIsSemidirected : {I : Type ℓi} (α : I → D) → isProp (isSemidirected α)
  isPropIsSemidirected α = isPropΠ2 (λ i j → isPropPropTrunc)

  isDirected : {I : Type ℓi} (α : I → D) → Type (ℓ-max ℓi ℓt)
  isDirected {I = I} α = ∥ I ∥₁ × isSemidirected α

  isPropIsDirected : {I : Type ℓi} (α : I → D) → isProp (isDirected α)
  isPropIsDirected α = isProp× isPropPropTrunc (isPropIsSemidirected α)

  inhabitedIfDirected : {I : Type ℓi} {α : I → D} → isDirected α → ∥ I ∥₁
  inhabitedIfDirected = fst

  semidirectedIfDirected : {I : Type ℓi} {α : I → D} → isDirected α → isSemidirected α
  semidirectedIfDirected = snd

  isUpperbound : {I : Type ℓi} (x : D) (α : I → D) → Type (ℓ-max ℓi ℓt)
  isUpperbound {I = I} x α = (i : I) → α i ⊑ x

  isPropIsUpperbound : {I : Type ℓi}
                     → IsPoset _⊑_
                     → (x : D) (α : I → D) → isProp (isUpperbound x α)
  isPropIsUpperbound isPoset x α = isPropΠ λ i → is-prop-valued (α i) x
    where
      open IsPoset isPoset

  isLowerboundOfUpperbounds : {I : Type ℓi} (x : D) (α : I → D) → Type (ℓ-max (ℓ-max ℓi ℓd) ℓt)
  isLowerboundOfUpperbounds x α = (v : D) → isUpperbound v α → x ⊑ v

  isPropIsLowerboundOfUpperbounds : {I : Type ℓi}
                                  → IsPoset _⊑_
                                  → (x : D) (α : I → D)
                                  → isProp (isLowerboundOfUpperbounds x α)
  isPropIsLowerboundOfUpperbounds isPoset x α = isPropΠ2 (λ v _ → is-prop-valued x v)
    where
      open IsPoset isPoset

  isSup : {I : Type ℓi} (x : D) (α : I → D) → Type (ℓ-max (ℓ-max ℓi ℓd) ℓt)
  isSup x α = isUpperbound x α × isLowerboundOfUpperbounds x α

  isPropIsSup : {I : Type ℓi}
              → IsPoset _⊑_
              → (x : D) (α : I → D)
              → isProp (isSup x α)
  isPropIsSup isPoset x α = isProp× (isPropIsUpperbound isPoset x α)
                                    (isPropIsLowerboundOfUpperbounds isPoset x α)

  supIsUpperbound : {I : Type ℓi} {x : D} {α : I → D}
                  → isSup x α
                  → isUpperbound x α
  supIsUpperbound = fst

  supIsLowerboundOfUpperbounds : {I : Type ℓi} {x : D} {α : I → D}
                               → isSup x α
                               → isLowerboundOfUpperbounds x α
  supIsLowerboundOfUpperbounds = snd

  supsAreUnique : {I : Type ℓi}
                → IsPoset _⊑_
                → (α : I → D) (x y : D)
                → isSup x α
                → isSup y α
                → x ≡ y
  supsAreUnique isPoset α x y xIsSup yIsSup =
    is-antisym x y
      (supIsLowerboundOfUpperbounds xIsSup y (supIsUpperbound yIsSup))
      (supIsLowerboundOfUpperbounds yIsSup x (supIsUpperbound xIsSup))
    where
      open IsPoset isPoset

  hasSup : {I : Type ℓi} (α : I → D) → Type (ℓ-max (ℓ-max ℓi ℓd) ℓt)
  hasSup α = Σ[ x ∈ D ] isSup x α

  isPropHasSup : {I : Type ℓi} (α : I → D) → IsPoset _⊑_ → isProp (hasSup α)
  isPropHasSup α isPoset (u , uIsSup) (v , vIsSup) =
    Σ≡Prop (λ x → isPropIsSup isPoset x α)
      (supsAreUnique isPoset α u v uIsSup vIsSup)

  isDirectedComplete : Type (ℓ-max (ℓ-max (ℓ-suc ℓi) ℓd) ℓt)
  isDirectedComplete = {I : Type ℓi} {α : I → D} (δ : isDirected α) → hasSup α

  isPropIsDirectedComplete : IsPoset _⊑_ → isProp isDirectedComplete
  isPropIsDirectedComplete isPoset =
    isPropImplicitΠ2 λ I α →
      isPropΠ λ δ (x , xIsSup) (y , yIsSup) →
        Σ≡Prop (λ z → isPropIsSup isPoset z α)
               (supsAreUnique isPoset α x y xIsSup yIsSup)

  isLeast : (x : D) → Type (ℓ-max ℓd ℓt)
  isLeast x = (y : D) → x ⊑ y

record DCPOStr (ℓd ℓt : Level) (D : Type ℓd) : Type (ℓ-max (ℓ-max (ℓ-suc ℓi) (ℓ-suc ℓt)) ℓd) where
  constructor dcpostr

  field
    posetStr : PosetStr ℓt D

  _⊑_ : D → D → Type ℓt
  _⊑_ = PosetStr._≤_ posetStr

  field
    is-directed-complete : isDirectedComplete _⊑_

  module posetStr = PosetStr posetStr

DCPO : (ℓd ℓt : Level) → Type (ℓ-max (ℓ-max (ℓ-suc ℓi) (ℓ-suc ℓd)) (ℓ-suc ℓt))
DCPO ℓd ℓt = TypeWithStr ℓd (DCPOStr ℓd ℓt)

dcpo : (D : Type ℓd) (_⊑_ : D → D → Type ℓt)
     → IsPoset _⊑_
     → isDirectedComplete _⊑_
     → DCPO ℓd ℓt
dcpo D _⊑_ isPoset dc = D , dcpostr (posetstr _⊑_ isPoset) dc

order : (D : DCPO ℓd ℓt) → ⟨ D ⟩ → ⟨ D ⟩ → Type ℓt
order D = DCPOStr._⊑_ (str D)

infix 6 order
syntax order D x y = x ⊑⟨ D ⟩ y

posetAxioms : (D : DCPO ℓd ℓt) → IsPoset (order D)
posetAxioms D = DCPOStr.posetStr.isPoset (str D)

sethood : (D : DCPO ℓd ℓt) → isSet ⟨ D ⟩
sethood D = IsPoset.is-set (posetAxioms D)

propValuedness : (D : DCPO ℓd ℓt) → isPropValued (order D)
propValuedness D = IsPoset.is-prop-valued (posetAxioms D)

reflexivity : (D : DCPO ℓd ℓt) → isRefl (order D)
reflexivity D = IsPoset.is-refl (posetAxioms D)

transitivity : (D : DCPO ℓd ℓt) → isTrans (order D)
transitivity D = IsPoset.is-trans (posetAxioms D)

antisymmetry : (D : DCPO ℓd ℓt) → isAntisym (order D)
antisymmetry D = IsPoset.is-antisym (posetAxioms D)

≡→⊑ : (D : DCPO ℓd ℓt) {x y : ⟨ D ⟩} → x ≡ y → x ⊑⟨ D ⟩ y
≡→⊑ D {x = x} p = subst (λ y → x ⊑⟨ D ⟩ y) p (reflexivity D x)

∐ : (D : DCPO ℓd ℓt) {I : Type ℓi} {α : I → ⟨ D ⟩} → isDirected (order D) α → ⟨ D ⟩
∐ D δ = fst (DCPOStr.is-directed-complete (str D) δ)

∐isSup : (D : DCPO ℓd ℓt) {I : Type ℓi} {α : I → ⟨ D ⟩}
       → (δ : isDirected (order D) α)
       → isSup (order D) (∐ D δ) α
∐isSup D δ = snd (DCPOStr.is-directed-complete (str D) δ)

∐isUpperbound : (D : DCPO ℓd ℓt) {I : Type ℓi} {α : I → ⟨ D ⟩}
              → (δ : isDirected (order D) α)
              → isUpperbound (order D) (∐ D δ) α
∐isUpperbound D δ = fst (∐isSup D δ)

∐isLowerBoundOfUpperbounds : (D : DCPO ℓd ℓt) {I : Type ℓi} {α : I → ⟨ D ⟩}
                           → (δ : isDirected (order D) α)
                           → isLowerboundOfUpperbounds (order D) (∐ D δ) α
∐isLowerBoundOfUpperbounds D δ = snd (∐isSup D δ)

∐isMonotone : (D : DCPO ℓd ℓt) {I : Type ℓi} {α β : I → ⟨ D ⟩}
            → (δ : isDirected (order D) α)
            → (ε : isDirected (order D) β)
            → ((i : I) → α i ⊑⟨ D ⟩ β i)
            → ∐ D δ ⊑⟨ D ⟩ ∐ D ε
∐isMonotone D {I} {α} {β} δ ε p =
  ∐isLowerBoundOfUpperbounds D δ (∐ D ε)
    (λ i → transitivity D _ (β i) _ (p i) (∐isUpperbound D ε i))

constIsSup : (D : DCPO ℓd ℓt) {I : Type ℓi} (i : ∥ I ∥₁) {x : ⟨ D ⟩}
           → isSup (order D) x (const {B = I} x)
constIsSup D i {x} =
  ∥₁.rec (isPropIsSup (order D) (posetAxioms D) x (const x))
    (λ i → (λ _ → reflexivity D x) , (λ v vIsUpper → vIsUpper i))
    i

module DCPOReasoning where
  transitivity' : (D : DCPO ℓd ℓt) (x : ⟨ D ⟩) {y z : ⟨ D ⟩}
                → x ⊑⟨ D ⟩ y → y ⊑⟨ D ⟩ z → x ⊑⟨ D ⟩ z
  transitivity' D x = transitivity D x _ _

  reflexivity' = reflexivity

  syntax transitivity' D x x⊑y y⊑z = x ⊑⟨ D ⟩[ x⊑y ] y⊑z
  infixr 0 transitivity'

  syntax reflexivity' D x = x ∎⟨ D ⟩
  infix 1 reflexivity'

isContinuous : (D : DCPO ℓd ℓt) (E : DCPO ℓe ℓt')
             → (⟨ D ⟩ → ⟨ E ⟩)
             → Type (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) ℓd) ℓt) ℓe) ℓt')
isContinuous D E f = (I : Type ℓi) (α : I → ⟨ D ⟩) (δ : isDirected (order D) α)
                    → isSup (order E) (f (∐ D δ)) (f ∘ α)

isPropIsContinuous : (D : DCPO ℓd ℓt) (E : DCPO ℓe ℓt') (f : ⟨ D ⟩ → ⟨ E ⟩)
                   → isProp (isContinuous D E f)
isPropIsContinuous D E f =
  isPropΠ3 (λ I α δ →
    isPropIsSup (order E) (posetAxioms E) (f (∐ D δ)) (f ∘ α))

isMonotone : (D : DCPO ℓd ℓt) (E : DCPO ℓe ℓt')
           → (⟨ D ⟩ → ⟨ E ⟩)
           → Type (ℓ-max (ℓ-max ℓd ℓt) ℓt')
isMonotone D E f = {x y : ⟨ D ⟩} → x ⊑⟨ D ⟩ y → f x ⊑⟨ E ⟩ f y

isPropIsMonotone : (D : DCPO ℓd ℓt) (E : DCPO ℓe ℓt')
                 → (f : ⟨ D ⟩ → ⟨ E ⟩)
                 → isProp (isMonotone D E f)
isPropIsMonotone D E f =
  isPropImplicitΠ2 (λ x y → isPropΠ (λ _ → propValuedness E (f x) (f y)))

isMonotone→imageIsDirected : (D : DCPO ℓd ℓt) (E : DCPO ℓe ℓt')
                           → (f : ⟨ D ⟩ → ⟨ E ⟩)
                           → isMonotone D E f
                           → {I : Type ℓi} {α : I → ⟨ D ⟩} (δ : isDirected (order D) α)
                           → isDirected (order E) (f ∘ α)
isMonotone→imageIsDirected D E f fMonotone δ =
  inhabitedIfDirected (order D) δ ,
  λ i j → ∥₁.map
            (λ (k , αᵢ⊑αₖ , αⱼ⊑αₖ) → k , fMonotone αᵢ⊑αₖ , fMonotone αⱼ⊑αₖ)
            (semidirectedIfDirected (order D) δ i j)

isContinuous→isMonotone : (D : DCPO ℓd ℓt) (E : DCPO ℓe ℓt')
                        → (f : ⟨ D ⟩ → ⟨ E ⟩)
                        → isContinuous D E f
                        → isMonotone D E f
isContinuous→isMonotone D E f fCont {x} {y} x⊑y =
  supIsUpperbound (order E) fySup (lift false)
  where
    α : Bool* → ⟨ D ⟩
    α (lift false) = x
    α (lift true)  = y

    δ : isDirected (order D) α
    δ = ∣ lift false ∣₁ ,
        λ { (lift false) (lift false) → ∣ true* , x⊑y , x⊑y ∣₁
          ; (lift false) (lift true)  → ∣ true* , x⊑y , reflexivity D y ∣₁
          ; (lift true)  (lift false) → ∣ true* , reflexivity D y , x⊑y ∣₁
          ; (lift true)  (lift true)  → ∣ true* , reflexivity D y , reflexivity D y ∣₁ }

    p : ∐ D δ ≡ y
    p = antisymmetry D _ _
          (∐isLowerBoundOfUpperbounds D δ y (λ { (lift false) → x⊑y
                                               ; (lift true)  → reflexivity D y}))
          (∐isUpperbound D δ (lift true))

    fySup : isSup (order E) (f y) (f ∘ α)
    fySup = subst (λ z → isSup (order E) (f z) (f ∘ α)) p (fCont Bool* α δ)

isContinuous→imageIsDirected : (D : DCPO ℓd ℓt) (E : DCPO ℓe ℓt')
                             → (f : ⟨ D ⟩ → ⟨ E ⟩)
                             → isContinuous D E f
                             → {I : Type ℓi} {α : I → ⟨ D ⟩} (δ : isDirected (order D) α)
                             → isDirected (order E) (f ∘ α)
isContinuous→imageIsDirected D E f fCont δ =
  isMonotone→imageIsDirected D E f (isContinuous→isMonotone D E f fCont) δ

continuous∐≡ : {I : Type ℓi} (D : DCPO ℓd ℓt) (E : DCPO ℓe ℓt')
             → (f : ⟨ D ⟩ → ⟨ E ⟩)
             → (fCont : isContinuous D E f)
             → {α : I → ⟨ D ⟩}
             → (δ : isDirected (order D) α)
             → f (∐ D δ)
             ≡ ∐ E {α = f ∘ α} (isContinuous→imageIsDirected D E f fCont δ)
continuous∐≡ {I = I} D E f fCont {α} δ =
  antisymmetry E _ _
    (supIsLowerboundOfUpperbounds (order E) (fCont I α δ)
      (∐ E (isContinuous→imageIsDirected D E f fCont δ))
      (∐isUpperbound E (isContinuous→imageIsDirected D E f fCont δ)))
    (supIsLowerboundOfUpperbounds (order E)
      (∐isSup E (isContinuous→imageIsDirected D E f fCont δ))
      (f (∐ D δ))
      (supIsUpperbound (order E) (fCont I α δ)))

record DCPOMorphism (D : DCPO ℓd ℓt) (E : DCPO ℓe ℓt') : Type (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) ℓd) ℓt) ℓe) ℓt') where
  constructor scottcontinuousmap
  field
    function   : ⟨ D ⟩ → ⟨ E ⟩
    continuity : isContinuous D E function

  monotonicty : isMonotone D E function
  monotonicty = isContinuous→isMonotone D E function continuity

  imageIsDirected : {I : Type ℓi} {α : I → ⟨ D ⟩} (δ : isDirected (order D) α)
                  → isDirected (order E) (function ∘ α)
  imageIsDirected = isMonotone→imageIsDirected D E function monotonicty

  supPreservation : {I : Type ℓi} {α : I → ⟨ D ⟩} (δ : isDirected (order D) α)
                  → function (∐ D δ)
                  ≡ ∐ E {α = function ∘ α} (imageIsDirected δ)
  supPreservation = continuous∐≡ D E function continuity
open DCPOMorphism public

isContinuous-∘ : (D : DCPO ℓd ℓt) (E : DCPO ℓe ℓt') (F : DCPO ℓf ℓt'')
               → (g : ⟨ E ⟩ → ⟨ F ⟩) (f : ⟨ D ⟩ → ⟨ E ⟩)
               → isContinuous E F g
               → isContinuous D E f
               → isContinuous D F (g ∘ f)
isContinuous-∘ D E F g f gCont fCont I α δ =
  subst⁻ (λ x → isSup (order F) x (g ∘ f ∘ α))
    (cong g (continuous∐≡ D E f fCont δ) ∙
     continuous∐≡ E F g gCont (isContinuous→imageIsDirected D E f fCont δ))
    (∐isSup F _)

unquoteDecl DCPOMorphismIsoΣ = declareRecordIsoΣ DCPOMorphismIsoΣ (quote DCPOMorphism)

DCPOMorphism≡ : {D : DCPO ℓd ℓt} {E : DCPO ℓe ℓt'}
              → {f g : DCPOMorphism D E}
              → function f ≡ function g
              → f ≡ g
DCPOMorphism≡ {D = D} {E = E} {f = f} {g = g} p =
  isoFunInjective DCPOMorphismIsoΣ f g
    (Σ≡Prop (isPropIsContinuous D E) p)

isSetDCPOMorphism : {D : DCPO ℓd ℓt} {E : DCPO ℓe ℓt'} → isSet (DCPOMorphism D E)
isSetDCPOMorphism {D = D} {E = E} =
  isOfHLevelRetractFromIso 2 DCPOMorphismIsoΣ
    (isSetΣ (isSetΠ (λ _ → sethood E)) λ f → isProp→isSet (isPropIsContinuous D E f))

constIsContinuous : (D : DCPO ℓd ℓt) (E : DCPO ℓe ℓt')
                  → {x : ⟨ E ⟩}
                  → isContinuous D E (const {B = ⟨ D ⟩} x)
constIsContinuous D E I α δ = constIsSup E (inhabitedIfDirected (order D) δ)

idIsContinuous : (D : DCPO ℓd ℓt)
               → isContinuous D D (λ x → x)
idIsContinuous D I α δ = ∐isSup D δ

idᵈᶜᵖᵒ : {D : DCPO ℓd ℓt} → DCPOMorphism D D
idᵈᶜᵖᵒ {D = D} = scottcontinuousmap (λ x → x) (idIsContinuous D)

module _ {D : DCPO ℓd ℓt} {E : DCPO ℓe ℓt'} {F : DCPO ℓf ℓt''} where
  infixr 9 _∘ᵈᶜᵖᵒ_
  _∘ᵈᶜᵖᵒ_ : (g : DCPOMorphism E F) (f : DCPOMorphism D E)
          → DCPOMorphism D F
  g ∘ᵈᶜᵖᵒ f =
    scottcontinuousmap (function g ∘ function f)
      (isContinuous-∘ D E F (function g) (function f) (continuity g) (continuity f))