Showing changes from revision #0 to #1:
Added | Removed | Changed
The univalence axiom for a universe states that for all , the map
defined by path induction?, is an equivalence.
Revision on February 18, 2014 at 12:40:14 by Mike Shulman. See the history of this page for a list of all contributions to it.