内涵类型论

内涵纪律把“算出来一样”和“有理由相信相等”分开。前一种相等由内核机械执行，像把两个表达式归约到同一结果；后一种相等是一份可传入函数、可组合、可在族之间运输的数据。这样做牺牲了一些无痕改写的便利，却让类型检查不必在每次 conversion 时解决任意数学定理。

名称中的 intensional 还提示：两个对象即使在外部观察上无法区分，若没有对应的计算规则或恒等项，也不会自动被判断式识别。它不是“只看语法、完全不看意义”，因为正规化语义、逻辑关系和模型仍可证明丰富结果；它只是把哪些意义相等进入内核判断这件事控制得很严格。

设自然数加法按第一个参数递归。归约直接给出 $0+n\equiv n$，而对变量 $n$，$n+0$ 不再展开。通过归纳可以构造

若 $v:\mathsf{Vec}(A,n+0)$，内涵内核不能只因 $p_n$ 存在就用 conversion 接受 $v:\mathsf{Vec}(A,n)$；程序需形成

当 $n$ 化为具体数值时，两端也许最终判断相等，运输随证明的具体形状继续计算；当 $p_n$ 保持抽象时，cast 可能留在规范形中。这份显式痕迹正是内涵与外延类型论公理库外延类型论Extensional type theory · ETT通过相等反映把恒等证明纳入判断转换、以无痕改写换取更强外延识别的类型论变体。在使用体验上的区别。

边界不能简化成“内涵必然可判定、外延必然不可执行”。带无约束递归或不可判定重写的内涵理论照样会失去转换可判定性；带额外公理但无计算规则的核心也可能保留 type checking，却让某些闭项停在公理常量上，从而破坏朴素 canonicity。反过来，内涵理论可通过 quotient、setoid 或高阶路径表达外延数学，只是改写发生在对象层，并需要相应证明工程。

相等分层让小型可信内核成为可能：elaborator 可以搜索等式证明、插入 transport，最终只把显式核心项交给内核；内核的 conversion 不必信任搜索策略。正规化与 NbE 可为特定内涵核心提供判断相等算法，恒等类型则承载超出该算法的代数定律、函数外延性或同伦结构。

实践中的 Agda、Coq 及许多依赖核心都以某种内涵纪律为基础，但它们在 η、proof irrelevance、宇宙和归纳计算上并不相同。评价一个系统时应列出完整规则，而不是仅凭 ITT 标签推断 UIP、强正规化或 canonicity。内涵与外延也不是“弱逻辑/强逻辑”的排名：前者常以显式证据换取算法边界，后者则把更多已证明相等交给 conversion。