ホモトピー型理論
[0053] 定義

iiを階数、n:TruncLeveln:\mathord {\textnormal {\textsf {TruncLevel}}}を要素とする。型n-Type(i):U(succ(i))\mathord {\langle n\rangle \mathord {\textnormal {\textsf {-Type}}}}(i):\mathcal {U}(\mathord {\textnormal {\textsf {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 \} }と定義する。