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

1. 1\(f\)は\(\mathord {\textnormal {\textsf {Psh}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(C)\)の射として同型である。
2. 2任意の対象\(x:C\)に対して、関数\(\lambda a.f(a):A(x)\to B(x)\)は同値である。