[004I] 他の同値の概念

[001Q]の他にも同値の概念の定義はある。

$$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型、 $f:A\to B$ を関数とする。

-型 $\mathord {\textnormal {\textsf {LInv}}}(f):\mathcal {U}(i)$ を $\mathord {\textnormal {\textsf {Record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {inv}}}:B\to A,\mathord {\textnormal {\textsf {is-linv}}}:\mathord {\textnormal {\textsf {inv}}}\circ f\sim \mathord {\textnormal {\textsf {id}}}\mathclose {|\negmedspace \} }$ と定義する。
-型 $\mathord {\textnormal {\textsf {RInv}}}(f):\mathcal {U}(i)$ を $\mathord {\textnormal {\textsf {Record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {inv}}}:B\to A,\mathord {\textnormal {\textsf {is-rinv}}}:f\circ \mathord {\textnormal {\textsf {inv}}}\sim \mathord {\textnormal {\textsf {id}}}\mathclose {|\negmedspace \} }$ と定義する。
-型 $\mathord {\textnormal {\textsf {IsBiinv}}}(f):\mathcal {U}(i)$ を $\mathord {\textnormal {\textsf {Record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {linv}}}:\mathord {\textnormal {\textsf {LInv}}}(f),\mathord {\textnormal {\textsf {rinv}}}:\mathord {\textnormal {\textsf {RInv}}}(f)\mathclose {|\negmedspace \} }$ と定義する。

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

の要素がある時、

\(f\)

は両側可逆(biinvertible)であると言う。

[004K] 命題

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

証明

[0026]と[002G]と[002F]と[002H]から従う。

[004J]の利点は比較的低級な概念で定義できる点である。この定義で使われている概念は恒等関数、合成、ホモトピーだけである。これらの概念は一般の高次圏で意味をなすものであり、実際、高次圏での同値は両側可逆性で定義できる。一方、ファイバーや可縮性には型理論の言語が本質的に使われている。ただ、[004J]から直接取り出せる情報はそれほど有益でなく、逆関数の取り方も二種類あるので使い勝手が良いとは言えない。

[004L] 定義

$$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型、 $f:A\to B$ を関数とする。型 $\mathord {\textnormal {\textsf {IsHAE}}}(f):\mathcal {U}(i)$ を次のレコード型と定義する。

- $\mathord {\textnormal {\textsf {inv}}}:B\to A$
- $\mathord {\textnormal {\textsf {unit}}}:\mathord {\textnormal {\textsf {inv}}}\circ f\sim \mathord {\textnormal {\textsf {id}}}$
- $\mathord {\textnormal {\textsf {counit}}}:f\circ \mathord {\textnormal {\textsf {inv}}}\sim \mathord {\textnormal {\textsf {id}}}$
- $\mathord {\textnormal {\textsf {coh}}}:\prod _{x:A}f(\mathord {\textnormal {\textsf {unit}}}(x))=\mathord {\textnormal {\textsf {counit}}}(f(x))$

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

の要素がある時、

\(f\)

は半随伴同値(half adjoint equivalence)であると言う。

[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)$ を示せる。)

[004L]は[004J]と比べて有益な情報が多い。その分、その定義には一つ高次の同一視( $\mathord {\textnormal {\textsf {coh}}}$ )を使う。

次の[004T]も同値の概念を定義しているように見えるかもしれないが、これは正しい同値の定義ではない。

[004T] 定義

$$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型、 $f:A\to B$ を関数とする。型 $\mathord {\textnormal {\textsf {QInv}}}(f):\mathcal {U}(i)$ を次のレコード型と定義する。

- $\mathord {\textnormal {\textsf {inv}}}:B\to A$
- $\mathord {\textnormal {\textsf {unit}}}:\mathord {\textnormal {\textsf {inv}}}\circ f\sim \mathord {\textnormal {\textsf {id}}}$
- $\mathord {\textnormal {\textsf {counit}}}:f\circ \mathord {\textnormal {\textsf {inv}}}\sim \mathord {\textnormal {\textsf {id}}}$

[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]を使う。

[004U]により、関数 $$f$$ が同値であることを示す目的では $\mathord {\textnormal {\textsf {QInv}}}(f)$ を使って何も問題はない。 $\mathord {\textnormal {\textsf {QInv}}}(f)$ が他に挙げた正しい同値の概念と決定的に違うのは、同一でない二つの $\mathord {\textnormal {\textsf {QInv}}}(f)$ の要素がありうる点である。後に示すが、(関数外延性の下で) $\mathord {\textnormal {\textsf {IsEquiv}}}(f)$ と $\mathord {\textnormal {\textsf {IsBiinv}}}(f)$ と $\mathord {\textnormal {\textsf {IsHAE}}}(f)$ はいずれも任意の二つの要素が同一視される([0044]と[004O]と[004R])。 $\mathord {\textnormal {\textsf {QInv}}}(f)$ についてはこの性質は示せないどころか、一価性公理の下で $\mathord {\textnormal {\textsf {QInv}}}(f)$ が同一でない二つの要素を持つような $$f$$ を構成できることが知られている。