# Homotopy Type Theory univalence axiom (Rev #2)

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).$

Revision on February 19, 2014 at 12:56:43 by Steve Awodey?. See the history of this page for a list of all contributions to it.