Homotopy Type Theory
univalent universe > history (Rev #5, changes)
Showing changes from revision #4 to #5:
Added | Removed | Changed
The univalence axiom for a universe states that for all , the map
defined by path induction?path induction, is an equivalence. So we have
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.