\(i\)を階数、\(A:\mathcal {U}(i)\)を型とする。

• -関数\(\mathord {\textnormal {\textsf {sym}}}:\prod _{\lbrace x_{1},x_{2}:A\rbrace }x_{1}=x_{2}\to x_{2}=x_{1}\)を\(\lambda (x_{1},x_{2},z).\mathord {\textnormal {\textsf {ext}}}(z,\mathord {\textnormal {\textsf {refl}}})\)と定義する。\(\mathord {\textnormal {\textsf {sym}}}(p)\)を\({p}^{-1}\)とも書く。
• -関数\(\mathord {\textnormal {\textsf {trans}}}:\prod _{\lbrace x_{1},x_{2},x_{3}:A\rbrace }x_{1}=x_{2}\to x_{2}=x_{3}\to x_{1}=x_{3}\)を\(\lambda (x_{1},x_{2},x_{3},z,w).\mathord {\textnormal {\textsf {ext}}}({z}^{-1},w)\)と定義する。\(\mathord {\textnormal {\textsf {trans}}}(p,q)\)を\(q\circ p\)とも書く。