宇宙 (类型论)

依值类型论中的宇宙在思想上类似于 “类型的类型”, 一般记作 $\mathcal{U}$. 为了规避 Russell 悖论, 宇宙不能直接定义为 “所有类型的类型”, 否则它就会成为它自己的类型 ($\mathcal{U}:\mathcal{U}$).

宇宙可以视为 Grothendieck 宇宙在类型论中的类比.

1定义

最简单的方案是, 对于类型 $X$, 直接允许相继式 $\Gamma ⊢X:\mathcal{U}$. 更加谨慎的方案是认为 $\mathcal{U}$ 的元素仅仅是表示类型的符号, 并不等同于类型本身. 为了区分, 这里使用 $\mathtt{X}$ 表示类型的符号, $X$ 表示真正的类型.

定义 1.1 (Russell 宇宙). 若 $X:\mathcal{U}$ 为类型本身, 比如对于类型 $\mathbb{N}$ 同时有 $0:\mathbb{N}$ 和 $\mathbb{N}:\mathcal{U}$, 那么该宇宙叫做 Russell 宇宙.

定义 1.2 (Tarski 宇宙). 若 $\mathtt{X}:\mathcal{U}$ 为类型的表示, 对应的类型则记作 $\mathrm{el}(\mathtt{X})$, 比如有 $0:\mathrm{el}(\mathbb{N})$ 和 $\mathbb{N}:\mathcal{U}$, 那么该宇宙叫做 Tarski 宇宙. [Martin-Löf–Sambin 1984]

定义 1.3 (Coquand 宇宙). 若在 Tarski 宇宙的基础上, 对于一个类型 $X$ 有反向的操作 $R(X):\mathcal{U}$ 得到它的表示, 则称其为 Coquand 宇宙. 有时候 Coquand 宇宙也被归类为 Tarski 宇宙的变体. [Kovács 2021]

在强调某个 Tarski 宇宙不支持 Coquand 宇宙的 $R$ 操作时, 可以称该宇宙为弱 Tarski 宇宙.

在定义类型论的语义时, Tarski (或 Coquand) 式宇宙有显著的优点, 比如可以将类型解释为它的实例的集合, 而宇宙 $\mathcal{U}$ 也不过是一个类型而已, 它的每个实例都有一个对应的集合, 就不需要说 $\mathcal{U}$ 的实例都是集合. 但它无疑也使得关于类型和宇宙的记号变得啰嗦, 因此在讨论类型论的宇宙时, 一般使用 Russell 宇宙的写法, 并假定它会被解释成 Tarski (或 Coquand) 宇宙的形式.

Coquand 类型规则

根据定义 1.3, 可以写下宇宙作为一个类型的规则:

$$\Gamma ⊢\mathcal{U}$$

构造规则:

$$\frac{\Gamma ⊢A}{\Gamma ⊢R(A):\mathcal{U}}$$

消去规则:

$$\frac{\Gamma ⊢\mathtt{A}:\mathcal{U}}{\Gamma ⊢\mathrm{el}(\mathtt{A})}$$

计算规则:

$$\begin{array}{rl}R(\mathrm{el}(\mathtt{A}))& =\mathtt{A}\\ \mathrm{el}(R(A))& =A:\mathcal{U}\end{array}$$

层级

以上两个定义都没有考虑 $\mathcal{U}$ 本身的类型, 处理这个问题有两种方法:

•	让 $\mathcal{U}$ 这个表达式没有类型. 这样, F 系统里的构造就不能使用了, 因此这是一个有效但消极的做法.

•	引入宇宙层级, 即给宇宙加上一个自然数下标, 例如 ${\mathcal{U}}_0,{\mathcal{U}}_1$, 以此类推, 并且令 ${\mathcal{U}}_i$ 的类型为 ${\mathcal{U}}_{i+1}$.

有了宇宙层级之后, 就需要处理以下规则的层级$$\frac{A:{\mathcal{U}}_{i}B:{\mathcal{U}}_j}{A\to B:{\mathcal{U}}_{?}}$$在构造演算中, 选择的是 $?=j$. 构造演算只有两个宇宙层级 $i\in \{0,1\}$. 这个选择下如果允许第三个宇宙层级, 就会出现 Girard 悖论. 因此 $?$ 需要同时不小于 $i$ 和 $j$. 最自然的选择是 $\max \{i,j\}$, 注意这里的自然数都是元语言中的自然数, 与类型论本身的自然数没有必然关系. 可以看作是为每个 $i,j$ 分别添加了一条规则.

除此之外, 宇宙层级还有一个很重要的性质, 即对于 $i<j$ 都存在一个 “提升” 操作 ${\mathcal{U}}_i\to {\mathcal{U}}_j$. 如果这个提升操作不需要显式写出来, 那么类型的规则就会变成一种子类型:

$$\frac{\Gamma ⊢X:{\mathcal{U}}_{i}i\le j}{\Gamma ⊢X:{\mathcal{U}}_j}$$

这种情况下宇宙被称为 (隐式) 累积的.

注 1.4. 一般的子类型对类型论整体的性质有很大的破坏性, 但隐式累积的宇宙是相对保守的: 它仅仅使得类型的具体层级变得不确定, 而不会引入过多的不确定性.

2宇宙多态

显然需要单独的词条

在有宇宙层级的情况下, 定义数学对象会变得不方便, 例如 ${\mathcal{U}}_0,{\mathcal{U}}_1$ 这两个不同宇宙内的类型上的群结构就变成了不同的定义了, 但我们显然希望能只验证一遍群论的定理就将它推广到任意宇宙层级.

为了方便起见, 出现了多种机制来简化这些相同但属于不同宇宙的定义.

(...)

3相关概念

•	泛等公理
•	同伦层级
•	命题宇宙
•	宇宙可以视为对类型判断的内化.

4参考文献

•	András Kovács (2021). “Generalized Universe Hierarchies and First-Class Universe Levels”. (doi) (web)
•	Per Martin-Löf, Giovanni Sambin (1984). Intuitionistic type theory, vol. 9. Bibliopolis Naples.

术语翻译

宇宙 • 英文 universe

宇宙层级 • 英文 universe hierarchy

宇宙多态 • 英文 universe polymorphism

累积 • 英文 cumulative