open import Cubical.Foundations.Prelude

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

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

open import Cubical.HITs.PropositionalTruncation as ∥₁

open import Cubical.Relation.Binary.Order.Poset

open import DCPO ℓi

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

⊑lift : (ℓa ℓt : Level) {A : Type ℓa'} (_⊑_ : A → A → Type ℓt')
      → Lift {j = ℓa} A → Lift {j = ℓa} A → Type (ℓ-max ℓt ℓt')
⊑lift ℓa ℓt _⊑_ (lift a) (lift a') = Lift {j = ℓt} (a ⊑ a')

module _ {A : Type ℓa'} {_⊑_ : A → A → Type ℓt'} (isPoset : IsPoset _⊑_) where

  open IsPoset

  isPoset⊑lift : IsPoset (⊑lift ℓa ℓt _⊑_)
  isPoset⊑lift .is-set = isOfHLevelLift  (isPoset .is-set)
  isPoset⊑lift .is-prop-valued x y = isOfHLevelLift  (isPoset .is-prop-valued (lower x) (lower y))
  isPoset⊑lift .is-refl x = lift (isPoset .is-refl (lower x))
  isPoset⊑lift .is-trans x y z x⊑y y⊑z = lift (isPoset .is-trans (lower x) (lower y) (lower z) (lower x⊑y) (lower y⊑z))
  isPoset⊑lift .is-antisym x y x⊑y y⊑x = liftExt (isPoset .is-antisym (lower x) (lower y) (lower x⊑y) (lower y⊑x))

module _ {A : Type ℓa'} where
  lowerIsDirected : (ℓa ℓt : Level) (_⊑_ : A → A → Type ℓt')
                  → {I : Type ℓi} {α : I → Lift A}
                  → (δ : isDirected (⊑lift ℓa ℓt _⊑_) α)
                  → isDirected _⊑_ (lower ∘ α)
  lowerIsDirected ℓa ℓt _⊑_ δ =
    inhabitedIfDirected (⊑lift ℓa ℓt _⊑_) δ ,
    λ i j →
      ∥₁.map
        (λ (k , αᵢ⊑αₖ , αⱼ⊑αₖ)  → k , lower αᵢ⊑αₖ , lower αⱼ⊑αₖ)
        (semidirectedIfDirected (⊑lift ℓa ℓt _⊑_) δ i j)


module _ (ℓd ℓt : Level) (D : DCPO ℓd' ℓt') where
  private
    _⊑_ = ⊑lift ℓd ℓt (order D)

  lowerIsDirected' : {I : Type ℓi} {α : I → Lift ⟨ D ⟩}
                   → (δ : isDirected _⊑_ α)
                   → isDirected (order D) (lower ∘ α)
  lowerIsDirected' δ = lowerIsDirected ℓd ℓt (order D) δ

  liftDCPO : DCPO (ℓ-max ℓd ℓd') (ℓ-max ℓt ℓt')
  liftDCPO = dcpo (Lift {j = ℓd} ⟨ D ⟩) _⊑_ (isPoset⊑lift (posetAxioms D)) dc
    where
      dc : isDirectedComplete _⊑_
      dc δ = lift (∐ D (lowerIsDirected' δ)) ,
             (λ i → lift (∐isUpperbound D (lowerIsDirected' δ) i)) ,
             (λ v vIsUpper → lift (∐isLowerBoundOfUpperbounds D (lowerIsDirected' δ) (lower v) (lower ∘ vIsUpper)))

lowerIsContinuous : (ℓd ℓt : Level) (D : DCPO ℓd' ℓt')
                  → isContinuous (liftDCPO ℓd ℓt D) D lower
lowerIsContinuous ℓd ℓt D I α δ = ∐isSup D (lowerIsDirected' ℓd ℓt D δ)

liftIsContinuous : (ℓd ℓt : Level) (D : DCPO ℓd' ℓt')
                 → isContinuous D (liftDCPO ℓd ℓt D) lift
liftIsContinuous ℓd ℓt D I α δ =
  (λ i → lift (∐isUpperbound D δ i)) ,
  (λ v vIsUpper → lift (∐isLowerBoundOfUpperbounds D δ (lower v) (lower ∘ vIsUpper)))