coq - 我可以安全地假设同构类型是相等的吗？

Question

让 A和 B是 Type s 和 f : A -> B和 g : B -> A是互逆的函数。换句话说 A和 B是同构类型。

真的不能证明A <> B ?

我可以安全地添加 A = B 的公理吗？ ?

这个公理与 Coq 标准库的其他公理兼容吗？而且，如果是，为什么不在标准库中？

Answer 1

这类问题是homotopy type theory的偏爱领域。但这是对您的问题的初步综合答案。
在 CIC(± Coq 的理想理论)中，我们说两种类型 A和 B如果有函数 f : A -> B 是等价的与左逆 g : B -> A (即 f o g = id_B )和右逆 h : B -> A (即 h o f = id_B )。
您可以使用从 A 到 B 的同构来证明它们是等价的。
同伦类型理论涉及在 CIC(或者更确切地说 MLTT)中添加一个称为单价的公理，它粗略地表明类型之间的等价性和等价性是一致的(更准确地说，有一个映射 id_to_equiv : A = B -> equiv A B 并且单价表示这个映射是本身是等价的)。
在存在验证该公理的 CIC 模型的意义上，Univalence 与 CIC 兼容。
所以回答你的问题:

是的，无法证明A <> B在 CIC 中，因为任何这样的证明都会与单价相矛盾(因此不存在 CIC + 单价的模型)

您将无法证明 False ，因为它是具有模型的单价特例，但是 Coq 的计算内容将部分丢失(因为添加任何公理总是如此)。

单价与 Coq 标准库的一些公理兼容(例如排除中间)，但与其他公理不兼容(身份证明的唯一性，又名 UIP，单价声明有 2 个 Bool = Bool 的证明)。关于标准库中单价性的缺失，源于标准库在Prop中定义了等价性，这与身份的多重见证人的存在不相容。但是，您提到的公理可能以与 UIP 兼容的方式表达(鲍尔和温特哈尔特在所谓的类型论的基本模型上做了一些工作)。必须检查它是否与标准库中的其他公理兼容。