集合 (类型论)

在类型论中, 集合是指同伦层级为 $0$ 的类型, 也是 $n$-类型中 $n=0$ 的特例. 也就是元素之间的相等是单纯的命题而不包含复杂数据的类型. 这是集合的类比.

在同伦类型论视角下, 集合对应的是离散的拓扑空间.

在 K 公理成立的类型论中, 所有的类型都是集合.

1定义

定义 1.1. 若 $\Gamma ⊢A$ 是类型, 则它是集合当且仅当它元素上的相等关系是平凡的, 即满足$$\Gamma ⊢\prod _{a,b:A}\prod _{p,q:\mathrm{Id}(a,b)}\mathrm{Id}(p,q)$$

引理 1.2. 如下两命题等价: $$\begin{array}{rl}\mathrm{isSet}(A)& :\prod _{a,b:A}\prod _{p,q:\mathrm{Id}(a,b)}\mathrm{Id}(p,q)\\ \mathrm{isSet}(A)& :\prod _{a,b:A}\mathrm{isProp}(\mathrm{Id}(a,b))\end{array}$$其中 $\mathrm{isProp}$ 定义于命题宇宙.

按照这个定义, 可以像命题宇宙一样定义集合的宇宙, 即 ${\sum }_{A:\mathcal{U}}\mathrm{isSet}A$.

引理 1.3. 若 K 公理成立, 则所有类型都是集合.