\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(B,C:A\to \mathcal {U}(i)\)を型の族、\(r:\prod _{x:A}\mathord {\textnormal {\textsf {Retract}}}(B(x),C(x))\)を要素とすると、\(\mathord {\textnormal {\textsf {Retract}}}(\sum _{x:A}B(x),\sum _{x:A}C(x))\)の要素を構成できる。
証明
仮定\(r\)から関数\(f:\prod _{\lbrace x:A\rbrace }B(x)\to C(x)\)と\(g:\prod _{\lbrace x:A\rbrace }C(x)\to B(x)\)と同一視\(p:\prod _{x:A}\prod _{y:B(x)}g(f(y))=y\)を得る。関数\(F:(\sum _{x:A}B(x))\to (\sum _{x:A}C(x))\)を\(\lambda z.\mathord {\textnormal {\textsf {pair}}}(\mathord {\textnormal {\textsf {proj}}}_{1}(z),f(\mathord {\textnormal {\textsf {proj}}}_{2}(z)))\)と定義する。関数\(G:(\sum _{x:A}C(x))\to (\sum _{x:A}B(x))\)も同様に\(g\)を使って定義される。同一視\(P:\prod _{z:\sum _{x:A}B(x)}G(F(z))=z\)を定義するために、\(z:\sum _{x:A}B(x)\)を仮定する。構成から\(\mathord {\textnormal {\textsf {proj}}}_{1}(G(F(z)))\equiv \mathord {\textnormal {\textsf {proj}}}_{1}(z)\)であり、\(p(\mathord {\textnormal {\textsf {proj}}}_{1}(z),\mathord {\textnormal {\textsf {proj}}}_{2}(z)):\mathord {\textnormal {\textsf {proj}}}_{2}(G(F(z)))=\mathord {\textnormal {\textsf {proj}}}_{2}(z)\)を得る。[001X]を使って、\(\mathord {\textnormal {\textsf {pair}}}(\mathord {\textnormal {\textsf {refl}}},p(\mathord {\textnormal {\textsf {proj}}}_{1}(z),\mathord {\textnormal {\textsf {proj}}}_{2}(z)))\)から\(G(F(z))=z\)の要素を構成できる。