Homotopy Type Theory
univalence axiom (Rev #2)

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

(A= UB)Equiv(A,B) (A=_U B) \to Equiv(A,B)

defined by path induction?, is an equivalence.

{ why not use infix notation ABA \simeq B here? otherwise it would seem more natural to use Id U(A,B) Id_U(A, B) rather than (A= UB) (A=_U B) . }

So we have

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