累积宇宙层级

累积层级像逐层扩大的图书馆：高层阅览室收录低层全部书目，还额外容纳低层目录本身。一本位于 ${\mathcal{U}}_0$ 的书不因被拿到 ${\mathcal{U}}_1$ 使用就变成另一种内容；但两间阅览室绝不是同一个房间。这个区别让用户能自然复用小类型，同时让内核保留阻止自包含悖论所需的尺寸信息。

非累积系统则要求每次跨层明确装箱或 lifting。两种政策都能保持一致，只是在项语法、转换规则和错误信息上承担不同成本。典型歧义和 universe polymorphism 可以隐藏下标，却只是在约束求解后选择合适层级，并没有抹去层级。

设 $\mathsf{Bool}:{\mathcal{U}}_0$、$\mathbb{N}:{\mathcal{U}}_0$。累积性立即允许把两者当作 ${\mathcal{U}}_1$ 中的类型，所以异层依赖对

可在 ${\mathcal{U}}_1$ 中形成：定义域 ${\mathcal{U}}_0$ 本身位于 ${\mathcal{U}}_1$，每个余类型 $A\to {\mathcal{U}}_0$ 也至多需要 ${\mathcal{U}}_1$。具体居民可以取 $(\mathsf{Bool},\lambda \mathrm{\_}.\mathbb{N})$。若一个函数要求参数 $X:{\mathcal{U}}_1$，便可直接传入 $\mathsf{Bool}$；这一步是层级提升，不是证明 $\mathsf{Bool}$ 与 ${\mathcal{U}}_1$ 相等。

反例是从 $A:{\mathcal{U}}_1$ 反推 $A:{\mathcal{U}}_0$。累积关系只有向上方向；一个以 ${\mathcal{U}}_0$ 为元素的“大”类型通常没有低层表示。也不能由 ${\mathcal{U}}_i:{\mathcal{U}}_{i+1}$ 和累积性推出 ${\mathcal{U}}_i:{\mathcal{U}}_i$，因为规则要求起始归属层不高于目标层，不能把 $i+1$ 降为 $i$。若约束生成同时要求 $i<j$ 与 $j\le i$，正确结果是层级不一致，而非悄悄选取无限层。

累积性让大型库免于在每个组合点插入显式 lift。一个对 $A:{\mathcal{U}}_j$ 定义的容器可接收任何 $A:{\mathcal{U}}_i$（$i\le j$）；包含小范畴、模型或语法解释的结构也可逐级上移。实现通常收集不等式约束，再求一个满足所有 $max$、后继和严格不等式的层级赋值；层级多态把这一过程参数化，使同一定义可在多层实例化。

便利也带来元理论义务。转换检查必须决定不同提升路径是否相同，归纳类型的大消去要说明目标宇宙许可范围，resizing 原理则可能把原本只可向上的信息重新压低，因而不是累积性自身的推论。本页的层级政策与集合论的累积层级公理库累积层级Cumulative hierarchy · von Neumann hierarchy · V hierarchy沿序数阶段反复取幂集并在极限阶段取并，组织全部良基集合的层级。只有类比关系：后者按秩构造集合，前者控制类型形成与量化的大小。