[0062] 命題\(i\)を階数、\(A,B:\mathcal {U}(i)\)を型、\(f:A\to B\)を関数とする。次は論理的に同値である。 1\(f\)は埋め込みである。2任意の\(x_{1}:A\)に対して、\(\sum _{x_{2}:A}f(x_{1})=f(x_{2})\)は可縮である。証明[005R]より、1は任意の\(x_{1},x_{2}:A\)に対して\(\mathord {\textnormal {\textsf {ap}}}(f):x_{1}=x_{2}\to f(x_{1})=f(x_{2})\)が同値であることと論理的に同値である。[001S]より、これは2と論理的に同値である。