## 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]]. ## Properties ## ## See also ## * [[univalence]] * [[homotopy]] * [[axioms]] ## References ## * [[HoTT book]] category: axioms, type theory