open import Cubical.Foundations.Prelude

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

open import Cubical.Data.Unit

open import DCPO ℓi
open import DCPO.Constructions.Discrete ℓi
open import DCPO.Constructions.Lift ℓi

unitDCPO : ∀ {ℓd ℓt} → DCPO ℓd ℓt
unitDCPO {ℓd} {ℓt} = liftDCPO ℓd ℓt (discreteDCPO Unit isSetUnit)