\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(n:\mathord {\textnormal {\textsf {TruncLevel}}}\)を要素とする。\(A\)が\(n\)型ならば、\(A\)は\(\mathord {\textnormal {\textsf {succ}}}(n)\)型である。
証明
\(n\)についての帰納法による。\(n\)が\(-2\)の場合は[001L]による。
\(n\)の場合に主張が成り立つと仮定して、\(\mathord {\textnormal {\textsf {succ}}}(n)\)の場合を示す。\(A\)が\(\mathord {\textnormal {\textsf {succ}}}(n)\)型と仮定して、任意の\(x_{1},x_{2}:A\)に対して\(x_{1}=x_{2}\)が\(\mathord {\textnormal {\textsf {succ}}}(n)\)型であることを示せばよいが、仮定と帰納法の過程から直ちに従う。