\(i\)を階数、\(A,B:\mathcal {U}(i)\)を型とする。型\(A\simeq B:\mathcal {U}(i)\)を\(\mathord {\textnormal {\textsf {Record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {fun}}}:A\to B,\mathord {\textnormal {\textsf {is-equiv}}}:\mathord {\textnormal {\textsf {IsEquiv}}}(\mathord {\textnormal {\textsf {fun}}})\mathclose {|\negmedspace \} }\)と定義する。