2024/02/05 by Igor Arrieta, Arrieta, Igor, Martı́n Hötzel Escardó +3
Mathematics · #03F65 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Rings, Modules, and Algebras
paper · pdf · doi:10.48550/arxiv.2402.03134
openalex publication_date 2024/02/05 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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 and locally small frames with small bases. This requires predicative reformulations of several fundamental concepts of locale theory in predicative HoTT/UF, which we investigate systematically.