\(i\)を階数、\(A,B:\mathcal {U}(i)\)を型、\(r:\mathord {\textnormal {\textsf {Retract}}}(A,B)\)を要素とする。\(B\)が可縮ならば\(A\)も可縮である。
証明
\(d:\mathord {\textnormal {\textsf {IsContr}}}(B)\)と仮定する。要素\(a:A\)と\(p:\prod _{x:A}a=x\)を構成すればよい。仮定\(d\)から\(b:B\)と\(q:\prod _{y:B}b=y\)を得る。仮定\(r\)から\(f:B\to A\)と\(g:A\to B\)と\(t:\prod _{x:A}f(g(x))=x\)を得る。\(a\equiv f(b)\)と定義する。\(p\)を定義するために、\(x:A\)を仮定する。\(q(g(x)):b=g(x)\)と\(t(x):f(g(x))=x\)に注意して、\(p(x)\equiv t(x)\circ \mathord {\textnormal {\textsf {ap}}}(f,q(g(x)))\)と定義すればよい。