宇宙类型

没有宇宙时，类型只出现在判断的右侧，程序不能接收“一个类型”再返回以它为参数的结构。宇宙像经过尺寸分区的类型目录：${\mathcal{U}}_i$ 列出第 $i$ 层允许谈论的小类型，而目录本身太大，必须放进更高层 ${\mathcal{U}}_{i+1}$。这样既可写多态程序，又不让目录把自己作为普通条目吞进去。

“小”不是元素个数少，而是相对于当前宇宙层级可编码。自然数、有限类型、由小类型形成的 Π/Σ 往往仍小；${\mathcal{U}}_i$ 自己相对于本层则是大类型。层级因此承担逻辑防火墙的角色，也为实现中的 universe constraint 留出精确含义。

多态恒等函数可写成

由于量化变量 $A$ 的定义域是 ${\mathcal{U}}_0:{\mathcal{U}}_1$，整个 Π 类型一般位于 ${\mathcal{U}}_1$，而不是仍在 ${\mathcal{U}}_0$。实例化给出

只要 $\mathsf{Bool}:{\mathcal{U}}_0$。这个推导展示宇宙的实际用途：$A$ 在项位置被传入，随后又在余类型中充当类型。

核心禁区是 $\mathcal{U}:\mathcal{U}$。把包含自身、并对依赖函数封闭的宇宙与足够强的类型构造结合，会触发 Girard 悖论；因此不能为了省略层级而把 ${\mathcal{U}}_i:{\mathcal{U}}_i$ 写成 harmless shorthand。层级多态可以让源码省略具体下标，但内核仍要生成并求解 $i<j$ 或 $max(i,j)$ 等约束。宇宙也不是集合论的冯·诺伊曼累积层级：两者都有分层思想，元素关系、相等概念和闭包规则却不同。

宇宙使泛型库、类型族和内部化语义成为可能。容器可按 $A:{\mathcal{U}}_i$ 参数化，解释器可把语法代码映到 ${\mathcal{U}}_i$ 中的意义，较高宇宙还能容纳“小类型范畴”一类整体结构。证明助理据此检查用户定义究竟是 universe-polymorphic，还是只在某个固定层可用；错误的层级约束会在形成类型时暴露，而非演化成逻辑矛盾。

宇宙本身不决定累积性、不可达基数式闭包、命题宇宙或 resizing 原理。非累积系统可要求显式 lifting；累积系统可允许低层类型在高层重用；Tarski 系统可能把 lifting 表示为代码函数。每种扩展都改变 formation 与 conversion 的细节，相关正规化和一致性结论必须针对选定规则重新建立。