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

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