在什么情况下可以判定平等的平等？

Question

考虑以下目标：

Goal forall (x y: I = I), x = y.
Proof.
Abort.

Goal forall (x y: tt = tt), x = y.
Proof.
Abort.

这两个I和tt是单类型的成员。前者住Prop，后者住Set。这些是非常简单的类型，因此我不希望它们在任何设置中都支持丰富的相等类型。这些目标是否可以在 Coq 中证明而不诉诸身份证明公理的唯一性？

Answer 1

一个常见的充分条件是类型具有可判定的相等性；另请参阅此常见问题解答：https : //github.com/coq/coq/wiki/The-Logic-of-Coq#i-have-two-proofs-of-an-equality-statement-can-i-prove-they - 相等