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

[004X] 命題

$i$ を階数、 $A:\mathcal {U}(i)$ を型、 $B:A\to \mathcal {U}(i)$ を型の族、 $n:\mathord {\textnormal {\textsf {TruncLevel}}}$ を要素とする。 $A$ が $n$ 型で、任意の $x:A$ に対して $B(x)$ が $n$ 型ならば、 $\sum _{x:A}B(x)$ も $n$ 型である。

証明

$n$ についての帰納法による。 $n$ が $-2$ の場合は容易である。

$n$ の場合に主張が成り立つと仮定し、 $\mathord {\textnormal {\textsf {succ}}}(n)$ の場合を示す。 $c_{1},c_{2}:\sum _{x:A}B(x)$ に対し、 $c_{1}=c_{2}$ が $n$ 型であることを示す。[002B]より、同値

(c_{1}=c_{2})\simeq (\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}))

を得る。仮定より、

\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})

は

n

型である。よって、帰納法の仮定を適用すればよい。