The necklace can be obtained from a circle by attaching $n$ 2-spheres along arcs, so the necklace is homotopy equivalent to the space obtained by attaching $n$ 2-spheres to a circle at points. My question is how to construct the necklace in homotopy type theory.