univalence axiom (Rev #5, changes)

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

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?~~path induction, is an equivalence. So we have

$(A=_U B) \simeq (A \simeq B).$