From ea0dae9a21e9ed728a539c02fa3b4be42cc366c0 Mon Sep 17 00:00:00 2001
From: Martin T <supermartruc@gmail.com>
Date: Sun, 25 Aug 2024 21:30:49 +0200
Subject: [PATCH] Added product of overt in Overtness, small eta-rule cleanup
 in Compactness

---
 source/SyntheticTopology/Compactness.lagda |  2 +-
 source/SyntheticTopology/Overtness.lagda   | 38 ++++++++++++++++++++--
 2 files changed, 37 insertions(+), 3 deletions(-)

diff --git a/source/SyntheticTopology/Compactness.lagda b/source/SyntheticTopology/Compactness.lagda
index 33022cbd9..cea7741da 100644
--- a/source/SyntheticTopology/Compactness.lagda
+++ b/source/SyntheticTopology/Compactness.lagda
@@ -108,7 +108,7 @@ module _ (𝒳 𝒴 : hSet 𝓤) where
     prop-y-open x = compact-Y ((λ y → (x , y) ∈ₚ P) , λ y → open-P (x , y))
 
     † : is-open-proposition chained-forall holds
-    † = compact-X ((λ x → prop-y x) , prop-y-open)
+    † = compact-X (prop-y , prop-y-open)
 
 \end{code}
 
diff --git a/source/SyntheticTopology/Overtness.lagda b/source/SyntheticTopology/Overtness.lagda
index a85e0fce0..f5702f95c 100644
--- a/source/SyntheticTopology/Overtness.lagda
+++ b/source/SyntheticTopology/Overtness.lagda
@@ -72,8 +72,7 @@ The type `𝟙` is always overt, regardless of the Sierpinski object.
 
 \end{code}
 
-We prove here, similar to `image-of-compact`, that image of `overt` sets are
-`overt`.
+Binary product of overt sets is overt.
 
 \begin{code}
 
@@ -84,6 +83,41 @@ module _ (𝒳 𝒴 : hSet 𝓤) where
   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