Grothendieck拓扑斯的严格宇宙
Strict universes for Grothendieck topoi
AI总结：
该研究调整Shulman的论证，在任意Grothendieck拓扑斯中构造出满足重排性质的累积宇宙层级，实现带累积宇宙的Martin-Löf类型论的直接解释，并拓展了相关合成方法的适用范围。
摘要：
Hofmann和Streicher的著名成果展示了如何将Grothendieck宇宙提升到预层拓扑斯中，Streicher又通过层化（sheafification）将该结果推广到层拓扑斯的情形。与此同时，van den Berg和Moerdijk在代数集合论的语境下证明，即使在更弱的元理论中，类似的构造依然适用。遗憾的是，层化似乎无法保持预层宇宙所具有的一项重要的重排性质，该性质在单值类型论模型以及合成泰特可计算性（synthetic Tait computability，一种新近用于确立类型论与程序语言句法性质的技术）中发挥着关键作用。在多宇宙语境下，重排性质还意味着每个宇宙层级的联结词编码具有一致选择，从而可以解释Martin-Löf类型论主流表述中存在的累积性规则。\n我们发现，对Shulman的一个论证稍加调整，就能在任意Grothendieck拓扑斯中构造出在每个层级都满足重排性质的累积宇宙层级。由此，带累积宇宙的Martin-Löf类型论可以直接风格地解释到所有Grothendieck拓扑斯中。进一步的推论是，将立方类型论语义学以及类型论与程序语言句法学元理论中近期合成方法的适用范围拓展到了所有Grothendieck拓扑斯。
英文摘要：
Hofmann and Streicher famously showed how to lift Grothendieck universes into presheaf topoi, and Streicher has extended their result to the case of sheaf topoi by sheafification. In parallel, van den Berg and Moerdijk have shown in the context of algebraic set theory that similar constructions continue to apply even in weaker metatheories. Unfortunately, sheafification seems not to preserve an important realignment property enjoyed by the presheaf universes that plays a critical role in models of univalent type theory as well as synthetic Tait computability, a recent technique to establish syntactic properties of type theories and programming languages. In the context of multiple universes, the realignment property also implies a coherent choice of codes for connectives at each universe level, thereby interpreting the cumulativity laws present in popular formulations of Martin-Löf type theory. We observe that a slight adjustment to an argument of Shulman constructs a cumulative universe hierarchy satisfying the realignment property at every level in any Grothendieck topos. Hence one has direct-style interpretations of Martin-Löf type theory with cumulative universes into all Grothendieck topoi. A further implication is to extend the reach of recent synthetic methods in the semantics of cubical type theory and the syntactic metatheory of type theory and programming languages to all Grothendieck topoi.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
