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.