在HOTT和CoQ中都不能证明UIP，即 Prod_{p：a=a}p=refl a

但可以证明： Prod_{p：a=a}(a，p)=(a，refl a)

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

推荐答案

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

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

由于等反射规则，我们可以很容易地在ETT中证明UIP，但在ITT中是否可证明UIP一直是未知的。我们不得不等到90年代Hofmann and Streicher的工作，这表明在ITT中不能通过构建一个UIP无效的模型来证明UIP。(也请查看Hofmannslides从历史角度解释这一问题的slides。)

编辑

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