\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(B:A\to \mathcal {U}(i)\)を型の族、\(a_{1},a_{2}:A\)を要素、\(p:a_{1}=a_{2}\)を同一視、\(b_{1}:B(a_{1})\)と\(b_{2}:B(a_{2})\)を要素とする。型\(b_{1}=_{p}^{B}b_{2}:\mathcal {U}(i)\)を\(\mathord {\textnormal {\textsf {transport}}}(B,p,b_{1})=b_{2}\)と定義する。\(b_{1}=_{p}^{B}b_{2}\)の要素を\(b_{1}\)と\(b_{2}\)の\(p\)上の同一視(identification over \(p\))と呼ぶ。