\(i\)を階数とする。
- -前圏\(C:\mathord {\textnormal {\textsf {PreCat}}}(i)\)に対して、型\(\mathord {\textnormal {\textsf {IsCat}}}(C):\mathcal {U}(i)\)を
\(\prod _{x:C}\mathord {\textnormal {\textsf {IsContr}}}(\sum _{y:C}x\cong y)\) と定義する。 - -型\(\mathord {\textnormal {\textsf {Cat}}}(i):\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))\)を\(\lbrace C:\mathord {\textnormal {\textsf {PreCat}}}(i)\mid \mathord {\textnormal {\textsf {IsCat}}}(C)\rbrace \)と定義する。