\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(B:A\to \mathcal {U}(i)\)を型の族、\(c_{1},c_{2}:\sum _{x:A}B(x)\)を要素とする。\(\prod _{x:A}\mathord {\textnormal {\textsf {IsProp}}}(B(x))\)の要素があるならば、同値\((c_{1}=c_{2})\simeq (\mathord {\textnormal {\textsf {proj}}}_{1}(c_{1})=\mathord {\textnormal {\textsf {proj}}}_{1}(c_{2}))\)を得る。