Martin-Löf 依赖类型论

可以把这套理论看成一门同时描述数据、程序与证据的微型语言。一个类型的意义由“怎样构造它的规范元素、怎样使用这些元素、构造后立即使用会怎样计算”给出，而不是先把类型解释成某个外部集合再开始推理。语境像一份有先后次序的实验记录：后面的假设可以引用前面的变量，所以删去或替换一个早期声明会沿着整条记录传播。

命题即类型的读法提供了重要解释，却不是对象层的字面等号。函数项可承载蕴含证明，依赖函数可承载全称证明，依赖对可承载存在见证；这是规则结构之间的对应，而非声称逻辑公式、运行时数据和类型表达式在所有语义中都是同一个对象。MLTT 的力量恰来自把这些角色放进同一判断框架，同时仍严格区分“计算得到相同项”和“构造了一个相等证明”。

设 $\mathsf{Bool}:{\mathcal{U}}_0$，并允许在更高一层宇宙中量化小类型。多态恒等项可逐层推出

在语境 $A:{\mathcal{U}}_0,x:A$ 中，变量规则给出 $x:A$；两次 Π-引入依次关闭 $x$ 与 $A$。把 $\mathsf{Bool}$ 代入 $A$，再把 $\mathsf{true}$ 代入 $x$，计算规则得到

这里两次代入不仅改写项，也改写余类型；这正是普通无类型 β-归约不足以独立承担的部分。另一个典型机制是长度索引向量：构造器决定索引，依赖消去的 motive 同时观察索引和向量，从而把“连接后长度为 $m+n$”变成返回类型，而非函数运行后的注释。

边界首先来自理论选择。若向核心加入无约束的一般递归，闭项可能不再正规化，按计算比较类型的过程也可能失去可判定性；若加入相等反映，则有恒等证明便可改变判断相等，内核的转换问题不再只是规范化计算。1984 年讲义、现代 Agda 风格内涵理论、HoTT 与立方类型论共享谱系却不具有完全相同的规则。也不能把 Lean、Coq、Agda 的表面语言逐字称为本页核心：它们还包含归纳声明、隐式参数、层级多态、终止检查和 elaboration 等工程层。

一旦 formation—introduction—elimination—computation 的循环闭合，就能分别研究替换、主体归约、正规化、可判定类型检查与一致性。证明通常沿 typing derivation 归纳；编译器或证明助理内核则把规则定向成检查过程，再由可靠性证明保证接受的核心项确有相应推导。规范形式定理还把逻辑结论还原成数据形状：在条件合适的纯核心里，闭合自然数项必须计算到零或有限次后继。

MLTT 因而同时服务于构造性数学和程序验证：证明的计算内容可以提取，接口不变量可以进入类型，机器只需检查相对很小的核心推导。不过这些收益都相对于明确的规则集合成立。添加新公理时应问它是否有判断式计算规则；添加新类型形成子时应重新证明代入与正规化，而不是把既有元定理当作自动继承的装饰。