\(i\)を階数、\(A,B:\mathcal {U}(i)\)を型とする。関数\(\mathord {\textnormal {\textsf {sym}}}(A,B):A\times B\to B\times A\)を\(\lambda z.\mathord {\textnormal {\textsf {pair}}}(\mathord {\textnormal {\textsf {proj}}}_{2}(z),\mathord {\textnormal {\textsf {proj}}}_{1}(z))\)と定義する。