\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(B:A\to \mathcal {U}(i)\)を型の族、\(f:\prod _{x:A}B(x)\)を関数とする。関数

\(\mathord {\textnormal {\textsf {apd}}}(f):\prod _{\lbrace x_{1},x_{2}:A\rbrace }\prod _{p:x_{1}=x_{2}}f(x_{1})=_{p}^{B}f(x_{2})\)を\(\mathord {\textnormal {\textsf {apd}}}(f,\mathord {\textnormal {\textsf {refl}}})\equiv \mathord {\textnormal {\textsf {refl}}}\)で定義する。