一価性と関数外延性を仮定する。\(i\)を階数、\(C,D:\mathord {\textnormal {\textsf {PreCat}}}(i)\)を前圏とする。同値

\((C=D)\simeq \lbrace F:\mathord {\textnormal {\textsf {Fun}}}(C,D)\mid \mathord {\textnormal {\textsf {IsIso}}}(F)\rbrace \)を構成せよ。