Higher Homotopies in a Hierarchy of Univalent Universes

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.

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

Cited by in corpus (3)

• Modalities in homotopy type theory
• Models of Type Theory with Strict Equality
• Internal $\infty$-Categorical Models of Dependent Type Theory: Towards 2LTT Eating HoTT