\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(B:A\to \mathcal {U}(i)\)を型の族、\(C:\prod _{x:A}B(x)\to \mathcal {U}(i)\)を型の族とする。

• -関数\(f:\prod _{z:\sum _{x:A}B(x)}C(\mathord {\textnormal {\textsf {proj}}}_{1}(z),\mathord {\textnormal {\textsf {proj}}}_{2}(z))\)に対し、カリー化(currying)\(\mathord {\textnormal {\textsf {curry}}}(f):\prod _{x:A}\prod _{y:B(x)}C(x,y)\)を\(\lambda (x,y).f(\mathord {\textnormal {\textsf {pair}}}(x,y))\)と定義する。
• -関数\(g:\prod _{x:A}\prod _{y:B(x)}C(x,y)\)に対し、逆カリー化(uncurrying)\(\mathord {\textnormal {\textsf {uncurry}}}(g):\prod _{z:\sum _{x:A}B(x)}C(\mathord {\textnormal {\textsf {proj}}}_{1}(z),\mathord {\textnormal {\textsf {proj}}}_{2}(z))\)を\(\lambda z.g(\mathord {\textnormal {\textsf {proj}}}_{1}(z),\mathord {\textnormal {\textsf {proj}}}_{2}(z))\)と定義する。