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.

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

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.

Not the answer you're looking for? Browse other questions tagged or ask your own question.