\(i\)を階数、\(A,B:\mathcal {U}(i)\)を型、\(f:A\to B\)を関数とする。関数\(g:A\to \mathbf {1}\)を\(\lambda \_.\mathord {\star }\)とする。\(f\)のコファイバー(cofiber) \(\mathord {\textnormal {\textsf {Cofiber}}}(f)\)を\(B\mathbin {{}_{f}\smash {+}_{g}}\mathbf {1}\)と定義する。