\(i\)を階数、\(A,B:\mathcal {U}(i)\)を型、\(f:A\to B\)を関数とする。関数

\(\mathord {\textnormal {\textsf {ap}}}(f):\prod _{\lbrace x_{1},x_{2}:A\rbrace }x_{1}=x_{2}\to f(x_{1})=f(x_{2})\)を\(\lambda (x_{1},x_{2},z).\mathord {\textnormal {\textsf {transport}}}(\lambda x.(f(x_{1})=f(x)),z,\mathord {\textnormal {\textsf {refl}}})\)と定義する。文脈上わかる場合は、\(\mathord {\textnormal {\textsf {ap}}}(f,p)\)のことを\(f(p)\)と書いてしまうこともある。