[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)$を得る。