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