Timeline for Why isn't $S^1$ contractible in homotopy type theory?
Current License: CC BY-SA 4.0
21 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 20, 2023 at 18:23 | comment | added | Vik78 | If the circle were contractible, then "contractible" would not be a great choice of for that property. | |
| Sep 18, 2023 at 3:56 | comment | added | Zach Teitler | I want to apologize for my rude comment. I don't think there's anything wrong with the question; the problem is my own lack of understanding. Still, it's amazing how different things can sound, in language that is not familiar. Perhaps this is how my students feel when I talk about things that they are still learning. | |
| Sep 15, 2023 at 13:33 | vote | accept | Daniel Murcia | ||
| Sep 15, 2023 at 0:42 | comment | added | Noah Snyder | The argument for sending it to math.stackexchange is not that basic things in HoTT are off topic, it's that a research mathematician should know that the circle is not contractible. (The question has since been edited and is now ok.) | |
| Sep 14, 2023 at 19:36 | comment | added | David E Speyer | HoTT is well beyond the standard graduate syllabus which a mathematician should be expected to know; there are many many of us who don't understand it. I don't think we should be closing down questions about how to do basic things in HoTT on the grounds that they are obvious to people who know HoTT. | |
| Sep 14, 2023 at 16:55 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
edited title
|
| Sep 14, 2023 at 8:56 | comment | added | Peter LeFanu Lumsdaine | As @AndrejBauer says, this question is very far from research-level — it would be a much better fit on Math Stackexchange than here. Voted to migrate. // @ Daniel: I think the short suggestion/answer is that your intuition either for what “contractible” means, or for what adding paths does, is not quite right. | |
| Sep 14, 2023 at 8:51 | history | edited | Max Horn | CC BY-SA 4.0 |
Attempt to clarify the title. Apologies if I messed it up
|
| Sep 14, 2023 at 8:49 | comment | added | Max Horn | I think it would help if you started out with a little bit of exposition -- like "In the context of homotopy type theory". As it is at first the question sounded like a "not even wrong" kind of question to me. Only after seeing Andrej Brauer's comment and the HoTT tag did I realize this is just taking about objects I (thought I) know in a context I am completely unfamiliar with. | |
| Sep 14, 2023 at 6:07 | answer | added | Andrej Bauer | timeline score: 6 | |
| Sep 14, 2023 at 5:56 | comment | added | Andrej Bauer | I would be curious to hear whether the close vote is the result of fear of the unknown, or a HoTT expert thinking this question is too basic for MO (which it is). | |
| Sep 14, 2023 at 2:37 | review | Close votes | |||
| Sep 15, 2023 at 14:00 | |||||
| Sep 14, 2023 at 2:32 | answer | added | Tim Campion | timeline score: 5 | |
| Sep 14, 2023 at 1:46 | history | edited | Daniel Murcia | CC BY-SA 4.0 |
deleted 1 character in body
|
| Sep 14, 2023 at 1:36 | comment | added | Daniel Murcia | I would like to improve the question, any suggestions? | |
| Sep 14, 2023 at 1:33 | history | edited | Daniel Murcia | CC BY-SA 4.0 |
edited body
|
| Sep 14, 2023 at 1:31 | comment | added | Daniel Asimov | Nor do I. (But at least the question has the correct spelling of "contractible".) | |
| Sep 14, 2023 at 0:53 | comment | added | Zach Teitler | Wow, I don't understand this question at all. | |
| Sep 14, 2023 at 0:49 | comment | added | Noah Snyder | The circle is connected, but not contractable. That is, everything of type $S^1$ is merely equal to base, but the statement you're trying to prove is false. | |
| Sep 14, 2023 at 0:49 | history | edited | LSpice | CC BY-SA 4.0 |
`\mathit` and `\DeclareMathOperator`
|
| Sep 14, 2023 at 0:43 | history | asked | Daniel Murcia | CC BY-SA 4.0 |