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

• -要素\(a_{2}:A\)に対し、同一視型(identity type)\(a_{1}=a_{2}:\mathcal {U}(i)\)を構成できる。\(a_{1}=a_{2}\)の要素を\(a_{1}\)と\(a_{2}\)の同一視(identification)と呼ぶ。
• -要素\(\mathord {\textnormal {\textsf {refl}}}\lbrace a_{1}\rbrace :a_{1}=a_{1}\)を構成できる。
• -\(a_{2}:A\)と\(p:a_{1}=a_{2}\)を要素、\(j\)を階数、\(B:\prod _{\lbrace x:A\rbrace }a_{1}=x\to \mathcal {U}(j)\)を型の族、\(b:B(\mathord {\textnormal {\textsf {refl}}})\)を要素とすると、要素\(\mathord {\textnormal {\textsf {ind}}}_{=}(p,B,b):B(p)\)を構成できる。
• -\(j\)を階数、\(B:\prod _{\lbrace x:A\rbrace }a_{1}=x\to \mathcal {U}(j)\)を型の族、\(b:B(\mathord {\textnormal {\textsf {refl}}})\)を要素とすると、\(\mathord {\textnormal {\textsf {ind}}}_{=}(\mathord {\textnormal {\textsf {refl}}},B,b)\equiv b\)と定義される。