Extensionality

Definition

Extensionality is a principle stating that two objects are equal if and only if they have the same observable behavior or properties. In other words, objects are identified by their external interface rather than their internal structure or definition.

Extensionality contrasts with intensional equality, where objects are equal only if they are defined in the same way or are syntactically identical.

Extensionality Principles

Different types admit different extensionality principles:

Function Extensionality

Two functions $f,g:A\to B$ are equal if they produce the same output for every input:

$f=g⟺\forall x:A.f(x)=g(x)$

This is Function Extensionality, which is independent of and stronger than the Eta Rule for functions.

Propositional Extensionality

Two propositions $P$ and $Q$ are equal if they are logically equivalent:

$P=Q⟺(P\leftrightarrow Q)$ Aside: This can be proven as a theorem within HoTT using univalence: we can construct an equivalence from bi-implication on prop, since inverses are trivial, hence we derive a path.

Set Extensionality

Two sets $A$ and $B$ are equal if they have the same elements:

$A=B⟺\forall x.(x\in A\leftrightarrow x\in B)$

Relationship to Eta Rules

Eta rules are a form of extensionality expressed at the level of definitional equality. However, extensionality principles are generally stronger:

• The η-rule for functions states $f=\lambda x.f(x)$ as a definitional equality
• Function Extensionality states that functions equal pointwise are propositionally equal
• Function extensionality cannot be proven from the η-rule alone in most type theories

Intensional vs Extensional Type Theory

Type theories can be classified by their treatment of equality:

• Type Theory: Equality is based on computational/syntactic identity. Only requires η-rules at the definitional level.
• Extensional type theory: Equality is based on observable behavior. Includes extensionality principles as axioms or rules.

Intensional type theories typically have decidable type checking, while extensional type theories may not.

Examples

Extensional Equality

Consider two functions:

• $f(x)=x+0$
• $g(x)=x$

By function extensionality, $f=g$ because they produce the same output for all inputs, even though they are defined differently.

Intensional Inequality

Without extensionality, these functions may be considered distinct because they have different definitions, even though they behave identically.

Status in Type Theory

In many type theories (such as Martin-Löf Type Theory or Coq’s Calculus of Inductive Constructions):

• Eta rules are built-in for some types
• Function extensionality is not provable and must be added as an axiom if desired
• Adding extensionality axioms can affect computational properties

In Homotopy Type Theory, extensionality principles are derivable from the univalence axiom in some cases.

Related Concepts

• Function Extensionality: Extensionality principle for functions
• Eta Rule: Definitional form of extensionality for some types
• Type Theory: The formal system where these principles apply
• Homotopy Type Theory: A type theory with strong extensionality principles
• Univalence Principle: An extensionality principle for types themselves