\(i\)を階数、\(A:\mathcal {U}(i)\)を型とする。関数\(\lambda z.\mathord {\textnormal {\textsf {proj}}}_{1}(z):(\sum _{x_{1},x_{2}:A}x_{1}=x_{2})\to A\)は同値である。
\(i\)を階数、\(A:\mathcal {U}(i)\)を型とする。関数\(\lambda z.\mathord {\textnormal {\textsf {proj}}}_{1}(z):(\sum _{x_{1},x_{2}:A}x_{1}=x_{2})\to A\)は同値である。