\(i\)を階数、\(n:\mathord {\textnormal {\textsf {TruncLevel}}}\)を要素とする。型\(\mathord {\langle n\rangle \mathord {\textnormal {\textsf {-Type}}}}(i):\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))\)を\(\mathord {\textnormal {\textsf {Record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {Type}}}:\mathcal {U}(i),\mathord {\textnormal {\textsf {is-trunc}}}:\mathord {\textnormal {\textsf {IsTrunc}}}(n,\mathord {\textnormal {\textsf {Type}}})\mathclose {|\negmedspace \} }\)と定義する。