关于Awodey论文及Coq中内涵与外延类型论Equality特性的疑问

你的困惑完全合理——毕竟等量替换（莱布尼茨律）确实是我们直觉中等式的核心性质！不过这里的关键是要区分内涵等式和外延等式在类型论中的不同定义，以及Awodey这句话里的“上下文”到底指向什么。

我们来考虑内涵类型论与外延类型论的例子。外延理论中的Equality概念显然“更强”，因为它允许在所有上下文中直接进行等量替换。相比之下，在内涵系统中，可能存在a = b且语句Φ(a)成立，但Φ(b)却不成立的情况。

核心区别：内涵等式 vs 外延等式 #

• 外延类型论：这里的等式是命题等式，并且直接内置了莱布尼茨替换规则——只要a = b是一个真命题，任何依赖于a的命题Φ(a)都能直接替换成Φ(b)，且真值不变。这种等式完全贴合我们数学里“相等就是完全等价”的直觉。
• 内涵类型论：这里的等式分为判断等式和命题等式两种。判断等式是元层面的“定义相等”（比如def x := 5，那x和5在判断上就是相等的），这种相等确实支持任意上下文的直接替换；但Awodey提到的a = b是命题等式——它本身是一个类型（类型论中命题即类型），需要你构造一个证明项来确认a和b相等。内涵系统默认不会把命题等式和判断等式划等号，所以即使你有p : a = b的证明，也不能直接在所有上下文中把a换成b，必须显式用这个证明项来完成替换（比如Coq里的rewrite策略）。

Coq中的实际案例 #

Coq是典型的内涵类型论系统，用一个简单例子就能直观说明：
假设我们定义两个函数：

Definition f (n : nat) : nat := n + 0.
Definition g (n : nat) : nat := n.

从外延上看，f和g完全相等——对任何自然数n，f n和g n的结果都一致。但在Coq的内涵规则下，f和g的判断等式不成立（因为它们的定义语法不同），而f = g是一个需要证明的命题（你得先用plus_n_O定理证明forall n, f n = g n，再借助函数外延性公理推导出f = g）。

如果现在有一个内涵上下文Φ，比如“这个函数的定义是n + 0”，那么Φ(f)为真，但Φ(g)就为假——这正是Awodey所说的“命题等式a = b成立，但Φ(a)真而Φ(b)假”的情况，因为这个上下文依赖的是函数的定义形式而非行为结果。

要是在Coq中启用函数外延性公理（FunctionalExtensionality），甚至是Awodey论文的核心——单值公理（Univalence），就能让命题等式更贴近外延等式，支持更多上下文的替换，缩小内涵与外延系统的差距。

总结来说：内涵系统里的“等量替换”并没有失效，而是替换需要显式的证明支撑，且仅在外延上下文中成立；而外延系统直接把命题等式和判断等式绑定，默认支持所有上下文的替换，所以说它的Equality概念“更强”。

内容的提问来源于stack exchange，提问作者Cryptostasis