# Construction of the necklace by homotopy type theory [closed]

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.

## closed as unclear what you're asking by Vladimir Dotsenko, Wolfgang, Marco Golla, Jan-Christoph Schlage-Puchta, Peter HumphriesDec 17 '15 at 23:17

Please clarify your specific problem or add additional details to highlight exactly what you need. As it's currently written, it’s hard to tell exactly what you're asking. See the How to Ask page for help clarifying this question. If this question can be reworded to fit the rules in the help center, please edit the question.

• Can you include how you might set up notation for this in homotopy type theory, to set some conventions for answers? – j0equ1nn Dec 17 '15 at 7:16

Inductive Necklace (n:nat) :=