関数外延性を仮定する。\(i\)を階数、\(A,B:\mathord {\textnormal {\textsf {Set}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(i)\)を対象、\(f:\mathord {\textnormal {\textsf {Map}}}(A,B)\)を射とする。次は論理的に同値である。

1. 1\(f\)は\(\mathord {\textnormal {\textsf {Set}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(i)\)の射として同型である。
2. 2\(f\)は関数として同値である。