类型积的内射性有意义吗？

Question

如何在Coq中证明以下内容？

Goal forall (A B : Type), (A*A = B*B)%type -> A = B.

如果无法证明，可以安全地将其作为公理添加吗？

Answer 1

编辑：以下答案假定您的陈述要比问题中的答案更强：forall (A B C D : Type), (A*B = C*D)%type -> A = C。因此，答案实际上并未回答问题。

您的目标是不可证明的，因为它与独立于Coq的univalence相矛盾。之所以出现矛盾，是因为对于任何A * False，False与A同构。然后，单价意味着A * False = False，您的目标就可以让我们得出A = B和A中任何一个的B。特别是True = False，通过运输产生False的证据。因此，如果您的目标是可证明的，则Coq将是反单价的。

我不知道你的目标是否没有盲目性也会导致矛盾。