\(i\)を階数、\(C:\mathord {\textnormal {\textsf {PreCat}}}(i)\)を前圏、\(x_{1},x_{2}:C\)を対象、\(f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})\)を射とする。
- -型\(\mathord {\textnormal {\textsf {LInv}}}(f):\mathcal {U}(i)\)を\(\mathord {\textnormal {\textsf {Record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {inv}}}:\mathord {\textnormal {\textsf {Map}}}(x_{2},x_{1}),\mathord {\textnormal {\textsf {id}}}:\mathord {\textnormal {\textsf {inv}}}\circ f=\mathord {\textnormal {\textsf {id}}}\mathclose {|\negmedspace \} }\)と定義する。
- -型\(\mathord {\textnormal {\textsf {RInv}}}(f):\mathcal {U}(i)\)を\(\mathord {\textnormal {\textsf {Record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {inv}}}:\mathord {\textnormal {\textsf {Map}}}(x_{2},x_{1}),\mathord {\textnormal {\textsf {id}}}:f\circ \mathord {\textnormal {\textsf {inv}}}=\mathord {\textnormal {\textsf {id}}}\mathclose {|\negmedspace \} }\)と定義する。
- -型\(\mathord {\textnormal {\textsf {IsIso}}}(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 \} }\)と定義する。