Patch Locale of a Spectral Locale in Univalent Type Theory

TL;DR

This paper demonstrates how to translate a proof about spectral locales from topos theory into univalent type theory without resizing axioms, using predicative reformulations of locale concepts.

Contribution

It provides a novel method to formalize locale theory in univalent type theory without relying on resizing axioms, expanding the foundational tools available.

Findings

Successfully translated the proof without resizing axioms

Developed predicative reformulations of locale concepts

Extended the formalization framework for locale theory

Abstract

Stone locales together with continuous maps form a coreflective subcategory of spectral locales and perfect maps. A proof in the internal language of an elementary topos was previously given by the second-named author. This proof can be easily translated to univalent type theory using resizing axioms. In this work, we show how to achieve such a translation without resizing axioms, by working with large, locally small, and small complete frames with small bases. This turns out to be nontrivial and involves predicative reformulations of several fundamental concepts of locale theory.