関数外延性と一価性を仮定する。\(i\)を階数、\(C:\mathord {\textnormal {\textsf {PreCat}}}(i)\)を前圏とすると、\(\mathord {\textnormal {\textsf {Psh}}}(C)\)は圏である。