Showing changes from revision #1 to #2:
Added | Removed | Changed
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.
The axiom of functional extensionality says that for all , there is a function
Last revised on June 9, 2022 at 20:35:15. See the history of this page for a list of all contributions to it.