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. { why not use infix notation $A \simeq B $ here? otherwise it would seem more natural to use $ Id_U(A, B) $ rather than $ (A=_U B) $. } So we have $$ (A=_U B) \simeq (A \simeq B). $$ [[!redirects univalence]]