[004N] 同値の概念

[0044]より、関数が同値であることは命題であることが分かったが、[004I]で導入した他の同値の概念が命題であることも示す。

まずは両側可逆性([004J])を考える。

関数外延性を仮定する。 $$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型、 $f:A\to B$ を関数とする。 $$f$$ は同値であると仮定して、次を示せ。

1任意の型 $X:\mathcal {U}(i)$ に対して、関数 $\lambda g.f\circ g:(X\to A)\to (X\to B)$ は同値である。
2任意の型 $Y:\mathcal {U}(i)$ に対して、関数 $\lambda h.h\circ f:(B\to Y)\to (A\to Y)$ は同値である。

関数外延性を仮定する。 $$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型、 $f:A\to B$ を関数とする。 $$f$$ が同値ならば、 $\mathord {\textnormal {\textsf {LInv}}}(f)$ と $\mathord {\textnormal {\textsf {RInv}}}(f)$ は可縮である。

証明

関数外延性から、レトラクト $\mathord {\textnormal {\textsf {RInv}}}(f)\triangleleft \mathord {\textnormal {\textsf {Fiber}}}(\lambda (g:B\to A).f\circ g,\mathord {\textnormal {\textsf {id}}})$ を得て、右辺は[004P]より可縮である。 $\mathord {\textnormal {\textsf {LInv}}}(f)$ についても同様である。

[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)$ が可縮であることが従う。

次に、半随伴同値([004L])を考える。

[004S] 補題

$$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型、 $f:A\to B$ を関数、 $a_{1},a_{2}:A$ を要素とする。 $$f$$ が同値ならば $\mathord {\textnormal {\textsf {ap}}}(f):a_{1}=a_{2}\to f(a_{1})=f(a_{2})$ は同値である。

証明

[004F]と[005R]から従う。

[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

{[001A]}

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

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