\(i\)を階数、\(A:\mathcal {U}(i)\)を型とする。恒等関数(identity function)\(\mathord {\textnormal {\textsf {id}}}:A\to A\)を\(\mathord {\textnormal {\textsf {id}}}(x)\equiv x\)と定義する。