Showing changes from revision #3 to #4:
Added | Removed | Changed
The univalence axiom for a universe states that for all , the map
defined by path induction? , is an equivalence. So we have
why not use infix notation here? otherwise it would seem more natural to use rather than .
So we have
Revision on March 3, 2014 at 14:14:01 by Mike Shulman. See the history of this page for a list of all contributions to it.