ホモトピー型理論
[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]と帰納法の仮定から直ちに従う。