A Foundation for Synthetic Stone Duality

Abstract

The language of homotopy type theory has proved to be an appropriate internal language for various higher toposes, for example for the Zariski topos in Synthetic Algebraic Geometry. This paper aims to do the same for the higher topos of light condensed anima of Dustin Clausen and Peter Scholze. This seems to be an appropriate setting for synthetic topology in the style of Martín Escardó.
We use homotopy type theory extended with 4 axioms. We prove Markov’s principle, LLPO and the negation of WLPO. Then we define a type of open propositions, inducing a topology on any type such that any map is continuous. We give a synthetic definition of second countable Stone and compact Hausdorff spaces, and show that their induced topologies are as expected. This means that any map from e.g. the unit interval 𝕀 to itself is continuous in the usual epsilon-delta sense.
With the usual definition of cohomology in homotopy type theory, we show that H¹(S,ℤ) = 0 for S Stone and that H¹(X,ℤ) for X compact Hausdorff can be computed using Čech cohomology. We use this to prove H¹(𝕀¹,ℤ) = 0 and H¹(𝕊¹,ℤ) = ℤ where 𝕊¹ is the set ℝ/ℤ. As an application, we give a synthetic proof of Brouwer’s fixed-point theorem.