coq - 向标准 Coq 添加“类型扩展性”。（单价公理的一部分）

Question

我有一个天真的问题：

我们为什么不将这个公理添加到 Coq：

Axiom type_extensionality : forall (A B:Type)
 (f:A->B) (invf:B->A) (H1: forall b, (f (invf b)) = b)
 (H2: forall a, (invf (f a)) = a), A = B.

好的，它允许诸如 (nat->Prop)=(nat->bool) 和 (A\/B)->(A+B) 之类的非构造定理（证明在这里）。但是 Coq 的标准库已经有很多非建设性的公理。

它会导致矛盾吗？（如果是这样，我在哪里可以阅读证明？）或者只是还没有证明公理不会导致矛盾？也许它只是没用？

也许这就是 HoTT 库在https://github.com/HoTT/HoTT/blob/master/theories/Basics/Overture.v中重新定义路径类型的原因。这个“type_extensionality”公理不如单价公理强。如果存在 ProofIrrelevance、PropositionExtensionality，最后一个将失败。（bool 以两种不同的方式等效于自身，而 bool=bool 类型仅包含一个元素）。