恒等类型

恒等类型把“相等的证据”放进类型世界。定义相等像排字阶段发现两段表达式计算后本就是同一行，不需要票据；恒等类型则像一条可携带、可组合的路径，即使两个端点没有化成相同语法，也可能有项证明它们相连。路径归纳说明所有这类证据的合法使用最终由反身路径生成，但这并不宣告所有路径彼此判断相等。

这种区分让等式既有计算内容又不吞没类型检查。程序可接收 $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 解释冲突。反之，证明无关性若只针对命题层，也不能未经规则说明推广到所有恒等类型。

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

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