1から2を示す。\(c:\prod _{x:A}\mathord {\textnormal {\textsf {IsContr}}}(B(x))\)を仮定する。仮定\(c\)より、関数\(f:\prod _{x:A}B(x)\)と同一視\(p:\prod _{x:A}\prod _{y:B(x)}f(x)=y\)を得る。同一視\(q:\prod _{g:\prod _{x:A}B(x)}f=g\)を構成すればよい。任意の\(g:\prod _{x:A}B(x)\)に対して、\(\lambda x.p(x,g(x)):\prod _{x:A}f(x)=g(x)\)を得るが、関数外延性と[001S]により\(f=g\)の要素を得る。

2から1を示す。\(A:\mathcal {U}(i)\)を型、\(B:A\to \mathcal {U}(i)\)を型の族、\(f:\prod _{x:A}B(x)\)を関数とする。[001A]より、\(\sum _{g:\prod _{x:A}B(x)}\prod _{x:A}f(x)=g(x)\)は\(\prod _{x:A}\sum _{y:B(x)}f(x)=y\)のレトラクトであるが、後者は仮定と[001N]により可縮である。よって、[001K]から前者も可縮である。