HiveBrain v1.2.0
Get Started
← Back to all entries
patternMinor

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

Submitted by: @import:stackexchange-cs··
0
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:

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?

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.