ホモトピー型理論
[004M] 演習

\(i\)を階数、\(A,B:\mathcal {U}(i)\)を型、\(f:A\to B\)を関数とする。型\(\mathord {\textnormal {\textsf {IsEquiv}}}(f)\)\(\mathord {\textnormal {\textsf {IsHAE}}}(f)\)は論理的に同値であることを示せ。(ヒント:[002H]の証明を拡張すれば\(\mathord {\textnormal {\textsf {IsEquiv}}}(f)\to \mathord {\textnormal {\textsf {IsHAE}}}(f)\)を示せる。)