单值类型论中谱格点的补丁局部
Patch Locale of a Spectral Locale in Univalent Type Theory
AI总结：
本文在单值类型论中，不使用重缩放公理，通过预测式重构格点理论基本概念，证明了 Stone 格点构成谱格点的余反射子范畴。
摘要：
Stone 格点与连续映射构成谱格点和完美映射的一个余反射子范畴。第二作者此前在初等拓扑斯的内语言中给出了一个证明。该证明可以借助重缩放公理轻松翻译到单值类型论中。在本工作中，我们展示了如何在不使用重缩放公理的情况下实现这样的翻译，通过使用具有小基的大、局部小、小完备框架。这被证明是非平凡的，并涉及格点理论几个基本概念的预测式重构。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
