関数外延性を仮定する。\(i\)を階数、\(C:\mathord {\textnormal {\textsf {PreCat}}}(i)\)を前圏、\(A:\mathord {\textnormal {\textsf {Psh}}}(C)\)を前層とする。\(C\)が圏ならば、\(\mathord {\textnormal {\textsf {IsRepr}}}(A)\)は命題である。