Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Last revision Both sides next revision | ||
|
univalence_axiom [2014/11/18 13:30] nikolaj |
univalence_axiom [2016/07/18 00:27] nikolaj |
||
|---|---|---|---|
| Line 47: | Line 47: | ||
| $Id_U(A,B)\simeq(A\simeq B)$ | $Id_U(A,B)\simeq(A\simeq B)$ | ||
| - | Here $\simeq$ is defined like a homotopy equivalence, in support of the $\infty$-groupoid pov. One could say that equality is dropped in favor of equivalence, however we keep the computational aspect. (141111 I'm not sure how the implementation of univalent foundation actually compares to properly weak higher category theory.) | + | Here $\simeq$ is defined like a homotopy equivalence, in support of the $\infty$-groupoid pov. (I've written down some explanations of the univalence axiom in the HoTT Wikipedia article.) |
| An isomorphism of a plain set is of course an invertible function - a bijection. Note that if by the set of natural numbers and set of rational numbers you merely mean the collection of their elements, then they are equal in HoTT (there is a bijection)! But as soon as you consider them equipped them with their structure (e.g. $+$ arithmetic), they are not equal. | An isomorphism of a plain set is of course an invertible function - a bijection. Note that if by the set of natural numbers and set of rational numbers you merely mean the collection of their elements, then they are equal in HoTT (there is a bijection)! But as soon as you consider them equipped them with their structure (e.g. $+$ arithmetic), they are not equal. | ||
