equality - COQ 和 HOTT 中相等定义的原因

Question

在 HOTT 和 COQ 中，无法证明 UIP，即
\Prod_{p:a=a} p = refl a

但可以证明：
\Prod_{p:a=a} (a,p) = (a, refl a)

为什么这样定义？是不是因为想要一个好的同伦解释？或者这个定义有什么自然的、更深层的原因？

Answer 1

今天我们知道了拒绝 UIP 的一个很好的理由：它与同伦类型理论中的单价原则不相容，后者粗略地说可以识别同构类型。然而，据我所知，Coq 的相等性不能验证 UIP 的原因主要是从它的一个祖先那里继承下来的历史偶然：Martin-Löf 的内涵类型理论，它比 HoTT 早了很多年。

ITT 中的平等行为最初是出于保持类型检查可判定的愿望。这在 ITT 中是可能的，因为它要求我们在证明中明确标记每个重写步骤。（形式上，这些重写步骤对应eq_rect于 Coq 中等式消除器的使用。）相比之下，Martin-Löf 设计了另一个称为外延类型理论的系统，其中重写是隐式的：只要两个项a和b相等，在我们可以证明的意义上也就是说a = b，它们可以互换使用。这依赖于平等反射规则它说命题上相等的元素在定义上也是相等的。不幸的是，这种便利是要付出代价的：类型检查变得不可判定。粗略地说，类型检查算法关键依赖于 ITT 的显式重写步骤来指导其计算，而 ETT 中没有这些提示。

由于等式反射规则，我们可以在 ETT 中轻松证明 UIP；但是，很长一段时间以来，人们都不清楚 UIP 是否可以在 ITT 中得到证明。我们不得不等到 90 年代Hofmann 和 Streicher的工作，这表明在 ITT 中无法通过构建 UIP 无效的模型来证明 UIP。（也请查看 Hofmann 的这些幻灯片，它们从历史的角度解释了这个问题。）

编辑

这并不意味着 UIP 与可判定类型检查不兼容：后来证明它可以从 Martin-Löf 类型理论的其他可判定变体（例如 Agda）中推导出来，并且可以安全地作为公理添加到像 Coq 这样的系统。

Answer 2

直觉上，我倾向于认为a = a是 pi_1(A,a)，即从 a 到自身的路径类模同伦等价；而我认为是{ x:A | a = x }A 的全覆盖空间，即从 a 到 A 模同伦等价的其他点的路径。因此，虽然 pi_1(A,a) 通常不平凡，但我们确实知道 A 的全覆盖空间是可收缩的。