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 中对局部格理论的若干基本概念进行可预测性重构，我们对此进行了系统研究。