预范畴

预范畴是同伦类型论中对传统意义上的范畴的直接翻译, 它把对象的集合换成类型 (或者说$\infty$-群胚) , 把态射的集合换成同伦类型论中的集合.

1定义

定义 1.1. 预范畴 $\mathcal{C}$ 由下列信息组成:

•	一个类型 $\mathrm{Ob}(\mathcal{C})$, 其实例对应 $\mathcal{C}$ 的对象.

•	对任意 $A,B:\mathrm{Ob}(\mathcal{C})$, 有一个集合 $\mathcal{C}(A,B)$, 其实例对应从 $x$ 到 $y$ 的态射.

•	对于 $A,B,C:\mathrm{Ob}(\mathcal{C})$, 有二元函数$${\circ }_{A,B,C}:\mathcal{C}(A,B)\to \mathcal{C}(B,C)\to \mathcal{C}(A,C)$$对应态射的复合.

•	对于 $A:\mathrm{Ob}(\mathcal{C})$, 有态射$$1_A\in \mathcal{C}(A,A),$$对应 $A$ 的恒同态射.

其中复合操作和恒同态射需要满足类似范畴的定义中的单位律和结合律.

2例子

传统范畴论中的范畴中, 如果对象的类能用同伦类型论中的类型定义, 那么直接翻译得到的范畴就是一个预范畴.

在有宇宙 $\mathcal{U}$ 的类型论中, 以类型 $\mathcal{U}$ 为对象, 函数类型的 $1$-截断为态射, 可以得到一个预范畴, 该范畴叫类型的同伦预范畴.

3相关概念

•	泛等范畴
•	Rezk 完备化

术语翻译

预范畴 • 英文 precategory • 法文 précatégorie • 拉丁文 praecategoria