\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(B:A\to \mathcal {U}(i)\)を型の族とする。\(\prod _{x:A}\mathord {\textnormal {\textsf {IsContr}}}(B(x))\)の要素があるならば、関数\(\lambda z.\mathord {\textnormal {\textsf {proj}}}_{1}(z):(\sum _{x:A}B(x))\to A\)は同値である。