\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(B:A\to \mathcal {U}(i)\)を型の族、\(a:A\)を要素とする。\(A\)が可縮ならば\((\sum _{x:A}B(x))\mathrel {\triangleleft \triangleright }B(a)\)の要素を構成できる。
証明
\(A\)が可縮であると仮定する。[001L]より、関数\(p:\prod _{x:A}x=a\)を得る。関数\(f:(\sum _{x:A}B(x))\to B(a)\)を\(\lambda z.\mathord {\textnormal {\textsf {transport}}}(B,p(\mathord {\textnormal {\textsf {proj}}}_{1}(z)),\mathord {\textnormal {\textsf {proj}}}_{2}(z))\)と定義し、関数\(g:B(a)\to (\sum _{x:A}B(x))\)を\(\lambda y.\mathord {\textnormal {\textsf {pair}}}(a,y)\)と定義する。定義より、任意の\(z:\sum _{x:A}B(x)\)に対して、\(p(\mathord {\textnormal {\textsf {proj}}}_{1}(z)):\mathord {\textnormal {\textsf {proj}}}_{1}(z)=\mathord {\textnormal {\textsf {proj}}}_{1}(g(f(z)))\)と\(\mathord {\textnormal {\textsf {refl}}}:\mathord {\textnormal {\textsf {transport}}}(B,p(\mathord {\textnormal {\textsf {proj}}}_{1}(z)),\mathord {\textnormal {\textsf {proj}}}_{2}(z))=\mathord {\textnormal {\textsf {proj}}}_{2}(g(f(z)))\)を得るので、[001X]より同一視\(q:\prod _{z}g(f(z))=z\)を得る。また、[001L]より同一視\(r:p(a)=\mathord {\textnormal {\textsf {refl}}}\)も得られるので、同一視\(\lambda y.\mathord {\textnormal {\textsf {ap}}}(\lambda w.\mathord {\textnormal {\textsf {transport}}}(B,w,y),r):\prod _{y:B(a)}f(g(y))=y\)を得る。