\(i\)を階数、\(C:\mathord {\textnormal {\textsf {PreCat}}}(i)\)を前圏、\(x_{1},x_{2}:C\)を対象とする。型\(x_{1}\cong x_{2}:\mathcal {U}(i)\)を\(\lbrace f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})\mid \mathord {\textnormal {\textsf {IsIso}}}(f)\rbrace \)と定義する。