[0064] 系(圏の構造同一原理)一価性と関数外延性を仮定する。\(i\)を階数、\(C,D:\mathord {\textnormal {\textsf {Cat}}}(i)\)を圏とすると、同値 \((C=D)\simeq \lbrace F:\mathord {\textnormal {\textsf {Fun}}}(C,D)\mid \mathord {\textnormal {\textsf {IsWCatEquiv}}}(F)\rbrace \) を得る。