Higher Homotopies in a Hierarchy of Univalent Universes

Nicolai Kraus, Christian Sattler

Research output: Contribution to journalArticlepeer-review

7 Citations (Scopus)


For Martin-Lof type theory with a hierarchy U0 : U1 : U2 : . . . of univalent universes, we show that Un 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, Un 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.
Original languageEnglish
Article number18
Number of pages12
JournalACM Transactions on Computational Logic
Issue number2
Publication statusPublished - Apr 2015


  • Homotopy type theory
  • loop spaces
  • truncation levels
  • univalent universes


Dive into the research topics of 'Higher Homotopies in a Hierarchy of Univalent Universes'. Together they form a unique fingerprint.

Cite this