在Coq中，为何假设单例消除与定义性证明无关会导出UIP？

我正在阅读论文《Definitional proof-irrelevance without K》，其第3页提到：

若相等类型满足证明无关性，则每个等式至多有一个证明，即身份证明唯一性（UIP）。因此，同时假设证明无关性与单例消除会为理论引入新公理，例如与HoTT的单值公理不兼容。

我有以下疑问：

• 无法理解上述推导逻辑，不清楚单例消除规则的作用
• 我原以为只要对eq类型应用定义性证明无关性就能得到K公理，只有阻止eq类型的定义性证明无关性才能避开K公理，想知道这个理解哪里有误？

核心概念拆解 #

• 证明无关性：同一命题的任意两个证明在定义上相等（即p ≡ q对任意p, q : P成立），而非仅仅命题等价。
• 单例消除：针对单例类型（比如由eq a a的自反证明refl a生成的类型）的消除规则——允许从“某个元素属于以refl为唯一成员的单例类型”这一前提，推导出该元素等于refl。
• K公理：本质是自反等式的UIP强化，即所有eq a a的证明都等于refl a；多数类型论系统中K与UIP等价。

论文推导逻辑解释 #

1. 若假设相等类型的证明无关性，则任意等式x = y的两个证明p, q都满足p ≡ q——这直接就是UIP的定义。
2. 再引入单例消除：它会强制所有eq a a的证明都归约为refl a，结合证明无关性，就会推导出K公理。
3. HoTT的单值公理允许同一类型存在不同的等价关系（即不同的等式证明），因此上述组合导出的K公理与单值公理完全冲突。

你的理解偏差纠正 #

你错误地将“对eq类型应用定义性证明无关性”和“得到K公理”直接划等号，但实际上单例消除是必要的推导桥梁。论文的核心贡献正是提出：无需完全禁止eq类型的证明无关性，而是通过以下方式避开K公理：

• 限制证明无关性的适用范围，仅让它作用于特定的“命题类型”（而非所有类型，包括eq）；
• 调整单例消除规则，使其仅对未标记为证明无关的类型生效。

换句话说，通过拆分证明无关性的作用域+限制单例消除的对象，就能在保留部分证明无关性特性的同时，避免触发K公理的推导——这也是论文标题“Definitional proof-irrelevance without K”的核心思路。

内容的提问来源于stack exchange，提问作者Henrique Guerra