仮定\(e\)から\(f:A\to B\)と\(H:\mathord {\textnormal {\textsf {IsEquiv}}}(f)\)を得る。任意の\(y:B\)に対して\(H(y):\mathord {\textnormal {\textsf {IsContr}}}(\mathord {\textnormal {\textsf {Fiber}}}(f,y))\)を得るので、特に関数\(G:\prod _{y:B}\mathord {\textnormal {\textsf {Fiber}}}(f,y)\)を得る。[001A]の要領で\(G\)から関数\(g:B\to A\)と同一視\(p:\prod _{y:B}f(g(y))=y\)を得る。これで要素\(\mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {retraction}}}\equiv f,\mathord {\textnormal {\textsf {section}}}\equiv g,\mathord {\textnormal {\textsf {r-s}}}\equiv p\mathclose {|\negmedspace \} }:\mathord {\textnormal {\textsf {Retract}}}(B,A)\)を構成できた。