立方集中的单值性公理
逻辑
2017-10-31 v1 计算机科学中的逻辑
摘要
在本注记中，我们证明 Voevodsky 的单值性公理在基于对称立方集的类型论模型中成立。我们还将讨论 Swan 在此种立方集变体中对恒等类型的构造。这证明我们有一个支持依赖积、依赖和、单值性宇宙以及具有通常判断性等式的恒等类型的类型论模型，并且该模型是在构造性元理论中表述的。
引用
@article{arxiv.1710.10941,
title = {The univalence axiom in cubical sets},
author = {Marc Bezem and Thierry Coquand and Simon Huber},
journal= {arXiv preprint arXiv:1710.10941},
year = {2017}
}
备注
12 pages