K 公理

K 公理是 Thomas Streicher 给相等类型设计的另一条消去规则, 它不能代替 J 公理.

K 公理有些类似单位类型的消去规则. 和 J 公理类似, 它也有计算规则. 该规则非常强, 因此蕴含了比 J 公理更多的定理, 但也对相等类型的语义解释带来了更多限制.

J 公理对形如 ${\mathrm{Id}}_A(x,y)$ 的类型进行消去, 其中 $x\ne y$, 而 K 公理则考虑形如 ${\mathrm{Id}}_A(x,x)$ 的类型, 它认为该类型唯一的实例就是 ${\mathrm{refl}}_x$.

这间接否认了泛等公理, 代入 $[A\mapsto \mathbb{N},x\mapsto 0]$ 就可以看出一个反例: 泛等公理认为自然数类型上的任何一个自同构都可以构成一个 $\mathrm{Id}(\mathbb{N},\mathbb{N})$ 的实例, 不同的自同构给出不同的实例, 而 K 公理只承认其中的平凡自同构.

“相等” 在英语中是以字母 I 开头的单词, 它的下一个字母 J 被 J 公理占用, 因此叫 K 公理.

1定义

类似 J 规定, 定义 K 公理也需要如下值存在:

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

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

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

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

计算规则如下:

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

2性质

引理 2.1 (相等证明唯一). 考虑$$\begin{array}{rl}\Gamma & ⊢p:\mathrm{Id}(x,y)\\ \Gamma & ⊢q:\mathrm{Id}(x,y)\end{array}$$如下命题成立: $${\mathrm{Id}}_{\mathrm{Id}(x,y)}(p,q)$$换言之, 如下命题成立: $$\Gamma ⊢{\Pi }_{p:\mathrm{Id}(x,y)}{\Pi }_{q:\mathrm{Id}(x,y)}{\mathrm{Id}}_{\mathrm{Id}(x,y)}(p,q)$$

在使用 $\Pi$ 类型的等价形式中, 将两个类型相同的参数分开写是为了使得证明更可读.

证明. 首先借助 J 公理简化问题: $$\lambda p.J(\boxed{\lambda x.\lambda y.\lambda p.{\Pi }_{q:\mathrm{Id}(x,y)}{\mathrm{Id}}_{\mathrm{Id}(x,y)}(p,q)},子问题,p)$$可以看出子问题的类型如下: $$子问题:{\Pi }_{q:\mathrm{Id}(x,x)}{\mathrm{Id}}_{\mathrm{Id}(x,x)}({\mathrm{refl}}_x,q)$$再通过 K 公理证明即可: $$\lambda q.K(\boxed{\lambda q.{\mathrm{Id}}_{\mathrm{Id}(x,x)}({\mathrm{refl}}_x,q)},{\mathrm{refl}}_{{\mathrm{refl}}_x},q)$$

$\square$

从这个证明中可以萃取出一个 J 公理的推论, 即 2.1 可以转化为上面的子问题.

3相关概念

•	相等类型包含了相等类型的定义和 J 公理的变种.
•	J 公理是相等类型的另一条消去规则.
•	K 公理虽然在同伦类型论中不成立, 但对于某些类型是可以证明出来的, 这些类型就是集合 (类型论), 也就是$n$-类型中 $n=0$ 的类型. 这个原理类似于排中律在类型论中虽然只能是公理, 但在 “两个自然数是否相等” 这件事上的排中律我们依然可以证明.

4参考资料

•	Thomas Streicher (1993). “Investigations into intensional type theory”. Habilitationsschrift, Ludwig-Maximilians-Universität München.