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

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $n:\mathord {\textnormal {\textsf {TruncLevel}}}$ を要素とする。次は論理的に同値である。

1 $$A$$ は $$n$$ 型である。
2関数 $\lambda x.{|x|}_{n}:A\to {\| A\| }_{n}$ は同値である。
3 $$A$$ は ${\| A\| }_{n}$ のレトラクトである。

証明

2から3は自明である。3から1は[0045]による。

1から2を示す。 $$A$$ が $$n$$ 型なので、帰納法より関数 $g:{\| A\| }_{n}\to A$ であって任意の $$a:A$$ に対して $g({|a|}_{n})\equiv a$ となるものを構成できる。特に、 $g\circ (\lambda x.{|x|}_{n})\sim \mathord {\textnormal {\textsf {id}}}$ である。 $(\lambda x.{|x|}_{n})\circ g\sim \mathord {\textnormal {\textsf {id}}}$ を示す。各 $z:{\| A\| }_{n}$ に対して ${|g(z)|}_{n}=z$ は[0052]より $$n$$ 型なので、帰納法により $\prod _{x:A}{|g({|x|}_{n})|}_{n}={|x|}_{n}$ を示せばよいがこれは定義から明らかである。