関数外延性を仮定する。\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(n:\mathord {\textnormal {\textsf {TruncLevel}}}\)を要素とすると、\(\mathord {\textnormal {\textsf {IsTrunc}}}(n,A)\)は命題である。