Homotopy Type Theory
function extensionality > history (Rev #2, changes)
Showing changes from revision #1 to #2:
Added | Removed | Changed
Idea
< function extensionality
Remember that when two functions are homotopic we have a witness to
but as discussed in the homotopy article, it is not the case that .
Function extensionality simply assumes this is the case as an axiom.
Definition
The axiom of functional extensionality says that for all , there is a function
This allows homotopic functions to be equal.
Properties
See also
References
Revision on June 9, 2022 at 20:35:15 by
Anonymous?.
See the history of this page for a list of all contributions to it.