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}fx=gx\right)\to f=g$

If $fx=gx$ for all $x:A$, then $f=g$.

Status in Type Theory

• 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

Properties

• Function extensionality is implied by the univalence principle.

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 Principle: A related axiom in homotopy type theory
• Proposition Extensionality: Extensionality for propositions