外延类型论

外延纪律把“已经证明相等”视作“此后内核可无痕当作相同”。这很符合普通数学书写：证明两个集合或函数相同后，读者往往不再标记每一次运输。依赖类型中的索引改写因而更顺滑，quotient 与函数外延原则也更接近日常推理。

代价是转换不再是一台只执行固定化简规则的计算器，而会读取证明环境。类型检查某个看似局部的应用，可能依赖远处是否能建立一个等式定理。外延性改善对象语言的等式体验，却把相当一部分证明搜索推入了 judgmental equality；这正是它与内涵类型论公理库内涵类型论Intensional type theory · ITT将判断相等限制为受控计算、把一般相等保留为恒等类型证据的依赖类型论取向。的工程分界，而不是价值高低之分。

仍取按首参数递归的加法，并由归纳得到

在含 $p_n$ 的语境中，reflection 给出 $n+0\equiv n:\mathbb{N}$，同余进一步给出

因此 $v:\mathsf{Vec}(A,n+0)$ 可通过 conversion 直接获得类型 $\mathsf{Vec}(A,n)$，生成的项仍是 $v$；内涵系统则通常留下显式 transport。若随后替换 $n:=2$，整条相等推导和 $v$ 的类型同步实例化，说明 reflection 不是一次非类型化强制转换。

边界之一是运行语义：无痕转换不意味着 $p_n$ 被“执行并返回 true”，也不自动给未知函数等式一个计算规则。项的 β/ι 归约可能仍强正规化，但 judgmental equality 的可判定性已不再等同于求规范形。边界之二是 UIP/K：某些 ETT 把证明无关性内建为判断规则，另一些只加入 reflection；讨论路径唯一性时必须注明版本。边界之三是 extensional equality 并非任意语义等价：只有理论能够形成恒等证明或明确加入的外延原则才进入转换。

外延类型论适合把 quotient、集合式函数外延和等式替换直接融入数学语法。范畴语义可把 judgmental equality 解释为模型中的严格等同，或者借助 quotient/completion 把内涵呈现的证据压平。对用户而言，这减少了 transport 堆叠和 setoid bookkeeping；对实现而言，则常需把外延表面理论 elaboration 到可判定的内涵核心，或接受交互式、非完全算法化的 checking。

相等反映也改变元理论证明的方法。不能仅凭一个归约器宣称 conversion 完备，更不能把普通内涵 MLTT 的 normalization 决定过程原封不动搬来。若通过两层系统、显式 coercion 或 observational equality 恢复算法性，应把那套实现称为对外延概念的表示，而不是声称原始 reflection 规则突然变得语法可判定。