diff --git a/README.md b/README.md
index 756e277ca..acc702848 100644
--- a/README.md
+++ b/README.md
@@ -56,6 +56,7 @@ Please add yourself the first time you contribute.
 * Lane Biocini
 * Marc Bezem
 * Martin Escardo
+* Martin Trucchi
 * Nicolai Kraus
 * Ohad Kammar
 * Paul Levy (i)
diff --git a/source/SyntheticTopology/Compactness.lagda b/source/SyntheticTopology/Compactness.lagda
new file mode 100644
index 000000000..cea7741da
--- /dev/null
+++ b/source/SyntheticTopology/Compactness.lagda
@@ -0,0 +1,183 @@
+---
+title:        Compactness in Synthetic Topology
+author:       Martin Trucchi
+date-started: 2024-05-28
+---
+
+\begin{code}
+
+{-# OPTIONS --safe --without-K #-}
+
+open import MLTT.Spartan
+open import SyntheticTopology.SierpinskiObject
+open import UF.Base
+open import UF.DiscreteAndSeparated
+open import UF.FunExt
+open import UF.Powerset
+open import UF.PropTrunc
+open import UF.Sets
+open import UF.Sets-Properties
+open import UF.Subsingletons
+open import UF.Subsingletons-Properties
+open import UF.SubtypeClassifier
+
+module SyntheticTopology.Compactness
+        (𝓤  𝓥 : Universe)
+        (fe : Fun-Ext)
+        (pe : Prop-Ext)
+        (pt : propositional-truncations-exist)
+        (𝕊 : Generalized-Sierpinski-Object fe pe pt 𝓤 𝓥)
+        where
+
+open import UF.ImageAndSurjection pt
+open import UF.Logic
+open import SyntheticTopology.SetCombinators 𝓤 fe pe pt
+
+open AllCombinators pt fe
+open PropositionalTruncation pt hiding (_∨_)
+open Sierpinski-notations fe pe pt 𝕊
+
+\end{code}
+
+We here start to investigate a notion of compactness defined in [1] and [2].
+
+A type `X` is called `compact` if its universal quantification on
+`intrinsically-open` predicates is an open proposition.
+
+\begin{code}
+
+module _ (𝒳 : hSet 𝓤) where
+ private
+  X = underlying-set 𝒳
+
+ is-compact : Ω (𝓤 ⁺ ⊔ 𝓥)
+ is-compact =
+  Ɐ (P , open-P) ꞉ 𝓞 𝒳 , is-open-proposition (Ɐ x ꞉ X , x ∈ₚ P)
+
+\end{code}
+
+The type `𝟙` is compact i.e. the empty product is compact, regardless of the
+Sierpinski Object.
+
+\begin{code}
+
+𝟙-is-compact : is-compact 𝟙ₛ holds
+𝟙-is-compact (P , open-P) =
+ ⇔-open (⋆ ∈ₚ P) (Ɐ x ꞉ 𝟙 , x ∈ₚ P) eq (open-P ⋆)
+  where
+   eq : (⋆ ∈ₚ P ⇔ (Ɐ x ꞉ 𝟙 , x ∈ₚ P)) holds
+   eq = (λ pstar  x → pstar) , (λ f → f ⋆)
+
+\end{code}
+
+Binary products of compact types are compact.
+
+\begin{code}
+
+module _ (𝒳 𝒴 : hSet 𝓤) where
+ private
+  X = underlying-set 𝒳
+  Y = underlying-set 𝒴
+
+ ×-is-compact : is-compact 𝒳 holds
+              → is-compact 𝒴 holds
+              → is-compact (𝒳 ×ₛ 𝒴)  holds
+
+ ×-is-compact compact-X compact-Y (P , open-P) =
+  ⇔-open chained-forall
+         tuple-forall
+         (p₁ , p₂)
+         †
+   where
+    tuple-forall : Ω 𝓤
+    tuple-forall = Ɐ z ꞉ (X × Y) , z ∈ₚ P
+
+    chained-forall : Ω 𝓤
+    chained-forall = Ɐ x ꞉ X , (Ɐ y ꞉ Y , (x , y) ∈ₚ P)
+
+    p₁ : (chained-forall ⇒ tuple-forall) holds
+    p₁ = λ Qxy z → Qxy (pr₁ z) (pr₂ z)
+
+    p₂ : (tuple-forall ⇒ chained-forall) holds
+    p₂ = λ Qz x' y' → Qz (x' , y')
+
+    prop-y : 𝓟 X
+    prop-y x = Ɐ y ꞉ Y , (x , y) ∈ₚ P
+
+    prop-y-open : (x : X) → is-open-proposition (prop-y x) holds
+    prop-y-open x = compact-Y ((λ y → (x , y) ∈ₚ P) , λ y → open-P (x , y))
+
+    † : is-open-proposition chained-forall holds
+    † = compact-X (prop-y , prop-y-open)
+
+\end{code}
+
+Images of compact types by surjective functions are compact.
+
+\begin{code}
+
+ image-of-compact : (f : X → Y)
+                  → is-surjection f
+                  → is-compact 𝒳 holds
+                  → is-compact 𝒴 holds
+ image-of-compact f sf compact-X (P , open-P) =
+  ⇔-open pre-image-forall image-forall (p₁ , p₂) †
+   where
+    pre-image-forall : Ω 𝓤
+    pre-image-forall = Ɐ x ꞉ X , (f x) ∈ₚ P
+
+    image-forall : Ω 𝓤
+    image-forall = Ɐ y ꞉ Y , y ∈ₚ P
+
+    p₁ : (pre-image-forall ⇒ image-forall) holds
+    p₁ pX y = surjection-induction f
+                                   sf
+                                   (_holds ∘ P)
+                                   (λ y → holds-is-prop (P y))
+                                   pX
+                                   y
+
+    p₂ : (image-forall ⇒ pre-image-forall) holds
+    p₂ pY x = pY (f x)
+
+    † : is-open-proposition pre-image-forall holds
+    † = compact-X (P ∘ f , open-P ∘ f)
+
+\end{code}
+
+This also works for any function, in which case we prove that `image f` is
+compact.
+
+We have to get out of the module defining `𝒳` and `𝒴` in order to apply the
+previous lemma.
+
+\begin{code}
+
+image-of-compact' : ((X , sX) : hSet 𝓤)
+                  → ((Y , sY) : hSet 𝓤)
+                  → (f : X → Y)
+                  → is-compact (X , sX) holds
+                  → is-compact (imageₛ (X , sX) (Y , sY) f) holds
+
+image-of-compact' (X , sX) (Y , sY) f compact-X =
+ image-of-compact (X , sX)
+                  (imageₛ (X , sX) (Y , sY) f)
+                  (corestriction f)
+                  (corestrictions-are-surjections f)
+                  compact-X
+
+\end{code}
+
+\section{References}
+
+- [1]: Davorin Lesňik. *Synthetic Topology and Constructive Metric Spaces*.
+
+  PhD Thesis, 2010
+
+  https://doi.org/10.48550/arXiv.2104.10399
+
+- [2]: Martín Escardó. *Topology via higher-order intuitionistic logic*
+
+  Unpublished notes, Pittsburgh, 2004
+
+  https://www.cs.bham.ac.uk/~mhe/papers/pittsburgh.pdf
diff --git a/source/SyntheticTopology/Density.lagda b/source/SyntheticTopology/Density.lagda
new file mode 100644
index 000000000..b6316a1de
--- /dev/null
+++ b/source/SyntheticTopology/Density.lagda
@@ -0,0 +1,84 @@
+---
+title:         Density in Synthetic Topology
+author:        Martin Trucchi
+date-started : 2024-05-28
+---
+
+\begin{code}
+
+{-# OPTIONS --safe --without-K #-}
+
+open import MLTT.Spartan
+open import UF.Base
+open import UF.FunExt
+open import UF.Powerset
+open import UF.PropTrunc
+open import UF.Sets
+open import UF.Sets-Properties
+open import UF.Subsingletons
+open import UF.SubtypeClassifier
+open import SyntheticTopology.SierpinskiObject
+
+module SyntheticTopology.Density
+        (𝓤  𝓥 : Universe)
+        (fe : Fun-Ext)
+        (pe : Prop-Ext)
+        (pt : propositional-truncations-exist)
+        (𝕊 : Generalized-Sierpinski-Object fe pe pt 𝓤 𝓥)
+        (𝒳 : hSet 𝓤)
+        where
+
+open import SyntheticTopology.Compactness 𝓤 𝓥 fe pe pt 𝕊
+open import SyntheticTopology.Overtness 𝓤 𝓥 fe pe pt 𝕊
+open import SyntheticTopology.SubObjects 𝓤 𝓥 fe pe pt 𝕊
+open import UF.ImageAndSurjection pt
+open import UF.Logic
+
+open AllCombinators pt fe
+open PropositionalTruncation pt hiding (_∨_)
+open Sierpinski-notations fe pe pt 𝕊
+
+\end{code}
+
+Density in synthetic topology. The definition comes from [1].
+
+A subset `D` of a set `X` is dense if `D` intersects every inhabited open
+subset of `X`. 
+
+The whole module is parametrized by a set `𝒳`.
+
+`is-dense 𝒳 D` should be read "D is dense in X".
+
+\begin{code}
+private
+ X = underlying-set 𝒳
+
+is-dense : (D : 𝓟 X) → Ω (𝓤 ⁺ ⊔ 𝓥)
+is-dense D =
+ Ɐ (U , open-U) ꞉ 𝓞 𝒳 ,
+  (Ǝₚ x ꞉ X , x ∈ₚ U) ⇒
+   (Ǝₚ x ꞉ X , (x ∈ₚ (D ∩ U)))
+
+\end{code}
+
+We now prove two lemmas, stating respectively that a set is dense in itself
+and that a set containing a subovert dense subset is itself overt.
+
+\begin{code}
+
+self-is-dense-in-self : is-dense full holds
+self-is-dense-in-self (P , open-P) inhabited-P =
+ ∥∥-rec (holds-is-prop (Ǝₚ x' ꞉ X , (x' ∈ₚ (full ∩ P)))) † inhabited-P
+  where
+   † : Σ x ꞉ X , x ∈ₚ P holds → (Ǝₚ x' ꞉ X , (x' ∈ₚ (full ∩ P))) holds
+   † (x , Px) = ∣ x , ⊤-holds , Px  ∣
+
+\end{code}
+
+\section{References}
+
+- [1]: Davorin Lesňik. *Synthetic Topology and Constructive Metric Spaces*.
+
+  PhD Thesis, 2010
+
+  https://doi.org/10.48550/arXiv.2104.10399
diff --git a/source/SyntheticTopology/Discreteness.lagda b/source/SyntheticTopology/Discreteness.lagda
new file mode 100644
index 000000000..624911f8b
--- /dev/null
+++ b/source/SyntheticTopology/Discreteness.lagda
@@ -0,0 +1,134 @@
+---
+title:          Discreteness in Synthetic Topology
+author:         Martin Trucchi
+date-started:   2024-05-28
+dates-modified: [2024-06-07]
+---
+
+We here implement the notion of discreteness in Synthetic Topology defined
+in [1] and [2], and then prove two lemmas.
+
+\begin{code}
+
+{-# OPTIONS --safe --without-K #-}
+
+open import MLTT.Spartan
+open import UF.Base
+open import UF.FunExt
+open import UF.PropTrunc
+open import UF.Powerset
+open import UF.Sets
+open import UF.Sets-Properties
+open import UF.Subsingletons
+open import UF.SubtypeClassifier
+open import SyntheticTopology.SierpinskiObject
+
+module SyntheticTopology.Discreteness
+        (𝓤 𝓥 : Universe)
+        (fe : Fun-Ext)
+        (pe : Prop-Ext)
+        (pt : propositional-truncations-exist)
+        (𝕊 : Generalized-Sierpinski-Object fe pe pt 𝓤 𝓥)
+        where
+
+open import SyntheticTopology.Compactness 𝓤 𝓥 fe pe pt 𝕊
+open import SyntheticTopology.SetCombinators 𝓤 fe pe pt
+open import SyntheticTopology.SierpinskiAxioms 𝓤 𝓥 fe pe pt 𝕊
+open import UF.ImageAndSurjection pt
+open import UF.Logic
+
+open AllCombinators pt fe
+open PropositionalTruncation pt hiding (_∨_)
+open Sierpinski-notations fe pe pt 𝕊
+
+\end{code}
+
+Discrete sets.
+
+A set `𝒳` is `discrete` if its equality map `λ (x , y) → x ＝ y` is
+`intrinsically-open` in the product set `𝒳 × 𝒳`.
+
+\begin{code}
+
+module _ (𝒳 : hSet 𝓤) where
+ private
+  X = underlying-set 𝒳
+  set-X = pr₂ 𝒳
+  open Equality set-X
+
+ is-discrete : Ω (𝓤 ⊔ 𝓥)
+ is-discrete = is-intrinsically-open (𝒳 ×ₛ 𝒳) (λ (x , y) → x ＝ₚ y)
+
+\end{code}
+
+We prove here that `𝟙` is discrete as long as the true truth value lies in the
+Sierpinski object's image.
+
+\begin{code}
+
+𝟙-is-discrete : contains-top holds
+              → is-discrete 𝟙ₛ holds
+
+𝟙-is-discrete ct (⋆ , ⋆) =
+ ⇔-open ⊤ (⋆ ＝ₚ ⋆) (p₁ , p₂) ct
+  where
+   open Equality 𝟙ₛ-is-set
+
+   p₁ : (⊤ ⇒ (⋆ ＝ₚ ⋆)) holds
+   p₁ = λ _ → refl
+
+   p₂ : ((⋆ ＝ₚ ⋆) ⇒ ⊤) holds
+   p₂ = λ _ → ⊤-holds
+
+\end{code}
+
+Compact indexed product of discrete set is itself discrete.
+
+\begin{code}
+
+module _ (𝒳 : hSet 𝓤) where
+ private
+  X = underlying-set 𝒳
+
+ compact-Π-discrete : (Y : X → hSet 𝓤)
+                    → is-compact 𝒳 holds
+                    → ((x : X) → is-discrete (Y x) holds)
+                    → is-discrete (Πₛ 𝒳 Y) holds
+ compact-Π-discrete Y compact-X discrete-Y (y₁ , y₂) =
+  ⇔-open extensional-eq global-eq (p₁ , p₂) †
+   where
+    open Equality (pr₂ (Πₛ 𝒳 Y))
+
+    extensional-eq : Ω 𝓤
+    extensional-eq = Ɐ x ꞉ X , ((y₁ x ＝ y₂ x) , pr₂ (Y x))
+
+    global-eq : Ω 𝓤
+    global-eq = y₁ ＝ₚ y₂
+
+    p₁ : (extensional-eq ⇒ global-eq) holds
+    p₁ = dfunext fe
+
+    p₂ : (global-eq ⇒ extensional-eq) holds
+    p₂ y₁-eq-y₂ = transport (λ - → (x : X) → ((y₁ x) ＝ ( - x)))
+                             y₁-eq-y₂
+                             λ _ → refl
+
+    † : is-open-proposition extensional-eq holds
+    † = compact-X ((λ x → (y₁ x ＝ y₂ x) , pr₂ (Y x)) ,
+                  λ x → discrete-Y x (y₁ x , y₂ x))
+
+\end{code}
+
+\section{References}
+
+- [1]: Davorin Lesňik. *Synthetic Topology and Constructive Metric Spaces*.
+
+  PhD Thesis, 2010
+
+  https://doi.org/10.48550/arXiv.2104.10399
+
+- [2]: Martín Escardó. *Topology via higher-order intuitionistic logic*
+
+  Unpublished notes, Pittsburgh, 2004
+
+  https://www.cs.bham.ac.uk/~mhe/papers/pittsburgh.pdf
diff --git a/source/SyntheticTopology/Overtness.lagda b/source/SyntheticTopology/Overtness.lagda
new file mode 100644
index 000000000..f5702f95c
--- /dev/null
+++ b/source/SyntheticTopology/Overtness.lagda
@@ -0,0 +1,201 @@
+---
+title:          Overtness in Synthetic Topology
+author:         Martin Trucchi
+date-started:   2024-05-28
+dates-modified: [2024-06-06]
+---
+
+We implement here the notion of overtness in Synthetic Topology defined here :
+[1] and [2]. We then foramlize some lemmas.
+
+\begin{code}
+
+{-# OPTIONS --safe --without-K #-}
+
+open import MLTT.Spartan
+open import SyntheticTopology.SierpinskiObject
+open import UF.FunExt
+open import UF.Logic
+open import UF.Powerset
+open import UF.PropTrunc
+open import UF.Sets
+open import UF.Subsingletons
+open import UF.SubtypeClassifier
+
+module SyntheticTopology.Overtness
+        (𝓤  𝓥 : Universe)
+        (fe : Fun-Ext)
+        (pe : Prop-Ext)
+        (pt : propositional-truncations-exist)
+        (𝕊 : Generalized-Sierpinski-Object fe pe pt 𝓤 𝓥)
+        where
+
+open import SyntheticTopology.SetCombinators 𝓤 fe pe pt
+open import UF.ImageAndSurjection pt
+
+open AllCombinators pt fe
+open PropositionalTruncation pt hiding (_∨_)
+open Sierpinski-notations fe pe pt 𝕊
+
+\end{code}
+
+Overtness
+
+Overtness is a dual notion of compactness.
+A set is `overt` if the proposition `∃ x , x ∈ₚ P` is `open` whenever `P` is
+`open`.
+
+\begin{code}
+
+module _ (𝒳 : hSet 𝓤) where
+ private
+  X = underlying-set 𝒳
+
+ is-overt : Ω (𝓤 ⁺ ⊔ 𝓥)
+ is-overt = Ɐ (P , open-P) ꞉ 𝓞 𝒳 , is-open-proposition (Ǝₚ x ꞉ X , x ∈ₚ P)
+
+\end{code}
+
+The type `𝟙` is always overt, regardless of the Sierpinski object.
+
+\begin{code}
+
+𝟙-is-overt : is-overt 𝟙ₛ holds
+𝟙-is-overt (P , open-P) =
+ ⇔-open (⋆ ∈ₚ P) (Ǝₚ x ꞉ 𝟙 , x ∈ₚ P) (p₁ , p₂) (open-P ⋆)
+ where
+  p₁ : (⋆ ∈ₚ P ⇒ Ǝₚ x ꞉ 𝟙 , x ∈ₚ P) holds
+  p₁ P-star = ∣ ⋆ , P-star ∣
+
+  p₂ : (Ǝₚ x ꞉ 𝟙 , x ∈ₚ P ⇒ ⋆ ∈ₚ P) holds
+  p₂ exists-x = ∥∥-rec (holds-is-prop (⋆ ∈ₚ P)) (λ (x , Px) → Px) exists-x
+
+\end{code}
+
+Binary product of overt sets is overt.
+
+\begin{code}
+
+module _ (𝒳 𝒴 : hSet 𝓤) where
+ private
+  X = underlying-set 𝒳
+  Y = underlying-set 𝒴
+  set-Y = pr₂ 𝒴
+  open Equality set-Y
+
+ ×-is-overt : is-overt 𝒳 holds
+              → is-overt 𝒴 holds
+              → is-overt (𝒳 ×ₛ 𝒴)  holds
+ ×-is-overt overt-X overt-Y (P , open-P) =
+  ⇔-open chained-ex tuple-ex (p₁ , p₂) †
+   where
+    tuple-ex : Ω 𝓤
+    tuple-ex = Ǝₚ z ꞉ (X × Y) , z ∈ₚ P
+
+    chained-ex : Ω 𝓤
+    chained-ex = Ǝₚ x ꞉ X , (Ǝₚ y ꞉ Y , (x , y) ∈ₚ P)
+
+    p₁ : (chained-ex ⇒ tuple-ex) holds
+    p₁ = ∥∥-rec ∃-is-prop λ (x , hyp)
+       → ∥∥-rec ∃-is-prop (λ (y , hyp') → ∣ (x , y) , hyp' ∣) hyp
+
+    p₂ : (tuple-ex ⇒ chained-ex) holds
+    p₂ = ∥∥-rec ∃-is-prop λ ((x , y) , hyp) → ∣ x , ∣ y , hyp ∣ ∣
+    
+    prop-y : 𝓟 X
+    prop-y x = Ǝₚ y ꞉ Y , (x , y) ∈ₚ P
+    
+    prop-y-open : (x : X) → is-open-proposition (prop-y x) holds
+    prop-y-open x = overt-Y ((λ y → (x , y) ∈ₚ P) , λ y → open-P (x , y))
+    
+    † : is-open-proposition chained-ex holds
+    † = overt-X (prop-y , prop-y-open)
+
+\end{code}
+
+We prove here, similar to `image-of-compact`, that image of `overt` sets are
+`overt`.
+
+\begin{code}
+
+ image-of-overt : (f : X → Y)
+                → is-surjection f
+                → is-overt 𝒳 holds
+                → is-overt 𝒴 holds
+
+ image-of-overt f sf overt-X (P , open-P) =
+  ⇔-open preimage-exists image-exists (p₁ , p₂) †
+   where
+    preimage-exists : Ω 𝓤
+    preimage-exists = Ǝₚ x ꞉ X , (f x) ∈ₚ P
+
+    image-exists : Ω 𝓤
+    image-exists = Ǝₚ y ꞉ Y , y ∈ₚ P
+
+    p₁ : (preimage-exists ⇒ image-exists) holds
+    p₁ Px = ∥∥-rec (holds-is-prop image-exists)
+                   (λ (x , Pxf) → ∣ f x , Pxf  ∣)
+                   Px
+
+    exists-preimage-of-y : (y : Y) → (Ǝₚ x ꞉ X , (f x ＝ₚ y)) holds
+    exists-preimage-of-y y =
+     surjection-induction f
+                          sf
+                          (λ y → ((Ǝₚ x ꞉ X , (f x ＝ₚ y)) holds))
+                          (λ y → holds-is-prop
+                                  (Ǝₚ x ꞉ X , (f x ＝ₚ y)))
+                          (λ x → ∣ x , refl  ∣)
+                          y
+
+    p₂ : (image-exists ⇒ preimage-exists) holds
+    p₂ Py-prop = ∥∥-rec (holds-is-prop preimage-exists)
+                        (λ (y , Py) → ∥∥-rec (holds-is-prop preimage-exists)
+                                             (λ (x , x-eq-fy) →
+                                              ∣ x , transport (_holds ∘ P)
+                                                              (x-eq-fy ⁻¹)
+                                                              Py
+                                              ∣)
+                                             (exists-preimage-of-y y))
+                        Py-prop
+
+    † : is-open-proposition preimage-exists holds
+    † = overt-X (P ∘ f , open-P ∘ f)
+
+\end{code}
+
+As for `image-of-compact'`, there is a version for any function `f : X → Y`, in
+which case `image f` is overt as a set.
+
+We have to get out of the anonymous module to access the previous version of
+`image-of-overt`.
+
+\begin{code}
+
+image-of-overt' : ((X , sX) : hSet 𝓤)
+                → ((Y , sY) : hSet 𝓤)
+                → (f : X → Y)
+                → is-overt (X , sX) holds
+                → is-overt (imageₛ (X , sX) (Y , sY) f) holds
+
+image-of-overt' (X , sX) (Y , sY) f overt-X =
+ image-of-overt (X , sX)
+                  (imageₛ (X , sX) (Y , sY) f)
+                  (corestriction f)
+                  (corestrictions-are-surjections f)
+                  overt-X
+
+\end{code}
+
+\section{References}
+
+- [1]: Davorin Lesňik. *Synthetic Topology and Constructive Metric Spaces*.
+
+  PhD Thesis, 2010
+
+  https://doi.org/10.48550/arXiv.2104.10399
+
+- [2]: Martín Escardó. *Topology via higher-order intuitionistic logic*
+
+  Unpublished notes, Pittsburgh, 2004
+
+  https://www.cs.bham.ac.uk/~mhe/papers/pittsburgh.pdf
diff --git a/source/SyntheticTopology/SetCombinators.lagda b/source/SyntheticTopology/SetCombinators.lagda
new file mode 100644
index 000000000..42c93fb18
--- /dev/null
+++ b/source/SyntheticTopology/SetCombinators.lagda
@@ -0,0 +1,153 @@
+---
+title:          Definition of some combinators and shortcut for sets.
+author:         Martin Trucchi
+date-started:   2024-06-07
+---
+
+\begin{code}
+
+{-# OPTIONS --safe --without-K #-}
+
+open import MLTT.Spartan hiding (𝟚 ; ℕ)
+open import UF.DiscreteAndSeparated hiding (𝟚-is-set ; ℕ-is-set ; ℕ-is-discrete)
+open import UF.FunExt
+open import UF.Logic
+open import UF.Powerset
+open import UF.PropTrunc
+open import UF.Sets
+open import UF.Sets-Properties
+open import UF.Subsingletons
+open import UF.Subsingletons-Properties
+open import UF.SubtypeClassifier
+
+module SyntheticTopology.SetCombinators
+        (𝓤 : Universe)
+        (fe : Fun-Ext)
+        (pe : Prop-Ext)
+        (pt : propositional-truncations-exist) where
+
+open import Locales.DiscreteLocale.Two fe pe pt
+open import Locales.Frame pt fe
+open import UF.ImageAndSurjection pt
+
+open PropositionalTruncation pt
+
+\end{code}
+
+We here define some useful shortcuts for sets, as well as combinators to avoid
+messy code in the Synthetic Topology development.
+
+The first one turns propositions into sets, in order to be able to define
+compact propositions for example.
+
+\begin{code}
+
+Ωₛ : Ω 𝓤 → hSet 𝓤
+Ωₛ p = (p holds , props-are-sets (holds-is-prop p))
+
+\end{code}
+
+Here we define shortcuts rather than combinators for sets used in the module.
+
+\begin{code}
+
+𝟘ₛ-is-set = 𝟘-is-set
+
+𝟘ₛ : hSet 𝓤
+𝟘ₛ = 𝟘 , 𝟘ₛ-is-set
+
+𝟙ₛ-is-set = 𝟙-is-set
+
+𝟙ₛ : hSet 𝓤
+𝟙ₛ = 𝟙 , 𝟙ₛ-is-set
+
+\end{code}
+
+We use `𝟚` define in `Locales.DiscreteLocale.Two`, to have a universe
+polymorphic version of `𝟚`.
+
+\begin{code}
+
+𝟚ₛ-is-set = 𝟚-is-set 𝓤
+
+𝟚ₛ : hSet 𝓤
+𝟚ₛ = (𝟚 𝓤) , 𝟚ₛ-is-set
+
+\end{code}
+
+I did not find a universe polymorphic version of `ℕ`. Here it is.
+
+\begin{code}
+
+data ℕ : 𝓤 ̇  where
+ zero : ℕ
+ succ : ℕ → ℕ
+
+pred : ℕ → ℕ
+pred zero = zero
+pred (succ n) = n
+
+boom : ℕ → 𝓤 ̇
+boom zero = 𝟘
+boom (succ _) = 𝟙
+
+ℕ-is-discrete : is-discrete ℕ
+ℕ-is-discrete zero zero = inl refl
+ℕ-is-discrete zero (succ m) = inr λ p → 𝟘-elim (𝟘-is-not-𝟙 (ap boom p))
+ℕ-is-discrete (succ n) zero = inr λ p → 𝟘-elim (𝟘-is-not-𝟙 (ap boom (p ⁻¹)))
+ℕ-is-discrete (succ n) (succ m) =
+ cases (λ p → inl (ap succ p))
+       (λ p → inr λ ps → p (ap pred ps))
+       (ℕ-is-discrete n m)
+
+ℕ-is-set : is-set ℕ
+ℕ-is-set = discrete-types-are-sets ℕ-is-discrete
+
+ℕₛ-is-set = ℕ-is-set
+
+ℕₛ : hSet 𝓤
+ℕₛ = ℕ , ℕₛ-is-set
+
+\end{code}
+
+We now define the set combinators.
+
+We have the same convention of using `𝒳` as a generic set along with the proof,
+with its underlying set being `X`.
+
+Note : for `imageₛ` , the fact that `𝒳` is a set is not useful, but
+we define it this way to keep the coherence between the arguments.
+
+\begin{code}
+
+module _ (𝒳 : hSet 𝓤) where
+ private
+  X = underlying-set 𝒳
+  set-X = pr₂ 𝒳
+
+ Πₛ : (X → hSet 𝓤) → hSet 𝓤
+ Πₛ f = Π (underlying-set ∘ f) , Π-is-set fe (pr₂ ∘ f)
+
+ module _ (𝒴 : hSet 𝓤) where
+  private
+   Y = underlying-set 𝒴
+   set-Y = pr₂ 𝒴
+
+  _×ₛ_ : hSet 𝓤
+  _×ₛ_ = (X × Y) , ×-is-set set-X set-Y
+
+  imageₛ : (X → Y) → hSet 𝓤
+  imageₛ f = (image f , Σ-is-set set-Y λ y → props-are-sets ∃-is-prop)
+
+\end{code}
+
+We now define a combinator to get the set induced by a subset. That is, if
+`𝒳 = (X , set-X)` is a set, and `U : 𝓟 X` is a subset of 𝒳, we can get the
+set induced by `U` using `𝕋ₛ U`.
+
+\begin{code}
+
+ 𝕋ₛ : 𝓟 X → hSet 𝓤
+ 𝕋ₛ U = 𝕋 U , Σ-is-set set-X λ x → props-are-sets (holds-is-prop (U x))
+
+\end{code}
diff --git a/source/SyntheticTopology/SierpinskiAxioms.lagda b/source/SyntheticTopology/SierpinskiAxioms.lagda
new file mode 100644
index 000000000..e96ffb544
--- /dev/null
+++ b/source/SyntheticTopology/SierpinskiAxioms.lagda
@@ -0,0 +1,213 @@
+---
+title:          Axioms about the Sierpinski object
+authors:        ["Martin Trucchi" , "Ayberk Tosun"]
+date-started:   2024-05-28
+dates-modified: [2024-06-07]
+---
+
+We write down here various axioms for the Sierpinski object, defined in [1].
+
+\begin{code}
+
+{-# OPTIONS --safe --without-K #-}
+
+open import MLTT.Spartan
+open import UF.Base
+open import UF.FunExt
+open import UF.Logic
+open import UF.Powerset
+open import UF.PropTrunc
+open import UF.Sets
+open import UF.Sets-Properties
+open import UF.Subsingletons
+open import UF.SubtypeClassifier
+open import SyntheticTopology.SierpinskiObject
+
+module SyntheticTopology.SierpinskiAxioms
+        (𝓤  𝓥 : Universe)
+        (fe : Fun-Ext)
+        (pe : Prop-Ext)
+        (pt : propositional-truncations-exist)
+        (𝕊 : Generalized-Sierpinski-Object fe pe pt 𝓤 𝓥)
+        where
+
+open AllCombinators pt fe
+open PropositionalTruncation pt hiding (_∨_)
+open Sierpinski-notations fe pe pt 𝕊
+
+\end{code}
+
+
+\section{Dominance axiom}
+
+The dominance axiom is the most used axiom in our setting.
+
+\begin{code}
+
+contains-top : Ω 𝓥
+contains-top = is-open-proposition ⊤
+
+openness-is-transitive : Ω (𝓤 ⁺ ⊔ 𝓥)
+openness-is-transitive =
+ Ɐ u ꞉ Ω 𝓤 ,
+  (is-open-proposition u
+   ⇒ (Ɐ p ꞉ Ω 𝓤 ,
+    (u ⇒ (is-open-proposition p))
+     ⇒ (is-open-proposition (u ∧ p))))
+
+is-synthetic-dominance : Ω (𝓤 ⁺ ⊔ 𝓥)
+is-synthetic-dominance = contains-top ∧ openness-is-transitive
+
+\end{code}
+
+We also give a natural axiom saying that the Sierpinski object is being closed
+under binary (and thus, finite if `contains-top` holds) meets :
+
+\begin{code}
+
+closed-under-binary-meets : Ω (𝓤 ⁺ ⊔ 𝓥)
+closed-under-binary-meets =
+ Ɐ p ꞉ Ω 𝓤 ,
+  Ɐ q ꞉ Ω 𝓤 ,
+   ((is-open-proposition p ∧ is-open-proposition q)
+    ⇒ is-open-proposition (p ∧ q))
+
+\end{code}
+
+Added by Martin Trucchi - 3rd June 2024.
+
+The latter directly follows from `openness-is-transitive`. It is a particular
+case in which both `P` and `Q` are known to be `open-proposition`.
+
+\begin{code}
+
+open-transitive-gives-cl-∧
+ : (openness-is-transitive ⇒ closed-under-binary-meets) holds
+open-transitive-gives-cl-∧ open-transitive p q (open-p , open-q) =
+  open-transitive p open-p q λ _ → open-q
+
+\end{code}
+
+
+\section{Standard topology}
+
+We define here the axiom of being a `standard-topology`, defined on 5.9 of [2].
+
+Note that not all "used" Sierpiński verify this (for example, see the Sierpiński
+defined in [3])
+
+\begin{code}
+
+contains-bot : Ω 𝓥
+contains-bot = is-open-proposition ⊥
+
+closed-under-binary-joins : Ω (𝓤 ⁺ ⊔ 𝓥)
+closed-under-binary-joins =
+ Ɐ p ꞉ Ω 𝓤 ,
+  Ɐ q ꞉ Ω 𝓤 ,
+   ((is-open-proposition p ∧ is-open-proposition q)
+    ⇒ is-open-proposition (p ∨ q))
+
+is-standard : Ω (𝓤 ⁺ ⊔ 𝓥)
+is-standard = contains-bot ∧ closed-under-binary-joins
+
+\end{code}
+
+\section{Phoa's principle}
+
+\begin{code}
+
+phoa’s-principle : contains-top holds → contains-bot holds → Ω (𝓤 ⁺ ⊔ 𝓥)
+phoa’s-principle ct cb =
+  Ɐ f ꞉ (Ωₒ → Ωₒ) ,
+    (Ɐ (q , open-q) ꞉ Ωₒ , pr₁ (f (q , open-q))
+      ⇔ ((pr₁ (f (⊤ , ct)) ∧ q) ∨ pr₁ (f (⊥ , cb))))
+
+\end{code}
+
+As proved in [1] , `phoa’s-principle` implies that all endomaps of the
+Sierpinski are monotonous.
+
+\begin{code}
+
+⇒-functor : (p p' q q' : Ω 𝓤)
+      → ((p ⇔ p') holds)
+      → ((q ⇔ q') holds)
+      → ((p ⇒ q) holds)
+      → ((p' ⇒ q') holds)
+
+⇒-functor p p' q q' p-eq-p' q-eq-q' p-gives-q p'-holds =
+ ⇔-transport pe q q' _holds q-eq-q'
+   (p-gives-q (⇔-transport pe p' p _holds (⇔-swap pe p p' p-eq-p') p'-holds))
+
+phoa’s-principle-gives-monotonous-maps
+ : (ct : contains-top holds) → (cb : contains-bot holds) →
+  (phoa’s-principle ct cb ⇒
+    (Ɐ f ꞉ (Ωₒ → Ωₒ) ,
+      (Ɐ (p , open-p) ꞉ Ωₒ , (Ɐ (q , open-q) ꞉ Ωₒ ,
+        (p ⇒ q) ⇒ (pr₁ (f (p , open-p)) ⇒ pr₁ (f (q , open-q))))))) holds
+
+phoa’s-principle-gives-monotonous-maps
+ ct cb phoa-p f (p , open-p) (q , open-q) p-gives-q =
+  ⇔-transport pe
+              ((((pr₁ (f (⊤ , ct))) ∧ p) ∨ (pr₁ (f (⊥ , cb))))
+               ⇒ (((pr₁ (f (⊤ , ct))) ∧ q) ∨ (pr₁ (f (⊥ , cb)))))
+              ((pr₁ (f (p , open-p))) ⇒ (pr₁ (f (q , open-q))))
+              _holds
+              (equiv₁ , equiv₂)
+              †
+   where
+    equiv₁ : (((pr₁ (f (⊤ , ct)) ∧ p ∨ (pr₁ (f (⊥ , cb))))
+             ⇒ (pr₁ (f (⊤ , ct)) ∧ q ∨ pr₁ (f (⊥ , cb))))
+                ⇒ pr₁ (f (p , open-p)) ⇒ pr₁ (f (q , open-q))) holds
+    equiv₁ = ⇒-functor ((pr₁ (f (⊤ , ct))) ∧ p ∨ (pr₁ (f (⊥ , cb))))
+                       ((pr₁ (f (p , open-p))))
+                       ((pr₁ (f (⊤ , ct))) ∧ q ∨ (pr₁ (f (⊥ , cb))))
+                       ((pr₁ (f (q , open-q))))
+                       (⇔-swap pe ((pr₁ (f (p , open-p))))
+                               ((pr₁ (f (⊤ , ct))) ∧ p ∨ (pr₁ (f (⊥ , cb))))
+                                        (phoa-p f (p , open-p)))
+                       (⇔-swap pe ((pr₁ (f (q , open-q))))
+                         ((pr₁ (f (⊤ , ct))) ∧ q ∨ (pr₁ (f (⊥ , cb))))
+                                        (phoa-p f (q , open-q)))
+
+    equiv₂ : (((pr₁ (f (p , open-p))) ⇒ (pr₁ (f (q , open-q))))
+             ⇒ ((pr₁ (f (⊤ , ct))) ∧ p ∨ (pr₁ (f (⊥ , cb))))
+             ⇒ ((pr₁ (f (⊤ , ct))) ∧ q ∨ (pr₁ (f (⊥ , cb))))) holds
+    equiv₂ = ⇒-functor ((pr₁ (f (p , open-p))))
+                       ((pr₁ (f (⊤ , ct))) ∧ p ∨ (pr₁ (f (⊥ , cb))))
+                       ((pr₁ (f (q , open-q))))
+                       ((pr₁ (f (⊤ , ct))) ∧ q ∨ (pr₁ (f (⊥ , cb))))
+                       (phoa-p f (p , open-p))
+                       (phoa-p f (q , open-q))
+
+    † : (((pr₁ (f (⊤ , ct))) ∧ p ∨ (pr₁ (f (⊥ , cb))))
+     ⇒ ((pr₁ (f (⊤ , ct))) ∧ q ∨ (pr₁ (f (⊥ , cb))))) holds
+    † and-or-p =
+     ∥∥-rec (holds-is-prop ((pr₁ (f (⊤ , ct))) ∧ q ∨ (pr₁ (f (⊥ , cb)))))
+            (cases (λ (f-top-holds , p-holds) →
+                                   ∣ inl (f-top-holds , p-gives-q p-holds)  ∣)
+                                   (∣_∣ ∘ inr))
+                        and-or-p
+
+\end{code}
+
+\section{References}
+
+- [1]: Davorin Lesňik. *Synthetic Topology and Constructive Metric Spaces*.
+
+  PhD Thesis, 2010
+
+  https://doi.org/10.48550/arXiv.2104.10399
+
+- [2]: Martín Escardó. *Topology via higher-order intuitionistic logic*
+
+  Unpublished notes, Pittsburgh, 2004
+
+  https://www.cs.bham.ac.uk/~mhe/papers/pittsburgh.pdf
+
+- [3]: Martín Escardó. *Synthetic topology of data types and classical spaces*.
+
+  ENTCS, Elsevier, volume 87, pages 21-156, November 2004.
+
+  https://www.cs.bham.ac.uk/~mhe/papers/entcs87.pdf
diff --git a/source/SyntheticTopology/SierpinskiObject.lagda b/source/SyntheticTopology/SierpinskiObject.lagda
new file mode 100644
index 000000000..1699c897e
--- /dev/null
+++ b/source/SyntheticTopology/SierpinskiObject.lagda
@@ -0,0 +1,177 @@
+---
+title:          Definition of Sierpinski object synthetic topology
+authors:        ["Ayberk Tosun", "Martin Trucchi"]
+date-started:   2024-05-02
+date-completed: 2024-05-31
+dates-updated:  [2024-05-28, 2024-06-05 , 2024-06-07]
+---
+
+\begin{code}
+
+{-# OPTIONS --safe --without-K #-}
+
+open import MLTT.Spartan
+open import UF.FunExt
+open import UF.Powerset
+open import UF.PropTrunc
+open import UF.Sets
+open import UF.Sets-Properties
+open import UF.Subsingletons
+open import UF.Subsingletons-Properties
+open import UF.SubtypeClassifier
+
+module SyntheticTopology.SierpinskiObject
+        (fe : Fun-Ext)
+        (pe : Prop-Ext)
+        (pt : propositional-truncations-exist) where
+
+open import UF.Classifiers
+open import UF.Embeddings
+open import UF.Equiv
+open import UF.ImageAndSurjection pt
+open import UF.Logic
+open import UF.Subsingletons-FunExt
+open import UF.Univalence
+open import UF.UniverseEmbedding
+
+open AllCombinators pt fe
+open PropositionalTruncation pt hiding (_∨_)
+
+\end{code}
+
+What is a Sierpiński object? In Martín Escardó´s unpublished note [2],
+a Sierpiński object is defined in the setting of a topos as a subobject of the
+subobject classifier. This is also given in Definition 2.4 of Davorin Lesnik's
+thesis [1], who took this unpublished note as a starting point for his PhD
+thesis.
+
+The purpose of this development is to develop these notions in the context of
+HoTT/UF, where we look at subtypes of the subtype classifier. Because we work
+predicatively, however, the definition of the notion of Sierpiński object is not
+that straightforward in our setting.
+
+In the impredicative setting of topos theory, one works with the topos of 𝓤-sets
+over some universe 𝓤, and the Sierpiński object in that setting would translate
+to:
+
+\begin{code}
+
+Sierpinski-Object₀ : (𝓤 : Universe) → 𝓤 ⁺  ̇
+Sierpinski-Object₀ 𝓤 = Subtype' 𝓤 (Ω 𝓤)
+
+\end{code}
+
+However, many dominances that we are interested in do not fit this definition in
+a predicative setting. For example, the largest possible dominance of `Ω 𝓤` is
+𝓤⁺-set rather than a 𝓤-set. Accordingly, we generalize the universes in the
+notion of Sierpiński object as follows:
+
+\begin{code}
+
+Generalized-Sierpinski-Object : (𝓤 𝓥 : Universe) → (𝓤 ⊔ 𝓥) ⁺  ̇
+Generalized-Sierpinski-Object 𝓤 𝓥 = Ω 𝓤 → Ω 𝓥
+
+\end{code}
+
+We think that in most cases, our dominances will be of the form `Ω 𝓤 → Ω (𝓤 ⁺)`,
+but because we can prove things in this general setting, we choose to work with
+the generalized definition instead.
+
+We define some notation to refer to components of a Sierpiński object.
+
+In the module below, we assume the existence of a Sierpiński object `𝕊` and
+define some notions _synthetically_, following the work of Martín Escardó (and
+Davorin Lešnik).
+
+\begin{code}
+
+module Sierpinski-notations (𝕊 : Generalized-Sierpinski-Object 𝓤 𝓥) where
+
+\end{code}
+
+The propositions in `Ω` that fall in the subset `𝕊` are called _open
+propositions_. We introduce suggestive terminology accordingly.
+
+The type of open proposition is noted Ωₒ
+
+\begin{code}
+
+ is-open-proposition : Ω 𝓤 → Ω 𝓥
+ is-open-proposition = 𝕊
+
+ Ωₒ : 𝓤 ⁺ ⊔ 𝓥  ̇
+ Ωₒ = Σ p ꞉ Ω 𝓤 , is-open-proposition p holds
+
+\end{code}
+
+Here, we only work with sets.
+
+We defined some combinators for the sake of notational simplicity in the module
+SetCombinators.
+
+To define this and some related notions, we work in a module parameterized by an
+hSet `𝒳`. We adopt the convention of using calligraphic letters `𝒳`, `𝒴`, ...
+for inhabitants of the type `hSet`.
+
+\begin{code}
+
+ module _ (𝒳 : hSet 𝓤) where
+
+\end{code}
+
+We denote by `X` the underlying set of `𝒳`.
+
+\begin{code}
+
+  private
+   X = underlying-set 𝒳
+
+\end{code}
+
+A subset of a set is said to be `intrinsically open` if it is a predicate
+defined by open propositions.
+
+\begin{code}
+
+  is-intrinsically-open : 𝓟 X → Ω (𝓤 ⊔ 𝓥)
+  is-intrinsically-open P = Ɐ x ꞉ X , is-open-proposition (x ∈ₚ P)
+
+\end{code}
+
+For convenience, we write down the subtype of open propositions (= subset) of a
+set `X`
+
+\begin{code}
+
+  𝓞 : 𝓤 ⁺ ⊔ 𝓥  ̇
+  𝓞 = Σ P ꞉ 𝓟 X , is-intrinsically-open P holds
+
+  underlying-prop : 𝓞 → 𝓟 X
+  underlying-prop = pr₁
+
+\end{code}
+
+We also prove the following convenient lemma.
+
+\begin{code}
+
+ ⇔-open
+  : (p q : Ω 𝓤)
+  → ((p ⇔ q) ⇒ is-open-proposition p ⇒ is-open-proposition q) holds
+ ⇔-open p q = ⇔-transport pe p q (_holds ∘ is-open-proposition)
+
+\end{code}
+
+\section{References}
+
+- [1]: Davorin Lesňik. *Synthetic Topology and Constructive Metric Spaces*.
+
+  PhD Thesis, 2010
+
+  https://doi.org/10.48550/arXiv.2104.10399
+
+- [2]: Martín Escardó. *Topology via higher-order intuitionistic logic*
+
+  Unpublished notes, Pittsburgh, 2004
+
+  https://www.cs.bham.ac.uk/~mhe/papers/pittsburgh.pdf
diff --git a/source/SyntheticTopology/SubObjects.lagda b/source/SyntheticTopology/SubObjects.lagda
new file mode 100644
index 000000000..6110b728d
--- /dev/null
+++ b/source/SyntheticTopology/SubObjects.lagda
@@ -0,0 +1,246 @@
+---
+title:        Subobjects in Synthetic Topology
+author:       Martin Trucchi
+date-started: 2024-05-28
+---
+
+\begin{code}
+
+{-# OPTIONS --safe --without-K #-}
+
+open import MLTT.Spartan
+open import UF.Base
+open import UF.FunExt
+open import UF.Powerset
+open import UF.PropTrunc
+open import UF.Sets
+open import UF.Sets-Properties
+open import UF.Subsingletons
+open import UF.SubtypeClassifier
+open import SyntheticTopology.SierpinskiObject
+
+module SyntheticTopology.SubObjects
+        (𝓤 𝓥 : Universe)
+        (fe : Fun-Ext)
+        (pe : Prop-Ext)
+        (pt : propositional-truncations-exist)
+        (𝕊 : Generalized-Sierpinski-Object fe pe pt 𝓤 𝓥)
+        where
+
+open import SyntheticTopology.Compactness 𝓤 𝓥 fe pe pt 𝕊
+open import SyntheticTopology.Discreteness 𝓤 𝓥 fe pe pt 𝕊
+open import SyntheticTopology.Overtness 𝓤 𝓥 fe pe pt 𝕊
+open import SyntheticTopology.SetCombinators 𝓤 fe pe pt
+open import SyntheticTopology.SierpinskiAxioms 𝓤 𝓥 fe pe pt 𝕊
+open import UF.ImageAndSurjection pt
+open import UF.Logic
+
+open AllCombinators pt fe
+open PropositionalTruncation pt hiding (_∨_)
+open Sierpinski-notations fe pe pt 𝕊
+
+\end{code}
+
+We define notions involving sub-objects (sub-overtness, sub-compactness...)
+defined in [2].
+We also prove some lemmas that are in [1] and [2].
+
+Because of predicativity, we have to use definitions 2. of 7.2 and 8.2
+for subcompactness and subovertness in [2].
+
+\begin{code}
+
+module subdefinitions (𝒳 : hSet 𝓤) where
+ private
+  X = underlying-set 𝒳
+  set-X = pr₂ 𝒳
+
+ is-subcompact : (U : 𝓟 X) → Ω (𝓤 ⁺ ⊔ 𝓥)
+ is-subcompact U =
+  Ɐ (P , open-P) ꞉ 𝓞 𝒳
+   , is-open-proposition (Ɐ x ꞉ X , (x ∈ₚ U) ⇒ x ∈ₚ P)
+
+ is-subcompact' : (U : 𝓟 X) → Ω (𝓤 ⁺ ⊔ 𝓥)
+ is-subcompact' U =
+  Ɐ (P , open-P) ꞉ 𝓞 𝒳
+   , is-open-proposition (Ɐ (x , Ux) ꞉ (𝕋 U) , x ∈ₚ P)
+
+ is-subovert : (U : 𝓟 X) → Ω (𝓤 ⁺ ⊔ 𝓥)
+ is-subovert U =
+  Ɐ (P , open-P) ꞉ 𝓞 𝒳 , is-open-proposition (Ǝₚ (x , Ux) ꞉ (𝕋 U) , x ∈ₚ P)
+
+\end{code}
+
+First, we can prove that the two notions of subcompactness are equivalent.
+
+\begin{code}
+
+ sub-gives-sub' : (U : 𝓟 X) → is-subcompact U holds → is-subcompact' U holds
+ sub-gives-sub' U sub-U (P , open-P) =
+  ⇔-open (Ɐ x ꞉ X , x ∈ₚ U ⇒ x ∈ₚ P) (Ɐ (x , Ux) ꞉ (𝕋 U) , x ∈ₚ P)
+          ((λ hyp (x , Ux) → hyp x Ux) , λ hyp x Ux → hyp (x , Ux))
+          (sub-U ((λ x → x ∈ₚ P) , open-P))
+
+
+ sub'-gives-sub : (U : 𝓟 X) → is-subcompact' U holds → is-subcompact U holds
+ sub'-gives-sub U sub'-U (P , open-P) =
+  ⇔-open (Ɐ (x , Ux) ꞉ (𝕋 U) , x ∈ₚ P) (Ɐ x ꞉ X , x ∈ₚ U ⇒ x ∈ₚ P)
+          ((λ hyp x Ux → hyp (x , Ux)) , (λ hyp (x , Ux) → hyp x Ux))
+          (sub'-U ((λ x → x ∈ₚ P) , open-P))
+
+\end{code}
+
+Then we prove some lemmas.
+
+\begin{code}
+
+ subovert-of-discrete-is-open : (U : 𝓟 X)
+                              → is-subovert U holds
+                              → is-discrete 𝒳 holds
+                              → is-intrinsically-open 𝒳 U holds
+
+ subovert-of-discrete-is-open U subovert-U discrete-X x =
+  ⇔-open (Ǝₚ (y , Uy) ꞉ (𝕋 U) , (x ＝ₚ y)) (x ∈ₚ U) (p₁ , p₂) †
+   where
+    open Equality set-X
+
+    p₁ : ((Ǝₚ (y , Uy) ꞉ (𝕋 U) , (x ＝ₚ y)) ⇒ x ∈ₚ U) holds
+    p₁ ex-y = ∥∥-rec (holds-is-prop (x ∈ₚ U))
+                     (λ ((y , Uy) , y-eq-x) → transport (_holds ∘ U)
+                                                        (y-eq-x ⁻¹)
+                                                        Uy)
+                     ex-y
+
+    p₂ : (x ∈ₚ U ⇒ Ǝₚ (y , Uy) ꞉ (𝕋 U) , (x ＝ₚ y)) holds
+    p₂ Ux = ∣ (x , Ux) , refl ∣
+
+    † : is-open-proposition (Ǝₚ (y , Uy) ꞉ (𝕋 U) , (x ＝ₚ y)) holds
+    † = subovert-U ((λ y → x ＝ₚ y) , λ y → discrete-X (x , y))
+
+
+ subovert-inter-open-subovert : closed-under-binary-meets holds
+                              → (Ɐ A ꞉ (𝓟 X) ,
+                                  Ɐ (U , _) ꞉ 𝓞 𝒳 ,
+                                   is-subovert A
+                                    ⇒ is-subovert (A ∩ U)) holds
+
+ subovert-inter-open-subovert cl-∧ A (U , open-U) subovert-A (V , open-V) =
+  ⇔-open T-A
+         T-A∩U
+         (p₁ , p₂)
+         (subovert-A (U ∩ V , λ x → cl-∧ (U x) (V x) ((open-U x) , (open-V x))))
+   where
+    T-A : Ω 𝓤
+    T-A = Ǝₚ (x , Ax) ꞉ (𝕋 A) , (x ∈ₚ (U ∩ V))
+
+    T-A∩U : Ω 𝓤
+    T-A∩U = Ǝₚ (x , A-U-x) ꞉ (𝕋 (A ∩ U)) , (x ∈ₚ V)
+
+    p₁ : (T-A ⇒ T-A∩U) holds
+    p₁ ex-U-V = ∥∥-rec (holds-is-prop T-A∩U)
+                       (λ ((x , Ax) , Ux , Vx) → ∣ (x , Ax , Ux) , Vx  ∣)
+                       ex-U-V
+
+    p₂ : (T-A∩U ⇒ T-A) holds
+    p₂ ex-V = ∥∥-rec (holds-is-prop T-A)
+                     (λ ((x , Ax , Ux) , Vx) → ∣ (x , Ax) , Ux , Vx  ∣)
+                     ex-V
+
+ open-subset-of-overt-is-subovert : closed-under-binary-meets holds
+                                  → (Ɐ (U , _) ꞉ 𝓞 𝒳 ,
+                                     is-overt 𝒳 ⇒ is-subovert U) holds
+
+ open-subset-of-overt-is-subovert cl-∧ (U , open-U) overt-X (V , open-V) =
+  ⇔-open (Ǝₚ x ꞉ X , x ∈ₚ (U ∩ V))
+         (Ǝₚ (x , Ux) ꞉ (𝕋 U) , (x ∈ₚ V))
+         ((λ ex-U∩V → ∥∥-rec (holds-is-prop (Ǝₚ (x , Ux) ꞉ (𝕋 U) , (x ∈ₚ V)))
+                             (λ (x , Ux , Vx) → ∣ (x , Ux) , Vx ∣)
+                             ex-U∩V) ,
+           (λ ex-V → ∥∥-rec (holds-is-prop (Ǝₚ x ꞉ X , (x ∈ₚ (U ∩ V))))
+                             (λ ((x , Ux) , Vx) → ∣ x , Ux , Vx ∣)
+                             ex-V))
+         (overt-X ((U ∩ V) , (λ x → cl-∧ (x ∈ₚ U)
+                                         (x ∈ₚ V)
+                                         ((open-U x) , (open-V x)))))
+
+\end{code}
+
+We have some lemmas that states the consistency of "sub" definitions
+related to "plain" ones.
+
+\begin{code}
+
+ compact-iff-subcompact-in-self
+  : ((is-compact 𝒳 ⇔ (is-subcompact full))) holds
+
+ compact-iff-subcompact-in-self =
+  compact-gives-subcompact , subcompact-gives-compact
+
+  where
+    compact-gives-subcompact :
+     (is-compact 𝒳 ⇒ is-subcompact full) holds
+    compact-gives-subcompact compact-X (U , open-U) =
+     ⇔-open (Ɐ x ꞉ X , x ∈ₚ U)
+            (Ɐ x ꞉ X , ⊤ ⇒ U x)
+            ((λ hyp x _ → hyp x) , (λ hyp x → hyp x ⊤-holds))
+            (compact-X (U , open-U))
+
+    subcompact-gives-compact :
+     ( is-subcompact full ⇒ is-compact 𝒳) holds
+    subcompact-gives-compact = λ subcompact-X (U , open-U) →
+     ⇔-open (Ɐ x ꞉ X , ⊤ ⇒ x ∈ₚ U)
+            (Ɐ x ꞉ X , x ∈ₚ U)
+            ((λ hyp x → hyp x ⊤-holds) , (λ hyp x _ → hyp x))
+            (subcompact-X ((λ z → z ∈ₚ U) , open-U))
+
+
+ overt-iff-subovert-in-self
+  : ((is-overt 𝒳 ⇔ (is-subovert full))) holds
+
+ overt-iff-subovert-in-self =
+  overt-gives-subovert , subovert-gives-overt
+   where
+    p₁ : (U : 𝓟 X)
+       → ((Ǝₚ x ꞉ X , x ∈ₚ U) ⇒ (Ǝₚ (x , true) ꞉ (𝕋 full) , x ∈ₚ U)) holds
+    p₁ U ex-U = ∥∥-rec (holds-is-prop (Ǝₚ (x , true) ꞉ (𝕋 full) , x ∈ₚ U))
+                       (λ (x , Ux) → ∣ (x , ⊤-holds) , Ux ∣)
+                       ex-U
+
+    p₂ : (U : 𝓟 X)
+       → ((Ǝₚ (x , true) ꞉ (𝕋 full) , x ∈ₚ U) ⇒ (Ǝₚ x ꞉ X , x ∈ₚ U)) holds
+    p₂ U ex-full = ∥∥-rec (holds-is-prop (Ǝₚ x ꞉ X , x ∈ₚ U))
+                          (λ ((x , true) , Ux) → ∣ x , Ux ∣)
+                          ex-full
+
+    overt-gives-subovert :
+     (is-overt 𝒳 ⇒ is-subovert full) holds
+
+    overt-gives-subovert overt-X (U , open-U) =
+     ⇔-open (Ǝₚ x ꞉ X , x ∈ₚ U)
+            (Ǝₚ (x , true) ꞉ (𝕋 full) , U x)
+            (p₁ U , p₂ U)
+            (overt-X (U , open-U))
+
+    subovert-gives-overt :
+     ( is-subovert full ⇒ is-overt 𝒳) holds
+
+    subovert-gives-overt = λ subovert-X (U , open-U) →
+      ⇔-open (Ǝₚ (x , true) ꞉ (𝕋 full) , U x)
+             (Ǝₚ x ꞉ X , x ∈ₚ U)
+             (p₂ U , p₁ U)
+             (subovert-X (U , open-U))
+\end{code}
+
+\section{References}
+
+- [1]: Davorin Lesňik. *Synthetic Topology and Constructive Metric Spaces*.
+
+  PhD Thesis, 2010
+
+  https://doi.org/10.48550/arXiv.2104.10399
+
+- [2]: Martín Escardó. *Topology via higher-order intuitionistic logic*
+
+  Unpublished notes, Pittsburgh, 2004
+
+  https://www.cs.bham.ac.uk/~mhe/papers/pittsburgh.pdf
diff --git a/source/SyntheticTopology/index.lagda b/source/SyntheticTopology/index.lagda
new file mode 100644
index 000000000..e882d6bf4
--- /dev/null
+++ b/source/SyntheticTopology/index.lagda
@@ -0,0 +1,76 @@
+\begin{code}
+
+{-# OPTIONS --safe --without-K #-}
+
+module SyntheticTopology.index where
+
+\end{code}
+
+The import lines are sorted alphabetically.
+
+The module `Compactness` defines the synthetic notion of compact sets.
+
+\begin{code}
+
+import SyntheticTopology.Compactness
+
+\end{code}
+
+The module `Density` defines the synthetic notion of dense subsets.
+
+\begin{code}
+
+import SyntheticTopology.Density
+
+\end{code}
+
+The module `Discreteness` defines the synthetic notion of discrete sets.
+
+\begin{code}
+
+import SyntheticTopology.Discreteness
+
+\end{code}
+
+The module `Overtness` defines the synthetic notion of overt sets.
+
+\begin{code}
+
+import SyntheticTopology.Overtness
+
+\end{code}
+
+We define in this module useful combinators and shortcut for sets :
+
+\begin{code}
+
+import SyntheticTopology.SetCombinators
+
+\end{code}
+
+
+The axioms considered on Sierpiński objects live in module `SierpinskiAxioms`:
+
+\begin{code}
+
+import SyntheticTopology.SierpinskiAxioms
+
+\end{code}
+
+The following module contains definition of the notion of Sierpiński object.
+It is the "root" module.
+
+\begin{code}
+
+import SyntheticTopology.SierpinskiObject
+
+\end{code}
+
+The module `Subproperties` defines the analogous notions of overtness and
+compactness for subsets and states somme lemmas.
+
+\begin{code}
+
+import SyntheticTopology.SubObjects
+
+\end{code}
diff --git a/source/UF/Logic.lagda b/source/UF/Logic.lagda
index 9c8571cd8..ede918d94 100644
--- a/source/UF/Logic.lagda
+++ b/source/UF/Logic.lagda
@@ -210,6 +210,18 @@ Added by Martin Escardo 1st Nov 2023.
 
 End of addition.
 
+Added by Martin Trucchi and Ayberk Tosun 2024-05-28.
+
+\begin{code}
+
+  ⇔-transport : (P Q : Ω 𝓤) → (B : Ω 𝓤 → 𝓦  ̇) → ((P ⇔ Q) holds) → B P → B Q
+  ⇔-transport {𝓤} P Q (𝓟) P-iff-Q Prop-P = transport 𝓟 q Prop-P
+    where
+     q : P ＝ Q
+     q = ⇔-gives-＝ P Q (holds-gives-equal-⊤ pe fe (P ⇔ Q) P-iff-Q)
+
+\end{code}
+
 \section{Disjunction}
 
 \begin{code}
diff --git a/source/index.lagda b/source/index.lagda
index cb03a76b9..b58be4bcc 100644
--- a/source/index.lagda
+++ b/source/index.lagda
@@ -55,9 +55,9 @@
 
      (https://www.cs.bham.ac.uk/~mhe/TypeTopology/AllModulesIndex.html)
 
-   * In our last count, on 2024.09.12, this development has 788 Agda
-     files with 226K lines of code, including comments and blank
-     lines.
+   * In our last count, on 2024.07.18, this development has 778 Agda
+     files with 222K lines of code, including comments and blank
+     lines. But we don't update the count frequently.
 
 Philosophy of the repository
 ----------------------------