定义相等

定义相等描述内核愿意“视为同一个程序”的表达式。它像编译器在核对接口前进行的透明计算：函数刚应用就代入，递归子刚遇到构造器就展开，类型中的算术也按同样规则化简。用户无需提交一份等式证书，因为这次识别属于判断过程自身。

把它限制在受控计算上非常重要。若每个数学上可证明的等式都自动进入转换，类型检查器为了判断一个函数调用是否合法，就可能被迫搜索任意证明。内涵理论把较大的相等空间留给恒等类型，只让稳定、可计算的一部分成为定义相等，从而在表达力与可判定内核之间划界。

设自然数加法按第一个参数递归：

若 $v:\mathsf{Vec}(A,1+1)$，计算给出 $1+1\equiv 2$，conversion 于是接受 $v:\mathsf{Vec}(A,2)$，无需插入运输项。对变量 $n$，$0+n\equiv n$ 可直接化简；但 $n+0$ 的首参数未知，通常停在中立项，所以 $n+0\equiv n$ 不成立为同一判断。后一个等式可用对 $n$ 的归纳构造 $p:{\mathsf{Id}}_{\mathbb{N}}(n+0,n)$，恰好展示命题相等比当前计算规则覆盖得更广。

定义相等也受透明度控制。若常量 $c$ 的定义被标记不透明，$\delta$-展开不能越过它，即使用户知道其实现返回零，$c\equiv 0$ 也未必被内核接受。加入无约束递归会使规范化可能发散；加入 equality reflection 会把任意恒等证明送入转换，并使一般类型检查失去可判定算法。反过来，可判定也不是仅凭“叫 definitional”就自动拥有，必须对选定规则证明正规化或给出另一个终止、可靠且完备的比较过程。

定义相等让类型中的计算无需显式改写，支撑依赖函数应用、索引归纳和模块透明展开。实现通常先比较类型头部：遇到 Π、Σ 或构造器便结构递归，遇到中立项则比较头变量与 spine；需要时才继续求值，避免先完全正规化所有表达式。正确性要求算法接受恰好声明规则生成的等同，且不把运行时副作用或不终止计算带进内核转换。

在元理论中，定义相等的规范形唯一性可推出类型构造器的可辨识性，例如若两个 Π 类型定义相等，则其定义域与适当余类型也相等；这些引理又服务于类型检查可靠性。它还影响库设计：把定律做成判断计算可改善化简与执行，把定律只做成恒等证明则保持较小内核。两种选择没有通用优胜者，必须按正规化、可判定性和用户可见计算行为共同评估。