Editing Extensionality (section)

==Extensionality principles==
There are various extensionality principles in mathematics. 
* '''Propositional extensionality''' of predicates <math>P,Q</math>: if <math>P\iff Q</math> then <math>P = Q</math>
* '''Functional extensionality''' of functions <math>f,g</math>: if <math>\forall x, f x = g x</math> then <math>f = g</math>
* '''Univalence''' of types <math>A</math>, <math>B</math>:<ref name=HoTTBook>{{cite book | url=https://books.google.com/books?id=LkDUKMv3yp0C | title=Homotopy Type Theory: Univalent Foundations of Mathematics | author=The Univalent Foundations Program | publisher=[[Institute for Advanced Study]] | location=Princeton, NJ | year=2013 | mr=3204653}} </ref>{{rp|2.10}} if  <math>A\simeq B</math> then <math>A = B</math>, where <math>\simeq</math> denotes homotopy equivalence. 
Depending on the chosen foundation, some extensionality principles may imply another. For example it is well known that in [[univalent foundations]], the univalence axiom implies both propositional and functional extensionality. Extensionality principles are usually assumed as axioms, especially in type theories where computational content must be preserved. However, in set theory and other extensional foundations, functional extensionality can be proven to hold by default.