[0029]を適用する。\(A:\mathcal {U}(i)\)を型、\(B:A\to \mathcal {U}(i)\)を型の族とし、各\(B(x)\)は可縮であると仮定する。[007C]より、関数\(\lambda z.\mathord {\textnormal {\textsf {proj}}}_{1}(z):(\sum _{x:A}B(x))\to A\)は同値である。これと[007B]より、\(\mathord {\textnormal {\textsf {Sect}}}(A,B)\)は可縮である。したがって、[007A]と[001K]より\(\prod _{x:A}B(x)\)は可縮である。