Definition 1.5.1.  Let X, Y be sets. We define:
(X → Y) :=: {(X → Yx ↦ yx) | yx ∈ Y for each x ∈ X}
(X → Yx ↦ yx) = (X → Yx ↦ y'x)  :⇔  ∀ x ∈ X : yx = y'x  (yx ∈ Y for each x ∈ X, y'x ∈ Y for each x ∈ X)
We write “let f : X → Y be a function” for “let f ∈ (X → Y).”
We write “f :  X → Yx ↦ yx” for “f := (X → Yx ↦ yx).”
Remarks.

This definition uses binders as a built-in feature of the HLM logic. It is equivalent to the usual set-theoretic definition, which is called "mapping" in this library to distinguish the two definitions (see $../Relations/mapping, $"mapping as function").

The major advantage of the definition using binders is that given an explicitly defined function, determining the value at a specific input is simply a matter of resolving definitions.

Function extensionality is a consequence of the requirement to specify an equality definition for the constructor.

References.