Higher Homotopies in a Hierarchy of Univalent Universes

Nicolai Kraus, Christian Sattler

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…