univalence axiom (Rev #3, changes)

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

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

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