Categorical Logic and Type Theory

Categorical Logic and Type Theory (中译范畴逻辑与类型论) 是 Bart Jacobs 写的一本关于范畴逻辑和类型论的范畴语义的书.

1内容

•	第 0 章给出了本书的动机, 大致解释了各种类型论的变种, 指出纤维范畴, 初等意象和范畴语义的重要性. 该章节指出, 逻辑总是建立在类型论之上, 而类型论也可以在 Curry–Howard 对应的视角下建立在逻辑之上. 该章节定义了谓词范畴, 二元谓词范畴等构造并介绍相关的纤维范畴和伴随函子.

•	第 1 章从族纤维化作为例子引入了纤维范畴的定义, 介绍了集合范畴, $\omega$-集的范畴之间的各种函子.

•	第 2 章给出了简单类型 $\lambda$ 演算和单一类型 $\lambda$ 演算的范畴语义.

(...)

2部分定义

书中定义了许多奇特的概念, 以下列出一些.

如有必要, 可以单开词条.

定义 2.1. 对于含有积的范畴 $B$, 定义范畴 $s(B)$:

•	对象为 $B$ 中对象的二元组 $⟨I,X⟩$.

•	态射为 $B$ 中的态射 $⟨u,f⟩\in s(B)(⟨I,X⟩,⟨J,Y⟩)$, 其中 $u\in B(I,J)$, $f\in B(I\times X,Y)$.

•	态射复合由显然的组合给出.

定义 2.2. 如下遗忘函子 $s(B)$ 叫做简单纤维化: $$\begin{array}{rl}s(B)& \to B\\ ⟨I,X⟩& \mapsto I\\ ⟨u,f⟩& \mapsto u\end{array}$$容易验证这是一个纤维范畴.

定义 2.3. 对于范畴 $B$ 和 $T\subset \mathrm{Ob}B$, 二元组 $⟨B,T⟩$ 叫做一个语境–类型结构. 语境–类型结构之间的态射 $⟨B,T⟩\to ⟨A,S⟩$ 由满足如下条件的函子 $K:B\to A$ 组成:

•

保持有限积, 且

•	$X\in T⟹K(X)\in S$.

定义 2.4. 语境–类型结构 $⟨B,T⟩$ 满足如下条件时是非平凡的: 至少对于一个对象 $X\in T$ 存在 $u\in B(1,X)$, 其中 $1$ 是终对象.

非平凡的语境–类型结构类比为闭语境中有类型的类型论. 若 $T$ 是单点集合, 那么该语境–类型结构对应单一类型 $\lambda$ 演算.

如下定义将 2.3 和 2.1 联系起来.

定义 2.5. 对于语境–类型结构 $⟨B,T⟩$, 定义其上的简单纤维化 $s(T)$ 为 $s(B)$ 的全子范畴, 要求对象 $⟨I,X⟩$ 满足 $X\in T$.