\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(j\)を階数、\(B:A\to \mathcal {U}(j)\)を型の族とする。\(a_{1},a_{2}:A\)と\(p:a_{1}=a_{2}\)を要素とする。輸送関数(transport function)

\(\mathord {\textnormal {\textsf {transport}}}(B,p):B(a_{1})\to B(a_{2})\)を\(\mathord {\textnormal {\textsf {transport}}}(B,\mathord {\textnormal {\textsf {refl}}})\equiv \mathord {\textnormal {\textsf {id}}}\)で定義する。