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

由于等式反射规则，我们可以很容易地在 ETT 中证明 UIP；然而，长期以来一直不知道 UIP 是否可在 ITT 中证明。我们不得不等到 90 年代才开始工作 Hofmann and Streicher ，这表明通过构建 UIP 无效的模型，无法在 ITT 中证明 UIP。 (另请查看 Hofmann 的这些 slides，它们从历史角度解释了这个问题。)

编辑

这并不意味着 UIP 与可判定类型检查不兼容:后来证明它可以在 Martin-Löf 类型理论的其他可判定变体(例如 Agda)中派生，并且可以安全地作为公理添加到类似 Coq 的系统。