[0054] -- ホモトピー型理論

[0054] 命題

一価性と関数外延性を仮定する。 $$i$$ を階数、 $n:\mathord {\textnormal {\textsf {TruncLevel}}}$ を要素とする。 $\mathord {\langle n\rangle \mathord {\textnormal {\textsf {-Type}}}}(i)$ は $\mathord {\textnormal {\textsf {succ}}}(n)$ 型である。

証明

$A,B:\mathord {\langle n\rangle \mathord {\textnormal {\textsf {-Type}}}}(i)$ を要素とする。一価性と[0049]と[0043]より、同値 $(A=B)\simeq (A.\mathord {\textnormal {\textsf {Type}}}\simeq B.\mathord {\textnormal {\textsf {Type}}})$ を得て、後者は[0048]と[004X]と[0052]から $$n$$ 型である。