一価性と関数外延性を仮定する。\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(B:A\to \mathcal {U}(i)\)を型の族、\(n:\mathord {\textnormal {\textsf {TruncLevel}}}\)を要素とする。任意の\(x:A\)に対して\(B(x)\)は\(n\)型であると仮定する。[0054]より、帰納法で型の族\(T:{\| A\| }_{\mathord {\textnormal {\textsf {succ}}}(n)}\to \mathcal {U}(i)\)であって、任意の\(u:{\| A\| }_{\mathord {\textnormal {\textsf {succ}}}(n)}\)に対して\(T(u)\)は\(n\)型であり、任意の\(x:A\)に対して\(T({|x|}_{\mathord {\textnormal {\textsf {succ}}}(n)})\equiv B(x)\)であるものを構成できる。[004X]と[004F]より\(\sum _{u:{\| A\| }_{\mathord {\textnormal {\textsf {succ}}}(n)}}T(u)\)は\(\mathord {\textnormal {\textsf {succ}}}(n)\)型なので、関数\(\lambda z.\mathord {\textnormal {\textsf {pair}}}({|\mathord {\textnormal {\textsf {proj}}}_{1}(z)|}_{\mathord {\textnormal {\textsf {succ}}}(n)},\mathord {\textnormal {\textsf {proj}}}_{2}(z)):(\sum _{x:A}B(x))\to (\sum _{u:{\| A\| }_{\mathord {\textnormal {\textsf {succ}}}(n)}}T(u))\)は関数
証明
\(\sum _{u:{\| A\| }_{\mathord {\textnormal {\textsf {succ}}}(n)}}T(u)\)が\({\| \sum _{x:A}B(x)\| }_{\mathord {\textnormal {\textsf {succ}}}(n)}\)と同じ帰納法原理を満たすことを見る。\(C:(\sum _{u:{\| A\| }_{\mathord {\textnormal {\textsf {succ}}}(n)}}T(u))\to \mathcal {U}(i)\)を型の族とし、各\(C(u)\)は\(\mathord {\textnormal {\textsf {succ}}}(n)\)型であると仮定する。\(f:\prod _{z:\sum _{x:A}B(x)}C(\mathord {\textnormal {\textsf {pair}}}({|z|}_{\mathord {\textnormal {\textsf {succ}}}(n)},\mathord {\textnormal {\textsf {proj}}}_{2}(z)))\)を関数とする。\(D:\prod _{u:{\| A\| }_{\mathord {\textnormal {\textsf {succ}}}(n)}}T(u)\to \mathcal {U}(i)\)を\(C\)のカリー化、\(g:\prod _{x:A}\prod _{y:B(x)}D({|x|}_{\mathord {\textnormal {\textsf {succ}}}(n)},y)\)を\(f\)のカリー化とする。[0048]より各\(\prod _{v:T(u)}D(u,v)\)は\(\mathord {\textnormal {\textsf {succ}}}(n)\)型なので、帰納法で関数\(h:\prod _{u:{\| A\| }_{\mathord {\textnormal {\textsf {succ}}}(n)}}\prod _{v:T(u)}D(u,v)\)を得る。\(h\)を逆カリー化すればよい。