[002F] -- ホモトピー型理論

[002F] 命題

$$i$$ を階数、 $A,B,C,D:\mathcal {U}(i)$ を型、 $f:A\to B$ と $g:B\to C$ と $h:C\to D$ を関数とする。 $g\circ f$ と $h\circ g$ が同値ならば $$f$$ と $$g$$ と $$h$$ と $h\circ g\circ f$ も同値である。

証明

任意の要素 $$d:D$$ に対して、レトラクト

\mathord {\textnormal {\textsf {Fiber}}}(h\circ g\circ f,d)

\triangleleft

{[002L]}

\sum _{z:\mathord {\textnormal {\textsf {Fiber}}}(h,d)}\sum _{y:\mathord {\textnormal {\textsf {Fiber}}}(g,z.\mathord {\textnormal {\textsf {elem}}})}\mathord {\textnormal {\textsf {Fiber}}}(f,y.\mathord {\textnormal {\textsf {elem}}})

\triangleleft

{[002M]}

\sum _{z:\mathord {\textnormal {\textsf {Fiber}}}(h,d)}\sum _{y':\mathord {\textnormal {\textsf {Fiber}}}(g,z.\mathord {\textnormal {\textsf {elem}}})}\sum _{y:\mathord {\textnormal {\textsf {Fiber}}}(g,z.\mathord {\textnormal {\textsf {elem}}})}\mathord {\textnormal {\textsf {Fiber}}}(f,y.\mathord {\textnormal {\textsf {elem}}})

\triangleleft

{

h\circ g

が同値}

\sum _{y:\mathord {\textnormal {\textsf {Fiber}}}(g,\_)}\mathord {\textnormal {\textsf {Fiber}}}(f,y.\mathord {\textnormal {\textsf {elem}}})

を得て、最後の型は

g\circ f

が同値なので可縮である。よって、

h\circ g\circ f

は同値である。すると[002E]より残りの関数もすべて同値である。