恒等类型

恒等类型把“相等的证据”放进类型世界。变量 $p:{\mathsf{Id}}_A(a,b)$ 是可以传给函数的输入；即使 $a,b$ 没有按计算规则化成相同项，也可以利用 $p$ 证明关于它们的性质。与之不同，定义相等在类型检查时直接允许替换表达式，不要求接收一个 $p$。

路径归纳的关键是结论可以同时依赖第二个端点与路径：固定 $a:A$，考虑 $C(b,p)$，并给出 $d:C(a,{\mathsf{refl}}_a)$，就能构造任意 $b,p$ 下的 $C(b,p)$。这不表示先把任意固定端点间的 $p$ 改写成 $\mathsf{refl}$；端点也随归纳一起变化。忽略这项依赖，容易错误地推得所有相等证明唯一。

这种区分让等式既有计算内容又不吞没类型检查。程序可接收 $p:a{=}_{A}b$，沿 $p$ 把依赖于 $a$ 的数据运输到依赖于 $b$ 的位置；内核仍只用受控的判断相等核对每一步类型。高阶解释还允许路径之间再有恒等类型，因而同一端点间可能保留非平凡结构。

给定类型族 $B:A\to \mathcal{U}$，可由 J 定义运输

并满足

取 $A=\mathbb{N}$、$B(n)=\mathsf{Vec}(X,n)$。若 $p:{\mathsf{Id}}_{\mathbb{N}}(m,n)$ 且 $v:\mathsf{Vec}(X,m)$，则 ${\mathsf{transport}}_B(p,v):\mathsf{Vec}(X,n)$；没有 $p$ 时，不能把长度 $m$ 的向量无条件当作长度 $n$ 的向量。若 $p$ 恰为 ${\mathsf{refl}}_m$，运输判断式地化为 $v$；对抽象变量 $p$，运输通常保持为中立项，不会凭空约简。

一个具体边界来自自然数加法。若递归定义在第一个参数上，$0+n\equiv n$ 可能直接计算，而 $n+0=n$ 对变量 $n$ 通常需要归纳产生恒等项；后者成立不使两端自动成为判断相等。标准 J 也不推出 UIP 或 K，即不保证任意 $p,q:a{=}_{A}b$ 都相等；加入这类原则会排除某些高阶路径模型，并与通常的 univalence 解释冲突。反之，证明无关性若只针对命题层，也不能未经规则说明推广到所有恒等类型。

例如定义对称时，令 $C(b,p)={\mathsf{Id}}_A(b,a)$。反身分支取 $d={\mathsf{refl}}_a$，路径归纳便把输入 $p:a{=}_{A}b$ 送到 $p^{-1}:b{=}_{A}a$。反身输入按规则计算为自身；抽象输入 $p$ 的逆路径则是一个构造出的项，而不是把符号等号直接左右交换。运输、对称与路径连接都可按同样方式明确给出依赖目标和反身分支。

由路径归纳可定义对称、连接、函数作用于路径 $\mathsf{ap}$，并证明它们满足群胚律；这些律在普通内涵理论中多位于更高恒等类型，而非全部成为判断等式。运输则是改写、类型安全强制转换和索引精化的统一核心：等式证明不仅说明两个值相同，还解释依赖数据怎样随端点移动。

在程序验证中，恒等类型表达代数定律、数据结构不变量和程序等价；在同伦类型论中，它被解释为空间中的路径，迭代恒等类型记录高阶同伦。两种用途共享同一形成—反身—消去规则，但额外采用 UIP、函数外延性或 univalence 会改变可证明结构，必须清楚标注。