\(i\)を階層とする。宇宙\(\mathcal {U}(i)\)が一価性(univalence)を満たすとは、\(\prod _{X:\mathcal {U}(i)}\mathord {\textnormal {\textsf {IsContr}}}(\sum _{Y:\mathcal {U}(i)}X\simeq Y)\)の要素があることである。