patternMinor
Constructing a sphere ($S^2$) in HoTT directly?
Viewed 0 times
sphereconstructingdirectlyhott
Problem
(this is a repost of https://stackoverflow.com/questions/29802501/constructing-a-sphere-s2-in-hott-directly, which was voted out of SO)
I understand the construction of $S^2$ as a suspension of $S^1$ in homotopy type theory. I wonder whether one can build $S^2$ in one step as a base point and an open 2-surface. Something like this:
The above is probably something like a sausage with endpoints identified, though.
So my question is: Can an $S^2$ be built as a HIT from a closed 1-ball whose boundary is identified?
I understand the construction of $S^2$ as a suspension of $S^1$ in homotopy type theory. I wonder whether one can build $S^2$ in one step as a base point and an open 2-surface. Something like this:
data Sphere where
base : Sphere
skin : Id (Id Sphere base base) refl reflThe above is probably something like a sausage with endpoints identified, though.
So my question is: Can an $S^2$ be built as a HIT from a closed 1-ball whose boundary is identified?
Solution
This was asked once on the HoTT-cafe list. The answer is "yes" and I composed a short video which explains exactly how this happens.
Context
StackExchange Computer Science Q#41757, answer score: 6
Revisions (0)
No revisions yet.