Constructive and Predicative Locale Theory in Univalent Foundations

TL;DR

This paper develops a constructive and predicative approach to locale theory within univalent foundations, focusing on spectral and Stone locales, and formalizes the entire development in Agda.

Contribution

It introduces a predicative framework for locale theory in UF, avoiding impredicativity, and establishes categorical equivalences and topological characterizations within this setting.

Findings

Categorical equivalence between spectral locales and distributive lattices

Stone locales form a coreflective subcategory of spectral locales

Scott locale of a Scott domain is spectral and its patch characterizes sharp elements

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.