Tom de Jong, May 2019.
Refactored January 2020, December 2021.
February 2022: Show that pointed dcpos have semidirected and subsingleton
suprema.

We define dcpos with a least element, typically denoted by β₯, which are called
pointed dcpos. A map between pointed dcpos is called strict if it preserves
least elements. We show that every isomorphism of dcpos is strict.

Finally, we show that pointed dcpos have semidirected and subsingleton suprema
and that these are preserved by maps that are both strict and Scott continuous.

\begin{code}

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

open import MLTT.Spartan
open import UF.FunExt
open import UF.PropTrunc

module DomainTheory.Basics.Pointed
(pt : propositional-truncations-exist)
(fe : Fun-Ext)
(π₯ : Universe)
where

open PropositionalTruncation pt hiding (_β¨_)

open import UF.Subsingletons

open import DomainTheory.Basics.Dcpo pt fe π₯
open import DomainTheory.Basics.Miscelanea pt fe π₯

module _ {π€ π£ : Universe} where

DCPOβ₯ : (π₯ βΊ) β (π€ βΊ) β (π£ βΊ) Μ
DCPOβ₯ = Ξ£ π κ DCPO {π€} {π£} , has-least (underlying-order π)

_β» : DCPOβ₯ β DCPO
_β» = prβ

βͺ_β« : DCPOβ₯ β π€ Μ
βͺ π β« = β¨ π β» β©

underlying-orderβ₯ : (π : DCPOβ₯) β βͺ π β« β βͺ π β« β π£ Μ
underlying-orderβ₯ π = underlying-order (π β»)

syntax underlying-orderβ₯ π x y = x ββͺ π β« y

β₯ : (π : DCPOβ₯) β β¨ π β» β©
β₯ (π , x , p) = x

β₯-is-least : (π : DCPOβ₯) β is-least (underlying-order (π β»)) (β₯ π)
β₯-is-least (π , x , p) = p

transitivity'' : (π : DCPOβ₯) (x : βͺ π β«) {y z : βͺ π β«}
β x ββͺ π β« y β y ββͺ π β« z β x ββͺ π β« z
transitivity'' π = transitivity' (π β»)

reflexivity' : (π : DCPOβ₯) β reflexive (underlying-order (π β»))
reflexivity' (D , _) = reflexivity D

syntax transitivity'' π x u v = x ββͺ π β«[ u ] v
infixr 0 transitivity''

syntax reflexivity' π x = x ββͺ π β«
infix 1 reflexivity'

is-a-non-trivial-pointed-dcpo : (π : DCPOβ₯ {π€} {π£}) β π€ Μ
is-a-non-trivial-pointed-dcpo π = β x κ βͺ π β« , x β  β₯ π

οΌ-to-β₯-criterion : (π : DCPOβ₯ {π€} {π£}) {x : βͺ π β«} β x ββͺ π β« β₯ π β x οΌ β₯ π
οΌ-to-β₯-criterion π {x} x-below-β₯ =
antisymmetry (π β») x (β₯ π) x-below-β₯ (β₯-is-least π x)

DCPOβ₯[_,_] : DCPOβ₯ {π€} {π£} β DCPOβ₯ {π€'} {π£'} β (π₯ βΊ) β π€ β π£ β π€' β π£' Μ
DCPOβ₯[ π , π ] = DCPO[ π β» , π β» ]

is-strict : (π : DCPOβ₯ {π€} {π£}) (π : DCPOβ₯ {π€'} {π£'})
β (βͺ π β« β βͺ π β«)
β π€' Μ
is-strict π π f = f (β₯ π) οΌ β₯ π

