相等类型

在 Martin-Löf 类型论中, 相等类型是类型中某两个实例间所有相等关系构成的类型, 记作$${\mathrm{Id}}_A(a,b)\text{或}a{=}_{A}b,$$其中 $a:A$ 且 $b:A$, 当 $A$ 显然时也可将其从记号中略去. 若存在 $p:{\mathrm{Id}}_A(a,b)$, 则称 $a,b$ 两者命题相等.

相等类型大致可以视为 “相等关系 $a=b$ 的所有不同证明” 构成的类型; 对两个证明 $p,q:{\mathrm{Id}}_A(a,b)$, 其相等类型 ${\mathrm{Id}}_{{\mathrm{Id}}_A(a,b)}(p,q)$ 则由证明间的等价 (之证明) 构成, 如此等等.

从同伦类型论的视角看, 类型可以类比于 $\infty$-群胚, 而相等类型则类比于 $\infty$-群胚 $A$ 中的态射空间 $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