$i$を階数、$A:\mathcal {U}(i)$を型、$a_{0},a_{1},a_{2}:A$を要素、$p_{1}:a_{0}=a_{1}$と$p_{2}:a_{0}=a_{2}$を同一視とする。同一視$\mathord {\textnormal {\textsf {ext}}}(p_{1},p_{2}):a_{1}=a_{2}$を$\mathord {\textnormal {\textsf {transport}}}(\lambda x.(x=a_{2}),p_{1},p_{2})$と定義する。