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

• -\(\mathord {\textnormal {\textsf {Obj}}}\equiv \mathord {\textnormal {\textsf {Fun}}}(C,D)\)
• -\(\mathord {\textnormal {\textsf {Map}}}\equiv \lambda (F,G).\mathord {\textnormal {\textsf {NatTrans}}}(F,G)\)
• -恒等射と合成は[0067]の通り。
• -残りは[0068]から容易に示せる。