#
Homotopy Type Theory
function extensionality > history (changes)

Showing changes from revision #1 to #2:
Added | ~~Removed~~ | ~~Chan~~ged

## Idea

< function extensionality

~~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

~~
~~~~
~~## References

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