[004U] -- ホモトピー型理論

$$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型、 $f:A\to B$ を関数とする。型 $\mathord {\textnormal {\textsf {IsEquiv}}}(f)$ と $\mathord {\textnormal {\textsf {QInv}}}(f)$ は論理的に同値である。

証明

$\mathord {\textnormal {\textsf {IsHAE}}}(f)\to \mathord {\textnormal {\textsf {QInv}}}(f)$ と $\mathord {\textnormal {\textsf {QInv}}}(f)\to \mathord {\textnormal {\textsf {IsBiinv}}}(f)$ は容易に示せるので、[004K]と[004M]を使う。