Univalent foundations refer to Voevodsky’s programme for a new foundation of mathematics based on intuitionistic type theory and employing ideas from homotopy theory. Here every type \(A\) is considered as a space, and the identity type \(\I(A,a,b)\) is the space of paths from point \(a\) to point \(b\) in \(A\). Iterated identity types represent higher homotopies, e.g.