J 公理

J 公理是 Per Martin-Löf 给相等类型设计的消去规则, 因此又叫 J 规则. 它看起来和其它的消去规则不太一样, 所以被称为公理, 但它实际上不是公理, 因为它有计算规则.

一般来说, 消去规则和构造规则是两组看起来可以互相抵消的操作, 比如积类型、函数类型、无交并类型都符合这样的特征, 但相等类型却不然. Martin-Löf 类型论中的相等类型的构造规则如下:

$$\frac{\Gamma ⊢x:X}{\Gamma ⊢\mathrm{ref}{\mathrm{l}}_{\mathrm{x}}:{\mathrm{Id}}_X(x,x)}$$

换言之, 只有当 $x,y$ 为同一个表达式时, 才可能构造出 $\mathrm{Id}(x,y)$ 这个类型的实例, 因此它的反向操作应该是 “若存在 $p:\mathrm{Id}(x,y)$ 则 $x,y$ 为同一个表达式” 才对, 但这一描述和类型论中其它的消去规则又很不一样了: 一般的消去规则的定义中是不含等式的, 等式只在计算规则中会用到. 相等类型的消除规则若如此定义便会影响类型论的全局性质, 这类类型论被称为外延的, 见外延类型论.

J 规则相对含蓄地表达了一个类似的观点: 它认为如果存在 $p:\mathrm{Id}(x,y)$ 那么任意语境中的 $y$ 可以被替换为 $x$, 也就是说任何含有 $x$ 的类型中的这些 $x$ 都可以被替换为 $y$, 巧妙地绕开了对 “相等” 的直接讨论. 这也间接带来了同伦类型论的研究. 这种描述方式和 Leibniz 相等原则非常接近.

“相等” 在英语中是以字母 I 开头的单词, 因此相等类型的消去规则的名字就采用了 I 的下一个字母 J. 在 J 公理之后, 还有 K 公理.

1定义

定义 J 规则需要如下值存在:

$$\Gamma ⊢\mathrm{ref}{\mathrm{l}}_{\mathrm{x}}:\mathrm{Id}(x,x)$$

这对应相等类型的自反性, 注意这里没有要求它是相等类型的构造规则, 只需要它存在即可.

定义 1.1. J 公理类型规则如下: $$\begin{array}{rl}& \Gamma ⊢A:\mathcal{U}\Gamma ⊢x,y:A\\ & \Gamma ⊢P:{\Pi }_{x,y:A}\mathrm{Id}(x,y)\to \mathcal{U}\\ & \Gamma ⊢p:{\Pi }_{x:A}P(x,x,{\mathrm{refl}}_x)\\ & \Gamma ⊢q:\mathrm{Id}(x,y)\\ & \\ & \overline{\Gamma ⊢J(P,p,q):P(x,y,q)}\end{array}$$

有时可以从语境中推导出 $P$ 所以也可以省略掉, 直接写 $J(p,q)$.

计算规则如下:

$$J(P,p,{\mathrm{refl}}_x)=p(x)$$

2性质

引理 2.1. 命题相等是一个等价关系. 换言之, 考虑 $\Gamma ⊢x,y,z:A$, 如下引理成立: $$\begin{array}{rl}\Gamma & ⊢\mathrm{Id}(x,y)\to \mathrm{Id}(y,x)\\ \Gamma & ⊢\mathrm{Id}(x,y)\to \mathrm{Id}(y,z)\to \mathrm{Id}(x,z)\end{array}$$

证明. 前者的证明如下: $$\lambda q.J(\boxed{\lambda x.\lambda y.\lambda p.\mathrm{Id}(y,x)},\lambda x.{\mathrm{refl}}_x,q)$$后者证明如下: $$\lambda q.J(\boxed{\lambda x.\lambda y.\lambda p.\mathrm{Id}(y,z)\to \mathrm{Id}(x,z)},\boxed{\lambda x.\lambda p.p},q)$$这也意味着前者遇到参数为 ${\mathrm{refl}}_x$ 时返回 ${\mathrm{refl}}_x$, 后者遇到第一个参数为 ${\mathrm{refl}}_x$ 时直接返回第二个参数.

$\square$

引理 2.2. 考虑 $\Gamma ⊢x,y:A$ 和 $\Gamma ⊢f:A\to B$, $$\Gamma ⊢{\mathrm{Id}}_A(x,y)\to {\mathrm{Id}}_B(fx,fy)$$

证明类似, 留作练习.

定理 2.3 (等量代换). 考虑 $\Gamma ⊢x,y:A$, $$\mathrm{subst}:(P:A\to \mathcal{U})\to {\mathrm{Id}}_A(x,y)\to P(x)\to P(y)$$

证明. $$\lambda P.\lambda q.J(\boxed{\lambda x.\lambda y.\lambda p.P(x)\to P(y)},\boxed{\lambda x.\lambda p.p},q)$$这也意味着当第二个参数为 ${\mathrm{refl}}_x$ 时该定理表现为恒同映射.

$\square$

该定理非常重要, 它不仅蕴含 2.1, 且在定义各种消去规则上有丰富的应用, 例如圆周的消去规则就需要用到这个操作.

3相关概念

•	相等类型包含了相等类型的定义和 J 公理的变种.
•	K 公理是相等类型的另一条消去规则.
•	Leibniz 相等原则可以看作相等类型的 $\lambda$ 编码.
•	Andrew Swan 问题