open import Cubical.Foundations.Prelude

module DCPO.Constructions.Discrete (ℓi : Level) where

open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure

open import Cubical.Data.Sigma

open import Cubical.HITs.PropositionalTruncation as ∥₁

open import Cubical.Relation.Binary.Order.Poset

open import DCPO ℓi

private
  variable
    ℓa ℓd ℓt : Level

module _(A : Type ℓa) (isSetA : isSet A) where
  open IsPoset

  isPoset≡ : IsPoset _≡_
  isPoset≡ .is-set = isSetA
  isPoset≡ .is-prop-valued = isSetA
  isPoset≡ .is-refl a = refl
  isPoset≡ .is-trans a b c = _∙_
  isPoset≡ .is-antisym a b a≡b _ = a≡b

  isConstantFamily : {I : Type ℓi} (α : I → A) → Type (ℓ-max ℓi ℓa)
  isConstantFamily {I = I} α = Σ[ a ∈ A ] ((i : I) → α i ≡ a)

  theConstantElement : {I : Type ℓi} {α : I → A}
                     → isConstantFamily α
                     → A
  theConstantElement = fst

  αᵢ≡theConstantElement : {I : Type ℓi} {α : I → A}
                        → (γ : isConstantFamily α)
                        → (i : I) → α i ≡ theConstantElement γ
  αᵢ≡theConstantElement = snd

  isPropIsConstantFamily : {I : Type ℓi} (α : I → A) (δ : isDirected _≡_ α)
                         → isProp (isConstantFamily α)
  isPropIsConstantFamily α δ =
    ∥₁.rec isPropIsProp
      (λ i x y →
        ΣPathP (sym (αᵢ≡theConstantElement x i) ∙ αᵢ≡theConstantElement y i ,
                isProp→PathP (λ _ → isPropΠ λ _ → isSetA _ _) _ _))
      (inhabitedIfDirected _≡_ δ)

  discreteDirectedFamilyIsConst : {I : Type ℓi} (α : I → A) (δ : isDirected _≡_ α)
                                → isConstantFamily α
  discreteDirectedFamilyIsConst α δ =
    ∥₁.rec (isPropIsConstantFamily α δ)
      (λ i →
        α i ,
        λ j →
          ∥₁.rec (isSetA (α j) (α i))
            (λ (k , p , q) → q ∙ sym p)
            (semidirectedIfDirected _≡_ δ i j))
      (inhabitedIfDirected _≡_ δ)

  discreteDCPO : DCPO ℓa ℓa
  discreteDCPO = dcpo A _≡_ isPoset≡ dc
    where
      dc : isDirectedComplete _≡_
      dc {α = α} δ =
          theConstantElement (discreteDirectedFamilyIsConst α δ) ,
          αᵢ≡theConstantElement (discreteDirectedFamilyIsConst α δ) ,
          λ v vIsUpper →
            ∥₁.rec (isSetA _ _)
              (λ i →
                sym (αᵢ≡theConstantElement (discreteDirectedFamilyIsConst α δ) i) ∙
                vIsUpper i)
              (inhabitedIfDirected _≡_ δ)

  discreteFunctionIsContinuous : (D : DCPO ℓd ℓt) (f : A → ⟨ D ⟩)
                               → isContinuous discreteDCPO D f
  discreteFunctionIsContinuous D f I α δ =
    (λ i → ≡→⊑ D (cong f (αᵢ≡theConstantElement (discreteDirectedFamilyIsConst α δ) i))) ,
    (λ v vIsUpper →
      ∥₁.rec (propValuedness D (f (∐ discreteDCPO δ)) v)
        (λ i →
          transitivity D _ _ _
            (≡→⊑ D (cong f (sym (αᵢ≡theConstantElement (discreteDirectedFamilyIsConst α δ) i))))
            (vIsUpper i))
        (inhabitedIfDirected _≡_ δ))