\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(n:\mathord {\textnormal {\textsf {TruncLevel}}}\)を要素とする。

• -\(n\)切り詰め(\(n\)-truncation)\({\| A\| }_{n}:\mathcal {U}(i)\)を構成できる。
• -\({\| A\| }_{n}\)は\(n\)型である(ことを示す要素を構成できる)。
• -要素\(a:A\)に対して、要素\({|a|}_{n}:{\| A\| }_{n}\)を構成できる。
• -\(c:{\| A\| }_{n}\)を要素、\(j\)を階数、\(B:{\| A\| }_{n}\to \mathcal {U}(j)\)を型の族、\(f:\prod _{x:A}B({|x|}_{n})\)を関数とする。\(\prod _{z:{\| A\| }_{n}}\mathord {\textnormal {\textsf {IsTrunc}}}(n,B(z))\)の要素があるなら、要素\(\mathord {\textnormal {\textsf {ind}}}_{{\| A\| }_{n}}(c,B,f):B(c)\)を構成できる。
• -\(a:A\)を要素、\(j\)を階数、\(B:{\| A\| }_{n}\to \mathcal {U}(j)\)を型の族、\(f:\prod _{x:A}B({|x|}_{n})\)を関数とする。\(\prod _{z:{\| A\| }_{n}}\mathord {\textnormal {\textsf {IsTrunc}}}(n,B(z))\)の要素があるなら、\(\mathord {\textnormal {\textsf {ind}}}_{{\| A\| }_{n}}(a,B,f)\equiv f(a)\)を定義される。