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

• -関数\(\mathord {\textnormal {\textsf {dist}}}(C):(\prod _{x:A}\sum _{y:B(x)}C(x,y))\to (\sum _{f:\prod _{x:A}B(x)}\prod _{x:A}C(x,f(x)))\)を\(\lambda h.\mathord {\textnormal {\textsf {pair}}}(\lambda x.\mathord {\textnormal {\textsf {proj}}}_{1}(h(x)),\lambda x.\mathord {\textnormal {\textsf {proj}}}_{2}(h(x)))\)と定義する。
• -関数\(\mathord {\textnormal {\textsf {dist}}}^{-1}(C):(\sum _{f:\prod _{x:A}B(x)}\prod _{x:A}C(x,f(x)))\to (\prod _{x:A}\sum _{y:B(x)}C(x,y))\)を\(\lambda k.\lambda x.\mathord {\textnormal {\textsf {pair}}}(\mathord {\textnormal {\textsf {proj}}}_{1}(k(x)),\mathord {\textnormal {\textsf {proj}}}_{2}(k(x)))\)と定義する。