[006Z] -- ホモトピー型理論

[006Z] 補題

$$i$$ を階数、 $C,D:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏、 $F:\mathord {\textnormal {\textsf {Fun}}}(C,D)$ を関手、 $$y:D$$ を対象とする。 $$C$$ が圏で、 $$F$$ が充満忠実ならば、 $\mathord {\textnormal {\textsf {Fiber}}}^{\cong }(F,y)$ は命題である。

証明

[0041]を適用し、 $a:\mathord {\textnormal {\textsf {Fiber}}}^{\cong }(F,y)$ を仮定して $\mathord {\textnormal {\textsf {Fiber}}}^{\cong }(F,y)$ が可縮であることを示す。レトラクト

\mathord {\textnormal {\textsf {Fiber}}}^{\cong }(F,y)

\triangleleft

{定義}

\sum _{x:C}F(x)\cong y

\triangleleft

{

a.\mathord {\textnormal {\textsf {iso}}}

と合成}

\sum _{x:C}F(a.\mathord {\textnormal {\textsf {obj}}})\cong F(x)

\triangleleft

{[0060]と[0061]}

\sum _{x:C}a.\mathord {\textnormal {\textsf {obj}}}\cong x

を得て、最後の型は

\(C\)

が圏なので可縮である。