Showing changes from revision #2 to #3:
Added | Removed | Changed
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 . }
why not use infix notation here? otherwise it would seem more natural to use rather than .
So we have