The Borsuk-Ulam Theorem in Synthetic Stone Duality

Abstract

The recently introduced synthetic Stone duality [1] is an extension of homotopy type theory (HoTT), which is conjecturally modeled in the higher topos of light condensed anima as recently introduced by Clausen and Scholze [2]. As it turns out, synthetic Stone duality turns out to be an appropriate setting in which to develop a restricted form of point-set topology. We survey the development of point-set topology within synthetic Stone duality, recovering a working theory of second countable compact Hausdorff spaces and, in particular, a working interval whose topology is the usual metric topology. Using the interval, we are able to define topological paths and loops, as well as the topological fundamental group, in the standard way. We then turn to the theory of higher modalities in HoTT to relate topological spaces, as developed within synthetic Stone duality, to their homotopy types. After recalling the basics of the theory of higher modalities we are able to define the shape modality as the nullification of the interval. The shape modality, which is conjectured to more generally convert (topological) finite CW complexes to their homotopy types, converts the topological circle 𝕊1 into its higher inductive counterpart 𝑆1. Using shape, we are able to pass back and forth between reasoning about the topological and homotopical circle as convenient. As an application, we use the shape modality to provide a characterization of ℝ, long known as folklore, in terms of the modal unit 𝜂 : 𝕊1 → 𝑆1 for the topological circle. Similarly using the shape modality, we are able to show that topological paths in 𝕊1 lift through the standard covering map ℝ ↠ 𝕊1 while bypassing the standard covering space theory, and prove the two-dimensional Borsuk-Ulam theorem as an application.