立方类型论：单值公理的构造性解释
计算机科学中的逻辑
2016-11-14 v1 逻辑
摘要
本文提出了一种类型论，基于依赖类型论在立方集模型中的解释，可直接操纵维立方体（点、线、正方形、立方体等）。这为推理恒等式类型提供了新的方法，例如，函数外延性可在系统中直接证明。此外，Voevodsky的单值公理在该系统中可证。我们还解释了带有一些高阶归纳类型（如圆和命题截断）的扩展。最后，我们在构造性元理论中为这种立方类型论提供了语义。
引用
@article{arxiv.1611.02108,
title = {Cubical Type Theory: a constructive interpretation of the univalence axiom},
author = {Cyril Cohen and Thierry Coquand and Simon Huber and Anders Mörtberg},
journal= {arXiv preprint arXiv:1611.02108},
year = {2016}
}
备注
To be published in the post-proceedings of the 21st International Conference on Types for Proofs and Programs, TYPES 2015