ホモトピー型理論
[0075] 補題

\(i\)を階数、\(C,D:\mathord {\textnormal {\textsf {PreCat}}}(i)\)を前圏、\(F:\mathord {\textnormal {\textsf {Fun}}}(C,D)\)を関手とする。\(D\)が圏で、\(F\)が本質的全射ならば、\(F.\mathord {\textnormal {\textsf {obj}}}:C.\mathord {\textnormal {\textsf {Obj}}}\to D.\mathord {\textnormal {\textsf {Obj}}}\)は全射である。

証明

定義からすぐである。