一元类型论中谱局部的一个补局部
计算机科学中的逻辑
2023-06-22 v4 一般拓扑
摘要
斯通局部与连续映射一起构成谱局部与完美映射的一个余反射子范畴。第二作者此前在初等拓扑斯的內部语言中给出了一个证明。该证明可借助重整公理轻易翻译到一元类型论中。在这项工作中，我们展示了如何在不使用重整公理的情况下实现这种翻译，即通过处理具有小基的大、局部小和小的完备框架。这被证明是非平凡的，并涉及局部理论若干基本概念的可预测重新表述。
引用
@article{arxiv.2301.04728,
title = {Patch Locale of a Spectral Locale in Univalent Type Theory},
author = {Ayberk Tosun and Martín Hötzel Escardó},
journal= {arXiv preprint arXiv:2301.04728},
year = {2023}
}