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

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