Ayberk Tosun.

Started  on: 29 September 2023.
Finished on: 2 October 2023.

This module contains the definition of the Scott locale of a large and locally
small dcpo with a specified small compact basis, a notion defined in Tom de
Jong's domain theory development.

If one starts with a dcpo with a specified small compact basis, one can ensure
that the resulting Scott locale is locally small by quantifying over only the
basic/compact opens. This is the difference between the construction in this
module and the one in `ScottLocale.Definition`

\begin{code}[hide]

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

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

\end{code}

We assume the existence of propositional truncations as well as function
extensionality, and we assume a universe `𝓀` over which we consider large and
locally small dcpos.

\begin{code}

module Locales.ScottLocale.ScottLocalesOfAlgebraicDcpos
        (pt : propositional-truncations-exist)
        (fe : Fun-Ext)
        (𝓀  : Universe)
        where

open Universal fe
open Implication fe
open Existential pt
open Conjunction

open import Locales.Frame pt fe

open import DomainTheory.Basics.Dcpo                   pt fe 𝓀 renaming
                                                                (⟨_⟩ to ⟨_βŸ©βˆ™)
open import DomainTheory.Topology.ScottTopology        pt fe 𝓀
open import DomainTheory.BasesAndContinuity.Continuity pt fe 𝓀
open import DomainTheory.BasesAndContinuity.Bases      pt fe 𝓀

open import Locales.ScottLocale.Definition pt fe 𝓀

open Locale

open PropositionalTruncation pt

\end{code}

The construction is carried out over a large and locally small dcpo `𝓓` equipped
with a small compact basis. Because the type of small compact bases for large
and locally small dcpos has _split support_, the construction can also be
carried out without assuming a specified small compact basis.

TODO: use the following module to do the same construction with only the
truncation of the basis in consideration.

\begin{code}

module ScottLocaleConstruction (𝓓    : DCPO {𝓀 ⁺} {𝓀})
                               (hscb : has-specified-small-compact-basis 𝓓)
                               (pe   : propext 𝓀)                          where

 open DefnOfScottTopology 𝓓 𝓀
 open DefnOfScottLocale 𝓓 𝓀 pe using (π’ͺβ‚›-equality; _βŠ†β‚›_; βŠ†β‚›-is-reflexive;
                                      βŠ†β‚›-is-transitive; βŠ†β‚›-is-antisymmetric;
                                      βŠ€β‚›; βŠ€β‚›-is-top; _βˆ§β‚›_; βˆ§β‚›-is-meet;
                                      distributivityβ‚›; ⋁ₛ_; ⋁ₛ-is-join)
                               renaming (ScottLocale to ScottLocaleβ€²)

\end{code}

We denote by `𝕒` the fact that the dcpo `𝓓` in consideration is _structurally
algebraic_.

\begin{code}

 𝕒 : structurally-algebraic 𝓓
 𝕒 = structurally-algebraic-if-specified-small-compact-basis 𝓓 hscb

\end{code}

We denote by `I` the index type of the basis and by `Ξ²` its enumeration
function.

\begin{code}

 private
  I = index-of-compact-basis     𝓓 hscb
  Ξ² = family-of-compact-elements 𝓓 hscb

\end{code}

\begin{code}

 ℬ : Fam 𝓀 ⟨ 𝓓 βŸ©βˆ™
 ℬ = I , Ξ²

\end{code}

The order `_βŠ†β‚–_` is the small version of the relation that quantifies only over
the basic opens. The order `_βŠ†β‚›_` is the large version.

