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

[0045] 命題

$$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型、 $r:\mathord {\textnormal {\textsf {Retract}}}(A,B)$ と $n:\mathord {\textnormal {\textsf {TruncLevel}}}$ を要素とする。 $$B$$ が $$n$$ 型ならば、 $$A$$ も $$n$$ 型である。

証明

$$n$$ についての帰納法による。 $$n$$ が $$-2$$ の時は[001K]による。

$$n$$ について主張が成り立つと仮定し、 $\mathord {\textnormal {\textsf {succ}}}(n)$ の場合を示す。 $x_{1},x_{2}:A$ に対して、 $\mathord {\textnormal {\textsf {IsTrunc}}}(n,x_{1}=x_{2})$ を示せばよいが、[0046]と帰納法の仮定から直ちに従う。