Homotopy Type Theory
univalent universe > history (Rev #2)
The univalence axiom for a universe states that for all , the map
defined by path induction?, is an equivalence.
{ why not use infix notation here? otherwise it would seem more natural to use rather than . }
So we have
Revision on February 19, 2014 at 12:56:43 by
Steve Awodey?.
See the history of this page for a list of all contributions to it.