関数外延性を仮定する。\(i\)を階数、\(A,B:\mathcal {U}(i)\)を型、\(f:A\to B\)を関数とする。\(f\)が同値ならば、\(\mathord {\textnormal {\textsf {LInv}}}(f)\)と\(\mathord {\textnormal {\textsf {RInv}}}(f)\)は可縮である。
証明
関数外延性から、レトラクト\(\mathord {\textnormal {\textsf {RInv}}}(f)\triangleleft \mathord {\textnormal {\textsf {Fiber}}}(\lambda (g:B\to A).f\circ g,\mathord {\textnormal {\textsf {id}}})\)を得て、右辺は[004P]より可縮である。\(\mathord {\textnormal {\textsf {LInv}}}(f)\)についても同様である。