一元类型论预层模型中路径类型与恒等类型的分离
逻辑
2018-10-18 v3 范畴论
摘要
我们给出了一系列关于基于预层的某类类型论模型中路径类型、恒等类型与一元宇宙的结果。主要结果是：在基于第一与第二 Kleene 代数的预层装配中的任何 Orton-Pitts 风格的一元类型论模型（带命题截断）里，路径类型不能直接用作恒等类型。我们还给出了一个 Brouwer 式反例，表明当宇宙基于 Hofmann 与 Streicher 的标准构造且路径类型为恒等类型时，不存在构造性证明表明预层中存在 Orton-Pitts 类型论模型。一个类似证明表明：只要在实化 topos 的内部预层中某个宇宙可扩展为一元宇宙，路径类型就不是恒等类型。我们展示了关键引理在 intensional type theory 中具有纯语法的变体，并用它来对语法范畴中余纤维化的一些行为做出微小但奇特观察。
引用
@article{arxiv.1808.00920,
title = {Separating Path and Identity Types in Presheaf Models of Univalent Type Theory},
author = {Andrew Swan},
journal= {arXiv preprint arXiv:1808.00920},
year = {2018}
}
备注
Version 3 is another fairly major revision, this time to the second key lemma