一価性と関数外延性を仮定する。\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(a_{1},a_{2}:A\)を要素、\(n:\mathord {\textnormal {\textsf {TruncLevel}}}\)を要素とすると、同値\(({|a_{1}|}_{\mathord {\textnormal {\textsf {succ}}}(n)}={|a_{2}|}_{\mathord {\textnormal {\textsf {succ}}}(n)})\simeq {\| a_{1}=a_{2}\| }_{n}\)を構成できる。
証明
[0056]を型の族\(\lambda x.{\| a_{1}=x\| }_{n}:A\to \mathcal {U}(i)\)に適用すると、[001S]より、\({\| \sum _{x:A}{\| a_{1}=x\| }_{n}\| }_{\mathord {\textnormal {\textsf {succ}}}(n)}\)が可縮であることを示せば十分である。要素\(c_{1}:{\| \sum _{x:A}{\| a_{1}=x\| }_{n}\| }_{\mathord {\textnormal {\textsf {succ}}}(n)}\)を\({|\mathord {\textnormal {\textsf {pair}}}(a_{1},{|\mathord {\textnormal {\textsf {refl}}}|}_{n})|}_{\mathord {\textnormal {\textsf {succ}}}(n)}\)と定義する。任意の\(w:{\| \sum _{x:A}{\| a_{1}=x\| }_{n}\| }_{\mathord {\textnormal {\textsf {succ}}}(n)}\)に対して同一視\(c_{1}=w\)を構成する。[0052]よりこの同一視型は\(\mathord {\textnormal {\textsf {succ}}}(n)\)型なので、帰納法より任意の\(x:A\)と\(v:{\| a_{1}=x\| }_{n}\)に対して同一視\(c_{1}={|\mathord {\textnormal {\textsf {pair}}}(x,v)|}_{\mathord {\textnormal {\textsf {succ}}}(n)}\)を構成すればよい。この同一視型は定義から\(n\)型なので、帰納法より任意の\(x:A\)と\(y:a_{1}=x\)に対して同一視\(c_{1}={|\mathord {\textnormal {\textsf {pair}}}(x,{|y|}_{n})|}_{\mathord {\textnormal {\textsf {succ}}}(n)}\)を構成すればよいが、同一視型の帰納法で\(\mathord {\textnormal {\textsf {refl}}}\)を与えればよい。