范畴语义

类型论的范畴语义是指一类在范畴论中的构造, 使得类型论中的研究对象如类型、值、各种规则可以被解释为某些态射, 并且至少需要满足类型论中相等的值在解释后得到的态射也相等.

关于范畴语义的研究一般归类于范畴逻辑.

1基本思想

简单类型

参见: Curry–Howard–Lambek 对应

简单类型 $\lambda$ 演算里的值可以解释为积闭范畴里的态射. 在这个视角下, 积闭范畴里的对象对应了类型.

依值类型

假设存在一个由语境为对象、替换操作为态射的范畴 $\mathsf{Ctx}$, 这往往也是类型论的句法范畴. 这个范畴本身并不能直接讨论类型 (只能讨论语境之间的操作) , 因此需要单独构造依值类型的解释. 考虑依值类型 $\Gamma ⊢A$, 这意味着如下事实:

•	$\Gamma \in \mathrm{Ob}(\mathsf{Ctx})$, 这是前提.

•	存在合法的语境 $\boxed{\Gamma ,A}\in \mathrm{Ob}(\mathsf{Ctx})$, 这个过程叫做语境的延伸, 也就是给现存的语境加上一个类型.

•	如果有一组语境之间的替换 $\sigma \in \mathsf{Ctx}(\Delta ,\Gamma )$, 那么 $A$ 可以被 $\sigma$ 替换为 $\Delta ⊢A\sigma$ 这个新的类型.

那么定义依值类型本身就显然需要在 $\Gamma$、$\boxed{\Gamma ,A}$ 这两个对象上做文章, 而最适合的定义便是一种态射 ${\pi }_A\in \mathsf{Ctx}(\boxed{\Gamma ,A},\Gamma )$, 它对应着类型论中 “将 $\Gamma$ 里的变量原封不动输出, 扔掉最后的 $A$ 类型的实例” 的一种替换. 这个态射又叫形式丛, 见形式丛范畴. 很显然对于每个依值类型都能定义出这样的态射, 且这个定义有如下好处:

•	这个态射本身包含了类型所在的语境 $\Gamma$ 的信息.

•	类型 $A$ 的实例 $\Gamma ⊢a:A$ 可以编码为替换 $\Gamma ⊢\boxed{1_{\Gamma },a}:\boxed{\Gamma ,A}$, 其中 $1_{\Gamma },a$ 代表 “对 $\Gamma$ 里的变量什么都不做, 但在最后加上一个 $A$ 类型的实例 $a$” 的替换, 很显然所有 $A$ 的实例都可以定义出这样的态射, 而且这样的态射正好都是 ${\pi }_A$ 的右逆元.

•	直接要求 ${\pi }_A$ 和任意态射都能取拉回, 就给出了类型上的替换操作.

定义 1.1. 若 $\mathsf{Ctx}$ 中的每个对象都可以表示为空语境的解释或者某个语境进行延申操作的结果, 那么该范畴满足语境性.

可以粗略地认为满足语境性的含族范畴就是 C 系统.

定义 1.2. 令 $1\in \mathrm{Ob}(\mathsf{Ctx})$ 表示空语境的解释. 若 $\mathsf{Ctx}$ 中的每个对象都和某个可以写作 $\boxed{1,A}\in \mathrm{Ob}(\mathsf{Ctx})$ 的语境同构 (其中 $A$ 是任意类型), 那么该范畴语义满足民主性.

引理 1.3. 若类型论存在 $\Sigma$ 类型且范畴语义满足语境性, 则该范畴语义是民主的.

同伦类型论

2例子

对于简单类型的情况, 积闭范畴已经最合适的范畴语义了, 因此只有依值类型论才拥有丰富的语义模型:

•	C 系统
•	含族范畴
•	概括范畴
•	形式丛范畴

但这些具体的构造在讨论语境和替换操作的解释时, 都非常类似 依值类型 中的描述. 另外局部积闭范畴也能解释依值类型论, 但这个构造不是专门为解释依值类型论而设计的.

(.. 同伦类型论)

3始模型猜想

以后可以移动到单独的词条

范畴语义一般自身就是一个范畴, 而对于同一个类型论, 可能存在多个这样的范畴, 这些范畴间可能存在保持类型论中的研究对象的解释的函子, 于是这些作为语义的范畴又形成一个更大的范畴. 这个更大的范畴中的始对象就非常接近类型论的句法范畴.

始模型猜想的内容就是 “类型论的句法范畴就是这个更大的范畴中的始对象”. 很明显, 对于任何具体的类型论都有它自己的始模型猜想, 在 1978 年由 John Cartmell 借助 C 系统证明 Martin-Löf 类型论的版本, 1991 年由 Thomas Streicher 证明构造演算的版本, 2019 年由 Guillaume Brunerie、Peter LeFanu Lumsdaine 等人给出一个在计算机中形式化、且较为模块化的证明, 降低了始模型猜想的证明拓展到新的类型论的难度.

术语翻译

范畴语义 • 英文 categorical semantics

始模型猜想 • 英文 initiality conjecture

语境性 • 英文 contextuality

形式丛 • 英文 display map

民主性 • 英文 democracy