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