# Constructing a sphere ($S^2$) in HoTT directly?

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

• 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.) – heisenbug Apr 24 '15 at 8:31