\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(B:A\to \mathcal {U}(i)\)を型の族、\(f,g:\prod _{x:A}B(x)\)を関数とする。型\(f\sim g:\mathcal {U}(i)\)を\(\prod _{x:A}f(x)=g(x)\)と定義する。\(f\sim g\)の要素を\(f\)と\(g\)の間のホモトピー(homotopy)と呼ぶ。