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 Humphries Dec 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.
My guess would be
Inductive Necklace (n:nat) := | strand : Circle -> Necklace | bead : forall (k:nat), k<n -> Sphere2 -> Necklace | attach : forall (k:nat) (p:k<n), strand base = bead k p base2.