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](/nlab/show/inductive+type#PathInduction), is an equivalence. So we have $$ (A=_U B) \simeq (A \simeq B). $$ [[!redirects univalence]]