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