ホモトピー型理論
[005P] 定理

\(i\)を階数、\(C,D:\mathord {\textnormal {\textsf {PreCat}}}(i)\)を前圏、\(F:\mathord {\textnormal {\textsf {Fun}}}(C,D)\)を関手とする。\(C\)\(D\)が圏ならば、次は論理的に同値である。

  1. 1\(F\)は前圏の同型である。
  2. 2\(F\)は弱圏同値である。

証明

1から2は自明である。

2から1を示す。\(F.\mathord {\textnormal {\textsf {obj}}}:C.\mathord {\textnormal {\textsf {Obj}}}\to D.\mathord {\textnormal {\textsf {Obj}}}\)が同値であることを示せばよいが、これは[005X][0063][0074][0075]から従う。