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 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.
Post Closed as "Needs details or clarity" by Vladimir Dotsenko, Wolfgang, Marco Golla, Jan-Christoph Schlage-Puchta, Peter Humphries