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

• -関数\(f:\prod _{z:A+B}D(z)\)を\(\lambda z.\mathord {\textnormal {\textsf {ind}}}_{+}(z,D,d_{1},d_{2})\)と定義する。
• -関数\(f:\prod _{z:A+B}D(z)\)を\(f(\mathord {\textnormal {\textsf {in}}}_{1}(x))\equiv d_{1}(x)\)と\(f(\mathord {\textnormal {\textsf {in}}}_{2}(y))\equiv d_{2}(y)\)で定義する。
• -\(z:A+B\)を要素とする。要素\(f(z):D(z)\)を\(f(\mathord {\textnormal {\textsf {in}}}_{1}(x))\equiv d_{1}(x)\)と\(f(\mathord {\textnormal {\textsf {in}}}_{2}(y))\equiv d_{2}(y)\)で定義する。