\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(E:A\to A\to \mathcal {U}(i)\)を型の族、\(r:\prod _{x:A}E(x,x)\)と\(f:\prod _{x_{1},x_{2}:A}E(x_{1},x_{2})\to x_{1}=x_{2}\)を関数とする。\(\prod _{x_{1},x_{2}:A}\mathord {\textnormal {\textsf {IsProp}}}(E(x_{1},x_{2}))\)の要素がある時、同値\(\prod _{x_{1}(x_{2},A)}(x_{1}=x_{2})\simeq E(x_{1},x_{2})\)を構成でき、特に\(A\)は集合である。
証明
\(r\)から同一視型の帰納法より関数\(g:\prod _{x_{1},x_{2}:A}x_{1}=x_{2}\to E(x_{1},x_{2})\)を得る。\(E(x_{1},x_{2})\)が命題であるという仮定から、\(f\)と\(g\)はレトラクト\(E(x_{1},x_{2})\triangleleft (x_{1}=x_{2})\)を定める。よって、[001S]より同値\((x_{1}=x_{2})\simeq E(x_{1},x_{2})\)を得る。