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

[002E] 補題

$$i$$ を階数、 $A,B,C:\mathcal {U}(i)$ を型、 $f:A\to B$ と $g:B\to C$ を関数とする。 $$f$$ と $$g$$ と $g\circ f$ のうちいずれか二つが同値ならば残りの一つも同値である。つまり、次の型の要素を構成できる。

- $\mathord {\textnormal {\textsf {IsEquiv}}}(f)\to \mathord {\textnormal {\textsf {IsEquiv}}}(g)\to \mathord {\textnormal {\textsf {IsEquiv}}}(g\circ f)$
- $\mathord {\textnormal {\textsf {IsEquiv}}}(f)\to \mathord {\textnormal {\textsf {IsEquiv}}}(g\circ f)\to \mathord {\textnormal {\textsf {IsEquiv}}}(g)$
- $\mathord {\textnormal {\textsf {IsEquiv}}}(g)\to \mathord {\textnormal {\textsf {IsEquiv}}}(g\circ f)\to \mathord {\textnormal {\textsf {IsEquiv}}}(f)$

証明

$$f$$ が同値であると仮定すると、[002L]と[001K]から $\mathord {\textnormal {\textsf {IsEquiv}}}(g)\leftrightarrow \mathord {\textnormal {\textsf {IsEquiv}}}(g\circ f)$ が従う。

$$g$$ と $g\circ f$ が同値であると仮定する。 $$b:B$$ を仮定する。 $r:\mathord {\textnormal {\textsf {Fiber}}}(g,g(b))$ を $\mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {elem}}}\equiv b,\mathord {\textnormal {\textsf {id}}}\equiv \mathord {\textnormal {\textsf {refl}}}\mathclose {|\negmedspace \} }$ と定義する。レトラクト

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

\mathrel {\triangleleft \triangleright }

{[002L]}

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

\mathrel {\triangleleft \triangleright }

{

\(g\)

が同値}

\mathord {\textnormal {\textsf {Fiber}}}(f,r.\mathord {\textnormal {\textsf {elem}}})

を得て、

r.\mathord {\textnormal {\textsf {elem}}}\equiv b

であることに注意すると、

g\circ f

が同値なので

\mathord {\textnormal {\textsf {Fiber}}}(f,b)

は可縮である。