[0041]より、\(\mathord {\textnormal {\textsf {IsContr}}}(A)\to \mathord {\textnormal {\textsf {IsContr}}}(\mathord {\textnormal {\textsf {IsContr}}}(A))\)を示せばよい。\(A\)が可縮であると仮定する。要素\(a_{0}:A\)を得る。レトラクトの列

\(\mathord {\textnormal {\textsf {IsContr}}}(A)\)\(\triangleleft \) {定義}\(\sum _{a:A}\prod _{x:A}a=x\)\(\triangleleft \) {\(A\)は可縮}\(\prod _{x:A}a_{0}=x\) を得て、最後の型は[001L]と[0029]より可縮である。