带严格等式的类型论模型
计算机科学中的逻辑
2017-02-17 v1
摘要
本论文介绍了两层类型论的思想，它是 Martin-Löf 类型论的扩展，添加了严格等式这一概念作为内部原语。一种在常规等式形式之外还具有严格等式的类型论（后者对于同伦类型论（HoTT）的近期创新具有根本重要性）最初由 Voevodsky 提出，通常被称为 HTS。在此，我们推广并扩展了这一思想，通过开发一个语义框架来系统性地描述两层系统的类型构造子，并证明了一个相对于像 HoTT 这样的常规类型论的保守性结果。最后，我们展示了如何使用两层理论为 HoTT 中的开放问题提供部分解。特别地，我们用它来构造半单纯类型，并构建了 -范畴内蕴理论的基础。
引用
@article{arxiv.1702.04912,
title = {Models of Type Theory with Strict Equality},
author = {Paolo Capriotti},
journal= {arXiv preprint arXiv:1702.04912},
year = {2017}
}