\(\mathord {\textnormal {\textsf {ind}}}_{=}\)を使って関数を定義するには次のいずれかのような言い回しをする。

• -関数\(f:\prod _{\lbrace x:A\rbrace }\prod _{p:a_{1}=x}B(p)\)を\(\lambda (x,p).\mathord {\textnormal {\textsf {ind}}}_{=}(p,B,b)\)と定義する。
• -関数\(f:\prod _{\lbrace x:A\rbrace }\prod _{p:a_{1}=x}B(p)\)を\(f(\mathord {\textnormal {\textsf {refl}}})\equiv b\)で定義する。
• -\(x:A\)を要素、\(p:a_{1}=x\)を同一視とする。要素\(f(p):B(p)\)を\(f(\mathord {\textnormal {\textsf {refl}}})\equiv b\)で定義する。