Homotopy Type Theory
univalence axiom (Rev #5)

The univalence axiom for a universe UU states that for all A,B:UA,B:U, the map

(A= UB)(AB) (A=_U B) \to (A\simeq B)

defined by path induction, is an equivalence. So we have

(A= UB)(AB). (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.