I'm having some beginner problems understanding / proving simple facts about higher inductive type paths.

If you take this higher inductive type for natural numbers modulo 1:

```
hit N1 :=
| 0 : N1
| S : N1 -> N1
| mod : 0 = 1
```

..I have the strong feeling that this corresponds exactly to (is equivalent to) the circle $S^1$ (with $b:S^1$ and $l:b=b$). Where the circle has $\pi_1(S¹, b) \cong (\mathbb{Z}, +, 0)$ by the isomorphism $n \mapsto l^n$, I'd think that `N1`

has $\pi_1($`N1`

$, 0) \cong (\mathbb{Z}, +, 0)$ too, by the isomorphism $n \mapsto \textrm{mod}^n$.

However, I have to take into account $\textrm{ap}_S$ as well. If it doesn't hold that $\textrm{ap}_S(\textrm{mod})= \textrm{mod}$, then things are obviously more complicated. I feel that this must hold, because of course $\textrm{ap}_S$ doesn't create new paths out of the blue, and thus the only paths that it could map $\textrm{mod}$ to are the $\textrm{mod}^n$, of which only $\textrm{mod}$ seems reasonable.

Does this hold, and if so, how would I prove it, and if not, what mistakes am I making?

(I know that I'm glossing over details, because, for one, $\textrm{mod}:0=1$, and therefore literal $\textrm{mod}\cdot\textrm{mod}$ doesn't even typecheck. But I don't believe this is relevant, because substituting all these $\textrm{mod}$'s by $(\textrm{mod}^{-1})_\star(\textrm{mod}) : 0=0$, for the family $P(n) := 0=n$, would solve these superficial issues.)