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.

翻译：Stone场所与连续映射构成谱场所与完美映射的一个余反射子范畴。第二作者先前在基本拓扑斯的内语言中给出了一个证明。该证明可利用重缩放公理轻松转换为单值类型论。在本文中，我们展示如何在不使用重缩放公理的情况下实现这种转换——通过处理具有小基的大、局部小及小完备框架。这一过程颇具挑战性，涉及对场所论若干基本概念进行谓词性重构。