関数外延性を仮定する。\(i\)を階数、\(C:\mathord {\textnormal {\textsf {PreCat}}}(i)\)を前圏とする。\(\mathord {\textnormal {\textsf {Psh}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(C)\)と\(\mathord {\textnormal {\textsf {Fun}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(\mathord {\textnormal {\textsf {Op}}}(C),\mathord {\textnormal {\textsf {Set}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(i))\)の間の前圏の同型を構成せよ。