関数外延性を仮定する。\(i\)を階数、\(A,B:\mathcal {U}(i)\)を型、\(f:A\to B\)を関数とすると、\(\mathord {\textnormal {\textsf {IsEquiv}}}(f)\)は命題である。