example of a type that is not sequentially Hausdorff

martinescardo · Jul 18, 2024 · 21f9f71 · 21f9f71
1 parent 1a118b1
commit 21f9f71
Show file tree

Hide file tree

Showing 3 changed files with 57 additions and 17 deletions.
diff --git a/source/TypeTopology/FailureOfTotalSeparatedness.lagda b/source/TypeTopology/FailureOfTotalSeparatedness.lagda
@@ -37,13 +37,13 @@ closed terms, and which is a theorem rather than a metatheorem.
 
 open import UF.FunExt
 
-module TypeTopology.FailureOfTotalSeparatedness (fe : FunExt) where
+module TypeTopology.FailureOfTotalSeparatedness (fe₀ : funext₀) where
 
 open import MLTT.Spartan
 
 open import MLTT.Two-Properties
 open import CoNaturals.Type
-open import Taboos.BasicDiscontinuity (fe 𝓤₀ 𝓤₀)
+open import Taboos.BasicDiscontinuity fe₀
 open import Taboos.WLPO
 open import UF.Base
 open import Notation.CanonicalMap
@@ -110,7 +110,7 @@ module concrete-example where
    p₁ u = p (u , λ r → ₁)
 
    lemma : (n : ℕ) → p₀ (ι n) ＝ p₁ (ι n)
-   lemma n = ap (λ - → p (ι n , -)) (dfunext (fe 𝓤₀ 𝓤₀) claim)
+   lemma n = ap (λ - → p (ι n , -)) (dfunext fe₀ claim)
     where
      claim : (r : ι n ＝ ∞) → (λ r → ₀) r ＝ (λ r → ₁) r
      claim s = 𝟘-elim (∞-is-not-finite n (s ⁻¹))
@@ -120,7 +120,10 @@ module concrete-example where
  𝟚-indistinguishability : ¬ WLPO → (p : X → 𝟚) → p ∞₀ ＝ p ∞₁
  𝟚-indistinguishability nwlpo p = 𝟚-is-¬¬-separated (p ∞₀) (p ∞₁)
                                    (not-Σ-implies-Π-not
-                                   (contrapositive (λ σ → failure (pr₁ σ) (pr₂ σ)) nwlpo) p)
+                                     (contrapositive
+                                       (λ (p , ν) → failure p ν)
+                                       nwlpo)
+                                     p)
 \end{code}
 
  Precisely because one cannot construct maps from X into 𝟚 that
@@ -139,7 +142,7 @@ module concrete-example where
    t = transport (λ - → - ＝ ∞ → 𝟚)
 
    claim₀ : refl ＝ p
-   claim₀ = ℕ∞-is-set (fe 𝓤₀ 𝓤₀) refl p
+   claim₀ = ℕ∞-is-set fe₀ refl p
 
    claim₁ : t p (λ p → ₀) ＝ (λ p → ₁)
    claim₁ = from-Σ-＝' r
@@ -177,7 +180,12 @@ unchanged.
 
 \begin{code}
 
-module general-example (𝓤 : Universe) (X : 𝓤 ̇ ) (a : X) where
+module general-example
+        (fe : FunExt)
+        (𝓤 : Universe)
+        (X : 𝓤 ̇ )
+        (a : X)
+       where
 
  Y : 𝓤 ̇
  Y = Σ x ꞉ X , (x ＝ a → 𝟚)

diff --git a/source/TypeTopology/SequentiallyHausdorff.lagda b/source/TypeTopology/SequentiallyHausdorff.lagda
@@ -134,19 +134,51 @@ closed under products (and hence function spaces and more generally
 form an exponential ideal) and under retracts, as proved in the above
 import TypeTopology.TotallySeparated.
 
-But there are also counterexamples, which, in particular, show that
-totally separated types are not necessarily closed under sums.
+And here is an example of a non-sequentially Hausdorff space, which
+was originally offered in the following imported module as an example
+of a type which is not totally separated in general.
 
 \begin{code}
 
-import TypeTopology.FailureOfTotalSeparatedness
+open import TypeTopology.FailureOfTotalSeparatedness fe₀
+
+ℕ∞₂ : 𝓤₀ ̇
+ℕ∞₂ = Σ u ꞉ ℕ∞ , (u ＝ ∞ → 𝟚)
+
+ℕ∞₂-is-not-sequentially-Hausdorff : ¬ is-sequentially-Hausdorff ℕ∞₂
+ℕ∞₂-is-not-sequentially-Hausdorff h = III
+ where
+  open concrete-example
+
+  f g : ℕ∞ → ℕ∞₂
+  f u = u , (λ (e : u ＝ ∞) → ₀)
+  g u = u , (λ (e : u ＝ ∞) → ₁)
+
+  I : (n : ℕ) → (λ (e : ι n ＝ ∞) → ₀) ＝ (λ (e : ι n ＝ ∞) → ₁)
+  I n = dfunext fe₀ (λ (e : ι n ＝ ∞) → 𝟘-elim (∞-is-not-finite n (e ⁻¹)))
+
+  a : (n : ℕ) → f (ι n) ＝ g (ι n)
+  a n = ap (ι n ,_) (I n)
+
+  II : ∞₀ ＝ ∞₁
+  II = h f g a
+
+  III : 𝟘
+  III = ∞₀-and-∞₁-different II
 
 \end{code}
 
-It is a fact that the types defined in the above import are not
-sequentially Hausdorff in Johnstone's topological topos.
+The following was already proved in TypeTopology.FailureOfTotalSeparatedness.
+
+\begin{code}
+
+ℕ∞₂-is-not-always-totally-separated : is-totally-separated ℕ∞₂ → ¬¬ WLPO
+ℕ∞₂-is-not-always-totally-separated ts nwlpo =
+ ℕ∞₂-is-not-sequentially-Hausdorff
+  (totally-separated-types-are-sequentially-Hausdorff nwlpo ℕ∞₂ ts)
+
+\end{code}
 
-TODO. Prove this synthetically here, assuming ¬ WLPO. It is not
-possible to prove this without assuming anything, given what we proved
-above. I think I know how to prove this, but I haven't tested this
-here yet.
+The proof given here is the same, but factored in two steps. Notice
+that if ¬ WLPO is regarded as a continuity principle, then ¬¬ WLPO is
+a discontinuity principle.
diff --git a/source/TypeTopology/SigmaDiscreteAndTotallySeparated.lagda b/source/TypeTopology/SigmaDiscreteAndTotallySeparated.lagda
@@ -175,7 +175,7 @@ module _ (fe : FunExt) where
       ¬¬ WLPO
 
  Σ-totally-separated-taboo τ =
-   concrete-example.Failure fe
+   concrete-example.Failure fe₀
     (τ ℕ∞ (λ u → u ＝ ∞ → 𝟚)
        (ℕ∞-is-totally-separated fe₀)
           (λ u → Π-is-totally-separated fe₀ (λ _ → 𝟚-is-totally-separated)))
@@ -207,7 +207,7 @@ Even compact totally separated types fail to be closed under Σ:
       ¬¬ WLPO
 
  Σ-totally-separated-stronger-taboo τ =
-   concrete-example.Failure fe
+   concrete-example.Failure fe₀
     (τ ℕ∞ (λ u → u ＝ ∞ → 𝟚)
        (ℕ∞-compact fe₀)
        (λ _ → compact∙-types-are-compact