泛等范畴

泛等范畴是同伦类型论中提倡的范畴定义, 它把传统意义上的范畴的定义从集合论语言直接翻译到类型论语言后, 再加上了 “同构的对象相等” 的条件, 其中的相等便是同伦类型论的相等类型. 这个条件写出来非常像泛等公理, 这可能也是泛等范畴的名字来源.

泛等范畴的概念弥补了范畴的定义中对象之间的相等关系定义不明确的缺点 (见等价原理) .

1定义

引理 1.1. 对于预范畴 $\mathcal{C}$ 和 $A,B:\mathrm{Ob}(\mathcal{C})$, 存在映射$$id\to iso:{\mathrm{Id}}_{\mathrm{Ob}(\mathcal{C})}(A,B)\to A\simeq B$$其中 $\mathrm{Id}$ 对应相等类型, $\simeq$ 指同构.

定义 1.2. 对于预范畴 $\mathcal{C}$, 如果 $id\to iso$ 是一个等价, 那么称 $\mathcal{C}$ 为一个泛等范畴.

2性质

引理 2.1. 在泛等范畴 $\mathcal{C}$ 中, $\mathrm{Ob}(\mathcal{C})$ 是 $1$-类型 (参见 $n$-类型), 即群胚.

证明. 这本质上是在说对于 $A,B\in \mathrm{Ob}(\mathcal{C})$, 类型 ${\mathrm{Id}}_A(B)$ 是集合. 根据 1.2 我们已经知道它等价于类型 $A\simeq B$, 该类型为集合.

$\square$

预范畴间的函子无需增加条件即可适用于泛等范畴, 它们总是保持 $id\to iso$.

3例子

•	同伦类型论中由集合构成的范畴, 根据泛等公理可知这是一个泛等范畴.

4相关概念

•

预范畴

术语翻译

泛等范畴 • 英文 univalent category