\(i\)を階数、\(A,B:\mathcal {U}(i)\)を型、\(f:A\to B\)を関数とする。型\(\mathord {\textnormal {\textsf {IsEquiv}}}(f):\mathcal {U}(i)\)を\(\prod _{y:B}\mathord {\textnormal {\textsf {IsContr}}}(\mathord {\textnormal {\textsf {Fiber}}}(f,y))\)と定義する。\(\mathord {\textnormal {\textsf {IsEquiv}}}(f)\)の要素がある時、\(f\)は同値(equivalence)であると言う。