概括范畴

概括范畴是一种典型的依值类型论的范畴语义, 它在纤维范畴的基础上加入了一些条件来定义类型论中的依值类型. 它的意义在于建立一个范畴来解释类型论里的类型规则, 并用于证明类型论的性质.

1定义

首先, 记 $C^I$ 为 $C$ 的箭头范畴, 于是 $C^I$ 中的对象便是 $C$ 中的箭头. 令 $\mathrm{cod}:C^I\to C$ 为将 $C$ 中的态射 $f\in C(a,b)$ 映射到 $b$ 的函子.

注意: 下面的定义是纯粹的范畴论定义, 在解释类型论时, 需要加上严格的条件.

定义 1.1. 对于范畴 $E,C$, 函子 $p:E\to C^I$ 在满足如下条件时, 叫做概括:

•	$\mathrm{cod}\circ p:E\to C$ 是纤维范畴, 它也叫概括范畴. 为了便于定义下一条性质, 记 $f:=\mathrm{cod}\circ p$.

•	$p$ 将 $f$-拉回发送到 $C$ 中的拉回, 也就是 $C^I$ 中的 $\mathrm{cod}$-拉回. 换言之, $p$ 保持态射的 “纤维范畴-拉回” 性质.

其中, $E$ 是解释类型用的范畴, $C$ 是语境构成的范畴.

$E$ 中的对象被 $p$ 发送到 $C^I$ 中的过程, 就对应了依值类型 $A$ 被发送到它们所对应的态射 ${\pi }_A$ 的过程. 这样的定义认为类型本身是独立存在的对象, 只是它们可以被嵌入到语境的范畴里. 直接使用 ${\pi }_A$ 定义类型也是可行的.

相关定义

定义 1.2. 如果概括范畴是全忠实函子, 那么 $p$ 也叫满概括范畴.

定义 1.3. 如果概括范畴是分裂纤维化, 那么 $p$ 也叫分裂概括范畴.

分裂概括范畴就是能准确解释类型论的范畴语义.

2性质

引理 2.1. 如果 $\mathrm{cod}$ 也是纤维范畴 (也就是说 $C$ 包含所有的拉回) , 那么这个对应的类型论将会拥有外延相等类型, 该类型由 $C$ 中的等子给出.

3相关概念

•	纤维范畴
•	依值类型论

4参考资料

•	Bart Jacobs (2001). “Categorical Logic and Type Theory”. Studia Logica 69 (3), 429–431. (doi) (pdf)

术语翻译

概括范畴 • 英文 comprehension category