\(i\)を階数、\(A:\mathcal {U}(i)\)を型とする。関数\(f:A\to \mathbf {1}\)を\(\lambda \_.\mathord {\star }\)とする。懸垂(suspension) \(\mathord {\textnormal {\textsf {Susp}}}(A):\mathcal {U}(i)\)を\(\mathbf {1}\mathbin {{}_{f}\smash {+}_{f}}\mathbf {1}\)と定義する。