From a804cfde95181aaf6a3158cc89adcd48246cb62d Mon Sep 17 00:00:00 2001
From: Ayberk Tosun <ayberk.tosun@gmail.com>
Date: Sat, 19 Aug 2023 18:33:31 +0100
Subject: [PATCH 01/14] Move the definition of the `WayBelow` relation to a
 module of its own

---
 source/Locales/WayBelow.lagda | 40 +++++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)
 create mode 100644 source/Locales/WayBelow.lagda

diff --git a/source/Locales/WayBelow.lagda b/source/Locales/WayBelow.lagda
new file mode 100644
index 000000000..8bbc9694c
--- /dev/null
+++ b/source/Locales/WayBelow.lagda
@@ -0,0 +1,40 @@
+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]
+
+open import UF.Base
+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}

From 79c9efd610fcaa17a528bf3bcd383ff48e37158a Mon Sep 17 00:00:00 2001
From: Ayberk Tosun <ayberk.tosun@gmail.com>
Date: Sat, 19 Aug 2023 18:37:24 +0100
Subject: [PATCH 02/14] Move definitions of compactness to a new module of
 their own

---
 source/Locales/Compactness.lagda | 45 ++++++++++++++++++++++++++++++++
 1 file changed, 45 insertions(+)
 create mode 100644 source/Locales/Compactness.lagda

diff --git a/source/Locales/Compactness.lagda b/source/Locales/Compactness.lagda
new file mode 100644
index 000000000..a6a387614
--- /dev/null
+++ b/source/Locales/Compactness.lagda
@@ -0,0 +1,45 @@
+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]
+
+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 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}

From c226694f1dca31c97f04702ec934db792704f545 Mon Sep 17 00:00:00 2001
From: Ayberk Tosun <ayberk.tosun@gmail.com>
Date: Sun, 20 Aug 2023 19:04:07 +0100
Subject: [PATCH 03/14] Add flags

---
 source/Locales/Compactness.lagda | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/source/Locales/Compactness.lagda b/source/Locales/Compactness.lagda
index a6a387614..79b76de10 100644
--- a/source/Locales/Compactness.lagda
+++ b/source/Locales/Compactness.lagda
@@ -10,6 +10,8 @@ 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

From e41044c6618296c9bb4e1a84a2bca27ff87b6963 Mon Sep 17 00:00:00 2001
From: Ayberk Tosun <ayberk.tosun@gmail.com>
Date: Sun, 20 Aug 2023 19:04:19 +0100
Subject: [PATCH 04/14] Add flags

---
 source/Locales/WayBelow.lagda | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/source/Locales/WayBelow.lagda b/source/Locales/WayBelow.lagda
index 8bbc9694c..db342b32a 100644
--- a/source/Locales/WayBelow.lagda
+++ b/source/Locales/WayBelow.lagda
@@ -7,6 +7,8 @@ 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

From a900000e94fc60de20116355be4e1a0e81aa26a7 Mon Sep 17 00:00:00 2001
From: Ayberk Tosun <ayberk.tosun@gmail.com>
Date: Mon, 21 Aug 2023 00:52:07 +0100
Subject: [PATCH 05/14] Add the new definition of a spectral locale

---
 source/Locales/Spectral.lagda | 83 +++++++++++++++++++++++++++++++++++
 1 file changed, 83 insertions(+)
 create mode 100644 source/Locales/Spectral.lagda

