\(i\)を階数、\(A:\mathcal {U}(i)\)を型とする。関数\(\lambda x.\mathord {\textnormal {\textsf {pair}}}(x,\mathord {\textnormal {\textsf {pair}}}(x,\mathord {\textnormal {\textsf {refl}}})):A\to (\sum _{x_{1},x_{2}:A}x_{1}=x_{2})\)と\(\lambda z.\mathord {\textnormal {\textsf {proj}}}_{1}(\mathord {\textnormal {\textsf {proj}}}_{2}(z)):(\sum _{x_{1},x_{2}:A}x_{1}=x_{2})\to A\)は同値である。
証明
\(f\equiv \lambda z.\mathord {\textnormal {\textsf {proj}}}_{1}(z)\)と\(g\equiv \lambda x.\mathord {\textnormal {\textsf {pair}}}(x,\mathord {\textnormal {\textsf {pair}}}(x,\mathord {\textnormal {\textsf {refl}}}))\)と\(h\equiv \lambda z.\mathord {\textnormal {\textsf {proj}}}_{1}(\mathord {\textnormal {\textsf {proj}}}_{2}(z))\)と定義すると、\(f\circ g\equiv \mathord {\textnormal {\textsf {id}}}\)かつ\(h\circ g\equiv \mathord {\textnormal {\textsf {id}}}\)である。[002J]より\(f\)は同値であるから、[002E]と[0026]から\(g\)も同値であると分かる。すると、再び[002E]と[0026]から\(h\)も同値であると分かる。