COQ 和 HOTT 中平等定义的原因
Reason for equality definition in COQ and HOTT
在 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；然而，UIP 在 ITT 中是否可证明，一直是个未知数。等到90年代霍夫曼Hofmann and Streicher, which showed that UIP cannot be proved in ITT by constructing a model where UIP is not valid. (Check also these slides的著作，从历史的角度解释了这个问题。）
编辑
这并不意味着 UIP 与可判定类型检查不兼容：后来表明它可以在 Martin-Löf 类型理论的其他可判定变体（例如 Agda）中派生，并且可以安全地添加作为像 Coq 这样的系统中的公理。
直觉上，我倾向于认为a = a为pi_1(A,a)，即class从a到自身的路径模同伦等价；而我认为 { x:A | a = x } 是 A 的通用覆盖 space，即从 a 到 A 模同伦等价的某个其他点的路径。因此，虽然 pi_1(A,a) 通常不是平凡的，但我们确实知道 A 的通用覆盖 space 是可收缩的。
在 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；然而，UIP 在 ITT 中是否可证明，一直是个未知数。等到90年代霍夫曼Hofmann and Streicher, which showed that UIP cannot be proved in ITT by constructing a model where UIP is not valid. (Check also these slides的著作，从历史的角度解释了这个问题。）
编辑
这并不意味着 UIP 与可判定类型检查不兼容：后来表明它可以在 Martin-Löf 类型理论的其他可判定变体（例如 Agda）中派生，并且可以安全地添加作为像 Coq 这样的系统中的公理。
直觉上，我倾向于认为a = a为pi_1(A,a)，即class从a到自身的路径模同伦等价；而我认为 { x:A | a = x } 是 A 的通用覆盖 space，即从 a 到 A 模同伦等价的某个其他点的路径。因此，虽然 pi_1(A,a) 通常不是平凡的，但我们确实知道 A 的通用覆盖 space 是可收缩的。