\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(B:A\to \mathcal {U}(i)\)を型の族とする。関数\(p:(A\to (\sum _{x:A}B(x)))\to (A\to A)\)を\(\lambda f.\lambda x.\mathord {\textnormal {\textsf {proj}}}_{1}(f(x))\)とし、型\(\mathord {\textnormal {\textsf {Sect}}}(A,B):\mathcal {U}(i)\)を\(\mathord {\textnormal {\textsf {Fiber}}}(p,\mathord {\textnormal {\textsf {id}}})\)と定義する。