\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(a_{1},a_{2}:A\)を要素、\(p:a_{1}=a_{2}\)を同一視とする。同一視\(\mathord {\textnormal {\textsf {sym-sym}}}(p):{({p}^{-1})}^{-1}=p\)を帰納法により\(\mathord {\textnormal {\textsf {sym-sym}}}(\mathord {\textnormal {\textsf {refl}}})\equiv \mathord {\textnormal {\textsf {refl}}}\)と定義する。