\(i\)を階数、\(A,B:\mathcal {U}(i)\)を型、\(f:A\to B\)を関数、\(a_{1},a_{2}:A\)を要素とする。\(f\)が同値ならば\(\mathord {\textnormal {\textsf {ap}}}(f):a_{1}=a_{2}\to f(a_{1})=f(a_{2})\)は同値である。