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

• -関数\(h:\prod _{x:\mathbb {N}}A(x)\)を\(\lambda x.\mathord {\textnormal {\textsf {ind}}}_{\mathbb {N}}(x,A,a,f)\)と定義する。
• -関数\(h:\prod _{x:\mathbb {N}}A(x)\)を\(h(0)\equiv a\)と\(h(\mathord {\textnormal {\textsf {succ}}}(x))\equiv f(h(x))\)で定義する。
• -\(x:\mathbb {N}\)を要素とする。要素\(h(x):A(x)\)を\(h(0)\equiv a\)と\(h(\mathord {\textnormal {\textsf {succ}}}(x))\equiv f(h(x))\)で定義する。