Cry*_*sis 4 equality coq homotopy-type-theory
在HOTT和COQ中,人们无法证明UIP,即
\ Prod_ {p:a = a} p = refl a
但是可以证明:
\ Prod_ {p:a = a}(a,p)=(a,refl a)
为什么定义它是这样的？是吗,因为人们希望有一个很好的同伦解释？或者这个定义有一些自然的,更深层次的原因吗？
据我所知,这不是故意做的,而是试图保持类型检查可判定的结果.
这些系统中的平等概念可以追溯到Martin-Löf的内涵式理论.该系统具有可判定的类型检查,但要求我们明确标记证明中的每个重写步骤.(从形式上看,这些改写步骤与使用平等消除器eq_rect在勒柯克.)马丁- LOF还设计了第二个系统,称为外延型理论,其中重写是隐式:每当两个术语a和b相等,在这个意义上,我们可以证明a = b,它们可以互换使用.不幸的是,为这种便利付出了代价:类型检查变得不可判定.粗略地说,类型检查算法在很大程度上依赖于ITT的显式重写步骤来指导其计算,而这些提示在ETT中是不存在的.
很快就意识到UIP在ETT中是可证明的,但不知道这是否适用于ITT.我们不得不等到90年代Hofmann和Streicher的工作,这表明UIP无法通过构建UIP无效的模型在ITT中得到证明.(请查看霍夫曼的这些幻灯片,从历史的角度解释这个问题.)
这并不意味着UIP与可判定类型检查不兼容:后来证明它可以在Martin-Löf类型理论的其他可判断变体(例如Agda)中导出,并且可以安全地添加为公理中的公理.像Coq这样的系统.