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 : ⟨ 𝓓 ⟩ β†’ Ξ© 𝓦

   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}