\(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)\)は可縮である。