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

defined by 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.