Function Extensionality

Definition

Function extensionality is the principle that two functions are equal if they produce equal outputs for all inputs. For functions $f,g:A\to B$, function extensionality states:

$\left({\prod }_{x:A}f(x)=g(x)\right)\to f=g$

If $f(x)=g(x)$ for all $x:A$, then $f=g$.

Distinction from Eta Rule

Function extensionality is stronger than the η-rule for function types. The η-rule states:

$f=\lambda x.f(x)$

This is a definitional equality that holds when $f$ is syntactically a function term. Function extensionality, however, is a propositional principle that applies to any two functions, regardless of their syntactic form.

The key difference:

• Eta rule: Applies only when checking definitional equality of function terms
• Function extensionality: States that pointwise equal functions are propositionally equal, even if they are defined differently

Status in Type Theory

Function extensionality is not provable in basic intensional type theory such as Martin-Löf Type Theory. It must be added as an axiom if desired.

In various type theories:

• Intensional Type Theory: Function extensionality is typically an axiom
• Extensional Type Theory: Function extensionality holds by definition
• Homotopy Type Theory: Function extensionality is equivalent to univalence for function types
• Cubical Type Theory: Function extensionality is provable from the path structure

Consequences

With function extensionality:

• Reasoning about functions becomes more intuitive
• Two implementations of the same specification are equal
• The principle enables quotient types and set-theoretic reasoning
• It validates the notion that functions are determined by their input-output behavior

Examples

Without function extensionality, the following are not provably equal even though they compute the same values:

$\lambda x.x+0\ne \lambda x.x$

With function extensionality, we can prove them equal by showing $(x+0)=x$ for all $x$.

Relation to Univalence

In Homotopy Type Theory, function extensionality is closely related to the univalence axiom. For function types, univalence implies function extensionality, and function extensionality is a key component in establishing equivalences between types.

Related Concepts

• Extensionality: The general principle of equality based on observable behavior
• Eta Rule: The weaker definitional rule for function types
• Function Type: The type for which this principle applies
• Type Theory: The formal system in which this is considered
• Homotopy Type Theory: A setting where function extensionality has deep connections
• Univalence: A related axiom in homotopy type theory