\(i\)を階数、\(A,B:\mathcal {U}(i)\)を型、\(f:A\to B\)を関数とする。型\(\mathord {\textnormal {\textsf {IsEmb}}}(f):\mathcal {U}(i)\)を\(\mathord {\textnormal {\textsf {IsTruncMap}}}(-1,f)\)と定義する。\(\mathord {\textnormal {\textsf {IsEmb}}}(f)\)の要素がある時、\(f\)は埋め込み(embedding)であると言う。