# Homotopy Type Theory function extensionality > history (changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

## 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.

## References

category: axioms, type theory

Last revised on June 9, 2022 at 20:35:15. See the history of this page for a list of all contributions to it.