累积宇宙塔的存在性定理及其应用

本文构建了一个吉格尔宇宙的累积塔，为高类型论提供精确的大小规范。 从一系列递增的不可测基数开始，我们给出宇宙代码、其解码函子以及控制每个代码增长量的秩的归纳递归定义。 对塔的每个层级，我们证明其在依赖积、依赖和、恒等类型以及所有有限极限和余极限下的封闭性；其中，余极限部分通过秩稳定的商构造获得。 宇宙提升运算显示，在各层级之间严格的累积性。 在一个层级上假设命题调整，在此基础上我们构造了从减一截断类型的包含器的显式左伴随，证明调整自动提升到每个更高层级。 这些构件组合成一个存在性定理，声明在所选不可测基数的 Zermelo-Fraenkel 集合论之上，塔为高类型论提供了一个 sound 的集合论模型。 结果为后续关于 Rezk 完成和高 topos 模型的工作提供了大小基础设施。