恒等类型消去子

J 的思路是：若一项构造对“一个点到自身的反身路径”已经定义好，那么它可以一致地延伸到任意恒等证明。这里不是先检查路径的内部表示再分支；使用者只能通过反身生成原则观察它。motive 像一张随起点、终点和所走路径变化的任务单，反身分支则是在唯一基本施工现场完成的样板。

路径归纳之所以比普通模式匹配微妙，是因为匹配 $p$ 后，端点 $y$ 的类型信息也要随之精化为 $x$。J 把这种精化写进结论 $C(x,y,p)$，β-rule 再说明反身时精化具有实际计算效果。它既是等式推理规则，也是依赖程序中的安全运输机制。

给定族 $B:A\to \mathcal{U}$，令 motive 为

反身分支取 $d(x)=\lambda u.u$。J 随即给出

若 $B(n)=\mathsf{Vec}(X,n)$、$p:m{=}_{\mathbb{N}}n$，运输把 $v:\mathsf{Vec}(X,m)$ 送到 $\mathsf{Vec}(X,n)$。若把 motive 错写成固定返回 $B(x)$，就只能得到原类型中的值，无法解释目标纤维 $B(y)$，这是一项可直接由 typing judgment 检出的错误。

类似地，对 $f:A\to B$ 取 motive $C(x,y,p)={\mathsf{Id}}_B(f(x),f(y))$，反身分支为 ${\mathsf{refl}}_{f(x)}$，得到 ${\mathsf{ap}}_f(p)$。再以 J 定义路径逆与连接，可以证明单位律和结合律；普通内涵理论中这些律一般由更高恒等项见证，不必判断式成立。

J 不是 K 原理。K 允许在固定端点的自等式族上证明任意 $p:a{=}_{A}a$ 与 ${\mathsf{refl}}_a$ 相等，从而导向 UIP；它并不把抽象 $p$ 判断式归约为 ${\mathsf{refl}}_a$，也不能由标准 J 无条件推出。表面 dependent pattern matching 若允许在相等证明上任意细化，可能暗中获得 K，因此 without-K 风格系统会限制某些匹配。也不能把 β-rule 扩展成“J 对任意抽象 $p$ 都约简”：只有主参数明显为 $\mathsf{refl}$ 时才有该判断式计算。

J 系统地产生相等替换、运输、同余、对称和传递，并使 Leibniz 式“相等者可在性质中替换”成为类型论内部的可计算程序。证明助理的 rewrite、subst 与依赖 cast 最终都要产生等价的核心消去项；自动化可以隐藏 motive 推断，却不能绕开其良构性。

在高阶类型论中，J 还为路径群胚结构奠基：对路径再做 J，可处理路径之间的路径。它没有预设所有高阶结构平凡，因而既兼容集合式模型，也给同伦模型留下空间。加入额外相等原则时，应分别记录它们是新公理、命题式定理还是带判断式计算的新类型论规则。