Tom de Jong, 27 May 2019.
Refactored 29 April 2020.

We show that lifting (cf. EscardΓ³-Knapp) a set gives the free pointed dcpo on
that set.

When we start with a small set, then the lifting yields an algebraic pointed
dcpo as formalized in LiftingSetAlgebraic.lagda.

The construction that freely adds a least element to a dcpo is described in
LiftingDcpo.lagda.

\begin{code}

{-# OPTIONS --safe --without-K #-}

open import MLTT.Spartan

open import UF.FunExt
open import UF.PropTrunc
open import UF.Subsingletons

module DomainTheory.Lifting.LiftingSet
        (pt : propositional-truncations-exist)
        (fe : Fun-Ext)
        (𝓣 : Universe)
        (pe : propext 𝓣)
       where

open import UF.Base
open import UF.Equiv
open import UF.Hedberg
open import UF.ImageAndSurjection pt
open import UF.Sets
open import UF.Subsingletons-FunExt
open import UF.Subsingletons-Properties

open PropositionalTruncation pt

open import Lifting.Construction 𝓣 hiding (βŠ₯)
open import Lifting.Miscelanea 𝓣
open import Lifting.Miscelanea-PropExt-FunExt 𝓣 pe fe
open import Lifting.Monad 𝓣

open import DomainTheory.Basics.Dcpo pt fe 𝓣
open import DomainTheory.Basics.Miscelanea pt fe 𝓣
open import DomainTheory.Basics.Pointed pt fe 𝓣

open import OrderedTypes.Poset fe

\end{code}

We start by showing that the lifting of a set is indeed a pointed dcpo.

\begin{code}

module _ {𝓀 : Universe}
         {X : 𝓀 Μ‡ }
         (s : is-set X)
       where

 family-value-map : {I : 𝓣 Μ‡ }
                  β†’ (Ξ± : I β†’ 𝓛 X)
                  β†’ (Ξ£ i κž‰ I , is-defined (Ξ± i)) β†’ X
 family-value-map Ξ± (i , d) = value (Ξ± i) d

 directed-family-value-map-is-wconstant : {I : 𝓣 Μ‡ }
                                        β†’ (Ξ± : I β†’ 𝓛 X)
                                        β†’ (Ξ΄ : is-directed _βŠ‘'_ Ξ± )
                                        β†’ wconstant (family-value-map Ξ±)
 directed-family-value-map-is-wconstant {I} Ξ± Ξ΄ (iβ‚€ , dβ‚€) (i₁ , d₁) =
  Ξ³ (semidirected-if-directed _βŠ‘'_ Ξ± Ξ΄ iβ‚€ i₁)
   where
    f : (Ξ£ i κž‰ I , is-defined (Ξ± i)) β†’ X
    f = family-value-map Ξ±
    Ξ³ : (βˆƒ k κž‰ I , (Ξ± iβ‚€ βŠ‘' Ξ± k) Γ— (Ξ± i₁ βŠ‘' Ξ± k)) β†’ f (iβ‚€ , dβ‚€) = f (i₁ , d₁)
    Ξ³ = βˆ₯βˆ₯-rec s g
     where
      g : (Ξ£ k κž‰ I , (Ξ± iβ‚€ βŠ‘' Ξ± k)
                   Γ— (Ξ± i₁ βŠ‘' Ξ± k)) β†’ f (iβ‚€ , dβ‚€) = f (i₁ , d₁)
      g (k , l , m) =
       f (iβ‚€ , dβ‚€)                             =⟨ refl ⟩
       value (Ξ± iβ‚€) dβ‚€                         =⟨ =-of-values-from-= (l dβ‚€) ⟩
       value (Ξ± k) (=-to-is-defined (l dβ‚€) dβ‚€) =⟨ =-of-values-from-= ((m d₁) ⁻¹) ⟩
       value (Ξ± i₁) d₁                         =⟨ refl ⟩
       f (i₁ , d₁)                             ∎

 lifting-sup-value : {I : 𝓣 Μ‡ }
                   β†’ (Ξ± : I β†’ 𝓛 X)
                   β†’ (Ξ΄ : is-directed _βŠ‘'_ Ξ± )
                   β†’ (βˆƒ i κž‰ I , is-defined (Ξ± i)) β†’ X
 lifting-sup-value {I} Ξ± Ξ΄ =
  pr₁ (wconstant-map-to-set-factors-through-truncation-of-domain
        s (family-value-map Ξ±)
        (directed-family-value-map-is-wconstant Ξ± Ξ΄))

 lifting-sup : {I : 𝓣 Μ‡ } β†’ (Ξ± : I β†’ 𝓛 X) β†’ (Ξ΄ : is-directed _βŠ‘'_ Ξ±) β†’ 𝓛 X
 lifting-sup {I} Ξ± Ξ΄ =
  (βˆƒ i κž‰ I , is-defined (Ξ± i)) , lifting-sup-value Ξ± Ξ΄ , βˆ₯βˆ₯-is-prop

 lifting-sup-is-upperbound : {I : 𝓣 Μ‡ } β†’ (Ξ± : I β†’ 𝓛 X)
                             (Ξ΄ : is-directed _βŠ‘'_ Ξ±)
                           β†’ (i : I) β†’ Ξ± i βŠ‘' lifting-sup Ξ± Ξ΄
 lifting-sup-is-upperbound {I} Ξ± Ξ΄ i = Ξ³
  where
   Ξ³ : Ξ± i βŠ‘' lifting-sup Ξ± Ξ΄
   Ξ³ = βŠ‘-to-βŠ‘' (f , v)
    where
     f : is-defined (Ξ± i) β†’ is-defined (lifting-sup Ξ± Ξ΄)
     f d = ∣ i , d ∣
     v : (d : is-defined (Ξ± i)) β†’ value (Ξ± i) d = value (lifting-sup Ξ± Ξ΄) (f d)
     v d = value (α i) d                 =⟨ p    ⟩
           lifting-sup-value α δ (f d)   =⟨ refl ⟩
           value (lifting-sup α δ) (f d) ∎
      where
       p = (prβ‚‚ (wconstant-map-to-set-factors-through-truncation-of-domain
                  s (family-value-map Ξ±)
                  (directed-family-value-map-is-wconstant Ξ± Ξ΄)))
           (i , d)

 family-defined-somewhere-sup-= : {I : 𝓣 Μ‡ } {Ξ± : I β†’ 𝓛 X}
                                β†’ (Ξ΄ : is-directed _βŠ‘'_ Ξ±)
                                β†’ (i : I)
                                β†’ is-defined (Ξ± i)
                                β†’ Ξ± i = lifting-sup Ξ± Ξ΄
 family-defined-somewhere-sup-= {I} {α} δ i d =
  (lifting-sup-is-upperbound Ξ± Ξ΄ i) d

 lifting-sup-is-lowerbound-of-upperbounds : {I : 𝓣 Μ‡ }
                                          β†’ {Ξ± : I β†’ 𝓛 X}
                                          β†’ (Ξ΄ : is-directed _βŠ‘'_ Ξ±)
                                          β†’ (v : 𝓛 X)
                                          β†’ ((i : I) β†’ Ξ± i βŠ‘' v)
                                          β†’ lifting-sup Ξ± Ξ΄ βŠ‘' v
 lifting-sup-is-lowerbound-of-upperbounds {I} {Ξ±} Ξ΄ v b = h
  where
   h : lifting-sup Ξ± Ξ΄ βŠ‘' v
   h d = βˆ₯βˆ₯-rec (lifting-of-set-is-set s) g d
    where
     g : (Ξ£ i κž‰ I , is-defined (Ξ± i)) β†’ lifting-sup Ξ± Ξ΄ = v
     g (i , dᡒ) = lifting-sup α δ =⟨ (family-defined-somewhere-sup-= δ i dᡒ) ⁻¹ ⟩
                  α i             =⟨ b i dᡒ ⟩
                  v               ∎

 𝓛-DCPO : DCPO {𝓣 ⁺ βŠ” 𝓀} {𝓣 ⁺ βŠ” 𝓀}
 𝓛-DCPO = 𝓛 X , _βŠ‘'_ , pa , c
  where
   pa : PosetAxioms.poset-axioms _βŠ‘'_
   pa = sl , p , r , t , a
    where
     open PosetAxioms {_} {_} {𝓛 X} _βŠ‘'_
     sl : is-set (𝓛 X)
     sl = lifting-of-set-is-set s
     p : is-prop-valued
     p _ _ = βŠ‘'-prop-valued s
     r : is-reflexive
     r _ = βŠ‘'-is-reflexive
     a : is-antisymmetric
     a _ _ = βŠ‘'-is-antisymmetric
     t : is-transitive
     t _ _ _ = βŠ‘'-is-transitive
   c : (I : 𝓣 Μ‡ ) (Ξ± : I β†’ 𝓛 X) β†’ is-directed _βŠ‘'_ Ξ± β†’ has-sup _βŠ‘'_ Ξ±
   c I Ξ± Ξ΄ = lifting-sup Ξ± Ξ΄ ,
             lifting-sup-is-upperbound Ξ± Ξ΄ ,
             lifting-sup-is-lowerbound-of-upperbounds Ξ΄

 𝓛-DCPOβŠ₯ : DCPOβŠ₯ {𝓣 ⁺ βŠ” 𝓀} {𝓣 ⁺ βŠ” 𝓀}
 𝓛-DCPOβŠ₯ = 𝓛-DCPO , l , (Ξ» _ β†’ unique-from-𝟘)
  where
   l : 𝓛 X
   l = (𝟘 , 𝟘-elim , 𝟘-is-prop)

\end{code}

Minor addition by Ayberk Tosun.

The lifting of a set as a dcpo as defined above has an order that is essentially
locally small. It is sometimes convenient, however, to repackage the lifting
dcpo with the equivalent order that has small values.

The development where this function is used can be updated as to work on a dcpo
with an external proof of local smallness as to obviate the need for this
repackaging. This is a refactoring to consider in the future.

\begin{code}

 open import Lifting.UnivalentPrecategory 𝓣 X
 open PosetAxioms

 𝓛-DCPO⁻ : DCPO {𝓣 ⁺ βŠ” 𝓀} {𝓣 βŠ” 𝓀}
 𝓛-DCPO⁻ = 𝓛 X , _βŠ‘_ , †
  where
   Ξ³ : {x y : 𝓛 X} β†’ (x βŠ‘ y) ≃ (x βŠ‘' y)
   Ξ³ {x} {y} = logically-equivalent-props-are-equivalent
                (βŠ‘-prop-valued fe fe s x y)
                (βŠ‘'-prop-valued s)
                βŠ‘-to-βŠ‘' βŠ‘'-to-βŠ‘

   p : is-prop-valued _βŠ‘_
   p = βŠ‘-prop-valued fe fe s

   a : is-antisymmetric _βŠ‘_
   a l m p q = βŠ‘'-is-antisymmetric (βŠ‘-to-βŠ‘' p) (βŠ‘-to-βŠ‘' q)

   Ξ΄ : is-directed-complete _βŠ‘_
   Ξ΄ I ΞΉ (i , Ο…)  = lifting-sup ΞΉ Ξ΄β€² , Οƒ
    where
     Ξ΄β€² : is-directed _βŠ‘'_ ΞΉ
     Ξ΄β€² = i
        , Ξ» j k β†’
           βˆ₯βˆ₯-rec
            βˆƒ-is-prop
            (Ξ» { (i , p , q) β†’ ∣ i , βŠ‘-to-βŠ‘' p , βŠ‘-to-βŠ‘' q ∣ })
            (Ο… j k)

     σ₁ : (j : I) β†’ ΞΉ j βŠ‘ lifting-sup ΞΉ Ξ΄β€²
     σ₁ j = βŠ‘'-to-βŠ‘ (lifting-sup-is-upperbound ΞΉ Ξ΄β€² j)

     Οƒβ‚‚ : is-lowerbound-of-upperbounds _βŠ‘_ (lifting-sup ΞΉ Ξ΄β€²) ΞΉ
     Οƒβ‚‚ j Ο† = βŠ‘'-to-βŠ‘
               (lifting-sup-is-lowerbound-of-upperbounds Ξ΄β€² j Ξ» k β†’ βŠ‘-to-βŠ‘' (Ο† k))

     Οƒ : is-sup _βŠ‘_ (lifting-sup ΞΉ Ξ΄β€²) ΞΉ
     Οƒ = σ₁ , Οƒβ‚‚

   † : dcpo-axioms _βŠ‘_
   † = (lifting-of-set-is-set s , p , 𝓛-id , 𝓛-comp , a) , Ξ΄

\end{code}

Now that we have the lifting as a dcpo, we prove that the lifting functor and
Kleisli extension yield continuous maps.

\begin{code}

module _ {𝓀 : Universe}
         {X : 𝓀 Μ‡ }
         (sβ‚€ : is-set X)
         {π“₯ : Universe}
         {Y : π“₯ Μ‡ }
         (s₁ : is-set Y)
       where

 β™―-is-monotone : (f : X β†’ 𝓛 Y) β†’ is-monotone (𝓛-DCPO sβ‚€) (𝓛-DCPO s₁) (f β™―)
 β™―-is-monotone f l m ineq d = ap (f β™―) (ineq (β™―-is-defined f l d))

 β™―-is-continuous : (f : X β†’ 𝓛 Y) β†’ is-continuous (𝓛-DCPO sβ‚€) (𝓛-DCPO s₁) (f β™―)
 β™―-is-continuous f I Ξ± Ξ΄ = u , v
  where
   u : (i : I) β†’ (f β™―) (Ξ± i) βŠ‘βŸ¨ (𝓛-DCPO s₁) ⟩ (f β™―) (∐ (𝓛-DCPO sβ‚€) Ξ΄)
   u i = β™―-is-monotone f (Ξ± i) (∐ (𝓛-DCPO sβ‚€) Ξ΄)
         (∐-is-upperbound (𝓛-DCPO sβ‚€) Ξ΄ i)
   v : (m : ⟨ 𝓛-DCPO s₁ ⟩)
     β†’ ((i : I) β†’ (f β™―) (Ξ± i) βŠ‘βŸ¨ (𝓛-DCPO s₁) ⟩ m)
     β†’ (f β™―) (∐ (𝓛-DCPO sβ‚€) Ξ΄) βŠ‘βŸ¨ (𝓛-DCPO s₁) ⟩ m
   v m ineqs d =
    βˆ₯βˆ₯-rec (lifting-of-set-is-set s₁) g (β™―-is-defined f (∐ (𝓛-DCPO sβ‚€) Ξ΄) d)
     where
      g : (Ξ£ i κž‰ I , is-defined (Ξ± i)) β†’ (f β™―) (∐ (𝓛-DCPO sβ‚€) Ξ΄) = m
      g (i , dα΅’) = (f β™―) (∐ (𝓛-DCPO sβ‚€) Ξ΄) =⟨ h i dα΅’ ⟩
                   (f β™―) (Ξ± i)             =⟨ ineqs i (=-to-is-defined (h i dα΅’) d) ⟩
                   m                       ∎
       where
        h : (i : I) β†’ is-defined (Ξ± i) β†’ (f β™―) (∐ (𝓛-DCPO sβ‚€) Ξ΄) = (f β™―) (Ξ± i)
        h i d = ap (f β™―) ((family-defined-somewhere-sup-= sβ‚€ Ξ΄ i d) ⁻¹)

 𝓛̇-continuous : (f : X β†’ Y) β†’ is-continuous (𝓛-DCPO sβ‚€) (𝓛-DCPO s₁) (𝓛̇ f)
 𝓛̇-continuous f = transport
                   (is-continuous (𝓛-DCPO sβ‚€) (𝓛-DCPO s₁))
                   (dfunext fe (𝓛̇-β™―-∼ f))
                   (β™―-is-continuous (Ξ· ∘ f))

\end{code}

Finally we show that the lifting of a set gives the free pointed dcpo on that
set. The main technical tool in proving this is the use of subsingleton suprema,
cf. DomainTheory.Basics.Pointed.lagda, and the fact that every partial element
can be expressed as such a supremum.

\begin{code}

module _
         {X : 𝓀 Μ‡ }
         (X-is-set : is-set X)
       where

 private
  𝓛X : DCPOβŠ₯ {𝓣 ⁺ βŠ” 𝓀} {𝓣 ⁺ βŠ” 𝓀}
  𝓛X = 𝓛-DCPOβŠ₯ X-is-set

 all-partial-elements-are-subsingleton-sups :
    (l : βŸͺ 𝓛X ⟫)
  β†’ l = ∐˒˒ 𝓛X (Ξ· ∘ value l) (being-defined-is-prop l)
 all-partial-elements-are-subsingleton-sups (P , Ο• , ρ) =
  antisymmetry (𝓛X ⁻) (P , Ο• , ρ) (∐˒˒ 𝓛X (Ξ· ∘ Ο•) ρ) u v
   where
    v : ∐˒˒ 𝓛X (Ξ· ∘ Ο•) ρ βŠ‘' (P , Ο• , ρ)
    v = ∐˒˒-is-lowerbound-of-upperbounds 𝓛X (Ξ· ∘ Ο•) ρ (P , Ο• , ρ)
         (Ξ» p ⋆ β†’ (is-defined-Ξ·-= p) ⁻¹)
    u : (P , Ο• , ρ) βŠ‘' ∐˒˒ 𝓛X (Ξ· ∘ Ο•) ρ
    u p = antisymmetry (𝓛X ⁻) (P , Ο• , ρ) (∐˒˒ 𝓛X (Ξ· ∘ Ο•) ρ)
           u' v
     where
      u' = (P , Ο• , ρ)      βŠ‘βŸͺ 𝓛X ⟫[ =-to-βŠ‘ (𝓛X ⁻) (is-defined-Ξ·-= p) ]
           Ξ· (Ο• p)          βŠ‘βŸͺ 𝓛X ⟫[ ∐˒˒-is-upperbound 𝓛X (Ξ· ∘ Ο•) ρ p ]
           ∐˒˒ 𝓛X (Ξ· ∘ Ο•) ρ ∎βŸͺ 𝓛X ⟫

 module lifting-is-free-pointed-dcpo-on-set
         (𝓓 : DCPOβŠ₯ {π“₯} {𝓦})
         (f : X β†’ βŸͺ 𝓓 ⟫)
       where

  fΜƒ : βŸͺ 𝓛X ⟫ β†’ βŸͺ 𝓓 ⟫
  fΜƒ (P , Ο• , P-is-prop) = ∐˒˒ 𝓓 (f ∘ Ο•) P-is-prop

  fΜƒ-is-strict : is-strict 𝓛X 𝓓 fΜƒ
  fΜƒ-is-strict = strictness-criterion 𝓛X 𝓓 fΜƒ Ξ³
   where
    Ξ³ : fΜƒ (βŠ₯ 𝓛X) βŠ‘βŸͺ 𝓓 ⟫ βŠ₯ 𝓓
    Ξ³ = ∐˒˒-is-lowerbound-of-upperbounds 𝓓
         (f ∘ unique-from-𝟘) 𝟘-is-prop (βŠ₯ 𝓓) 𝟘-induction

  fΜƒ-is-continuous : is-continuous (𝓛X ⁻) (𝓓 ⁻) fΜƒ
  f̃-is-continuous I α δ = ub , lb-of-ubs
   where
    s : 𝓛 X
    s = ∐ (𝓛X ⁻) Ξ΄
    ρ : (l : 𝓛 X) β†’ is-prop (is-defined l)
    ρ = being-defined-is-prop
    lemma : (i : I) (p : is-defined (Ξ± i))
          β†’ value (Ξ± i) p = value s ∣ i , p ∣
    lemma i p = =-of-values-from-=
                 (family-defined-somewhere-sup-= X-is-set δ i p)
    ub : (i : I) β†’ fΜƒ (Ξ± i) βŠ‘βŸͺ 𝓓 ⟫ fΜƒ s
    ub i = ∐˒˒-is-lowerbound-of-upperbounds 𝓓 (f ∘ value (Ξ± i)) (ρ (Ξ± i)) (fΜƒ s) Ξ³
     where
      Ξ³ : (p : is-defined (Ξ± i))
        β†’ f (value (Ξ± i) p) βŠ‘βŸͺ 𝓓 ⟫ fΜƒ s
      Ξ³ p = f (value (Ξ± i) p)     βŠ‘βŸͺ 𝓓 ⟫[ β¦…1⦆ ]
            f (value s ∣ i , p ∣) βŠ‘βŸͺ 𝓓 ⟫[ β¦…2⦆ ]
            fΜƒ s                   ∎βŸͺ 𝓓 ⟫
       where
        β¦…1⦆ = =-to-βŠ‘ (𝓓 ⁻) (ap f (lemma i p))
        β¦…2⦆ = ∐˒˒-is-upperbound 𝓓 (f ∘ value s) (ρ s) ∣ i , p ∣
    lb-of-ubs : is-lowerbound-of-upperbounds (underlying-order (𝓓 ⁻))
                 (fΜƒ s) (fΜƒ ∘ Ξ±)
    lb-of-ubs y y-is-ub = ∐˒˒-is-lowerbound-of-upperbounds 𝓓 (f ∘ value s) (ρ s)
                           y Ξ³
     where
      Ξ³ : (q : is-defined s)
        β†’ (f (value s q)) βŠ‘βŸͺ 𝓓 ⟫ y
      Ξ³ q = βˆ₯βˆ₯-rec (prop-valuedness (𝓓 ⁻) (f (value s q)) y) r q
       where
        r : (Ξ£ i κž‰ I , is-defined (Ξ± i)) β†’ f (value s q) βŠ‘βŸͺ 𝓓 ⟫ y
        r (i , p) = f (value s q)                     βŠ‘βŸͺ 𝓓 ⟫[ β¦…1⦆       ]
                    f (value s ∣ i , p ∣)             βŠ‘βŸͺ 𝓓 ⟫[ β¦…2⦆       ]
                    f (value (Ξ± i) p)                 βŠ‘βŸͺ 𝓓 ⟫[ β¦…3⦆       ]
                    ∐˒˒ 𝓓 (f ∘ value (Ξ± i)) (ρ (Ξ± i)) βŠ‘βŸͺ 𝓓 ⟫[ y-is-ub i ]
                    y                                 ∎βŸͺ 𝓓 ⟫
         where
          β¦…1⦆ = =-to-βŠ‘ (𝓓 ⁻) (ap f (value-is-constant s q ∣ i , p ∣))
          β¦…2⦆ = =-to-βŠ’ (𝓓 ⁻) (ap f (lemma i p))
          β¦…3⦆ = ∐˒˒-is-upperbound 𝓓 (f ∘ value (Ξ± i))
                                    (being-defined-is-prop (Ξ± i)) p

  fΜƒ-after-Ξ·-is-f : fΜƒ ∘ Ξ· ∼ f
  fΜƒ-after-Ξ·-is-f x = antisymmetry (𝓓 ⁻) (fΜƒ (Ξ· x)) (f x) u v
   where
    u : fΜƒ (Ξ· x) βŠ‘βŸͺ 𝓓 ⟫ f x
    u = ∐˒˒-is-lowerbound-of-upperbounds 𝓓 (f ∘ (Ξ» _ β†’ x)) πŸ™-is-prop
         (f x) (Ξ» _ β†’ reflexivity (𝓓 ⁻) (f x))
    v : f x βŠ‘βŸͺ 𝓓 ⟫ fΜƒ (Ξ· x)
    v = ∐˒˒-is-upperbound 𝓓 (Ξ» _ β†’ f x) πŸ™-is-prop ⋆

  fΜƒ-is-unique : (g : βŸͺ 𝓛X ⟫ β†’ βŸͺ 𝓓 ⟫)
              β†’ is-continuous (𝓛X ⁻) (𝓓 ⁻) g
              β†’ is-strict 𝓛X 𝓓 g
              β†’ g ∘ Ξ· = f
              β†’ g ∼ fΜƒ
  fΜƒ-is-unique g con str eq (P , Ο• , ρ) = g (P , Ο• , ρ)        =⟨ β¦…1⦆  ⟩
                                         g (∐˒˒ 𝓛X (Ξ· ∘ Ο•) ρ) =⟨ β¦…2⦆  ⟩
                                         ∐˒˒ 𝓓 (g ∘ Ξ· ∘ Ο•) ρ  =⟨ β¦…3⦆  ⟩
                                         ∐˒˒ 𝓓 (f ∘ Ο•) ρ      =⟨ refl ⟩
                                         fΜƒ (P , Ο• , ρ)        ∎
    where
     β¦…1⦆ = ap g (all-partial-elements-are-subsingleton-sups (P , Ο• , ρ))
     β¦…2⦆ = ∐˒˒-=-if-continuous-and-strict 𝓛X 𝓓 g con str (Ξ· ∘ Ο•) ρ
     β¦…3⦆ = ∐˒˒-family-= 𝓓 ρ (ap (_∘ Ο•) eq)

  𝓛-gives-the-free-pointed-dcpo-on-a-set :
   βˆƒ! h κž‰ (βŸͺ 𝓛X ⟫ β†’ βŸͺ 𝓓 ⟫) , is-continuous (𝓛X ⁻) (𝓓 ⁻) h
                           Γ— is-strict 𝓛X 𝓓 h
                           Γ— (h ∘ Ξ· = f)
  𝓛-gives-the-free-pointed-dcpo-on-a-set =
   (f̃ , f̃-is-continuous , f̃-is-strict , (dfunext fe f̃-after-η-is-f)) , γ
    where
     Ξ³ : is-central (Ξ£ h κž‰ (βŸͺ 𝓛X ⟫ β†’ βŸͺ 𝓓 ⟫) , is-continuous (𝓛X ⁻) (𝓓 ⁻) h
                                            Γ— is-strict 𝓛X 𝓓 h
                                            Γ— (h ∘ Ξ· = f))
          (f̃ , f̃-is-continuous , f̃-is-strict , dfunext fe f̃-after-η-is-f)
     Ξ³ (g , cont , str , eq) =
      to-subtype-= (Ξ» h β†’ ×₃-is-prop (being-continuous-is-prop (𝓛X ⁻) (𝓓 ⁻) h)
                                     (being-strict-is-prop 𝓛X 𝓓 h)
                                     (equiv-to-prop
                                       (≃-funext fe (h ∘ Ξ·) f)
                                       (Ξ -is-prop fe (Ξ» _ β†’ sethood (𝓓 ⁻)))))
                                     ((dfunext fe
                                               (fΜƒ-is-unique g cont str eq)) ⁻¹)

\end{code}

In general, the lifting of a set is only directed complete and does not have all
(small) sups, but if we lift propositions, then we do get all small suprema.

As an application, we use this to prove that π““βˆž is algebraic in
DomainTheory.Bilimits.Dinfinity.lagda.

\begin{code}

open import DomainTheory.Basics.SupComplete pt fe 𝓣

module _
        {P : 𝓀 Μ‡ }
        (P-is-prop : is-prop P)
       where

 private
  𝓛P :  DCPO {𝓣 ⁺ βŠ” 𝓀} {𝓣 ⁺ βŠ” 𝓀}
  𝓛P = 𝓛-DCPO (props-are-sets (P-is-prop))

 lifting-of-prop-is-sup-complete : is-sup-complete 𝓛P
 lifting-of-prop-is-sup-complete = record { ⋁ = sup ; ⋁-is-sup = lemma }
  where
   sup-map : {I : 𝓣 Μ‡ } (Ξ± : I β†’ ⟨ 𝓛P ⟩) β†’ (βˆƒ i κž‰ I , is-defined (Ξ± i)) β†’ P
   sup-map Ξ± = βˆ₯βˆ₯-rec P-is-prop (Ξ» (i , q) β†’ value (Ξ± i) q)
   sup : {I : 𝓣 Μ‡ } (Ξ± : I β†’ ⟨ 𝓛P ⟩) β†’ ⟨ 𝓛P ⟩
   sup {I} Ξ± = ((βˆƒ i κž‰ I , is-defined (Ξ± i)) , sup-map Ξ± , βˆƒ-is-prop)
   lemma : {I : 𝓣 Μ‡ } (Ξ± : I β†’ ⟨ 𝓛P ⟩) β†’ is-sup _βŠ‘'_ (sup Ξ±) Ξ±
   lemma {I} Ξ± = (ub , lb-of-ubs)
    where
     ub : (i : I) β†’ Ξ± i βŠ‘' sup Ξ±
     ub i = βŠ‘-to-βŠ‘' (f , g)
      where
       f : is-defined (Ξ± i) β†’ βˆƒ i κž‰ I , is-defined (Ξ± i)
       f p = ∣ i , p ∣
       g : value (Ξ± i) ∼ (Ξ» q β†’ sup-map Ξ± ∣ i , q ∣)
       g q = P-is-prop (value (α i) q) (sup-map α ∣ i , q ∣)
     lb-of-ubs : is-lowerbound-of-upperbounds _βŠ‘'_ (sup Ξ±) Ξ±
     lb-of-ubs l l-is-ub = βŠ‘-to-βŠ‘' (f , g)
      where
       f : (βˆƒ i κž‰ I , is-defined (Ξ± i)) β†’ is-defined l
       f = βˆ₯βˆ₯-rec (being-defined-is-prop l) h
        where
         h : (Ξ£ i κž‰ I , is-defined (Ξ± i)) β†’ is-defined l
         h (i , q) = =-to-is-defined (l-is-ub i q) q
       g : sup-map Ξ± ∼ (Ξ» q β†’ value l (f q))
       g q = P-is-prop (sup-map Ξ± q) (value l (f q))

\end{code}

Added 5 June 2024.

An equivalence of types induces an isomorphism of pointed dcpos on the liftings.

\begin{code}

𝓛̇-β‰ƒα΅ˆαΆœα΅–α΅’βŠ₯ : {X : 𝓀 Μ‡  } {Y : 𝓦 Μ‡  } (i : is-set X) (j : is-set Y)
          β†’ X ≃ Y
          β†’ 𝓛-DCPOβŠ₯ i β‰ƒα΅ˆαΆœα΅–α΅’βŠ₯ 𝓛-DCPOβŠ₯ j
𝓛̇-β‰ƒα΅ˆαΆœα΅–α΅’βŠ₯ i j e = β‰ƒα΅ˆαΆœα΅–α΅’-to-β‰ƒα΅ˆαΆœα΅–α΅’βŠ₯ (𝓛-DCPOβŠ₯ i) (𝓛-DCPOβŠ₯ j) I
 where
  I : 𝓛-DCPO i β‰ƒα΅ˆαΆœα΅–α΅’ 𝓛-DCPO j
  I = 𝓛̇ ⌜ e ⌝ ,
      𝓛̇ ⌜ e ⌝⁻¹  ,
      (Ξ» x β†’ ap (Ξ» - β†’ 𝓛̇ - x) (dfunext fe (inverses-are-retractions' e))) ,
      (Ξ» x β†’ ap (Ξ» - β†’ 𝓛̇ - x) (dfunext fe (inverses-are-sections' e))) ,
      𝓛̇-continuous i j ⌜ e ⌝ ,
      𝓛̇-continuous j i ⌜ e ⌝⁻¹

𝓛̇-β‰ƒα΅ˆαΆœα΅–α΅’ : {X : 𝓀 Μ‡  } {Y : 𝓦 Μ‡  } (i : is-set X) (j : is-set Y)
         β†’ X ≃ Y
         β†’ 𝓛-DCPO i β‰ƒα΅ˆαΆœα΅–α΅’ 𝓛-DCPO j
𝓛̇-β‰ƒα΅ˆαΆœα΅–α΅’ i j e = β‰ƒα΅ˆαΆœα΅–α΅’βŠ₯-to-β‰ƒα΅ˆαΆœα΅–α΅’ (𝓛-DCPOβŠ₯ i) (𝓛-DCPOβŠ₯ j) (𝓛̇-β‰ƒα΅ˆαΆœα΅–α΅’βŠ₯ i j e)

\end{code}