Homotopy Type Theory univalence axiom (Rev #5)

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

Revision on March 4, 2014 at 02:23:58 by Alexis Hazell?. See the history of this page for a list of all contributions to it.