Homotopy Type Theory
function extensionality

Idea

Remember that when two functions $f,g : A \to B$ are homotopic we have a witness to

$$\prod_{x : A} f(x)=g(x)$$

but as discussed in the homotopy article, it is not the case that $f=g$.

Function extensionality simply assumes this is the case as an axiom.

Definition

The axiom of functional extensionality says that for all $A,B$, $f,g : A \to B$ there is a function

$$funext : (f \sim g) \to (f = g)$$

This allows homotopic functions to be equal.

Properties

See also

• univalence
• homotopy
• axioms

References

• HoTT book

category: axioms, type theory