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