\(i\)を階数、\(A,B:\mathcal {U}(i)\)を型、\(C:A\to B\to \mathcal {U}(i)\)を型の族、\(f:\prod _{x:A}\prod _{y:B}C(x,y)\)を関数とする。関数\(\mathord {\textnormal {\textsf {swap}}}(f):\prod _{y:B}\prod _{x:A}C(x,y)\)を\(\mathord {\textnormal {\textsf {swap}}}(f,y,x)\equiv f(x,y)\)と定義する。