diff --git a/source/Locales/Compactness.lagda b/source/Locales/Compactness.lagda
new file mode 100644
index 000000000..d7627b82d
--- /dev/null
+++ b/source/Locales/Compactness.lagda
@@ -0,0 +1,78 @@
+Ayberk Tosun, 19 August 2023
+
+The module contains the definitions of
+
+  (1) a compact open of a locale, and
+  (2) a compact locale.
+
+These used to live in the `CompactRegular` module which is now deprecated and
+will be broken down into smaller modules.
+
+\begin{code}[hide]
+
+{-# OPTIONS --safe --without-K --exact-split #-}
+
+open import UF.Base
+open import UF.Subsingletons
+open import UF.PropTrunc
+open import UF.FunExt
+open import MLTT.Spartan
+
+module Locales.Compactness (pt : propositional-truncations-exist)
+                           (fe : Fun-Ext)                          where
+
+open import Locales.Frame    pt fe
+open import Locales.WayBelow pt fe
+open import Slice.Family
+
+open Locale
+
+\end{code}
+
+An open `U : 𝒪(X)` of a locale `X` is called compact if it is way below itself.
+
+\begin{code}
+
+is-compact-open : (X : Locale 𝓤 𝓥 𝓦) → ⟨ 𝒪 X ⟩ → Ω (𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺)
+is-compact-open X U = U ≪[ 𝒪 X ] U
+
+\end{code}
+
+A locale `X` is called compact if its top element `𝟏` is compact.
+
+\begin{code}
+
+is-compact : Locale 𝓤 𝓥 𝓦 → Ω (𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺)
+is-compact X = is-compact-open X 𝟏[ 𝒪 X ]
+
+\end{code}
+
+We also define the type `𝒦 X` expressing the type of compact opens of a locale
+`X`.
+
+\begin{code}
+
+𝒦 : Locale 𝓤 𝓥 𝓦 → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺  ̇
+𝒦 X = Σ U ꞉ ⟨ 𝒪 X ⟩ , is-compact-open X U holds
+
+\end{code}
+
+Using this, we could define a family giving the compact opens of a locale `X`:
+
+\begin{code}
+
+ℬ-compact : (X : Locale 𝓤 𝓥 𝓦) → Fam (𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺) ⟨ 𝒪 X ⟩
+ℬ-compact X = 𝒦 X , pr₁
+
+\end{code}
+
+but the index of this family lives in `𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺`. This is to say that, if one
+starts with a large and locally small locale, the resulting family would live in
+`𝓤 ⁺` which means it would be *too big*.
+
+\begin{code}
+
+ℬ-compact₀ : (X : Locale (𝓤 ⁺) 𝓤 𝓤) → Fam (𝓤 ⁺) ⟨ 𝒪 X ⟩
+ℬ-compact₀ = ℬ-compact
+
+\end{code}
diff --git a/source/Locales/Spectrality.lagda b/source/Locales/Spectrality.lagda
new file mode 100644
index 000000000..a14adc6b8
--- /dev/null
+++ b/source/Locales/Spectrality.lagda
@@ -0,0 +1,88 @@
+Ayberk Tosun, 19 August 2023
+
+The module contains the definition of a spectral locale.
+
+This used to live in the `CompactRegular` module which is now deprecated and
+will be broken down into smaller modules.
+
+\begin{code}[hide]
+
+{-# OPTIONS --safe --without-K --exact-split --lossy-unification #-}
+
+open import MLTT.Spartan
+open import UF.Base
+open import UF.PropTrunc
+open import UF.FunExt
+open import UF.Univalence
+open import UF.FunExt
+open import UF.EquivalenceExamples
+open import MLTT.List hiding ([_])
+open import MLTT.Pi
+open import Slice.Family
+open import UF.Subsingletons
+open import UF.Subsingletons-FunExt
+open import UF.Logic
+
+module Locales.Spectrality (pt : propositional-truncations-exist)
+                           (fe : Fun-Ext)                          where
+
+open import Locales.Frame pt fe
+open import Locales.Compactness pt fe
+
+open AllCombinators pt fe
+
+open Locale
+
+\end{code}
+
+The following predicate expresses what it means for a locale's compact opens to
+be closed under binary meets.
+
+\begin{code}
+
+compacts-of-[_]-are-closed-under-binary-meets : Locale 𝓤 𝓥 𝓦 → Ω (𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺)
+compacts-of-[ X ]-are-closed-under-binary-meets =
+ let
+  _∧ₓ_ = meet-of (𝒪 X)
+ in
+  Ɐ K₁ ꞉ ⟨ 𝒪 X ⟩ , Ɐ K₂ ꞉ ⟨ 𝒪 X ⟩ ,
+   is-compact-open X K₁ ⇒ is-compact-open X K₂ ⇒ is-compact-open X (K₁ ∧ₓ K₂)
+
+\end{code}
+
+Now we express closure under finite meets, which amounts to closure under binary
+meets combined with the empty meet (i.e. the top element) being compact.
+
+\begin{code}
+
+compacts-of-[_]-are-closed-under-finite-meets : Locale 𝓤 𝓥 𝓦 → Ω (𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺)
+compacts-of-[ X ]-are-closed-under-finite-meets =
+ is-compact X ∧ compacts-of-[ X ]-are-closed-under-binary-meets
+
+\end{code}
+
+The following predicate expresses the property of a given family to consist of
+compact opens i.e. all the opens it gives being compact opens.
+
+\begin{code}
+
+consists-of-compact-opens : (X : Locale 𝓤 𝓥 𝓦) → Fam 𝓦 ⟨ 𝒪 X ⟩ → Ω (𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺)
+consists-of-compact-opens X S = Ɐ i ꞉ index S , is-compact-open X (S [ i ])
+
+\end{code}
+
+We are now ready to define the notion of a spectral locale:
+
+\begin{code}
+
+is-spectral : Locale 𝓤 𝓥 𝓦 → Ω (𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺)
+is-spectral {_} {_} {𝓦} X = ⦅𝟏⦆ ∧ ⦅𝟐⦆
+ where
+  ⦅𝟏⦆ = compacts-of-[ X ]-are-closed-under-finite-meets
+  ⦅𝟐⦆ = Ɐ U ꞉ ⟨ 𝒪 X ⟩ ,
+         Ǝ S ꞉ (Fam 𝓦 ⟨ 𝒪 X ⟩) ,
+            consists-of-compact-opens X S holds
+          × is-directed (𝒪 X) S holds
+          × (U ＝ ⋁[ 𝒪 X ] S)
+
+\end{code}
diff --git a/source/Locales/WayBelow.lagda b/source/Locales/WayBelow.lagda
new file mode 100644
index 000000000..d6f591c9a
--- /dev/null
+++ b/source/Locales/WayBelow.lagda
@@ -0,0 +1,41 @@
+Ayberk Tosun, 19 August 2023
+
+The module contains the definition of the way below relation.
+
+This used to live in the `CompactRegular` module which is now deprecated and
+will be broken down into smaller modules.
+
+\begin{code}[hide]
+
+{-# OPTIONS --safe --without-K --exact-split #-}
+
+open import UF.Subsingletons
+open import UF.PropTrunc
+open import UF.FunExt
+open import MLTT.Spartan
+open import UF.Logic
+open import Slice.Family
+
+module Locales.WayBelow (pt : propositional-truncations-exist)
+                        (fe : Fun-Ext)                          where
+
+open import Locales.Frame pt fe
+
+open AllCombinators pt fe
+
+\end{code}
+
+\begin{code}
+
+way-below : (F : Frame 𝓤 𝓥 𝓦) → ⟨ F ⟩ → ⟨ F ⟩ → Ω (𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺)
+way-below {𝓤 = 𝓤} {𝓦 = 𝓦} F U V =
+ Ɐ S ꞉ Fam 𝓦 ⟨ F ⟩ , is-directed F S ⇒
+  V ≤ (⋁[ F ] S) ⇒ (Ǝ i ꞉ index S , (U ≤ S [ i ]) holds)
+   where
+    open PosetNotation (poset-of F) using (_≤_)
+
+infix 5 way-below
+
+syntax way-below F U V = U ≪[ F ] V
+
+\end{code}