Timeline for Role of univalence in homotopy group calculations
Current License: CC BY-SA 4.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 12, 2021 at 4:49 | comment | added | Mike Shulman | BTW, I'm quite fond of the word identification for the elements of an identity type. I think it mediates quite well between the idea of "equality" and the fact that in general things aren't "just equal" but are identified in a specified way. I think mathematicians are used to the idea that we can, at least informally, "identify" two isomorphic structures, using a particular isomorphism. | |
| Aug 12, 2021 at 4:47 | comment | added | Mike Shulman | @NoahSnyder I don't disagree, but eventually you also have to tell people that when talking about ordinary mathematical objects like integers, the "isomorphisms/equivalences" specialize to the familiar notion of equality. | |
| Aug 11, 2021 at 23:32 | comment | added | Noah Snyder | Right, I think we're agreeing with each other. I think talking about redefining equality is too logic-y to communicate the point to most mathematicians, the point as you say is about $\infty$-groupoids forming an $\infty$-groupoid. | |
| Aug 11, 2021 at 22:56 | comment | added | Andrej Bauer | @NoahSnyder: How does the working mathematician imagine the space of (small) spaces, and what are the paths in this space? That's what univalence is about. | |
| Aug 11, 2021 at 19:26 | comment | added | Noah Snyder | For a "working mathematician" I feel like it's more informative to not use the word equality at all and say something like "each type of mathematical object forms a space if you think of the isomorphisms/equivalences as paths." | |
| Aug 11, 2021 at 18:43 | history | edited | David Corfield | CC BY-SA 4.0 |
Correct the typing in the final dependent sum.
|
| Aug 11, 2021 at 15:11 | history | answered | Mike Shulman | CC BY-SA 4.0 |