0
$\begingroup$

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.

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

1 Answer 1

Reset to default
2
$\begingroup$

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.
Improve this answer
$\endgroup$

Not the answer you're looking for? Browse other questions tagged .