\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(n:\mathord {\textnormal {\textsf {TruncLevel}}}\)を要素とする。\(A\)が\(n\)型かつ\(n\)連結ならば、\(A\)は可縮である。