\(i\)を階数、\(A,B:\mathcal {U}(i)\)を型、\(f:A\to B\)を関数とする。型\(\mathord {\textnormal {\textsf {IsSurj}}}(f):\mathcal {U}(i)\)を\(\forall _{y:B}\exists _{x:A}f(x)=y\)と定義する。\(\mathord {\textnormal {\textsf {IsSurj}}}(f)\)の要素がある時、\(f\)は全射(surjection)であると言う。