\(c:\mathord {\textnormal {\textsf {IsContr}}}(A)\)と仮定する。要素\(p:a_{1}=a_{2}\)と\(q:\prod _{z:a_{1}=a_{2}}p=z\)を構成すればよい。仮定\(c\)より\(a_{0}:A\)と\(r:\prod _{x:A}a_{0}=x\)を得る。\(p\equiv \mathord {\textnormal {\textsf {ext}}}(r(a_{1}),r(a_{2}))\)と定義する。\(q\)については、一般化したもの\(q':\prod _{x:A}\prod _{z:a_{1}=x}\mathord {\textnormal {\textsf {ext}}}(r(a_{1}),r(x))=z\)を構成し、\(q\equiv q'(a_{2})\)と定義する。同一視型の帰納法により、要素\(s:\mathord {\textnormal {\textsf {ext}}}(r(a_{1}),r(a_{1}))=\mathord {\textnormal {\textsf {refl}}}\)を構成すればよいが、これは[001M]で構成した。