Tom de Jong, 9 February 2022

We describe how to freely add a least element to a dcpo. This is done by lifting
the underlying set, but when ordering the lifting, we have to take the order on
the original dcpo into account.

We also show that taking the free dcpo on a set X coincides with freely adding a
least element to X when viewed as a discretely-ordered dcpo.

\begin{code}

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

open import MLTT.Spartan hiding (J)

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

module DomainTheory.Lifting.LiftingDcpo
        (pt : propositional-truncations-exist)
        (fe : Fun-Ext)
        (π“₯ : Universe)
        (pe : propext π“₯)
       where

open PropositionalTruncation pt

open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.ImageAndSurjection pt
open import UF.Sets
open import UF.Subsingletons-FunExt

open import Lifting.Construction π“₯ hiding (βŠ₯)
open import Lifting.IdentityViaSIP π“₯
open import Lifting.Miscelanea π“₯
open import Lifting.Miscelanea-PropExt-FunExt π“₯ pe fe
                                             renaming ( βŠ‘'-to-βŠ‘ to βŠ‘'-to-βŠ‘''
                                                      ; βŠ‘-to-βŠ‘' to βŠ‘''-to-βŠ‘')

open import OrderedTypes.Poset fe
open import DomainTheory.Basics.Dcpo pt fe π“₯
open import DomainTheory.Basics.Miscelanea pt fe π“₯
open import DomainTheory.Basics.Pointed pt fe π“₯
open import DomainTheory.Lifting.LiftingSet pt fe π“₯ pe
             renaming ( 𝓛-DCPO  to 𝓛-DCPO-on-set ; 𝓛-DCPOβŠ₯ to 𝓛-DCPOβŠ₯-on-set)

\end{code}

We first construct the pointed dcpo.

\begin{code}

