\(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})\)と定義する。