Grothendieck 拓扑中的严格宇宙

Hofmann 与 Streicher 著名地展示了如何将 Grothendieck 宇宙提升入预层拓扑，且 Streicher 已通过层化将其结果推广到层拓扑的情形。与此同时，van den Berg 与 Moerdijk 在代数集合论背景下表明，即便在更弱的元理论中类似构造仍继续适用。遗憾的是，层化似乎不保持预层宇宙所享有的一个重要重整性质，而该性质在单值类型论模型以及合成 Tait 可计算性（一种近期用于确立类型论与编程语言语法性质的技术）中起着关键作用。在多宇宙情形下，重整性质还意味着在每个宇宙层级上连贯地选择联结词的编码，从而解释流行 Martin-Löf 类型论表述中存在的累积律。我们观察到，对 Shulman 论证的轻微调整可在任意 Grothendieck 拓扑中构造出在每个层级均满足重整性质的累积宇宙层级。因此，人们可将带累积宇宙的 Martin-Löf 类型论直接式地解释入所有 Grothendieck 拓扑。进一步的推论是将近期立方类型论语义以及类型论与编程语言语法元理论中的合成方法的应用范围扩展到所有 Grothendieck 拓扑。