[004E]を適用する。\(E:A\to A\to \mathcal {U}(i)\)を次のように定義する。\(x_{1},x_{2}:A\)に対して、\(T(x_{1},x_{2}):(x_{1}=x_{2})+(x_{1}=x_{2}\to \mathbf {0})\to \mathcal {U}(i)\)を\(T(x_{1},x_{2},\mathord {\textnormal {\textsf {in}}}_{1}(z))\equiv \mathbf {1}\)と\(T(x_{2},x_{2},\mathord {\textnormal {\textsf {in}}}_{2}(z))\equiv \mathbf {0}\)で定義する。\(E(x_{1},x_{2})\equiv T(x_{1},x_{2},d(x_{1},x_{2}))\)と定義する。[001O]と[004F]と[004G]から、各\(E(x_{1},x_{2})\)は命題である。関数\(g:\prod _{z}T(x_{1},x_{2},z)\to x_{1}=x_{2}\)を\(g(\mathord {\textnormal {\textsf {in}}}_{1}(u),w)\equiv u\)と\(g(\mathord {\textnormal {\textsf {in}}}_{2}(v),w)\equiv \mathord {\textnormal {\textsf {ind}}}_{\mathbf {0}}(w,\_)\)で定義できるので、関数\(E(x_{1},x_{2})\to x_{1}=x_{2}\)を得る。最後に、任意の\(x:A\)に対して同値\(h:\prod _{z}T(x,x,z)\simeq \mathbf {1}\)を\(h(\mathord {\textnormal {\textsf {in}}}_{1}(u))\equiv \mathord {\textnormal {\textsf {id}}}\)と\(h(\mathord {\textnormal {\textsf {in}}}_{2}(v))\equiv \mathord {\textnormal {\textsf {ind}}}_{\mathbf {0}}(v(\mathord {\textnormal {\textsf {refl}}}),\_)\)と定義できるので、関数\(\prod _{x:A}E(x,x)\)を得る。