Higher Homotopies in a Hierarchy of Univalent Universes
Logic
2015-06-03 v3 Logic in Computer Science
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.
Keywords
Cite
@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}
}
Comments
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