Help with simple homotopy type theory proof [closed]

Question

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.)

Answer 1

Your type is contractible. Picture it like this: it has the natural numbers, a path from 0 to 1, and all the images of this path under the successor function, and thus paths from 1 to 2, 2 to 3, etc.

Here's a proof in Lean:

import cubical.square
open eq is_trunc

section
  parameter N₁ : Type₀
  parameter O : N₁
  parameter S : N₁ → N₁
  parameter mod : O = (S O)

  parameter N₁_elim : Π {P : N₁ → Type₀} (p_O : P O)
    (p_S : Π(n : N₁), P n → P (S n))
    (p_mod : p_O =[mod] p_S O p_O) (n : N₁), P n

  include N₁_elim

  definition is_contr_N₁ : is_contr N₁ :=
  begin
    apply is_contr.mk O,
    fapply N₁_elim,
    { reflexivity },
    { intros n IH, exact mod ⬝ ap S IH },
    { apply eq_pathover, esimp, rewrite [ap_constant,ap_id],
      apply square_of_eq, reflexivity }
  end
end