Constructive and predicative locale theory in univalent foundations

Tosun, Ayberk ORCID: 0000-0002-0190-3020 (2025). Constructive and predicative locale theory in univalent foundations. University of Birmingham. Ph.D.

Preview

Tosun2025PhD.pdf
Text - Accepted Version
Available under License All rights reserved.
Download (1MB) | Preview

Abstract

We develop locale theory constructively and predicatively in univalent foundations (also known as homotopy type theory or HoTT/UF), with a particular focus on the theory of spectral and Stone locales. The constructivity of our foundational setting means that we do not use any classical principles such as the axiom of choice (or any of its weaker forms), the law of excluded middle, or any form of the limited principle of omniscience. In the context of univalent foundations, predicativity refers specifically to the development of mathematics without the use of Voevodsky’s 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 and locales, 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. Our development here is inspired by de Jong and Escardó’s constructive and predicative development of domain theory in univalent foundations.

We first lay the groundwork for the predicative development of locale theory. We then orient this towards an investigation of the theory of spectral and Stone locales, using the univalence axiom and the set replacement principle to ensure a predicatively well-behaved notion of spectral locale. We also develop Stone duality in the context of spectral locales, showing that there is a categorical equivalence between the type of large, locally small, and small-complete spectral locales and the type of small distributive lattices. Moreover, we exhibit the category of Stone locales as a coreflective subcategory of the category of spectral locales and spectral maps, using the construction known as the patch locale of a spectral locale (the localic manifestation of the so-called constructible topology). Finally, we investigate the topology of algebraic DCPOs and Scott domains in this constructive and predicative framework for locale theory. 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.

Type of Work:

Thesis (Doctorates > Ph.D.)

Award Type:

Doctorates > Ph.D.

Supervisor(s):