Ayberk Tosun, 14 June 2023.

\begin{code}

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

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

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

open PropositionalTruncation pt

open import OrderedTypes.Poset fe
open import Slice.Family
open import UF.ImageAndSurjection pt
open import UF.Logic
open import UF.Powerset-MultiUniverse
open import UF.SubtypeClassifier
open import UF.Subsingletons
open import UF.Subsingletons-FunExt

open Universal fe
open Existential pt
open Implication fe
open Conjunction

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

underlying-orderβ : (π : DCPO {π€} {π£}) β β¨ π β© β β¨ π β© β Ξ© π£
underlying-orderβ π x y = (x ββ¨ π β© y) , prop-valuedness π x y

syntax underlying-orderβ π x y = x ββ¨ π β©β y

_βimageβ_ : {X : π€  Μ} {Y : π¦  Μ} β Y β (X β Y) β Ξ© (π€ β π¦)
y βimageβ f = y βimage f , β-is-prop

\end{code}

We define the notion of a Scott-open subset in the following module. The DCPO
π taken as an argument has a carrier set living in π€ and order living in π£.
The parameter π¦ is for the universe of the subsets for which Scott-openness is
defined. In other words, we define what it means for a subset P : β¨ π β© β Ξ© π¦
to be Scott-open.

\begin{code}

module DefnOfScottTopology (π : DCPO {π€} {π£}) (π¦ : Universe) where

\end{code}

I find it convenient to define the type of directed families.

\begin{code}

Famβ : π€ β π₯ βΊ β π£  Μ
Famβ = Ξ£ S κ Fam π₯ β¨ π β© , is-Directed π (S [_])

β_ : Famβ β β¨ π β©
β (S , Ξ΄) =
the-sup (underlying-order π) (directed-completeness π (index S) (S [_]) Ξ΄ )

β-is-sup : (S : Famβ) β is-sup (underlying-order π) (β S) (S .prβ [_])
β-is-sup (S , Ξ΄) =
sup-property (underlying-order π) (directed-completeness π (index S) (S [_]) Ξ΄)

β-is-upperbound : (S : Famβ) β is-upperbound (underlying-order π) (β S) (S .prβ [_])
β-is-upperbound S = prβ (β-is-sup S)

is-upwards-closed : π {π¦} β¨ π β© β Ξ© (π€ β π£ β π¦)
is-upwards-closed P = β±― x κ β¨ π β© , β±― y κ β¨ π β© , P x β x ββ¨ π β©β y β P y

is-inaccessible-by-directed-joins : π {π¦} β¨ π β© β Ξ© (π₯ βΊ β π€ β π£ β π¦)
is-inaccessible-by-directed-joins P =
β±― (S , Ξ΄) κ Famβ , P (β (S , Ξ΄)) β (Ζ i κ index S , P (S [ i ]) holds)

is-scott-open : π {π¦} β¨ π β© β Ξ© (π₯ βΊ β π€ β π£ β π¦)
is-scott-open P = is-upwards-closed P β§ is-inaccessible-by-directed-joins P

πͺβ : π€ β π¦ βΊ β π₯ βΊ β π£  Μ
πͺβ = Ξ£ P κ (β¨ π β© β Ξ© π¦) , is-scott-open P holds

x ββ U = U .prβ x

\end{code}

\begin{code}

record πͺβα΄Ώ : π€ β π¦ βΊ β π₯ βΊ β π£  Μ where
field

pred-is-upwards-closed : is-upwards-closed pred holds
pred-is-inaccessible-by-dir-joins : is-inaccessible-by-directed-joins pred holds

to-πͺβα΄Ώ : πͺβ β πͺβα΄Ώ
to-πͺβα΄Ώ (P , Ο , ΞΉ) = record
{ pred                              = P
; pred-is-upwards-closed            = Ο
; pred-is-inaccessible-by-dir-joins = ΞΉ
}

from-πͺβα΄Ώ : πͺβα΄Ώ β πͺβ
from-πͺβα΄Ώ π =
π .pred , π .pred-is-upwards-closed , π .pred-is-inaccessible-by-dir-joins
where
open πͺβα΄Ώ

upward-closure : (π : πͺβ) β  is-upwards-closed (Ξ» - β - ββ π) holds
upward-closure = πͺβα΄Ώ.pred-is-upwards-closed β to-πͺβα΄Ώ

scott-openness : (π : πͺβ) β is-scott-open (Ξ» - β - ββ π) holds
scott-openness π =
πͺβα΄Ώ.pred-is-upwards-closed πα΄Ώ , πͺβα΄Ώ.pred-is-inaccessible-by-dir-joins πα΄Ώ
where
πα΄Ώ : πͺβα΄Ώ
πα΄Ώ = to-πͺβα΄Ώ π

\end{code}