module freely-add-βŠ₯
        (𝓓 : DCPO {𝓀} {𝓣})
       where

 𝓛D : π“₯ ⁺ βŠ” 𝓀 Μ‡
 𝓛D = 𝓛 ⟨ 𝓓 ⟩

 _βŠ‘_ : 𝓛D β†’ 𝓛D β†’ π“₯ βŠ” 𝓣 Μ‡
 (P , Ο† , _) βŠ‘ (Q , ψ , _) = Ξ£ f κž‰ (P β†’ Q) , ((p : P) β†’ Ο† p βŠ‘βŸ¨ 𝓓 ⟩ ψ (f p))

 βŠ‘-is-prop-valued : (k l : 𝓛D) β†’ is-prop (k βŠ‘ l)
 βŠ‘-is-prop-valued k l =
  Ξ£-is-prop (Ξ -is-prop fe (Ξ» p β†’ being-defined-is-prop l))
            (Ξ» f β†’ Ξ -is-prop fe (Ξ» p β†’ prop-valuedness 𝓓
                                        (value k p) (value l (f p))))

 βŠ‘-is-reflexive : (l : 𝓛D) β†’ l βŠ‘ l
 βŠ‘-is-reflexive l = (id , (Ξ» p β†’ reflexivity 𝓓 (value l p)))

 βŠ‘-is-transitive : (k l m : 𝓛D) β†’ k βŠ‘ l β†’ l βŠ‘ m β†’ k βŠ‘ m
 βŠ‘-is-transitive k l m (f , s) (g , t) = (g ∘ f , Ξ³)
  where
   Ξ³ : (p : is-defined k) β†’ value k p βŠ‘βŸ¨ 𝓓 ⟩ value m (g (f p))
   Ξ³ p = value k p         βŠ‘βŸ¨ 𝓓 ⟩[ s p     ]
         value l (f p)     βŠ‘βŸ¨ 𝓓 ⟩[ t (f p) ]
         value m (g (f p)) ∎⟨ 𝓓 ⟩

 βŠ‘-is-antisymmetric : (k l : 𝓛D) β†’ k βŠ‘ l β†’ l βŠ‘ k β†’ k = l
 βŠ‘-is-antisymmetric k l (f , s) (g , t) = ⋍-to-= Ξ³
  where
   Ξ³ : k ⋍ l
   Ξ³ = (e , dfunext fe (Ξ» p β†’ antisymmetry 𝓓 (value k p) (value l (⌜ e ⌝ p))
                               (s p) (h p)))
    where
     e : is-defined k ≃ is-defined l
     e = logically-equivalent-props-are-equivalent (being-defined-is-prop k)
                                                   (being-defined-is-prop l) f g
     h : (p : is-defined k) β†’ value l (⌜ e ⌝ p) βŠ‘βŸ¨ 𝓓 ⟩ value k p
     h p = value l (⌜ e ⌝ p)     βŠ‘βŸ¨ 𝓓 ⟩[ t (⌜ e ⌝ p) ]
           value k (g (⌜ e ⌝ p)) βŠ‘βŸ¨ 𝓓 ⟩[ lemma       ]
           value k p             ∎⟨ 𝓓 ⟩
      where
       lemma = =-to-βŠ‘ 𝓓 (value-is-constant k (g (⌜ e ⌝ p)) p)

 family-in-dcpo : {I : π“₯ Μ‡ } (Ξ± : I β†’ 𝓛D) β†’ (Ξ£ i κž‰ I , is-defined (Ξ± i)) β†’ ⟨ 𝓓 ⟩
 family-in-dcpo {I} Ξ± (i , p) = value (Ξ± i) p

 family-in-dcpo-is-semidirected : {I : π“₯ Μ‡ } (Ξ± : I β†’ 𝓛D)
                                β†’ is-semidirected _βŠ‘_ Ξ±
                                β†’ is-semidirected (underlying-order 𝓓)
                                   (family-in-dcpo Ξ±)
 family-in-dcpo-is-semidirected {I} Ξ± Ξ±-semidir (i , pα΅’) (j , pβ±Ό) =
  βˆ₯βˆ₯-functor Ξ³ (Ξ±-semidir i j)
   where
    Ξ³ : (Ξ£ k κž‰ I , (Ξ± i βŠ‘ Ξ± k) Γ— (Ξ± j βŠ‘ Ξ± k))
      β†’ (Ξ£ q κž‰ domain (family-in-dcpo Ξ±) ,
               value (Ξ± i) pα΅’ βŠ‘βŸ¨ 𝓓 ⟩ value (Ξ± (pr₁ q)) (prβ‚‚ q)
             Γ— value (Ξ± j) pβ±Ό βŠ‘βŸ¨ 𝓓 ⟩ value (Ξ± (pr₁ q)) (prβ‚‚ q))
    Ξ³ (k , (f , s) , (g , t)) = ((k , f pα΅’) , (s pα΅’) , Ο„)
     where
      Ο„ = value (Ξ± j) pβ±Ό     βŠ‘βŸ¨ 𝓓 ⟩[ t pβ±Ό  ]
          value (Ξ± k) (g pβ±Ό) βŠ‘βŸ¨ 𝓓 ⟩[ lemma ]
          value (Ξ± k) (f pα΅’) ∎⟨ 𝓓 ⟩
       where
        lemma = =-to-βŠ‘ 𝓓 (value-is-constant (Ξ± k) (g pβ±Ό) (f pα΅’))

 family-in-dcpo-is-directed : {I : π“₯ Μ‡ } (Ξ± : I β†’ 𝓛D)
                            β†’ is-directed _βŠ‘_ Ξ±
                            β†’ βˆƒ i κž‰ I , is-defined (Ξ± i)
                            β†’ is-Directed 𝓓 (family-in-dcpo Ξ±)
 family-in-dcpo-is-directed Ξ± Ξ΄ q =
  (q , family-in-dcpo-is-semidirected Ξ± (semidirected-if-directed _βŠ‘_ Ξ± Ξ΄))

 𝓛-DCPO : DCPO {π“₯ ⁺ βŠ” 𝓀} {π“₯ βŠ” 𝓣}
 𝓛-DCPO = (𝓛D , _βŠ‘_ , (lifting-of-set-is-set (sethood 𝓓)
                    , βŠ‘-is-prop-valued
                    , βŠ‘-is-reflexive
                    , βŠ‘-is-transitive
                    , βŠ‘-is-antisymmetric) ,
                    Ξ³)
  where
   Ξ³ : is-directed-complete _βŠ‘_
   Ξ³ I Ξ± Ξ΄ = (s , s-is-ub , s-is-lb-of-ubs)
    where
     J : π“₯ Μ‡
     J = Ξ£ i κž‰ I , is-defined (Ξ± i)
     Ξ² : J β†’ ⟨ 𝓓 ⟩
     Ξ² = family-in-dcpo Ξ±
     Ξ΅ : βˆ₯ J βˆ₯ β†’ is-Directed 𝓓 Ξ²
     Ξ΅ = family-in-dcpo-is-directed Ξ± Ξ΄
     s : 𝓛D
     s = βˆ₯ J βˆ₯ , t
      where
       t : (βˆ₯ J βˆ₯ β†’ ⟨ 𝓓 ⟩) Γ— is-prop βˆ₯ J βˆ₯
       t = (Ξ» q β†’ ∐ 𝓓 (Ξ΅ q)) , βˆ₯βˆ₯-is-prop
     s-is-ub : (i : I) β†’ Ξ± i βŠ‘ s
     s-is-ub i = (f , (Ξ» qα΅’ β†’ ∐-is-upperbound 𝓓 (Ξ΅ (f qα΅’)) (i , qα΅’)))
      where
       f : is-defined (Ξ± i) β†’ βˆ₯ J βˆ₯
       f qᡒ = ∣ i , qᡒ ∣
     s-is-lb-of-ubs : is-lowerbound-of-upperbounds _βŠ‘_ s Ξ±
     s-is-lb-of-ubs l l-is-ub = (f , r)
      where
       f : βˆ₯ J βˆ₯ β†’ is-defined l
       f = βˆ₯βˆ₯-rec (being-defined-is-prop l) (Ξ» (i , qα΅’) β†’ pr₁ (l-is-ub i) qα΅’)
       r : (q : βˆ₯ J βˆ₯) β†’ ∐ 𝓓 (Ξ΅ q) βŠ‘βŸ¨ 𝓓 ⟩ value l (f q)
       r q = ∐-is-lowerbound-of-upperbounds 𝓓 (Ξ΅ q) (value l (f q)) ub
        where
         ub : (j : J) β†’ Ξ² j βŠ‘βŸ¨ 𝓓 ⟩ value l (f q)
         ub (i , qα΅’) = value (Ξ± i) qα΅’               βŠ‘βŸ¨ 𝓓 ⟩[ prβ‚‚ (l-is-ub i) qα΅’ ]
                       value l (pr₁ (l-is-ub i) qα΅’) βŠ‘βŸ¨ 𝓓 ⟩[ lemma              ]
                       value l (f q)                ∎⟨ 𝓓 ⟩
          where
           lemma = =-to-βŠ‘ 𝓓 (value-is-constant l (pr₁ (l-is-ub i) qα΅’) (f q))

 𝓛-DCPOβŠ₯ : DCPOβŠ₯ {π“₯ ⁺ βŠ” 𝓀} {π“₯ βŠ” 𝓣}
 𝓛-DCPOβŠ₯ = (𝓛-DCPO , (𝟘 , 𝟘-elim , 𝟘-is-prop)
                   , (Ξ» l β†’ 𝟘-elim , 𝟘-induction))

