[001X] -- ホモトピー型理論

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $B:A\to \mathcal {U}(i)$ を型の族、 $c_{1},c_{2}:\sum _{x:A}B(x)$ を要素とすると、

\mathord {\textnormal {\textsf {Retract}}}(\sum _{z:\mathord {\textnormal {\textsf {proj}}}_{1}(c_{1})=\mathord {\textnormal {\textsf {proj}}}_{1}(c_{2})}\mathord {\textnormal {\textsf {transport}}}(B,z,\mathord {\textnormal {\textsf {proj}}}_{2}(c_{1}))=\mathord {\textnormal {\textsf {proj}}}_{2}(c_{2}),c_{1}=c_{2})

の要素を構成できる。

証明

関数 $f:(\sum _{z:\mathord {\textnormal {\textsf {proj}}}_{1}(c_{1})=\mathord {\textnormal {\textsf {proj}}}_{1}(c_{2})}\mathord {\textnormal {\textsf {transport}}}(B,z,\mathord {\textnormal {\textsf {proj}}}_{2}(c_{1}))=\mathord {\textnormal {\textsf {proj}}}_{2}(c_{2}))\to c_{1}=c_{2}$ と $g:c_{1}=c_{2}\to (\sum _{z:\mathord {\textnormal {\textsf {proj}}}_{1}(c_{1})=\mathord {\textnormal {\textsf {proj}}}_{1}(c_{2})}\mathord {\textnormal {\textsf {transport}}}(B,z,\mathord {\textnormal {\textsf {proj}}}_{2}(c_{1}))=\mathord {\textnormal {\textsf {proj}}}_{2}(c_{2}))$ と同一視 $p:\prod _{w}g(f(w))=w$ を構成する。 $$f$$ についてはカリー化、一般化して

f':\prod _{\lbrace x:A\rbrace }\prod _{\lbrace y:B(x)\rbrace }\prod _{z:\mathord {\textnormal {\textsf {proj}}}_{1}(c_{1})=x}\mathord {\textnormal {\textsf {transport}}}(B,z,\mathord {\textnormal {\textsf {proj}}}_{2}(c_{1}))=y\to c_{1}=\mathord {\textnormal {\textsf {pair}}}(x,y)

を構成すればよいが、同一視型の帰納法により

f'(\mathord {\textnormal {\textsf {refl}}},\mathord {\textnormal {\textsf {refl}}})\equiv \mathord {\textnormal {\textsf {refl}}}

と定義できる。

\(g\)

は一般化して

g':\prod _{\lbrace y:\sum _{x:A}B(x)\rbrace }c_{1}=y\to (\sum _{z:\mathord {\textnormal {\textsf {proj}}}_{1}(c_{1})=\mathord {\textnormal {\textsf {proj}}}_{1}(y)}\mathord {\textnormal {\textsf {transport}}}(B,z,\mathord {\textnormal {\textsf {proj}}}_{2}(c_{1}))=\mathord {\textnormal {\textsf {proj}}}_{2}(y))

を帰納法で

g'(\mathord {\textnormal {\textsf {refl}}})\equiv \mathord {\textnormal {\textsf {pair}}}(\mathord {\textnormal {\textsf {refl}}},\mathord {\textnormal {\textsf {refl}}})

と定義する。

\(p\)

も

\(f\)

と同様にカリー化、一般化して

p':\prod _{\lbrace x\rbrace }\prod _{\lbrace y\rbrace }\prod _{z:\mathord {\textnormal {\textsf {proj}}}_{1}(c_{1})=x}\prod _{w:\mathord {\textnormal {\textsf {transport}}}(B,z,\mathord {\textnormal {\textsf {proj}}}_{2}(c_{1}))=y}g'(f'(z,w))=\mathord {\textnormal {\textsf {pair}}}(z,w)

を帰納法により

p'(\mathord {\textnormal {\textsf {refl}}},\mathord {\textnormal {\textsf {refl}}})\equiv \mathord {\textnormal {\textsf {refl}}}

と定義する。