ホモトピー型理論
[006J] 定理

関数外延性と一価性を仮定する。\(i\)を階数とすると、\(\mathord {\textnormal {\textsf {Set}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(i)\)は圏である。

証明

対象\(A,B:\mathord {\textnormal {\textsf {Set}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(i)\)に対して、[006I]より\((A\cong B)\simeq (A\simeq B)\)を得て、一価性と[0049]より\((A\simeq B)\simeq (A=B)\)を得る。