\begin{code}

 open structurally-algebraic

 _βŠ†β‚–_ : π’ͺβ‚› β†’ π’ͺβ‚› β†’ Ξ© 𝓀
 (U , _) βŠ†β‚– (V , _) = β±― i κž‰ I , U (ℬ [ i ]) β‡’ V (ℬ [ i ])

 βŠ†β‚–-implies-βŠ†β‚› : (π”˜ 𝔙 : π’ͺβ‚›) β†’ (π”˜ βŠ†β‚– 𝔙 β‡’ π”˜ βŠ†β‚› 𝔙) holds
 βŠ†β‚–-implies-βŠ†β‚› π”˜@(U , ι₁ , υ₁) 𝔙@(V , ΞΉβ‚‚ , Ο…β‚‚) Ο† x p =
  transport (Ξ» - β†’ (- βˆˆβ‚› 𝔙) holds) (eq ⁻¹) †
   where
    S : Fam 𝓀 ⟨ 𝓓 βŸ©βˆ™
    S = index-of-compact-family 𝕒 x , compact-family 𝕒 x

    S↑ : Fam↑
    S↑ = S , compact-family-is-directed 𝕒 x

    eq : x ＝ ⋁ S↑
    eq = compact-family-∐-＝ 𝕒 x ⁻¹

    pβ€² : ((⋁ S↑) βˆˆβ‚› π”˜) holds
    pβ€² = transport (Ξ» - β†’ (- βˆˆβ‚› π”˜) holds) eq p

    † : ((⋁ S↑) βˆˆβ‚› 𝔙) holds
    † = βˆ₯βˆ₯-rec (holds-is-prop ((⋁ S↑) βˆˆβ‚› 𝔙)) ‑ (υ₁ S↑ pβ€²)
     where
      ‑ : Ξ£ i κž‰ index S , ((S [ i ]) βˆˆβ‚› π”˜) holds β†’ ((⋁ S↑) βˆˆβ‚› 𝔙) holds
      ‑ (i , q) = ΞΉβ‚‚ (S [ i ]) (⋁ S↑) r (⋁-is-upperbound S↑ i)
       where
        r : ((S [ i ]) βˆˆβ‚› 𝔙) holds
        r = Ο† (pr₁ i) q

 βŠ†β‚›-implies-βŠ†β‚– : (π”˜ 𝔙 : π’ͺβ‚›) β†’ (π”˜ βŠ†β‚› 𝔙 β‡’ π”˜ βŠ†β‚– 𝔙) holds
 βŠ†β‚›-implies-βŠ†β‚– π”˜ 𝔙 p = p ∘ (ℬ [_])

 βŠ†β‚›-iff-βŠ†β‚– : (π”˜ 𝔙 : π’ͺβ‚›) β†’ (π”˜ βŠ†β‚› 𝔙 ⇔ π”˜ βŠ†β‚– 𝔙) holds
 βŠ†β‚›-iff-βŠ†β‚– π”˜ 𝔙 = βŠ†β‚›-implies-βŠ†β‚– π”˜ 𝔙 , βŠ†β‚–-implies-βŠ†β‚› π”˜ 𝔙

 βŠ†β‚–-is-reflexive : is-reflexive _βŠ†β‚–_ holds
 βŠ†β‚–-is-reflexive π”˜@(U , Ξ΄) = βŠ†β‚›-implies-βŠ†β‚– π”˜ π”˜ (βŠ†β‚›-is-reflexive π”˜)

 βŠ†β‚–-is-transitive : is-transitive _βŠ†β‚–_ holds
 βŠ†β‚–-is-transitive π”˜@(U , Ξ΄) 𝔙@(V , Ο΅) π”š@(W , ΞΆ) p q = βŠ†β‚›-implies-βŠ†β‚– π”˜ π”š †
  where
   † : (π”˜ βŠ†β‚› π”š) holds
   † = βŠ†β‚›-is-transitive π”˜ 𝔙 π”š (βŠ†β‚–-implies-βŠ†β‚› π”˜ 𝔙 p) (βŠ†β‚–-implies-βŠ†β‚› 𝔙 π”š q)

 βŠ†β‚–-is-antisymmetric : is-antisymmetric _βŠ†β‚–_
 βŠ†β‚–-is-antisymmetric {π”˜} {𝔙} p q = βŠ†β‚›-is-antisymmetric † ‑
  where
   † : (π”˜ βŠ†β‚› 𝔙) holds
   † = βŠ†β‚–-implies-βŠ†β‚› π”˜ 𝔙 p

   ‑ : (𝔙 βŠ†β‚› π”˜) holds
   ‑ = βŠ†β‚–-implies-βŠ†β‚› 𝔙 π”˜ q

 βŠ†β‚–-is-partial-order : is-partial-order π’ͺβ‚› _βŠ†β‚–_
 βŠ†β‚–-is-partial-order = (βŠ†β‚–-is-reflexive , βŠ†β‚–-is-transitive) , βŠ†β‚–-is-antisymmetric

 poset-of-scott-opensβ‚› : Poset (𝓀 ⁺) (𝓀 ⁺)
 poset-of-scott-opensβ‚› =
  π’ͺβ‚› , _βŠ†β‚›_ , (βŠ†β‚›-is-reflexive , βŠ†β‚›-is-transitive) , βŠ†β‚›-is-antisymmetric

\end{code}

The top open.