β-is-strict : {π€'' π£'' : Universe}
(π : DCPOβ₯ {π€} {π£}) (π : DCPOβ₯ {π€'} {π£'})
(π' : DCPOβ₯ {π€''} {π£''})
(f : βͺ π β« β βͺ π β«) (g : βͺ π β« β βͺ π' β«)
β is-strict π π f
β is-strict π π' g
β is-strict π π' (g β f)
β-is-strict π π π' f g sf sg = ap g sf β sg

being-strict-is-prop : (π : DCPOβ₯ {π€} {π£}) (π : DCPOβ₯ {π€'} {π£'})
(f : βͺ π β« β βͺ π β«)
β is-prop (is-strict π π f)
being-strict-is-prop π π f = sethood (π β»)

strictness-criterion : (π : DCPOβ₯ {π€} {π£}) (π : DCPOβ₯ {π€'} {π£'})
(f : βͺ π β« β βͺ π β«)
β f (β₯ π) ββͺ π β« β₯ π
β is-strict π π f
strictness-criterion π π f crit =
antisymmetry (π β») (f (β₯ π)) (β₯ π) crit (β₯-is-least π (f (β₯ π)))

\end{code}

Defining isomorphisms of pointed dcpos and showing that every isomorphism of
dcpos is automatically strict.

\begin{code}

_βα΅αΆα΅α΅β₯_ : (π : DCPOβ₯ {π€} {π£}) (π : DCPOβ₯ {π€'} {π£'}) β π₯ βΊ β π€ β π£ β π€' β π£' Μ
π βα΅αΆα΅α΅β₯ π = Ξ£ f κ (β¨ π β» β© β β¨ π β» β©) , Ξ£ g κ (β¨ π β» β© β β¨ π β» β©) ,
((d : β¨ π β» β©) β g (f d) οΌ d)
Γ ((e : β¨ π β» β©) β f (g e) οΌ e)
Γ is-continuous (π β») (π β») f
Γ is-continuous (π β») (π β») g
Γ is-strict π π f
Γ is-strict π π g

βα΅αΆα΅α΅β₯-to-βα΅αΆα΅α΅ : (π : DCPOβ₯ {π€} {π£}) (π : DCPOβ₯ {π€'} {π£'})
β π βα΅αΆα΅α΅β₯ π β (π β») βα΅αΆα΅α΅ (π β»)
βα΅αΆα΅α΅β₯-to-βα΅αΆα΅α΅ π π (f , g , s , r , cf , cg , sf , sg) =
f , g , s , r , cf , cg

βα΅αΆα΅α΅-to-βα΅αΆα΅α΅β₯ : (π : DCPOβ₯ {π€} {π£}) (π : DCPOβ₯ {π€'} {π£'})
β (π β») βα΅αΆα΅α΅ (π β») β π βα΅αΆα΅α΅β₯ π
βα΅αΆα΅α΅-to-βα΅αΆα΅α΅β₯ π π (f , g , gf , fg , cf , cg) =
f , g , gf , fg , cf , cg , sf , sg
where
sf : is-strict π π f
sf = antisymmetry (π β») (f (β₯ π)) (β₯ π) Ξ³ (β₯-is-least π (f (β₯ π)))
where
Ξ³ = f (β₯ π)     ββ¨ π β» β©[ lβ ]
f (g (β₯ π)) ββ¨ π β» β©[ lβ ]
β₯ π         ββ¨ π β» β©
where
lβ = monotone-if-continuous (π β») (π β») (f , cf) (β₯ π) (g (β₯ π))
(β₯-is-least π (g (β₯ π)))
lβ = οΌ-to-β (π β») (fg (β₯ π))
sg : is-strict π π g
sg = antisymmetry (π β») (g (β₯ π)) (β₯ π) Ξ³ (β₯-is-least π (g (β₯ π)))
where
Ξ³ = g (β₯ π)     ββ¨ π β» β©[ lβ ]
g (f (β₯ π)) ββ¨ π β» β©[ lβ ]
β₯ π         ββ¨ π β» β©
where
lβ = monotone-if-continuous (π β») (π β») (g , cg) (β₯ π) (f (β₯ π))
(β₯-is-least π (f (β₯ π)))
lβ = οΌ-to-β (π β») (gf (β₯ π))

\end{code}

Pointed dcpos have semidirected & subsingleton suprema and these are preserved
by maps that are both strict and continuous.

This is used to prove (in DomainTheroy.Lifting.LiftingSet.lagda) that the
lifting yields the free pointed dcpo on a set.

\begin{code}

add-β₯ : (π : DCPOβ₯ {π€} {π£}) {I : π₯ Μ } (Ξ± : I β βͺ π β«)
β (π{π₯} + I) β βͺ π β«
add-β₯ π Ξ± (inl β) = β₯ π
add-β₯ π Ξ± (inr i) = Ξ± i

add-β₯-is-directed : (π : DCPOβ₯ {π€} {π£}) {I : π₯ Μ } {Ξ± : I β βͺ π β«}
β is-semidirected (underlying-order (π β»)) Ξ±
β is-Directed (π β») (add-β₯ π Ξ±)
add-β₯-is-directed π {I} {Ξ±} Ο = β£ inl β β£ , Ξ΄
where
Ξ΄ : is-semidirected (underlying-order (π β»)) (add-β₯ π Ξ±)
Ξ΄ (inl β) a       = β£ a , β₯-is-least π (add-β₯ π Ξ± a) ,
reflexivity (π β») (add-β₯ π Ξ± a) β£
Ξ΄ (inr i) (inl β) = β£ (inr i) , reflexivity (π β») (Ξ± i)
, β₯-is-least π (Ξ± i)        β£
Ξ΄ (inr i) (inr j) = β₯β₯-functor (Ξ» (k , u , v) β (inr k , u , v)) (Ο i j)

adding-β₯-preserves-sup : (π : DCPOβ₯ {π€} {π£}) {I : π₯ Μ }
(Ξ± : I β βͺ π β«) (x : βͺ π β«)
β is-sup (underlying-order (π β»)) x Ξ±
β is-sup (underlying-order (π β»)) x (add-β₯ π Ξ±)
adding-β₯-preserves-sup π {I} Ξ± x x-is-sup = x-is-ub , x-is-lb-of-ubs
where
x-is-ub : (i : π + I) β add-β₯ π Ξ± i ββͺ π β« x
x-is-ub (inl β) = β₯-is-least π x
x-is-ub (inr i) = sup-is-upperbound (underlying-order (π β»)) x-is-sup i
x-is-lb-of-ubs : is-lowerbound-of-upperbounds (underlying-order (π β»))
x-is-lb-of-ubs y y-is-ub = sup-is-lowerbound-of-upperbounds
(underlying-order (π β»)) x-is-sup y
(Ξ» i β y-is-ub (inr i))

adding-β₯-reflects-sup : (π : DCPOβ₯ {π€} {π£}) {I : π₯ Μ }
(Ξ± : I β βͺ π β«) (x : βͺ π β«)
β is-sup (underlying-order (π β»)) x (add-β₯ π Ξ±)
β is-sup (underlying-order (π β»)) x Ξ±
adding-β₯-reflects-sup π {I} Ξ± x x-is-sup = x-is-ub , x-is-lb-of-ubs
where
x-is-ub : (i : I) β Ξ± i ββͺ π β« x
x-is-ub i = sup-is-upperbound (underlying-order (π β»)) x-is-sup (inr i)
x-is-lb-of-ubs : is-lowerbound-of-upperbounds (underlying-order (π β»)) x Ξ±
x-is-lb-of-ubs y y-is-ub = sup-is-lowerbound-of-upperbounds
(underlying-order (π β»)) x-is-sup y
h
where
h : is-upperbound (underlying-order (π β»)) y (add-β₯ π Ξ±)
h (inl β) = β₯-is-least π y
h (inr i) = y-is-ub i

semidirected-complete-if-pointed : (π : DCPOβ₯ {π€} {π£}) {I : π₯ Μ } {Ξ± : I β βͺ π β«}
β is-semidirected (underlying-order (π β»)) Ξ±
β has-sup (underlying-order (π β»)) Ξ±
semidirected-complete-if-pointed π {I} {Ξ±} Ο = x , x-is-sup
where
Ξ΄ : is-Directed (π β») (add-β₯ π Ξ±)
x : βͺ π β«
x = β (π β») Ξ΄
x-is-sup : is-sup (underlying-order (π β»)) x Ξ±
x-is-sup = adding-β₯-reflects-sup π Ξ± x (β-is-sup (π β») Ξ΄)

pointed-if-semidirected-complete : (π : DCPO {π€} {π£})
β ({I : π₯ Μ } {Ξ± : I β β¨ π β©}
β is-semidirected (underlying-order π) Ξ±
β has-sup (underlying-order π) Ξ±)
β has-least (underlying-order π)
pointed-if-semidirected-complete π c = x , x-is-least
where
Ξ± : π β β¨ π β©
Ξ± = π-elim
Ο : is-semidirected (underlying-order π) Ξ±
Ο = π-induction
x = the-sup (underlying-order π) (c Ο)
x-is-least : is-least (underlying-order π) x
x-is-least y =
sup-is-lowerbound-of-upperbounds
(underlying-order π)
(sup-property (underlying-order π) (c Ο))
y π-induction

βΛ’α΅ : (π : DCPOβ₯ {π€} {π£}) {I : π₯ Μ } {Ξ± : I β βͺ π β«}
β is-semidirected (underlying-order (π β»)) Ξ± β βͺ π β«
βΛ’α΅ π {I} {Ξ±} Ο = prβ (semidirected-complete-if-pointed π Ο)

βΛ’α΅-in-terms-of-β : (π : DCPOβ₯ {π€} {π£}) {I : π₯ Μ } {Ξ± : I β βͺ π β«}
(Ο : is-semidirected (underlying-order (π β»)) Ξ±)
β βΛ’α΅ π Ο οΌ β (π β») (add-β₯-is-directed π Ο)
βΛ’α΅-in-terms-of-β π {I} {Ξ±} Ο = refl

preserves-semidirected-sups-if-continuous-and-strict :
(π : DCPOβ₯ {π€} {π£}) (π : DCPOβ₯ {π€'} {π£'})
(f : βͺ π β« β βͺ π β«)
β is-continuous (π β») (π β») f
β is-strict π π f
β {I : π₯ Μ } {Ξ± : I β βͺ π β«}
β (Ο : is-semidirected (underlying-order (π β»)) Ξ±)
β is-sup (underlying-order (π β»)) (f (βΛ’α΅ π Ο)) (f β Ξ±)
preserves-semidirected-sups-if-continuous-and-strict π π f con str {I} {Ξ±} Ο =
ub , lb-of-ubs
where
Ξ΄ : is-Directed (π β») (add-β₯ π Ξ±)
claimβ : is-sup (underlying-order (π β»)) (f (β (π β») Ξ΄))
claimβ = con (π + I) (add-β₯ π Ξ±) (add-β₯-is-directed π Ο)
claimβ : is-sup (underlying-order (π β»)) (f (βΛ’α΅ π Ο))
claimβ = transportβ»ΒΉ
(Ξ» - β is-sup (underlying-order (π β»)) (f -) (f β (add-β₯ π Ξ±)))
(βΛ’α΅-in-terms-of-β π Ο) claimβ
ub : (i : I) β f (Ξ± i) ββͺ π β« f (βΛ’α΅ π Ο)
ub i = sup-is-upperbound (underlying-order (π β»)) claimβ (inr i)
lb-of-ubs : is-lowerbound-of-upperbounds (underlying-order (π β»)) (f (βΛ’α΅ π Ο))
(f β Ξ±)
lb-of-ubs y y-is-ub = sup-is-lowerbound-of-upperbounds (underlying-order (π β»))
claimβ y h
where
h : is-upperbound (underlying-order (π β»)) y (f β add-β₯ π Ξ±)
h (inl β) = f (β₯ π) ββͺ π β«[ οΌ-to-β (π β») str ]
β₯ π     ββͺ π β«[ β₯-is-least π y ]
y       ββͺ π β«
h (inr i) = y-is-ub i

subsingleton-indexed-is-semidirected : (π : DCPO {π€} {π£})
{I : π₯ Μ } (Ξ± : I β β¨ π β©)
β is-prop I
β is-semidirected (underlying-order π) Ξ±
subsingleton-indexed-is-semidirected π Ξ± Ο i j = β£ i , r , r' β£
where
r : Ξ± i ββ¨ π β© Ξ± i
r = reflexivity π (Ξ± i)
r' : Ξ± j ββ¨ π β© Ξ± i
r' = transport (Ξ» k β Ξ± k ββ¨ π β© Ξ± i) (Ο i j) r

subsingleton-complete-if-pointed : (π : DCPOβ₯ {π€} {π£}) {I : π₯ Μ } (Ξ± : I β βͺ π β«)
β is-prop I
β has-sup (underlying-order (π β»)) Ξ±
subsingleton-complete-if-pointed π Ξ± Ο =
semidirected-complete-if-pointed π Ο
where
Ο : is-semidirected (underlying-order (π β»)) Ξ±
Ο = subsingleton-indexed-is-semidirected (π β») Ξ± Ο

βΛ’Λ’ : (π : DCPOβ₯ {π€} {π£}) {I : π₯ Μ } (Ξ± : I β βͺ π β«)
β is-prop I β βͺ π β«
βΛ’Λ’ π {I} Ξ± Ο = prβ (subsingleton-complete-if-pointed π Ξ± Ο)

βΛ’Λ’-in-terms-of-βΛ’α΅ : (π : DCPOβ₯ {π€} {π£}) {I : π₯ Μ } {Ξ± : I β βͺ π β«}
(Ο : is-prop I)
β βΛ’Λ’ π Ξ± Ο
οΌ βΛ’α΅ π
(subsingleton-indexed-is-semidirected (π β») Ξ± Ο)
βΛ’Λ’-in-terms-of-βΛ’α΅ π {I} {Ξ±} Ο = refl

preserves-subsingleton-sups-if-continuous-and-strict :
(π : DCPOβ₯ {π€} {π£}) (π : DCPOβ₯ {π€'} {π£'})
(f : βͺ π β« β βͺ π β«)
β is-continuous (π β») (π β») f
β is-strict π π f
β {I : π₯ Μ } (Ξ± : I β βͺ π β«)
β (Ο : is-prop I)
β is-sup (underlying-order (π β»)) (f (βΛ’Λ’ π Ξ± Ο)) (f β Ξ±)
preserves-subsingleton-sups-if-continuous-and-strict π π f con str Ξ± Ο =
preserves-semidirected-sups-if-continuous-and-strict π π f con str
(subsingleton-indexed-is-semidirected (π β») Ξ± Ο)

βΛ’Λ’-is-upperbound : (π : DCPOβ₯ {π€} {π£}) {I : π₯ Μ } (Ξ± : I β βͺ π β«)
(Ο : is-prop I)
β is-upperbound
(underlying-order (π β»)) (βΛ’Λ’ π Ξ± Ο) Ξ±
βΛ’Λ’-is-upperbound π {I} Ξ± Ο i = β-is-upperbound (π β») Ξ΄ (inr i)
where
Ξ΄ : is-Directed (π β») (add-β₯ π Ξ±)
Ξ΄ = add-β₯-is-directed π (subsingleton-indexed-is-semidirected (π β») Ξ± Ο)

βΛ’Λ’-is-lowerbound-of-upperbounds : (π : DCPOβ₯ {π€} {π£}) {I : π₯ Μ } (Ξ± : I β βͺ π β«)
(Ο : is-prop I)
β is-lowerbound-of-upperbounds
(underlying-order (π β»)) (βΛ’Λ’ π Ξ± Ο) Ξ±
βΛ’Λ’-is-lowerbound-of-upperbounds π {I} Ξ± Ο y y-is-ub =
β-is-lowerbound-of-upperbounds (π β») Ξ΄ y h
where
Ξ΄ : is-Directed (π β») (add-β₯ π Ξ±)
Ξ΄ = add-β₯-is-directed π (subsingleton-indexed-is-semidirected (π β») Ξ± Ο)
h : (i : π + I) β add-β₯ π Ξ± i ββͺ π β« y
h (inl β) = β₯-is-least π y
h (inr i) = y-is-ub i

βΛ’Λ’-is-sup : (π : DCPOβ₯ {π€} {π£}) {I : π₯ Μ } (Ξ± : I β βͺ π β«) (Ο : is-prop I)
β is-sup (underlying-order (π β»)) (βΛ’Λ’ π Ξ± Ο) Ξ±
βΛ’Λ’-is-sup π Ξ± Ο = βΛ’Λ’-is-upperbound π Ξ± Ο
, βΛ’Λ’-is-lowerbound-of-upperbounds π Ξ± Ο

βΛ’Λ’-οΌ-if-continuous-and-strict : (π : DCPOβ₯ {π€} {π£}) (π : DCPOβ₯ {π€'} {π£'})
(f : βͺ π β« β βͺ π β«)
β is-continuous (π β») (π β») f
β is-strict π π f
β {I : π₯ Μ } (Ξ± : I β βͺ π β«)
β (Ο : is-prop I)
β f (βΛ’Λ’ π Ξ± Ο) οΌ βΛ’Λ’ π (f β Ξ±) Ο
βΛ’Λ’-οΌ-if-continuous-and-strict π π f con str Ξ± Ο =
sups-are-unique
(underlying-order (π β»))
(prβ (axioms-of-dcpo (π β»))) (f β Ξ±)
(preserves-subsingleton-sups-if-continuous-and-strict π π f con str Ξ± Ο)
(βΛ’Λ’-is-sup π (f β Ξ±) Ο)

βΛ’Λ’-family-οΌ : (π : DCPOβ₯ {π€} {π£}) {I : π₯ Μ } {Ξ± Ξ² : I β βͺ π β«} (Ο : is-prop I)
β Ξ± οΌ Ξ²
β βΛ’Λ’ π Ξ± Ο οΌ βΛ’Λ’ π Ξ² Ο
βΛ’Λ’-family-οΌ π Ο refl = refl

βΛ’Λ’-οΌ-if-domain-holds : (π : DCPOβ₯ {π€} {π£}) {I : π₯ Μ }
{Ξ± : I β βͺ π β«} (Ο : is-prop I)
β (i : I) β βΛ’Λ’ π Ξ± Ο οΌ Ξ± i
βΛ’Λ’-οΌ-if-domain-holds π {I} {Ξ±} Ο i =
antisymmetry (π β») (βΛ’Λ’ π Ξ± Ο) (Ξ± i)
(βΛ’Λ’-is-lowerbound-of-upperbounds π Ξ± Ο (Ξ± i) l)
(βΛ’Λ’-is-upperbound π Ξ± Ο i)
where
l : (j : I) β Ξ± j ββͺ π β« Ξ± i
l j = transport (Ξ» - β Ξ± - ββͺ π β« Ξ± i) (Ο i j) (reflexivity (π β») (Ξ± i))

\end{code}