[004O] 命題関数外延性を仮定する。\(i\)を階数、\(A,B:\mathcal {U}(i)\)を型、\(f:A\to B\)を関数とすると、型\(\mathord {\textnormal {\textsf {IsBiinv}}}(f)\)は命題である。証明[0041]より、\(f\)が両側可逆であると仮定して\(\mathord {\textnormal {\textsf {IsBiinv}}}(f)\)が可縮であることを示せばよいが、[004K]より\(f\)は同値なので、[004Q]から\(\mathord {\textnormal {\textsf {IsBiinv}}}(f)\)が可縮であることが従う。