ホモトピー型理論
[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 \)
を得る。