# Help with simple homotopy type theory proof [closed]

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

• I was wondering why this was put on hold, but then I just found out there are two distinct maths stackoverflows: mathoverflow and math.stackexchange ..! I bit confusing, but now I understand this was the wrong one to put up this question. Sorry!I was wondering why this was put on hold, but then I just found out there are two distinct maths stackoverflows: mathoverflow and math.stackexchange ..! I bit confusing, but now I understand this was the wrong one to put up this question. (Sorry! Remove at will.) – Kelley van Evert Oct 31 '16 at 10:00

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

• Thanks a lot :) This is very helpful, as it not only answers my question, but also gives some implicit direction in learning to effectively prove in Lean. I haven't used the eq_pathover method before. – Kelley van Evert Oct 30 '16 at 17:51