Homotopy Type Theory
function extensionality


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

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

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

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


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

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

This allows homotopic functions to be equal.


See also


category: axioms, type theory