[007A] -- ホモトピー型理論

[007A] 補題

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $B:A\to \mathcal {U}(i)$ を型の族とすると、 $\prod _{x:A}B(x)$ は $\mathord {\textnormal {\textsf {Sect}}}(A,B)$ のレトラクトである。

証明

関数 $F:(\prod _{x:A}B(x))\to \mathord {\textnormal {\textsf {Sect}}}(A,B)$ を

\lambda f.\mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {elem}}}\equiv \lambda x.\mathord {\textnormal {\textsf {pair}}}(x,f(x)),\mathord {\textnormal {\textsf {id}}}\equiv \mathord {\textnormal {\textsf {refl}}}\mathclose {|\negmedspace \} }

と定義し、関数

G:\mathord {\textnormal {\textsf {Sect}}}(A,B)\to (\prod _{x:A}B(x))

を

\lambda z.\lambda x.\mathord {\textnormal {\textsf {transport}}}(\lambda g.B(g(x)),z.\mathord {\textnormal {\textsf {id}}},\mathord {\textnormal {\textsf {proj}}}_{2}(z.\mathord {\textnormal {\textsf {elem}}}(x)))

と定義すると、

G\circ F\equiv \mathord {\textnormal {\textsf {id}}}

である。