関数外延性を仮定する。\(i\)を階数、\(C:\mathord {\textnormal {\textsf {PreCat}}}(i)\)を前圏とする。前圏\(\mathord {\textnormal {\textsf {Psh}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(C):\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))\)を次のように定義する。

• -\(\mathord {\textnormal {\textsf {Obj}}}\equiv \mathord {\textnormal {\textsf {Psh}}}(C)\)
• -\(\mathord {\textnormal {\textsf {Map}}}\equiv \lambda (A,B).\mathord {\textnormal {\textsf {Hom}}}(A,B)\)
• -恒等射と合成は[006L]の通りである。
• -前圏の公理は関数外延性から分かる。