関数を定義するには次のいずれかような言い回しをする。

• -関数\(f:\prod _{x:A}B(x)\)を\(\lambda x.b\)と定義する。
• -関数\(f:\prod _{x:A}B(x)\)を\(f(x)\equiv b\)と定義する。
• -\(x:A\)を要素とする。要素\(f(x):B(x)\)を\(b\)と定義する。

最後の記法において、\(f\)の引数のリストに現れない仮定は\(f\)の暗黙的引数([000J])と解釈する。