相等类型

在 Martin-Löf 类型论中, 相等类型是表示相等关系的类型, 记作 ${\mathrm{Id}}_A(a,b)$, 其中 $a:A$ 且 $b:A$, 当 $A$ 显然时可以省略.

若存在 $p:{\mathrm{Id}}_A(a,b)$ 则称 $a,b$ 两者命题相等.

部分文献中, 也记作 $a{=}_{A}b$, 但这个记号很容易和其它的等价关系尤其是类型论内置的值相等混淆.

1类型规则

$$\frac{\Gamma ⊢a:A\Gamma ⊢b:A}{\Gamma ⊢{\mathrm{Id}}_A(a,b)}$$

构造规则

该规则反映了相等类型满足的自反性.

$$\frac{\Gamma ⊢x:A}{\Gamma ⊢{\mathrm{refl}}_x:{\mathrm{Id}}_A(x,x)}$$

消去规则

参见: J 公理; K 公理; 外延类型论

J 公理为相等类型带来了非常丰富的语义, 例如它使得类型可以解释为群胚或者$\infty$-群胚. 而 K 公理则认为相等类型不包含多余的信息, 使得类型的性质更接近集合.

2性质

参见: J 公理; K 公理

相等类型有多种消去规则, 它们可以给出不一样的推论.

3范畴语义

若将类型解释为某种群胚, 那么相等类型就是里面的态射.

Yoneda 引理

因此, 相等类型给出了一种类型论版本的 Yoneda 嵌入, 这不仅在有 K 公理的情况下成立, 而且对同伦类型论里面的$n$-类型也成立. 为了叙述该嵌入, 需要使用$\Sigma$ 类型.

定义 3.1 (Yoneda 嵌入). 对于类型 $\Gamma ⊢A$, 可以将相等类型写作如下形式: $${\mathrm{Id}}_A:A\to (A\to \mathcal{U})$$这是一种 Yoneda 嵌入. 注意: 这里的 $\to$ 不是指 ${\mathrm{Id}}_A$ 是一个函数, 而是说这个类型本身里含有两个变量, 对它应用参数的时候, 不是在像函数应用一样对它进行消去, 而是在对它的参数进行指定. 符号上更严谨但比较繁琐的说法是, 对于 $a:A$, 它的 Yoneda 嵌入将其映射到如下类型: $$\sum _{b:A}{\mathrm{Id}}_A(a,b)$$

它对应的的 Yoneda 引理叙述如下:

引理 3.2 (Yoneda 引理). (承接 3.1 中的变量名) 对于任何 $a:A$, 类型$$\sum _{b:A}{\mathrm{Id}}_A(a,b)$$都只有唯一实例.

这样的话, 关于类型的论证就可以和关于值的论证互相转化了. 该引理被用在了泛等公理蕴涵函数外延性的证明上.

例 3.3. 令 $A:\mathcal{U}$ 为集合, 换言之, 该类型上的相等类型是命题, 即$${\mathrm{Id}}_A:A\to (A\to \mathrm{Prop})$$那么对于 $a:A$, 它的嵌入 ${\mathrm{Id}}_A(a,-)$ 显然只有唯一实例.

这个例子较为平凡, 暂时还不太能看出和范畴论中的 Yoneda 引理的关系, 因为它里面不涉及任何可以类比常见范畴的数学对象, 但下一个就不同了.

例 3.4. 令 $A:\mathcal{U}$ 为 $1$-类型, 换言之, 该类型上的相等类型是集合 (类型论), 即$${\mathrm{Id}}_A(x,-):A\to \mathrm{Set}$$在同伦类型论的视角下, 该类型是一个群胚, 也就是满足 $A^{op}=A$ 的范畴. 考虑另一种常见的 Yoneda 嵌入 (态射函子), 它的类型如下: $$A(-,x):A^{op}\to \mathrm{Set}$$根据群胚的性质可知它的类型也可以写作 $A\to \mathrm{Set}$, 和前面用相等类型给出的版本一致, 且两者的性质确实是相同的.

该引理可以推广到同伦层级更高的范畴.

4变种

参见: 观测类型论; 立方类型论

相等类型的规则无法推出函数外延性是 Martin-Löf 类型论和构造演算作为数学的基础的一大缺憾, 而为了从根源上解决这个问题 (而不是将该命题作为公理引入), 只能将相等类型本身的定义替换掉, 引入更底层的构造规则和消去规则, 再将自反性和 J 规则作为新的相等类型的定理证明出来.

观测类型论和立方类型论都做了这样的事, 并且都蕴涵函数类型的外延性.

异质相等

异质相等类型又叫 John Major 相等类型指如下类型:

$$\frac{\Gamma ⊢a:A\Gamma ⊢b:B}{\Gamma ⊢{\mathrm{JM}}_{A,B}(a,b)}$$

它也使用自反性作为唯一的构造规则.

为了与正常的相等类型区分, 相等类型也称为同质相等类型. 它的构造规则也是用自反性定义, 即 ${\mathrm{refl}}_{A,a}:{\mathrm{JM}}_{A,A}(a,a)$. 该类型有两种消去规则. 一种与 J 公理类似:

$$\begin{array}{rl}& \Gamma ⊢A:\mathcal{U}\Gamma ⊢x:A\\ & \Gamma ⊢P:{\Pi }_{x:A}{\Pi }_{y:B}{\mathrm{JM}}_{A,B}(x,y)\to \mathcal{U}\\ & \Gamma ⊢p:{\Pi }_{x:A}P(x,x,{\mathrm{refl}}_x)\\ & \Gamma ⊢q:{\mathrm{JM}}_{A,B}(x,y)\\ & \\ & \overline{\Gamma ⊢J(P,p,q):P(x,y,q)}\end{array}$$

这个规则蕴涵 K 公理. 另一种消去规则更弱 (需要额外提供类型 $A,B$ 之间的相等), 但是不蕴涵 K 公理, 使用这个消去规则时异质相等 ${\mathrm{JM}}_{A,B}(a,b)$ 完全与同质相等 ${\mathrm{Id}}_{{\Sigma }_{A:\mathcal{U}}A}(⟨A,a⟩,⟨B,b⟩)$ 等价.

术语翻译

相等类型 • 英文 identity type • 日文 同一視型

命题相等 (名词) • 英文 propositional equality

异质 • 英文 heterogeneous