Ayberk Tosun, 11 September 2023

\begin{code}

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

open import MLTT.Spartan hiding (𝟚)
open import UF.PropTrunc
open import UF.FunExt
open import UF.Size

module Locales.Stone (pt : propositional-truncations-exist)
                     (fe : Fun-Ext)
                     (sr : Set-Replacement pt)               where

\end{code}

Importation of foundational UF stuff.

\begin{code}

open import UF.SubtypeClassifier
open import UF.Logic

open AllCombinators pt fe
open PropositionalTruncation pt

\end{code}

Importations of other locale theory modules.

\begin{code}

open import Locales.Frame            pt fe
open import Locales.Compactness.Definition pt fe
open import Locales.ZeroDimensionality pt fe sr

open Locale

\end{code}

\begin{code}

stoneᴰ : (X : Locale 𝓤 𝓥 𝓦) → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺ ̇
stoneᴰ X = is-compact X holds × zero-dimensionalᴰ (𝒪 X)

\end{code}

\begin{code}

is-stone : (X : Locale 𝓤 𝓥 𝓦) → Ω (𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺)
is-stone X = is-compact X ∧ is-zero-dimensional (𝒪 X)

\end{code}

\begin{code}

stoneᴰ-implies-stone : (X : Locale 𝓤 𝓥 𝓦) → stoneᴰ X → is-stone X holds
stoneᴰ-implies-stone X σᴰ@(κ , zd) = κ , ∣ zd ∣

\end{code}