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

1. 1要素\(a_{1},a_{2},a_{3}:A\)と同一視\(p_{1}:a_{1}=a_{2}\)と\(p_{2}:a_{2}=a_{3}\)に対して、同一視\(\mathord {\textnormal {\textsf {ap-comp}}}(f,p_{2},p_{1}):\mathord {\textnormal {\textsf {ap}}}(f,p_{2}\circ p_{1})=\mathord {\textnormal {\textsf {ap}}}(f,p_{2})\circ \mathord {\textnormal {\textsf {ap}}}(f,p_{1})\)を構成できる。実際、\(\mathord {\textnormal {\textsf {ap-comp}}}(f,p_{2},\mathord {\textnormal {\textsf {refl}}})\equiv \mathord {\textnormal {\textsf {refl}}}\)と定義すればよい。
2. 2要素\(a_{1},a_{2}:A\)と同一視\(p:a_{1}=a_{2}\)に対して、同一視\(\mathord {\textnormal {\textsf {ap-inv}}}(f,p):\mathord {\textnormal {\textsf {ap}}}(f,{p}^{-1})={(\mathord {\textnormal {\textsf {ap}}}(f,p))}^{-1}\)を構成できる。実際、\(\mathord {\textnormal {\textsf {ap-inv}}}(f,\mathord {\textnormal {\textsf {refl}}})\equiv \mathord {\textnormal {\textsf {refl}}}\)と定義すればよい。