\(i\)を階数、\(A:\mathcal {U}(i)\)を型とする。\(n:\mathord {\textnormal {\textsf {TruncLevel}}}\)に対して、型\(\mathord {\textnormal {\textsf {IsTrunc}}}(n,A):\mathcal {U}(i)\)を次のように定義する。

• -\(\mathord {\textnormal {\textsf {IsTrunc}}}(-2,A)\equiv \mathord {\textnormal {\textsf {IsContr}}}(A)\)
• -\(\mathord {\textnormal {\textsf {IsTrunc}}}(\mathord {\textnormal {\textsf {succ}}}(n),A)\equiv \prod _{x_{1},x_{2}:A}\mathord {\textnormal {\textsf {IsTrunc}}}(n,x_{1}=x_{2})\)

\(\mathord {\textnormal {\textsf {IsTrunc}}}(n,A)\)の要素がある時、\(A\)は\(n\)型(\(n\)-type)である、または\(n\)-truncatedであると言う。