$a_{1},a_{2}:\mathbf {1}$を要素とする。同値$(a_{1}=a_{2})\simeq \mathbf {1}$を構成しよう。[001S]を適用する。$B:\mathbf {1}\to \mathcal {U}(0)$を$\lambda x.\mathbf {1}$と定義する。要素$\mathord {\star }:B(a_{1})$を得る。[001O]と[0024]により、$\sum _{x:\mathbf {1}}B(x)$は$B(a_{1})$のレトラクトである。再び[001O]により$B(a_{1})$は可縮なので、[001K]により$\sum _{x:\mathbf {1}}B(x)$は可縮である。