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.

翻译：Stone 局部格与连续映射构成谱局部格和完美映射的一个核心反射子范畴。第二作者此前已给出一个在基本拓扑斯内语言中的证明。该证明可借助尺寸调整公理轻松转换为单值类型论。在本工作中，我们展示如何在不依赖尺寸调整公理的情况下实现这种转换，通过处理具有小基的大局部格和局部小局部格。这需要对预测性 HoTT/UF 中局部格理论的若干基本概念进行预测性重构，我们对此进行了系统性研究。