Timeline for Why isn't $S^1$ contractible in homotopy type theory?
Current License: CC BY-SA 4.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 2 at 9:50 | comment | added | Naïm Favier | I know, but I didn't know which one you meant precisely! (Not that it matters, as they are equivalent.) | |
| Feb 2 at 9:24 | comment | added | Andrej Bauer | @NaïmFavier: thanks, fixed. By the way, you can just edit people's answers around here. | |
| Feb 2 at 9:24 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 3 characters in body
|
| Feb 2 at 9:01 | comment | added | Naïm Favier | That should either be $\| x = y \|_{-1}$ or $\| x \|_0 = \| y \|_0$. | |
| Sep 15, 2023 at 13:33 | vote | accept | Daniel Murcia | ||
| Sep 15, 2023 at 6:23 | comment | added | Andrej Bauer | Yes, it's a bit like that. | |
| Sep 14, 2023 at 23:19 | comment | added | Daniel Murcia | This answer brings me some ideas (correct me if I am misunderstanding): I cannot prove the first case, since the function itself could raise paths that will conflict in some way with univalence. By truncating it, we deny this possibility and make it consistent. Something similar as the case of LEM, where we can assume it consistently if we truncate it to only mere propositions. | |
| Sep 14, 2023 at 6:07 | history | answered | Andrej Bauer | CC BY-SA 4.0 |