\begin{code}

 βŠ€β‚›-is-top-wrt-βŠ†β‚– : (π”˜ : π’ͺβ‚›) β†’ (π”˜ βŠ†β‚– βŠ€β‚›) holds
 βŠ€β‚›-is-top-wrt-βŠ†β‚– π”˜ = βŠ†β‚›-implies-βŠ†β‚– π”˜ βŠ€β‚› (βŠ€β‚›-is-top π”˜)

\end{code}

The meet of two opens.

\begin{code}

 open Meets _βŠ†β‚–_

 βˆ§β‚›-is-meet-wrt-βŠ†β‚– : (π”˜ 𝔙 : π’ͺβ‚›) β†’ ((π”˜ βˆ§β‚› 𝔙) is-glb-of (π”˜ , 𝔙)) holds
 βˆ§β‚›-is-meet-wrt-βŠ†β‚– π”˜ 𝔙 = † , ‑
  where
   † : ((π”˜ βˆ§β‚› 𝔙) is-a-lower-bound-of (π”˜ , 𝔙)) holds
   † = βŠ†β‚›-implies-βŠ†β‚– (π”˜ βˆ§β‚› 𝔙) π”˜ (∧[ π’ͺ ScottLocaleβ€² ]-lower₁ π”˜ 𝔙)
     , βŠ†β‚›-implies-βŠ†β‚– (π”˜ βˆ§β‚› 𝔙) 𝔙 (∧[ π’ͺ ScottLocaleβ€² ]-lowerβ‚‚ π”˜ 𝔙)

   ‑ : ((W , _) : lower-bound (π”˜ , 𝔙)) β†’ (W βŠ†β‚– (π”˜ βˆ§β‚› 𝔙)) holds
   ‑ (π”š , p , q) =
    βŠ†β‚›-implies-βŠ†β‚– π”š (π”˜ βˆ§β‚› 𝔙) (∧[ π’ͺ ScottLocaleβ€² ]-greatest π”˜ 𝔙 π”š ♣ β™ )
     where
      ♣ : (π”š βŠ†β‚› π”˜) holds
      ♣ = βŠ†β‚–-implies-βŠ†β‚› π”š π”˜ p

      β™  : (π”š βŠ†β‚› 𝔙) holds
      β™  = βŠ†β‚–-implies-βŠ†β‚› π”š 𝔙 q

\end{code}

The 𝓀-join of opens.

\begin{code}

 open Joins _βŠ†β‚–_

 ⋁ₛ-is-join-wrt-βŠ†β‚– : (S : Fam 𝓀 π’ͺβ‚›) β†’ ((⋁ₛ S) is-lub-of S) holds
 ⋁ₛ-is-join-wrt-βŠ†β‚– S = † , ‑
  where
   † : ((⋁ₛ S) is-an-upper-bound-of S) holds
   † i = βŠ†β‚›-implies-βŠ†β‚– (S [ i ]) (⋁ₛ S) (⋁[ π’ͺ ScottLocaleβ€² ]-upper S i)

   ‑ : ((U , _) : upper-bound S) β†’ ((⋁ₛ S) βŠ†β‚– U) holds
   ‑ (π”˜ , p) = βŠ†β‚›-implies-βŠ†β‚– (⋁ₛ S) π”˜ ((⋁[ π’ͺ ScottLocaleβ€² ]-least S (π”˜ , β€»)))
    where
     β€» : (i : index S) β†’ ((S [ i ]) βŠ†β‚› π”˜) holds
     β€» i = βŠ†β‚–-implies-βŠ†β‚› (S [ i ]) π”˜ (p i)

\end{code}

\begin{code}

 π’ͺβ‚›-frame-structure : frame-structure 𝓀 𝓀 π’ͺβ‚›
 π’ͺβ‚›-frame-structure = (_βŠ†β‚–_ , βŠ€β‚› , _βˆ§β‚›_ , ⋁ₛ_)
                    , βŠ†β‚–-is-partial-order
                    , βŠ€β‚›-is-top-wrt-βŠ†β‚–
                    , (Ξ» (U , V) β†’ βˆ§β‚›-is-meet-wrt-βŠ†β‚– U V)
                    , ⋁ₛ-is-join-wrt-βŠ†β‚–
                    , Ξ» (U , S) β†’ distributivityβ‚› U S

\end{code}

We finally define the locally small Scott locale of algebraic dcpo `𝓓`:

\begin{code}

 ScottLocale : Locale (𝓀 ⁺) 𝓀 𝓀
 ScottLocale = record { ⟨_βŸ©β‚— = π’ͺβ‚› ; frame-str-of = π’ͺβ‚›-frame-structure }

\end{code}