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

Question

让A 和B 成为Types，并且f : A -> B 和g : B -> A 是彼此相反的函数。换句话说，A 和 B 是同构类型。

1. 真的不能证明A <> B吗？
2. 我可以安全地添加A = B 的公理吗？
3. 这个公理是否与 Coq 标准库的其他公理兼容？如果是，为什么不在标准库中？

Answer 1

这类问题是homotopy type theory 偏爱的领域，但这里是对您问题的初步综合答案。

在 CIC（± Coq 的理想理论）中，如果有一个函数 f : A -> B 与左反函数 g : B -> A（即f o g = id_B）和右逆h : B -> A（即h o f = id_B）。 您可以使用从 A 到 B 的同构来表明它们是等价的。 同伦类型理论涉及在 CIC（或者更确切地说是 MLTT）中添加一个名为 univalence 的公理，它粗略地指出类型之间的等价性和等价性重合（更准确地说，有一个映射 id_to_equiv : A = B -> equiv A B单价说这张地图本身就是一个等价物）。 单价与 CIC 兼容，因为存在验证该公理的 CIC 模型。

所以回答你的问题：

1. 是的，不能在 CIC 中证明 A <> B，因为任何此类证明都会与单价相矛盾（因此不存在 CIC + 单价的模型）
2. 您将无法证明 False，因为它是具有模型的单价的特殊情况，但是 Coq 的计算内容将部分丢失（添加任何公理时总是如此）。
3. Univalence 与 Coq 标准库的某些公理兼容（例如，excluded-middle），但与其他公理不兼容（身份证明的唯一性，也称为 UIP，单价声明有 2 个 Bool = Bool 证明）。关于标准库中单价性的缺失，源于标准库在 Prop 中定义了相等性，这与身份的多个见证者的存在是不相容的。但是，您提到的公理可能以与 UIP 兼容的方式制定（Bauer 和 Winterhalter 在所谓的类型论的基数模型上进行了一些工作）。必须检查它是否与标准库中的其他公理兼容。