Martin Escardo, 17th July 2024. Sequentially Hausdorff types. Motivated by https://grossack.site/2024/07/03/life-in-johnstones-topological-topos The idea in this file, and many files in TypeTopology, is that we are working in an arbitrary topos, which may or may not be a topological topos, and we are interested in proving things synthetically in topological toposes. \begin{code} {-# OPTIONS --safe --without-K #-} open import UF.FunExt module TypeTopology.SequentiallyHausdorff (feβ : funextβ) where open import CoNaturals.Type open import MLTT.Spartan open import Notation.CanonicalMap open import Taboos.BasicDiscontinuity feβ open import Taboos.WLPO \end{code} A topological space is sequentially Hausdorff if every sequence converges to at most one point. In our synthetic setting, this can be formulated as follows, following the above blog post by Chris Grossack. \begin{code} is-sequentially-Hausdorff : π€ Μ β π€ Μ is-sequentially-Hausdorff X = (f g : ββ β X) β ((n : β) β f (ΞΉ n) οΌ g (ΞΉ n)) β f β οΌ g β \end{code} If WLPO holds in our topos, then our topos is not topological, in any conceivable sense, and no type with two distinct points is sequentially Hausdorff. \begin{code} no-non-trivial-sequentially-Hausdorff-types-under-WLPO : WLPO β (X : π€ Μ ) β has-two-distinct-points X β Β¬ is-sequentially-Hausdorff X no-non-trivial-sequentially-Hausdorff-types-under-WLPO wlpo X ((xβ , xβ), d) X-is-seq-Haus = III where f : ββ β X f u = xβ g' : (u : ββ) β (u οΌ β) + (u β β) β X g' u (inl _) = xβ g' u (inr _) = xβ g : ββ β X g u = g' u (wlpo u) I : (n : β) (c : (ΞΉ n οΌ β) + (ΞΉ n β β)) β g' (ΞΉ n) c οΌ xβ I n (inl e) = π-elim (β-is-not-finite n (e β»ΒΉ)) I n (inr _) = refl a : (n : β) β f (ΞΉ n) οΌ g (ΞΉ n) a n = f (ΞΉ n) οΌβ¨ refl β© xβ οΌβ¨ (I n (wlpo (ΞΉ n)))β»ΒΉ β© g (ΞΉ n) β II : (c : (β οΌ β) + (β β β)) β g' β c οΌ xβ II (inl _) = refl II (inr Ξ½) = π-elim (Ξ½ refl) III : π III = d (xβ οΌβ¨ refl β© f β οΌβ¨ X-is-seq-Haus f g a β© g β οΌβ¨ II (wlpo β) β© xβ β) \end{code} The reason WLPO doesn't hold topological in toposes is that the negation of WLPO is a weak continuity principle [1], which holds in topological toposes. So it makes sense to investigate which sets are sequentially Hausdorff assuming Β¬ WLPO or stronger continuity principles. [1] https://doi.org/10.1017/S096012951300042X To begin with, we show that all totally separated types are sequentially Hausdorff in topological toposes. \begin{code} open import TypeTopology.TotallySeparated open import UF.DiscreteAndSeparated totally-separated-types-are-sequentially-Hausdorff : Β¬ WLPO β (X : π€ Μ ) β is-totally-separated X β is-sequentially-Hausdorff X totally-separated-types-are-sequentially-Hausdorff nwlpo X X-is-ts f g a = II where I : (p : X β π) β p (f β) οΌ p (g β) I p = Iβ where Iβ : (n : β) β p (f (ΞΉ n)) οΌ p (g (ΞΉ n)) Iβ n = ap p (a n) Iβ : p (f β) β p (g β) β WLPO Iβ = disagreement-taboo (p β f) (p β g) Iβ Iβ : Β¬ (p (f β) β p (g β)) Iβ = contrapositive Iβ nwlpo Iβ : p (f β) οΌ p (g β) Iβ = π-is-¬¬-separated (p (f β)) (p (g β)) Iβ II : f β οΌ g β II = X-is-ts I \end{code} There are plenty of totally separated types. For example, the types π, β and ββ are totally separated, and the totally separated types are 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. 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. This is the type βββ = Ξ£ u κ ββ , (u οΌ β β π), which amounts to ββ with the point β split into two copies ββ = (β , Ξ» _ β β), ββ = (β , Ξ» _ β β). \begin{code} open import TypeTopology.FailureOfTotalSeparatedness feβ βββ-is-not-sequentially-Hausdorff : Β¬ is-sequentially-Hausdorff βββ βββ-is-not-sequentially-Hausdorff h = III where 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} The following was already proved in TypeTopology.FailureOfTotalSeparatedness. \begin{code} βββ-is-not-totally-separated-in-topological-toposes : Β¬ WLPO β Β¬ is-totally-separated βββ βββ-is-not-totally-separated-in-topological-toposes nwlpo ts = βββ-is-not-sequentially-Hausdorff (totally-separated-types-are-sequentially-Hausdorff nwlpo βββ ts) \end{code} The proof given here is the same, but factored in two steps, by considering sequentially Hausdorff spaces as an intermediate step.