univalence axiom (Rev #4, changes)

Showing changes from revision #3 to #4:
Added | ~~Removed~~ | ~~Chan~~ged

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

$$(A{=}_{U}B)\to \mathrm{Equiv}(A,\simeq B)$$ (A=_U B) \to~~ Equiv(A,B)~~ (A\simeq B)

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

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 March 3, 2014 at 14:14:01 by Mike Shulman. See the history of this page for a list of all contributions to it.