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 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}

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}

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}