---
title:       Scott domains
author:      Ayberk Tosun
start-date:  2023-10-26
---

Ayberk Tosun.

Started on 26 October 2023.

\begin{code}[hide]

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

open import MLTT.Spartan
open import UF.FunExt
open import UF.Logic
open import UF.PropTrunc
open import UF.SubtypeClassifier
open import UF.Subsingletons

module DomainTheory.BasesAndContinuity.ScottDomain
        (pt : propositional-truncations-exist)
        (fe : Fun-Ext)
        (π“₯  : Universe)
       where

open import Slice.Family

open import DomainTheory.Basics.Dcpo                   pt fe π“₯
open import DomainTheory.BasesAndContinuity.Continuity pt fe π“₯
open import DomainTheory.BasesAndContinuity.Bases      pt fe π“₯

open import Locales.Frame hiding (⟨_⟩)

open Universal   fe
open Implication fe
open Existential pt
open Conjunction

open Locale

open PropositionalTruncation pt

\end{code}

We first define the notion of a 𝓣-family having an upper bound.

\begin{code}

module DefinitionOfBoundedCompleteness (𝓓 : DCPO {𝓀} {𝓣}) where

\end{code}

We denote by `_βŠ‘_` the informating ordering of the dcpo `𝓓`.

\begin{code}

 _βŠ‘_ : ⟨ 𝓓 ⟩ β†’ ⟨ 𝓓 ⟩ β†’ 𝓣  Μ‡
 x βŠ‘ y = x βŠ‘βŸ¨ 𝓓 ⟩ y

\end{code}

\begin{code}

 has-an-upper-bound : Fam 𝓣 ⟨ 𝓓 ⟩ β†’ Ξ© (𝓀 βŠ” 𝓣)
 has-an-upper-bound (_ , ΞΉ) =
  Ǝ u κž‰ ⟨ 𝓓 ⟩ , is-upperbound (underlying-order 𝓓) u ΞΉ

\end{code}

We also define a reformulation `has-supβ‚š` of `has-sup` from `Basics.Dcpo`. The
reason for this reformulation is to have a version more suitable to use with
notion of family that I (Ayberk) use, which is the one from `Slice.Family`.
Moreover, it is also convenient to have a version of this notion that is
packaged up with the proof of its propositionality so that it can be defined
directly as an `Ξ©`-valued function.

\begin{code}

 has-supβ‚š : Fam 𝓣 ⟨ 𝓓 ⟩ β†’ Ξ© (𝓀 βŠ” 𝓣)
 has-supβ‚š (I , ΞΉ) = has-sup (underlying-order 𝓓) ΞΉ
                  , having-sup-is-prop _βŠ‘_ (pr₁ (axioms-of-dcpo 𝓓)) ΞΉ

\end{code}

Bounded completeness then says that any family that has an upper bound also has
a least upper bound.

\begin{code}

 bounded-complete : Ξ© (𝓀 βŠ” 𝓣 ⁺)
 bounded-complete = β±― S κž‰ Fam 𝓣 ⟨ 𝓓 ⟩ , has-an-upper-bound S β‡’ has-supβ‚š S

\end{code}

We now proceed to define the notion of a Scott domain.

\begin{code}

module DefinitionOfScottDomain (𝓓 : DCPO {𝓀} {𝓣}) where

 open DefinitionOfBoundedCompleteness

 has-unspecified-small-compact-basisβ‚š : Ξ© (𝓀 βŠ” π“₯ ⁺ βŠ” 𝓣)
 has-unspecified-small-compact-basisβ‚š = has-unspecified-small-compact-basis 𝓓
                                      , βˆƒ-is-prop

 is-scott-domain : Ξ© (𝓀 βŠ” π“₯ ⁺ βŠ” 𝓣 ⁺)
 is-scott-domain =
  has-unspecified-small-compact-basisβ‚š ∧ bounded-complete 𝓓

\end{code}