$i$を階数、$A:\mathcal {U}(i)$を型、$B:A\to \mathcal {U}(i)$を型の族とする。関数外延性の下で$\prod _{x:A}\mathord {\textnormal {\textsf {IsProp}}}(B(x))$の要素がある時、$\sum _{x:A}B(x)$のことを$\lbrace x:A\mid B(x)\rbrace$と書くことがある。さらに、要素$c:\lbrace x:A\mid B(x)\rbrace$に対して、$\mathord {\textnormal {\textsf {proj}}}_{1}$を省略して$c$そのものを$A$の要素とみなすことがある。