\(i\)を階数、\(A:\mathcal {U}(i)\)を型とする。型\(\mathord {\textnormal {\textsf {IsProp}}}(A):\mathcal {U}(i)\)を\(\mathord {\textnormal {\textsf {IsTrunc}}}(-1,A)\)と定義する。\(\mathord {\textnormal {\textsf {IsProp}}}(A)\)の要素がある時、\(A\)は命題(proposition)であると言う。