diff --git a/source/Locales/Spectral.lagda b/source/Locales/Spectral.lagda
new file mode 100644
index 000000000..2bbe237ee
--- /dev/null
+++ b/source/Locales/Spectral.lagda
@@ -0,0 +1,83 @@
+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.Spectral (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 : (X : 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}
+
+\begin{code}
+
+compacts-closed-under-finite-meets : (X : Locale 𝓤 𝓥 𝓦) → Ω (𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺)
+compacts-closed-under-finite-meets X =
+ 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 U = Ɐ i ꞉ index U , is-compact-open X (U [ 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-closed-under-finite-meets X
+  ⦅𝟐⦆ = Ɐ U ꞉ ⟨ 𝒪 X ⟩ ,
+         Ǝ S ꞉ (Fam 𝓦 ⟨ 𝒪 X ⟩) ,
+          consists-of-compact-opens X S holds × (U ＝ ⋁[ 𝒪 X ] S)
+
+\end{code}

From 0dd731a2b258c621d91d4a5ae2fb0f24b063542f Mon Sep 17 00:00:00 2001
From: Ayberk Tosun <ayberk.tosun@gmail.com>
Date: Mon, 21 Aug 2023 12:55:31 +0100
Subject: [PATCH 06/14] renamed: Spectral.lagda -> Spectrality.lagda

---
 source/Locales/{Spectral.lagda => Spectrality.lagda} | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename source/Locales/{Spectral.lagda => Spectrality.lagda} (100%)

diff --git a/source/Locales/Spectral.lagda b/source/Locales/Spectrality.lagda
similarity index 100%
rename from source/Locales/Spectral.lagda
rename to source/Locales/Spectrality.lagda

From 03ee8d52f877c4c28b910ad6fa3598ad9ae62bfa Mon Sep 17 00:00:00 2001
From: Ayberk Tosun <ayberk.tosun@gmail.com>
Date: Mon, 21 Aug 2023 12:56:15 +0100
Subject: [PATCH 07/14] Change module name as to match file name

---
 source/Locales/Spectrality.lagda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/source/Locales/Spectrality.lagda b/source/Locales/Spectrality.lagda
index 2bbe237ee..86cb253e8 100644
--- a/source/Locales/Spectrality.lagda
+++ b/source/Locales/Spectrality.lagda
@@ -23,8 +23,8 @@ open import UF.Subsingletons
 open import UF.Subsingletons-FunExt
 open import UF.Logic
 
-module Locales.Spectral (pt : propositional-truncations-exist)
-                        (fe : Fun-Ext)                         where
+module Locales.Spectrality (pt : propositional-truncations-exist)
+                           (fe : Fun-Ext)                          where
 
 open import Locales.Frame pt fe
 open import Locales.Compactness pt fe

From 737f3f2080f295e7d834d53bf97ce7a5de57110f Mon Sep 17 00:00:00 2001
From: Ayberk Tosun <ayberk.tosun@gmail.com>
Date: Mon, 21 Aug 2023 13:00:01 +0100
Subject: [PATCH 08/14] Remove unused import

---
 source/Locales/WayBelow.lagda | 1 -
 1 file changed, 1 deletion(-)

diff --git a/source/Locales/WayBelow.lagda b/source/Locales/WayBelow.lagda
index db342b32a..d6f591c9a 100644
--- a/source/Locales/WayBelow.lagda
+++ b/source/Locales/WayBelow.lagda
@@ -9,7 +9,6 @@ will be broken down into smaller modules.
 
 {-# OPTIONS --safe --without-K --exact-split #-}
 
-open import UF.Base
 open import UF.Subsingletons
 open import UF.PropTrunc
 open import UF.FunExt

From 1bbfa14c3146ca95812332e9d6420e566ce45d64 Mon Sep 17 00:00:00 2001
From: Ayberk Tosun <ayberk.tosun@gmail.com>
Date: Mon, 21 Aug 2023 13:01:44 +0100
Subject: [PATCH 09/14] Improve comment

---
 source/Locales/Compactness.lagda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/source/Locales/Compactness.lagda b/source/Locales/Compactness.lagda
index 79b76de10..57e485a76 100644
--- a/source/Locales/Compactness.lagda
+++ b/source/Locales/Compactness.lagda
@@ -37,7 +37,7 @@ is-compact-open X U = U ≪[ 𝒪 X ] U
 
 \end{code}
 
-A locale `X` is called compact if its top element is compact.
+A locale `X` is called compact if its top element `𝟏` is compact.
 
 \begin{code}
 

From 3dec1b369c3c836cf424a2fd40e75a46ec882cff Mon Sep 17 00:00:00 2001
From: Ayberk Tosun <ayberk.tosun@gmail.com>
Date: Mon, 21 Aug 2023 13:03:40 +0100
Subject: [PATCH 10/14] Make naming more consistent

---
 source/Locales/Spectrality.lagda | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/source/Locales/Spectrality.lagda b/source/Locales/Spectrality.lagda
index 86cb253e8..6b1103e56 100644
--- a/source/Locales/Spectrality.lagda
+++ b/source/Locales/Spectrality.lagda
@@ -40,7 +40,7 @@ be closed under binary meets.
 
 \begin{code}
 
-compacts-of-[_]-are-closed-under-binary-meets : (X : Locale 𝓤 𝓥 𝓦) → Ω (𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺)
+compacts-of-[_]-are-closed-under-binary-meets : Locale 𝓤 𝓥 𝓦 → Ω (𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺)
 compacts-of-[ X ]-are-closed-under-binary-meets =
  let
   _∧ₓ_ = meet-of (𝒪 X)
@@ -52,8 +52,8 @@ compacts-of-[ X ]-are-closed-under-binary-meets =
 
 \begin{code}
 
-compacts-closed-under-finite-meets : (X : Locale 𝓤 𝓥 𝓦) → Ω (𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺)
-compacts-closed-under-finite-meets X =
+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}
@@ -75,7 +75,7 @@ We are now ready to define the notion of a spectral locale:
 is-spectral : Locale 𝓤 𝓥 𝓦 → Ω (𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺)
 is-spectral {_} {_} {𝓦} X = ⦅𝟏⦆ ∧ ⦅𝟐⦆
  where
-  ⦅𝟏⦆ = compacts-closed-under-finite-meets X
+  ⦅𝟏⦆ = compacts-of-[ X ]-are-closed-under-finite-meets
   ⦅𝟐⦆ = Ɐ U ꞉ ⟨ 𝒪 X ⟩ ,
          Ǝ S ꞉ (Fam 𝓦 ⟨ 𝒪 X ⟩) ,
           consists-of-compact-opens X S holds × (U ＝ ⋁[ 𝒪 X ] S)

From 9981d5112269bcd7447b234355db507e3ad30cee Mon Sep 17 00:00:00 2001
From: Ayberk Tosun <ayberk.tosun@gmail.com>
Date: Mon, 21 Aug 2023 13:05:01 +0100
Subject: [PATCH 11/14] Add comment

---
 source/Locales/Spectrality.lagda | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/source/Locales/Spectrality.lagda b/source/Locales/Spectrality.lagda
index 6b1103e56..1b89f8ade 100644
--- a/source/Locales/Spectrality.lagda
+++ b/source/Locales/Spectrality.lagda
@@ -50,6 +50,9 @@ compacts-of-[ X ]-are-closed-under-binary-meets =
 
 \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 𝓤 𝓥 𝓦 → Ω (𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺)

From e59f8a947aebb830d04562a9fdf3526e32987450 Mon Sep 17 00:00:00 2001
From: Ayberk Tosun <ayberk.tosun@gmail.com>
Date: Mon, 21 Aug 2023 13:05:37 +0100
Subject: [PATCH 12/14] Improve naming

---
 source/Locales/Spectrality.lagda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/source/Locales/Spectrality.lagda b/source/Locales/Spectrality.lagda
index 1b89f8ade..ca46c62db 100644
--- a/source/Locales/Spectrality.lagda
+++ b/source/Locales/Spectrality.lagda
@@ -67,7 +67,7 @@ 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 U = Ɐ i ꞉ index U , is-compact-open X (U [ i ])
+consists-of-compact-opens X S = Ɐ i ꞉ index S , is-compact-open X (S [ i ])
 
 \end{code}
 

From 7fc92f10d2494fb44682e4cf34c2f3495c966a3b Mon Sep 17 00:00:00 2001
From: Ayberk Tosun <ayberk.tosun@gmail.com>
Date: Mon, 21 Aug 2023 13:12:08 +0100
Subject: [PATCH 13/14] Add the forgotten directedness requirement

---
 source/Locales/Spectrality.lagda | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/source/Locales/Spectrality.lagda b/source/Locales/Spectrality.lagda
index ca46c62db..a14adc6b8 100644
--- a/source/Locales/Spectrality.lagda
+++ b/source/Locales/Spectrality.lagda
@@ -81,6 +81,8 @@ is-spectral {_} {_} {𝓦} X = ⦅𝟏⦆ ∧ ⦅𝟐⦆
   ⦅𝟏⦆ = compacts-of-[ X ]-are-closed-under-finite-meets
   ⦅𝟐⦆ = Ɐ U ꞉ ⟨ 𝒪 X ⟩ ,
          Ǝ S ꞉ (Fam 𝓦 ⟨ 𝒪 X ⟩) ,
-          consists-of-compact-opens X S holds × (U ＝ ⋁[ 𝒪 X ] S)
+            consists-of-compact-opens X S holds
+          × is-directed (𝒪 X) S holds
+          × (U ＝ ⋁[ 𝒪 X ] S)
 
 \end{code}

From 11cfb657c26509dcc271d1f404bfb68aa0694124 Mon Sep 17 00:00:00 2001
From: Ayberk Tosun <ayberk.tosun@gmail.com>
Date: Mon, 21 Aug 2023 14:31:40 +0100
Subject: [PATCH 14/14] Commit forgotten change

---
 source/Locales/Compactness.lagda | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)

diff --git a/source/Locales/Compactness.lagda b/source/Locales/Compactness.lagda
index 57e485a76..d7627b82d 100644
--- a/source/Locales/Compactness.lagda
+++ b/source/Locales/Compactness.lagda
@@ -23,6 +23,7 @@ module Locales.Compactness (pt : propositional-truncations-exist)
 
 open import Locales.Frame    pt fe
 open import Locales.WayBelow pt fe
+open import Slice.Family
 
 open Locale
 
@@ -45,3 +46,33 @@ 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}