関数外延性を仮定する。\(i\)を階数、\(C:\mathord {\textnormal {\textsf {PreCat}}}(i)\)を前圏とする。米田埋め込み\(\mathord {\textnormal {\textsf {よ}}}(C):\mathord {\textnormal {\textsf {Fun}}}(C,\mathord {\textnormal {\textsf {Psh}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(C))\)は充満忠実である。
証明
\(x_{1},x_{2}:C\)を対象とする。関数\(\lambda f.\mathord {\textnormal {\textsf {よ}}}(C)(f):\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})\to \mathord {\textnormal {\textsf {Map}}}(\mathord {\textnormal {\textsf {よ}}}(C)(x_{1}),\mathord {\textnormal {\textsf {よ}}}(C)(x_{2}))\)と\(\lambda h.h(\mathord {\textnormal {\textsf {gen}}}(x_{1})):\mathord {\textnormal {\textsf {Map}}}(\mathord {\textnormal {\textsf {よ}}}(C)(x_{1}),\mathord {\textnormal {\textsf {よ}}}(C)(x_{2}))\to \mathord {\textnormal {\textsf {よ}}}(C)(x_{2})(x_{1})\)の合成は\(\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})\)上の恒等関数と同一であることが分かる。よって、[002E]と[006T]から\(\lambda f.\mathord {\textnormal {\textsf {よ}}}(C)(f)\)は同値である。