[0053] 定義iiiを階数、n:TruncLeveln:\mathord {\textnormal {\textsf {TruncLevel}}}n:TruncLevelを要素とする。型⟨n⟩-Type(i):U(succ(i))\mathord {\langle n\rangle \mathord {\textnormal {\textsf {-Type}}}}(i):\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))⟨n⟩-Type(i):U(succ(i))をRecord{ ∣Type:U(i),is-trunc:IsTrunc(n,Type)∣ }\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 \} }Record{∣Type:U(i),is-trunc:IsTrunc(n,Type)∣}と定義する。