\(i\)を階数、\(C:\mathord {\textnormal {\textsf {PreCat}}}(i)\)を前圏とする。前圏\(\mathord {\textnormal {\textsf {Op}}}(C):\mathord {\textnormal {\textsf {PreCat}}}(i)\)を次のように定義する。

• -\(\mathord {\textnormal {\textsf {Obj}}}\equiv C.\mathord {\textnormal {\textsf {Obj}}}\)
• -\(\mathord {\textnormal {\textsf {Map}}}\equiv \lambda (x_{1},x_{2}).C.\mathord {\textnormal {\textsf {Map}}}(x_{2},x_{1})\)
• -\(\mathord {\textnormal {\textsf {id}}}\equiv \lambda x.C.\mathord {\textnormal {\textsf {id}}}\lbrace x\rbrace \)
• -\(\mathord {\textnormal {\textsf {comp}}}\equiv \lambda (x_{1},x_{2},x_{3}).\lambda (g:\mathord {\textnormal {\textsf {Map}}}(x_{2},x_{3}),f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})).C.\mathord {\textnormal {\textsf {comp}}}(f,g)\)
• -前圏の公理は\(C\)のそれから分かる。