(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:

data Sphere where
  base : Sphere
  skin : Id (Id Sphere base base) refl refl

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?


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.

  • $\begingroup$ That's great, thanks! So you have three identifications going on, first the end points and then the two resulting loops to a refl each. Wouldn't it be easier to identify the paths with refl and then obtain the identity of the end points as a corollary? Or is it the case that we aren't entitled to contract paths to refl unless we asserted that they are loops? (I think I answered my question already.) $\endgroup$ – heisenbug Apr 24 '15 at 8:31
  • $\begingroup$ Yes, you answered your question :-) $\endgroup$ – Andrej Bauer Apr 24 '15 at 9:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.