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

[004R] 命題

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

証明

[0041]より、 $$f$$ が半随伴同値であると仮定して $\mathord {\textnormal {\textsf {IsHAE}}}(f)$ が可縮であることを示せばよい。[004M]より $$f$$ は同値である。レトラクト

\mathord {\textnormal {\textsf {IsHAE}}}(f)

\triangleleft

{並び替え}

\sum _{g:B\to A}\sum _{\varepsilon :f\circ g\sim \mathord {\textnormal {\textsf {id}}}}\sum _{\eta :g\circ f\sim \mathord {\textnormal {\textsf {id}}}}\prod _{x:A}f(\eta (x))=\varepsilon (f(x))

\triangleleft

{[004Q]。可縮性から適当な

\(g\)

と

\varepsilon

を取れる。}

\sum _{\eta :g\circ f\sim \mathord {\textnormal {\textsf {id}}}}\prod _{x:A}f(\eta (x))=\varepsilon (f(x))

\triangleleft

\prod _{x:A}\sum _{p:g(f(x))=x}f(p)=\varepsilon (f(x))

を得て、最後の型は[004S]と[0029]より可縮である。