\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(a_{1},a_{2}:A\)を要素、\(n:\mathord {\textnormal {\textsf {TruncLevel}}}\)を要素とする。\(A\)が\(n\)型ならば、\(a_{1}=a_{2}\)も\(n\)型である。