ホモトピー型理論
[003L] 定義

\(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\))と呼ぶ。