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

• -対型(pair type)\(\sum _{x:A}B(x):\mathcal {U}(i)\)を構成できる。
• -要素\(a:A\)と\(b:B(a)\)に対し、対(pair)\(\mathord {\textnormal {\textsf {pair}}}(a,b):\sum _{x:A}B(x)\)を構成できる。
• -要素\(c:\sum _{x:A}B(x)\)に対し、射影(projection)\(\mathord {\textnormal {\textsf {proj}}}_{1}(c):A\)と\(\mathord {\textnormal {\textsf {proj}}}_{2}(c):B(\mathord {\textnormal {\textsf {proj}}}_{1}(c))\)を構成できる。
• -要素\(a:A\)と\(b:B(a)\)に対し、\(\mathord {\textnormal {\textsf {proj}}}_{1}(\mathord {\textnormal {\textsf {pair}}}(a,b))\equiv a\), \(\mathord {\textnormal {\textsf {proj}}}_{2}(\mathord {\textnormal {\textsf {pair}}}(a,b))\equiv b\)と定義される。
• -要素\(c:\sum _{x:A}B(x)\)に対し、\(c\equiv \mathord {\textnormal {\textsf {pair}}}(\mathord {\textnormal {\textsf {proj}}}_{1}(c),\mathord {\textnormal {\textsf {proj}}}_{2}(c))\)と定義される。