\(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)であると言う。