Constructive and Predicative Locale Theory in Univalent Foundations

Abstract

We develop locale theory constructively and predicatively in univalent foundations (UF), with a particular focus on the theory of spectral and Stone locales. In the context of UF, predicativity refers specifically to the development of mathematics without the use of propositional resizing axioms. The traditional approach to the predicative development of point-free topology is to work with presentations of locales known as formal topologies. Here, we take a different approach: we work directly with frames, keeping careful track of the universes involved and adopting certain size assumptions to ensure that the theory is amenable to predicative development. Although it initially appears that many fundamental constructions of locale theory rely on impredicativity, we show that these can be circumvented under rather natural size assumptions. We first lay the groundwork for the predicative development of locale theory. We then orient our development towards a systematic investigation of the theory of spectral and Stone locales. We establish a categorical equivalence between large, locally small, and small-complete spectral locales and small distributive lattices. Moreover, we exhibit the category of Stone locales as a coreflective subcategory of spectral locales and spectral maps, using the construction known as the patch locale. Finally, we investigate the topology of algebraic DCPOs and Scott domains. We develop the Scott locale of a Scott domain, show that it forms a spectral locale, and then proceed to investigate its patch. Using this, we obtain a topological characterization of de Jong's notion of sharp element: we establish a correspondence between the sharp elements of a Scott domain and the points of the patch of its Scott locale. Our development is completely formalized and has been machine-checked using the Agda proof assistant.