Skip to main content
2 of 2
add notations
Tom
  • 187
  • 1
  • 9

Construction of the necklace by homotopy type theory

The necklace can be obtained from a circle by attaching $n$ 2-spheres $S^2$ along arcs, so the necklace $N(n,S^1,a_i)$ is homotopy equivalent to the space obtained by attaching $n$ 2-spheres $S^2$ to a circle $S^1$ at points $a_i$ where $i \in [1,n]$. My question is how to construct the necklace $N(n,S^1,a_i)$ in homotopy type theory.

Tom
  • 187
  • 1
  • 9