要素\(c:\sum _{x:A}a=x\)と\(r:\prod _{z:\sum _{x:A}a=x}c=z\)を構成すればよい。\(c\equiv \mathord {\textnormal {\textsf {pair}}}(a,\mathord {\textnormal {\textsf {refl}}})\)と定義する。\(r\)については、カリー化([0014])により、\(\prod _{x:A}\prod _{w:a=x}c=\mathord {\textnormal {\textsf {pair}}}(x,w)\)の要素を構成すればよい。同一視型の帰納法により、\(c=\mathord {\textnormal {\textsf {pair}}}(a,\mathord {\textnormal {\textsf {refl}}})\)の要素を構成すればよいが、\(c\)の定義より\(\mathord {\textnormal {\textsf {refl}}}\)とすればよい。