Timeline for How to proceed with a type-theoretic proof that $\Sigma \mathbb{S}^1 \simeq \mathbb{S}^2$?
Current License: CC BY-SA 4.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 8, 2019 at 16:14 | history | edited | YCor |
edited tags
|
|
| Mar 8, 2019 at 16:05 | history | edited | 11Kilobytes | CC BY-SA 4.0 |
deleted 69 characters in body
|
| Feb 21, 2015 at 13:34 | vote | accept | 11Kilobytes | ||
| Feb 19, 2015 at 23:42 | answer | added | Anton Fetisov | timeline score: 4 | |
| Feb 18, 2015 at 23:03 | comment | added | Ptharien's Flame | @NoahSnyder The suspension of a type $T$ is defined as the higher inductive type $\Sigma T$ generated by two point constructors $\mathrm{N} : \Sigma T$ and $\mathrm{S} : \Sigma T$ and one 1-path constructor $\mathrm{merid} : T \to \mathrm{N} = \mathrm{S}$. This is the definition 11Kilobytes is using. | |
| Feb 17, 2015 at 20:29 | comment | added | Noah Snyder | I'm a bit confused about what your definition of $\Sigma S^1$ is. I would have expected it to be generated by one point, one 1-loop, and two 2-paths trivializing the 1-loop. But you seem to have two points. Could you clarify your notation a little? | |
| Feb 14, 2015 at 18:31 | review | First posts | |||
| Feb 14, 2015 at 18:45 | |||||
| Feb 14, 2015 at 18:28 | history | asked | 11Kilobytes | CC BY-SA 3.0 |