\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(P,B:A\to \mathcal {U}(i)\)を型の族、\(c:\sum _{x:A}P(x)\)を要素、\(b:B(\mathord {\textnormal {\textsf {proj}}}_{1}(c))\)を要素とする。\(\prod _{x:A}\mathord {\textnormal {\textsf {IsProp}}}(P(x))\)の要素があり、\(\sum _{x:A}B(x)\)は可縮であるならば、\(\sum _{z:\sum _{x:A}P(x)}B(\mathord {\textnormal {\textsf {proj}}}_{1}(z))\)は可縮である。
証明
並び換えによりレトラクト\((\sum _{z:\sum _{x:A}P(x)}B(\mathord {\textnormal {\textsf {proj}}}_{1}(z)))\triangleleft (\sum _{z:\sum _{x:A}B(x)}P(\mathord {\textnormal {\textsf {proj}}}_{1}(z)))\)を得る。後者は[004F]と[004X]より命題であり、要素\(\mathord {\textnormal {\textsf {pair}}}(\mathord {\textnormal {\textsf {pair}}}(\mathord {\textnormal {\textsf {proj}}}_{1}(c),b),\mathord {\textnormal {\textsf {proj}}}_{2}(c))\)を持つので、[0041]より可縮である。