\(i\)を階数とする。型\(\mathord {\textnormal {\textsf {PreCat}}}(i):\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))\)を次のレコード型と定義する。

• -対象(object)の型\(\mathord {\textnormal {\textsf {Obj}}}:\mathcal {U}(i)\)
• -射(morphism)の型の族\(\mathord {\textnormal {\textsf {Map}}}:\mathord {\textnormal {\textsf {Obj}}}\to \mathord {\textnormal {\textsf {Obj}}}\to \mathcal {U}(i)\)
• -恒等射(identity)\(\mathord {\textnormal {\textsf {id}}}:\prod _{\lbrace x:\mathord {\textnormal {\textsf {Obj}}}\rbrace }\mathord {\textnormal {\textsf {Map}}}(x,x)\)
• -射の合成(composition)\(\mathord {\textnormal {\textsf {comp}}}:\prod _{\lbrace x_{1},x_{2},x_{3}:\mathord {\textnormal {\textsf {Obj}}}\rbrace }\mathord {\textnormal {\textsf {Map}}}(x_{2},x_{3})\to \mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})\to \mathord {\textnormal {\textsf {Map}}}(x_{1},x_{3})\)
• -\(\_:\prod _{x_{1},x_{2}:\mathord {\textnormal {\textsf {Obj}}}}\mathord {\textnormal {\textsf {IsSet}}}(\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2}))\)
• -\(\_:\prod _{x_{1},x_{2}:\mathord {\textnormal {\textsf {Obj}}}}\prod _{f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})}\mathord {\textnormal {\textsf {comp}}}(\mathord {\textnormal {\textsf {id}}},f)=f\)
• -\(\_:\prod _{x_{1},x_{2}:\mathord {\textnormal {\textsf {Obj}}}}\prod _{f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})}\mathord {\textnormal {\textsf {comp}}}(f,\mathord {\textnormal {\textsf {id}}})=f\)
• -\(\_:\prod _{x_{1},x_{2},x_{3},x_{4}:\mathord {\textnormal {\textsf {Obj}}}}\prod _{f_{1}:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})}\prod _{f_{2}:\mathord {\textnormal {\textsf {Map}}}(x_{2},x_{3})}\prod _{f_{3}:\mathord {\textnormal {\textsf {Map}}}(x_{3},x_{4})}\mathord {\textnormal {\textsf {comp}}}(\mathord {\textnormal {\textsf {comp}}}(f_{3},f_{2}),f_{1})=\mathord {\textnormal {\textsf {comp}}}(f_{3},\mathord {\textnormal {\textsf {comp}}}(f_{2},f_{1}))\)

\(\mathord {\textnormal {\textsf {PreCat}}}(i)\)の要素を(階数\(i\)の)前圏(precategory)と呼ぶ。