The **univalence axiom** for a [[universe]] $U$ states that for all $A,B:U$, the map $$ (A=_U B) \to Equiv(A,B) $$ defined by [[path induction]], is an equivalence. [[!redirects univalence]]