[004I] 他の同値の概念

$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 \} }$と定義する。

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

$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))$

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

$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}}}$

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