関数外延性を仮定する。\(i\)を階数、\(C,D,X:\mathord {\textnormal {\textsf {PreCat}}}(i)\)を前圏とする。同値

\(\mathord {\textnormal {\textsf {Fun}}}(X,\mathord {\textnormal {\textsf {Fun}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(C,D))\simeq \mathord {\textnormal {\textsf {BiFun}}}(C,X;D)\) を構成せよ。