单值宇宙层级中的高阶同伦
逻辑
2015-06-03 v3 计算机科学中的逻辑
摘要
对于具有单值宇宙层级 U(0): U(1): U(2): ... 的 Martin-Lof 类型论，我们证明了 U(n) 不是一个 n-型。我们的构造也解决了在不使用高阶归纳类型的情况下寻找具有严格高截断水平的类型的问题。特别地，如果我们将 U(n) 限制为 n-型，它就是这样一种类型。我们已在依赖类型语言和证明助手 Agda 中完全形式化并验证了我们的结果。
引用
@article{arxiv.1311.4002,
title = {Higher Homotopies in a Hierarchy of Univalent Universes},
author = {Nicolai Kraus and Christian Sattler},
journal= {arXiv preprint arXiv:1311.4002},
year = {2015}
}
备注
v1: 30 pages, main results and a connectedness construction; v2: 14 pages, only main results, improved presentation, final journal version, ancillary files with electronic appendix; v3: content unchanged, different documentclass reduced the number of pages to 12