ホモトピー型理論
[004J] 定義

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

  • -LInv(f):U(i)\mathord {\textnormal {\textsf {LInv}}}(f):\mathcal {U}(i)Record{ ⁣inv:BA,is-linv:invfid ⁣}\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 \} }と定義する。
  • -RInv(f):U(i)\mathord {\textnormal {\textsf {RInv}}}(f):\mathcal {U}(i)Record{ ⁣inv:BA,is-rinv:finvid ⁣}\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 \} }と定義する。
  • -IsBiinv(f):U(i)\mathord {\textnormal {\textsf {IsBiinv}}}(f):\mathcal {U}(i)Record{ ⁣linv:LInv(f),rinv:RInv(f) ⁣}\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 \} }と定義する。
IsBiinv(f)\mathord {\textnormal {\textsf {IsBiinv}}}(f)の要素がある時、ff両側可逆(biinvertible)であると言う。