\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(a_{1},a_{2}:A\)を要素、\(p:a_{1}=a_{2}\)を同一視とする。同一視\(\mathord {\textnormal {\textsf {ext-self}}}(p):\mathord {\textnormal {\textsf {ext}}}(p,p)=\mathord {\textnormal {\textsf {refl}}}\)を構成する。定義より\(\mathord {\textnormal {\textsf {ext}}}(\mathord {\textnormal {\textsf {refl}}},\mathord {\textnormal {\textsf {refl}}})\equiv \mathord {\textnormal {\textsf {refl}}}\)なので帰納法により\(\mathord {\textnormal {\textsf {ext-self}}}(\mathord {\textnormal {\textsf {refl}}})\equiv \mathord {\textnormal {\textsf {refl}}}\)と定義すればよい。