Timeline for Role of univalence in homotopy group calculations
Current License: CC BY-SA 4.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 13, 2021 at 17:05 | vote | accept | user336697 | ||
| Aug 13, 2021 at 16:58 | comment | added | user336697 | Thanks so much! | |
| Aug 12, 2021 at 12:13 | comment | added | Noah Snyder | The recursion principal for the circle says that if you have such a $(T,t,p)$ you get a map from the circle sending the loop to p. If loop were trivial then p would be as well. In the other direction, if loop is nontrivial just take $(S^1, \mathrm{base}, \mathrm{loop})$. | |
| Aug 12, 2021 at 9:27 | comment | added | user336697 | Thanks. Can you elaborate on the sentence "By the universal property of S1 this is exactly saying that there exists some type T and some t:T and some loop p:t=t which is not trivial."? | |
| Aug 12, 2021 at 4:51 | comment | added | Mike Shulman | Good point. Maybe I'll just emphasize that univalence isn't just important for checking there are no additional relations, it's essential. Univalence is the only seriously proposed axiom for type theory that contradicts UIP, and UIP implies that all homotopy groups are trivial. | |
| Aug 11, 2021 at 19:16 | history | answered | Noah Snyder | CC BY-SA 4.0 |