\(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\)の要素とみなすことがある。