Eta Rule

Definition

An eta rule (or η-rule) in Type Theory is a definitional equality expressing that values of a type can be uniquely reconstructed from their elimination forms.

The η-rule is dual to the β-rule: while β-rules describe how eliminators compute on introduced values, η-rules describe how values can be reconstructed from their eliminations as definitional equalities.

General Pattern

For a type with elimination and introduction forms, the η-rule typically has the form:

$t=\text{introduce}({\text{eliminate}}_1(t),{\text{eliminate}}_2(t),\dots )$

This states that any value is equal to the result of eliminating it and then re-introducing those components.

Examples

Product Type

For product types, the η-rule states:

$p=({\pi }_1(p),{\pi }_2(p))$

Any pair is equal to the pair formed from its projections.

Function Type

For function types, the η-rule is:

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

This states that any function term $f$ is definitionally equal to the lambda abstraction that applies it. Note that this is weaker than Function Extensionality, which states that pointwise equal functions are propositionally equal.

Sum Type

For sum types, the η-rule states:

$s=\text{case}(s,\lambda x.\text{inl}(x),\lambda y.\text{inr}(y))$

Any sum value equals the result of case-analyzing it and re-injecting.

Unit Type

For the unit type $1$:

$u=\star$

All elements of the unit type are equal to the canonical element.

Relationship to Extensionality

Eta rules are related to but distinct from Extensionality principles:

• Eta rules express uniqueness at the level of definitional equality
• Extensionality principles (like Function Extensionality) are propositional statements about equality
• Eta rules apply to syntactic forms and are checked by the type checker
• Extensionality principles state that observationally equivalent values are propositionally equal

For example, the η-rule for functions ($f=\lambda x.f(x)$) is a definitional equality, while Function Extensionality ($\forall x.f(x)=g(x)\to f=g$) is a propositional principle that cannot be proven from the η-rule alone in most type theories.

Relationship to Computation

While β-rules are typically reduction rules (rewriting from left to right), η-rules may be used as:

• Expansion rules (rewriting from right to left)
• Equality principles (stating equivalence without direction)
• Definitional equalities in the type checker

Properties

• Eta rules ensure that canonical forms are unique representatives
• They operate at the level of definitional equality, not propositional equality
• In some type theories, η-rules are admissible but not primitive
• Eta rules interact with definitional equality and unification
• Eta rules preserve decidability of type checking

Related Concepts

• Computation Rule: The dual rules describing how eliminations reduce on introductions
• Introduction Rule: Rules for constructing values
• Elimination Rule: Rules for deconstructing values
• Extensionality: General principle of equality by observation
• Function Extensionality: Propositional principle stronger than the η-rule for functions
• Type Theory: The formal system containing these rules
• Product Type: Example type with η-rule for pairs
• Function Type: Example type with η-rule for functions