Higher Homotopies in a Hierarchy of Univalent Universes

Kraus, Nicolai; Sattler, Christian

Abstract

For Martin-Lof type theory with a hierarchy U(0): U(1): U(2): ... of univalent universes, we show that U(n) is not an n-type. Our construction also solves the problem of finding a type that strictly has some high truncation level without using higher inductive types. In particular, U(n) is such a type if we restrict it to n-types. We have fully formalized and verified our results within the dependently typed language and proof assistant Agda.

Citation

Kraus, N., & Sattler, C. (2015). Higher Homotopies in a Hierarchy of Univalent Universes. ACM Transactions on Computational Logic, 16(2), Article 18. https://doi.org/10.1145/2729979

• Journal Article Type: Article
• Acceptance Date: Jan 1, 2015
• Publication Date: 2015-04
• Deposit Date: Jul 15, 2020
• Journal: ACM Transactions on Computational Logic
• Print ISSN: 1529-3785
• Publisher: Association for Computing Machinery (ACM)
• Peer Reviewed: Peer Reviewed
• Volume: 16
• Issue: 2
• Article Number: 18
• DOI: https://doi.org/10.1145/2729979
• Keywords: Logic; Logic in Computer Science
• Public URL: https://nottingham-repository.worktribe.com/output/2461927
• Publisher URL: https://dl.acm.org/doi/10.1145/2729979