\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(B:A\to \mathcal {U}(i)\)を型の族とする。要素\(a_{1},a_{2},a_{3}:A\)と同一視\(p_{1}:a_{1}=a_{2}\)と\(p_{2}:a_{2}=a_{3}\)に対して、同一視\(\mathord {\textnormal {\textsf {transport-comp}}}(B,p_{2},p_{1}):\mathord {\textnormal {\textsf {transport}}}(B,p_{2}\circ p_{1})=\mathord {\textnormal {\textsf {transport}}}(B,p_{2})\circ \mathord {\textnormal {\textsf {transport}}}(B,p_{1})\)を構成できる。実際、\(\mathord {\textnormal {\textsf {transport-comp}}}(B,p_{2},\mathord {\textnormal {\textsf {refl}}})\equiv \mathord {\textnormal {\textsf {refl}}}\)と定義すればよい。