\end{code}

Added 3 July 2024 (but known much earlier of course).

\begin{code}

 𝓛-DCPO-is-locally-small : is-locally-small 𝓓 β†’ is-locally-small 𝓛-DCPO
 𝓛-DCPO-is-locally-small ls =
  record { _βŠ‘β‚›_ = _β‰Ό_ ;
           βŠ‘β‚›-≃-βŠ‘ = Ξ£-cong (Ξ» f β†’ Ξ -cong fe fe (Ξ» p β†’ βŠ‘β‚›-≃-βŠ‘)) }
  where
   open is-locally-small ls
   _β‰Ό_ : 𝓛D β†’ 𝓛D β†’ π“₯ Μ‡
   (P , Ο† , _) β‰Ό (Q , ψ , _) = Ξ£ f κž‰ (P β†’ Q) , ((p : P) β†’ Ο† p βŠ‘β‚› ψ (f p))

\end{code}

Of course, the map Ξ· from the dcpo to the lifted dcpo should be Scott
continuous.

\begin{code}

 Ξ·-is-continuous : is-continuous 𝓓 𝓛-DCPO Ξ·
 Ξ·-is-continuous I Ξ± Ξ΄ = (ub , lb-of-ubs)
  where
   ub : (i : I) β†’ Ξ· (Ξ± i) βŠ‘ Ξ· (∐ 𝓓 Ξ΄)
   ub i = ((Ξ» ⋆ β†’ ⋆) , (Ξ» ⋆ β†’ ∐-is-upperbound 𝓓 Ξ΄ i))
   lb-of-ubs : is-lowerbound-of-upperbounds (underlying-order 𝓛-DCPO) (Ξ· (∐ 𝓓 Ξ΄))
                (η ∘ α)
   lb-of-ubs l l-is-ub = βˆ₯βˆ₯-rec (prop-valuedness 𝓛-DCPO (Ξ· (∐ 𝓓 Ξ΄)) l)
                                Ξ³
                                (inhabited-if-Directed 𝓓 Ξ± Ξ΄)
    where
     q : (i : I) β†’ is-defined l
     q i = pr₁ (l-is-ub i) ⋆
     ub' : (i j : I) β†’ Ξ± j βŠ‘βŸ¨ 𝓓 ⟩ value l (q i)
     ub' i j = Ξ± j           βŠ‘βŸ¨ 𝓓 ⟩[ prβ‚‚ (l-is-ub j) ⋆ ]
               value l (q j) βŠ‘βŸ¨ 𝓓 ⟩[ =-to-βŠ‘ 𝓓 (value-is-constant l (q j) (q i)) ]
               value l (q i) ∎⟨ 𝓓 ⟩
     Ξ³ : I β†’ Ξ· (∐ 𝓓 Ξ΄) βŠ‘ l
     Ξ³ i = ((Ξ» ⋆ β†’ q i)
          , (Ξ» ⋆ β†’ ∐-is-lowerbound-of-upperbounds 𝓓 Ξ΄ (value l (q i)) (ub' i)))

 𝓛-order-lemma : {k l : 𝓛D} β†’ k βŠ‘' l β†’ k βŠ‘ l
 𝓛-order-lemma {k} {l} k-below-l = (pr₁ claim , (Ξ» p β†’ =-to-βŠ‘ 𝓓 (prβ‚‚ claim p)))
  where
   open import Lifting.UnivalentPrecategory π“₯ ⟨ 𝓓 ⟩ renaming (_βŠ‘_ to _βŠ‘''_)
   claim : k βŠ‘'' l
   claim = βŠ‘'-to-βŠ‘'' k-below-l

\end{code}

We now prove that the construction above freely adds a least element to the
dcpo.

\begin{code}

 module _
         (𝓔 : DCPOβŠ₯ {𝓀'} {𝓣'})
         (f : ⟨ 𝓓 ⟩ β†’ βŸͺ 𝓔 ⟫)
         (f-is-continuous : is-continuous 𝓓 (𝓔 ⁻) f)
        where

  open lifting-is-free-pointed-dcpo-on-set (sethood 𝓓) 𝓔 f

  fΜƒ-is-monotone : is-monotone 𝓛-DCPO (𝓔 ⁻) fΜƒ
  fΜƒ-is-monotone k l k-below-l = ∐˒˒-is-lowerbound-of-upperbounds 𝓔 (f ∘ value k)
                                 (being-defined-is-prop k) (f̃ l) lem
   where
    lem : (p : is-defined k) β†’ f (value k p) βŠ‘βŸͺ 𝓔 ⟫ fΜƒ l
    lem p = f (value k p) βŠ‘βŸͺ 𝓔 ⟫[ β¦…1⦆ ]
            f (value l q) βŠ‘βŸͺ 𝓔 ⟫[ β¦…2⦆ ]
            fΜƒ l           ∎βŸͺ 𝓔 ⟫
     where
      q : is-defined l
      q = pr₁ k-below-l p
      β¦…1⦆ = monotone-if-continuous 𝓓 (𝓔 ⁻) (f , f-is-continuous)
             (value k p) (value l q) (prβ‚‚ k-below-l p)
      β¦…2⦆ = ∐˒˒-is-upperbound 𝓔 (f ∘ value l) (being-defined-is-prop l) q

  fΜƒ-is-continuous' : is-continuous 𝓛-DCPO (𝓔 ⁻) fΜƒ
  fΜƒ-is-continuous' = continuity-criterion 𝓛-DCPO (𝓔 ⁻) fΜƒ fΜƒ-is-monotone Ξ³
   where
    Ξ³ : (I : π“₯ Μ‡ )(Ξ± : I β†’ ⟨ 𝓛-DCPO ⟩) (Ξ΄ : is-Directed 𝓛-DCPO Ξ±)
      β†’ fΜƒ (∐ 𝓛-DCPO {I} {Ξ±} Ξ΄) βŠ‘βŸͺ 𝓔 ⟫
        ∐ (𝓔 ⁻) (image-is-directed 𝓛-DCPO (𝓔 ⁻) fΜƒ-is-monotone {I} {Ξ±} Ξ΄)
    Ξ³ I Ξ± Ξ΄ = ∐˒˒-is-lowerbound-of-upperbounds 𝓔 (f ∘ value s)
               (being-defined-is-prop s) (∐ (𝓔 ⁻) Ξ΅) lem
     where
      s : ⟨ 𝓛-DCPO ⟩
      s = ∐ 𝓛-DCPO {I} {Ξ±} Ξ΄
      Ξ΅ : is-Directed (𝓔 ⁻) (fΜƒ ∘ Ξ±)
      Ξ΅ = image-is-directed 𝓛-DCPO (𝓔 ⁻) fΜƒ-is-monotone {I} {Ξ±} Ξ΄
      lem : (q : is-defined s) β†’ f (value s q) βŠ‘βŸͺ 𝓔 ⟫ ∐ (𝓔 ⁻) Ξ΅
      lem q = f (value s q) βŠ‘βŸͺ 𝓔 ⟫[ β¦…1⦆ ]
              f (∐ 𝓓 Ξ΄')    βŠ‘βŸͺ 𝓔 ⟫[ β¦…2⦆ ]
              ∐ (𝓔 ⁻) Ξ΅'    βŠ‘βŸͺ 𝓔 ⟫[ β¦…3⦆ ]
              ∐ (𝓔 ⁻) Ξ΅     ∎βŸͺ 𝓔 ⟫
       where
        Ξ΄' : is-Directed 𝓓 (family-in-dcpo Ξ±)
        Ξ΄' = family-in-dcpo-is-directed Ξ± Ξ΄ q
        Ξ΅' : is-Directed (𝓔 ⁻) (f ∘ family-in-dcpo Ξ±)
        Ξ΅' = image-is-directed' 𝓓 (𝓔 ⁻) (f , f-is-continuous) Ξ΄'
        β¦…1⦆ = reflexivity (𝓔 ⁻) (f (∐ 𝓓 Ξ΄'))
        β¦…2⦆ = continuous-∐-βŠ‘ 𝓓 (𝓔 ⁻) (f , f-is-continuous) Ξ΄'
        β¦…3⦆ = ∐-is-lowerbound-of-upperbounds (𝓔 ⁻) Ξ΅' (∐ (𝓔 ⁻) Ξ΅) claim
         where
          claim : ((i , p) : (Ξ£ i κž‰ I , is-defined (Ξ± i)))
                β†’ (f (value (Ξ± i) p)) βŠ‘βŸͺ 𝓔 ⟫ ∐ (𝓔 ⁻) Ξ΅
          claim (i , p) = (f (value (Ξ± i) p)) βŠ‘βŸͺ 𝓔 ⟫[ ⦅†⦆ ]
                          fΜƒ (Ξ± i)             βŠ‘βŸͺ 𝓔 ⟫[ ⦅‑⦆ ]
                          ∐ (𝓔 ⁻) Ξ΅           ∎βŸͺ 𝓔 ⟫
           where
            ⦅†⦆ = ∐˒˒-is-upperbound 𝓔 (f ∘ value (Ξ± i))
                   (being-defined-is-prop (Ξ± i)) p
            ⦅‑⦆ = ∐-is-upperbound (𝓔 ⁻) Ξ΅ i

  fΜƒ-is-strict' : is-strict 𝓛-DCPOβŠ₯ 𝓔 fΜƒ
  f̃-is-strict' = f̃-is-strict

  fΜƒ-after-Ξ·-is-f' : fΜƒ ∘ Ξ· ∼ f
  f̃-after-η-is-f' = f̃-after-η-is-f

  𝓛-DCPOβ‚› : DCPO
  𝓛-DCPOβ‚› = 𝓛-DCPO-on-set (sethood 𝓓)

  𝓛-monotone-lemma : (g : 𝓛D β†’ βŸͺ 𝓔 ⟫)
                   β†’ is-monotone 𝓛-DCPO  (𝓔 ⁻) g
                   β†’ is-monotone 𝓛-DCPOβ‚› (𝓔 ⁻) g
  𝓛-monotone-lemma g g-mon k l k-below-l = g-mon k l (𝓛-order-lemma k-below-l)

  𝓛-directed-lemma : {I : π“₯ Μ‡ } {Ξ± : I β†’ 𝓛D}
                   β†’ is-Directed 𝓛-DCPOβ‚› Ξ±
                   β†’ is-Directed 𝓛-DCPO Ξ±
  𝓛-directed-lemma {I} {Ξ±} Ξ΄ = (inhabited-if-Directed 𝓛-DCPOβ‚› Ξ± Ξ΄ , Οƒ)
   where
    Οƒ : is-semidirected _βŠ‘_ Ξ±
    Οƒ i j = βˆ₯βˆ₯-functor Ξ³ (semidirected-if-Directed 𝓛-DCPOβ‚› Ξ± Ξ΄ i j)
     where
      Ξ³ : (Ξ£ k κž‰ I , (Ξ± i βŠ‘' Ξ± k) Γ— (Ξ± j βŠ‘' Ξ± k))
        β†’ (Ξ£ k κž‰ I , (Ξ± i βŠ‘ Ξ± k) Γ— (Ξ± j βŠ‘ Ξ± k))
      Ξ³ (k , u , v) = (k , 𝓛-order-lemma u , 𝓛-order-lemma v)

  𝓛-sup-lemma : {I : π“₯ Μ‡ } {Ξ± : I β†’ 𝓛D} (Ξ΄ : is-Directed 𝓛-DCPOβ‚› Ξ±)
              β†’ ∐ 𝓛-DCPOβ‚› Ξ΄ = ∐ 𝓛-DCPO {I} {Ξ±} (𝓛-directed-lemma Ξ΄)
  𝓛-sup-lemma {I} {Ξ±} Ξ΄ = ⋍-to-= (e , dfunext fe Ξ³)
   where
    Ξ΅ : is-Directed 𝓛-DCPO Ξ±
    Ξ΅ = 𝓛-directed-lemma Ξ΄
    e : is-defined (∐ 𝓛-DCPOβ‚› Ξ΄) ≃ is-defined (∐ 𝓛-DCPO {I} {Ξ±} Ξ΅)
    e = ≃-refl (βˆƒ i κž‰ I , is-defined (Ξ± i))
    Ξ³ : (q : is-defined (∐ 𝓛-DCPO {I} {Ξ±} Ξ΅))
      β†’ value (∐ 𝓛-DCPOβ‚› Ξ΄) q = value (∐ 𝓛-DCPO {I} {Ξ±} Ξ΅) (⌜ e ⌝ q)
    Ξ³ q = βˆ₯βˆ₯-rec (sethood 𝓓) goal q
     where
      goal : (Ξ£ i κž‰ I , is-defined (Ξ± i))
           β†’ value (∐ 𝓛-DCPOβ‚› Ξ΄) q = value (∐ 𝓛-DCPO {I} {Ξ±} Ξ΅) (⌜ e ⌝ q)
      goal (i , qα΅’) = value (∐ 𝓛-DCPOβ‚› Ξ΄) q                =⟨ β¦…1⦆  ⟩
                      value (Ξ± i) qα΅’                       =⟨ β¦…2⦆  ⟩
                      ∐ 𝓓 Ξ΅'                               =⟨ refl ⟩
                      value (∐ 𝓛-DCPO {I} {Ξ±} Ξ΅) (⌜ e ⌝ q) ∎
       where
        Ξ΅' : is-Directed 𝓓 (family-in-dcpo Ξ±)
        Ξ΅' = family-in-dcpo-is-directed Ξ± Ξ΅ q
        β¦…1⦆ = (=-of-values-from-= (family-defined-somewhere-sup-=
                                   (sethood 𝓓) Ξ΄ i qα΅’)) ⁻¹
        β¦…2⦆ = antisymmetry 𝓓 (value (Ξ± i) qα΅’) (∐ 𝓓 Ξ΅') ⦅†⦆ ⦅‑⦆
         where
          ⦅†⦆ : value (Ξ± i) qα΅’ βŠ‘βŸ¨ 𝓓 ⟩ ∐ 𝓓 Ξ΅'
          ⦅†⦆ = ∐-is-upperbound 𝓓 Ξ΅' (i , qα΅’)
          ⦅‑⦆ : ∐ 𝓓 Ξ΅' βŠ‘βŸ¨ 𝓓 ⟩ value (Ξ± i) qα΅’
          ⦅‑⦆ = ∐-is-lowerbound-of-upperbounds 𝓓 Ξ΅' (value (Ξ± i) qα΅’) ub
           where
            ub : ((j , qβ±Ό) : Ξ£ i' κž‰ I , is-defined (Ξ± i'))
               β†’ value (Ξ± j) qβ±Ό βŠ‘βŸ¨ 𝓓 ⟩ value (Ξ± i) qα΅’
            ub (j , qβ±Ό) = =-to-βŠ‘ 𝓓 (=-of-values-from-= (lemma j qβ±Ό))
             where
              lemma : (j : I) (qβ±Ό : is-defined (Ξ± j)) β†’ Ξ± j = Ξ± i
              lemma j qβ±Ό =
               βˆ₯βˆ₯-rec (lifting-of-set-is-set (sethood 𝓓)) claim
                      (semidirected-if-Directed 𝓛-DCPOβ‚› Ξ± Ξ΄ i j)
               where
                claim : (Ξ£ k κž‰ I , (Ξ± i βŠ‘' Ξ± k) Γ— (Ξ± j βŠ‘' Ξ± k)) β†’ Ξ± j = Ξ± i
                claim (k , u , v) = v qβ±Ό βˆ™ (u qα΅’) ⁻¹

  𝓛-continuity-lemma : (g : 𝓛D β†’ βŸͺ 𝓔 ⟫)
                     β†’ is-continuous 𝓛-DCPO  (𝓔 ⁻) g
                     β†’ is-continuous 𝓛-DCPOβ‚› (𝓔 ⁻) g
  𝓛-continuity-lemma g g-cont = continuity-criterion' 𝓛-DCPOβ‚› (𝓔 ⁻) g g-mon lemma
   where
    g-mon : is-monotone 𝓛-DCPOβ‚› (𝓔 ⁻) g
    g-mon = 𝓛-monotone-lemma g (monotone-if-continuous 𝓛-DCPO (𝓔 ⁻) (g , g-cont))
    lemma : (I : π“₯ Μ‡ )(Ξ± : I β†’ 𝓛D) (Ξ΄ : is-Directed 𝓛-DCPOβ‚› Ξ±)
          β†’ is-lowerbound-of-upperbounds (underlying-order (𝓔 ⁻))
                                         (g (∐ 𝓛-DCPOβ‚› Ξ΄)) (g ∘ Ξ±)
    lemma I Ξ± Ξ΄ = transport T claim
                   (sup-is-lowerbound-of-upperbounds (underlying-order (𝓔 ⁻))
                                                     (g-cont I Ξ± Ξ΅))
     where
      T : 𝓛D β†’ π“₯ βŠ” 𝓀' βŠ” 𝓣' Μ‡
      T - = is-lowerbound-of-upperbounds (underlying-order (𝓔 ⁻)) (g -) (g ∘ Ξ±)
      Ξ΅ : is-Directed 𝓛-DCPO Ξ±
      Ξ΅ = 𝓛-directed-lemma Ξ΄
      claim : ∐ 𝓛-DCPO {I} {Ξ±} Ξ΅ = ∐ 𝓛-DCPOβ‚› {I} {Ξ±} Ξ΄
      claim = (𝓛-sup-lemma Ξ΄) ⁻¹

  fΜƒ-is-unique' : (g : 𝓛D β†’ βŸͺ 𝓔 ⟫)
               β†’ is-continuous 𝓛-DCPO (𝓔 ⁻) g
               β†’ is-strict 𝓛-DCPOβŠ₯ 𝓔 g
               β†’ g ∘ Ξ· = f
               β†’ g ∼ fΜƒ
  f̃-is-unique' g g-cont = f̃-is-unique g g-cont'
   where
    g-cont' : is-continuous (𝓛-DCPO-on-set (sethood 𝓓)) (𝓔 ⁻) g
    g-cont' = 𝓛-continuity-lemma g g-cont

  𝓛-gives-the-free-pointed-dcpo-on-a-dcpo :
   βˆƒ! h κž‰ (βŸͺ 𝓛-DCPOβŠ₯ ⟫ β†’ βŸͺ 𝓔 ⟫) , is-continuous (𝓛-DCPOβŠ₯ ⁻) (𝓔 ⁻) h
                                Γ— is-strict 𝓛-DCPOβŠ₯ 𝓔 h
                                Γ— (h ∘ Ξ· = f)
  𝓛-gives-the-free-pointed-dcpo-on-a-dcpo =
   (f̃ , f̃-is-continuous' , f̃-is-strict' , (dfunext fe f̃-after-η-is-f')) , γ
    where
     Ξ³ : is-central (Ξ£ h κž‰ (βŸͺ 𝓛-DCPOβŠ₯ ⟫ β†’ βŸͺ 𝓔 ⟫)
                         , is-continuous (𝓛-DCPOβŠ₯ ⁻) (𝓔 ⁻) h
                         Γ— is-strict 𝓛-DCPOβŠ₯ 𝓔 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 (𝓛-DCPOβŠ₯ ⁻) (𝓔 ⁻) h)
                           (being-strict-is-prop 𝓛-DCPOβŠ₯ 𝓔 h)
                           (equiv-to-prop
                             (≃-funext fe (h ∘ Ξ·) f)
                             (Ξ -is-prop fe (Ξ» _ β†’ sethood (𝓔 ⁻)))))
                           ((dfunext fe (fΜƒ-is-unique' g cont str eq)) ⁻¹)

\end{code}

Finally, we show that taking the free dcpo on a set X coincides with freely
adding a least element to X when viewed as a discretely-ordered dcpo. This also
follows abstractly from the fact that we can compose adjunctions, but we give a
direct proof.

\begin{code}

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

 XΜƒ : DCPO {𝓀} {𝓀}
 X̃ = (X , _=_ , pa , γ)
  where
   open PosetAxioms {𝓀} {𝓀} {X} _=_
   pa : poset-axioms
   pa = (X-is-set
      , (Ξ» x y β†’ X-is-set)
      , (Ξ» x β†’ refl)
      , (Ξ» x y z β†’ _βˆ™_)
      , (Ξ» x y u v β†’ u))
   γ : is-directed-complete _=_
   Ξ³ I Ξ± Ξ΄ = βˆ₯βˆ₯-rec (having-sup-is-prop _=_ pa Ξ±) lemma
                    (inhabited-if-directed _=_ α δ)
    where
     Ξ±-constant : (i j : I) β†’ Ξ± i = Ξ± j
     Ξ±-constant i j = βˆ₯βˆ₯-rec X-is-set h (semidirected-if-directed _=_ Ξ± Ξ΄ i j)
      where
       h : (Ξ£ k κž‰ I , (Ξ± i = Ξ± k) Γ— (Ξ± j = Ξ± k)) β†’ Ξ± i = Ξ± j
       h (k , p , q) = p βˆ™ q ⁻¹
     lemma : I β†’ has-sup _=_ Ξ±
     lemma i = (Ξ± i , ub , lb-of-ubs)
      where
       ub : (j : I) β†’ Ξ± j = Ξ± i
       ub j = Ξ±-constant j i
       lb-of-ubs : is-lowerbound-of-upperbounds _=_ (α i) α
       lb-of-ubs y y-is-ub = y-is-ub i

 module _ where
  open freely-add-βŠ₯ XΜƒ

  𝓛-order-lemma-converse : {k l : 𝓛 X} β†’ k βŠ‘ l β†’ k βŠ‘' l
  𝓛-order-lemma-converse {k} {l} k-below-l = βŠ‘''-to-βŠ‘' k-below-l

 open freely-add-βŠ₯

 liftings-coincide : 𝓛-DCPOβŠ₯ XΜƒ β‰ƒα΅ˆαΆœα΅–α΅’βŠ₯ 𝓛-DCPOβŠ₯-on-set X-is-set
 liftings-coincide = β‰ƒα΅ˆαΆœα΅–α΅’-to-β‰ƒα΅ˆαΆœα΅–α΅’βŠ₯ (𝓛-DCPOβŠ₯ XΜƒ) 𝓛-DCPOβŠ₯-X
                           (id , id , (Ξ» _ β†’ refl) , (Ξ» _ β†’ refl) ,
                            cont₁ , contβ‚‚)
  where
   𝓛-DCPOβŠ₯-X : DCPOβŠ₯
   𝓛-DCPOβŠ₯-X = 𝓛-DCPOβŠ₯-on-set X-is-set
   cont₁ : is-continuous (𝓛-DCPOβŠ₯ XΜƒ ⁻) (𝓛-DCPOβŠ₯-X ⁻) id
   cont₁ I Ξ± Ξ΄ = (ub , lb-of-ubs)
    where
     ub : (i : I) β†’ Ξ± i βŠ‘' ∐ (𝓛-DCPOβŠ₯ XΜƒ ⁻) {I} {Ξ±} Ξ΄
     ub i = (𝓛-order-lemma-converse (∐-is-upperbound (𝓛-DCPOβŠ₯ XΜƒ ⁻) {I} {Ξ±} Ξ΄ i))
     lb-of-ubs : is-lowerbound-of-upperbounds _βŠ‘'_ (∐ (𝓛-DCPOβŠ₯ XΜƒ ⁻) {I} {Ξ±} Ξ΄) Ξ±
     lb-of-ubs l l-is-ub = 𝓛-order-lemma-converse
                            (∐-is-lowerbound-of-upperbounds (𝓛-DCPOβŠ₯ XΜƒ ⁻) {I} {Ξ±}
                            Ξ΄ l
                            (Ξ» i β†’ 𝓛-order-lemma XΜƒ (l-is-ub i)))
   contβ‚‚ : is-continuous (𝓛-DCPOβŠ₯-X ⁻) (𝓛-DCPOβŠ₯ XΜƒ ⁻) id
   contβ‚‚ = 𝓛-continuity-lemma XΜƒ (𝓛-DCPOβŠ₯ XΜƒ) Ξ· (Ξ·-is-continuous XΜƒ)
            id (id-is-continuous (𝓛-DCPOβŠ₯ XΜƒ ⁻))

\end{code}