\(i\)を階数、\(A,B:\mathcal {U}(i)\)を型、\(c_{1},c_{2}:A\times B\)を要素とする。同値\((c_{1}=c_{2})\simeq (\mathord {\textnormal {\textsf {proj}}}_{1}(c_{1})=\mathord {\textnormal {\textsf {proj}}}_{1}(c_{2}))\times (\mathord {\textnormal {\textsf {proj}}}_{2}(c_{1})=\mathord {\textnormal {\textsf {proj}}}_{2}(c_{2}))\)を構成しよう。[001S]を適用する。\(E:A\times B\to \mathcal {U}(i)\)を\(\lambda z.(\mathord {\textnormal {\textsf {proj}}}_{1}(c_{1})=\mathord {\textnormal {\textsf {proj}}}_{1}(z))\times (\mathord {\textnormal {\textsf {proj}}}_{2}(c_{1})=\mathord {\textnormal {\textsf {proj}}}_{2}(z))\)と定義する。要素\(\mathord {\textnormal {\textsf {pair}}}(\mathord {\textnormal {\textsf {refl}}},\mathord {\textnormal {\textsf {refl}}}):E(c_{1})\)を得る。レトラクトの列

\(\sum _{z:A\times B}E(z)\)\(\triangleleft \) {並び換え}\(\sum _{x:A}\sum _{p:\mathord {\textnormal {\textsf {proj}}}_{1}(c_{1})=x}\sum _{y:B}\mathord {\textnormal {\textsf {proj}}}_{2}(c_{1})=y\)\(\triangleleft \) {[001N]と[0025]}\(\sum _{y:B}\mathord {\textnormal {\textsf {proj}}}_{2}(c_{1})=y\) を得て、最後の型は[001N]により可縮なので、[001K]より\(\sum _{z:A\times B}E(z)\)も可縮である。