如何解决我可以安全地假设同构类型是相等的吗?
设 A
和 B
为 Type
,f : A -> B
和 g : B -> A
为互逆函数。换句话说,A
和 B
是同构类型。
- 不能证明
A <> B
是真的吗? - 我可以安全地添加
A = B
的公理吗? - 这个公理与 Coq 标准库的其他公理兼容吗?而且,如果是,为什么它不在标准库中?
解决方法
这类问题是 homotopy type theory 偏爱的领域,但这里是您问题的初步综合答案。
在 CIC(± Coq 的理想理论)中,如果有一个函数 A
左逆B
(即f : A -> B
)和右逆g : B -> A
(即f o g = id_B
)。
您可以使用从 A 到 B 的同构来证明它们是等价的。
同伦类型理论涉及向 CIC(或者更确切地说是 MLTT)添加一个称为 univalence 的公理,该公理粗略地表明类型之间的等价性和相等性是一致的(更准确地说,有一个映射 {{1 }} 和单价表示这个映射本身是一个等价)。
在存在验证该公理的 CIC 模型的意义上,Univalence 与 CIC 兼容。
所以回答你的问题:
- 是的,不能在 CIC 中证明
h : B -> A
,因为任何这样的证明都会与单价相矛盾(因此不存在 CIC + 单价的模型) - 您将无法证明 False,因为它是具有模型的单价特例,但是 Coq 的计算内容将部分丢失(因为添加任何公理总是如此)。
- Univalence 与 Coq 标准库的一些公理兼容(例如,excluded-middle),但与其他公理不兼容(身份证明的唯一性,又名 UIP,univalence 声明有 2 个 Bool = Bool 的证明)。关于标准库中单价的缺失,源于标准库在Prop中定义了等价性,这与身份的多重见证人的存在是不相容的。但是,您提到的公理可能以与 UIP 兼容的方式表达(鲍尔和温特哈尔特在所谓的类型论的基数模型上做了一些工作)。必须检查它是否与标准库中的其他公理兼容。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。