\(i\)を階数、\(A:\mathcal {U}(i)\)を型とする。型\(\mathord {\textnormal {\textsf {IsSet}}}(A):\mathcal {U}(i)\)を\(\mathord {\textnormal {\textsf {IsTrunc}}}(0,A)\)と定義する。\(\mathord {\textnormal {\textsf {IsSet}}}(A)\)の要素がある時、\(A\)は集合(set)であると言う。