1
$\begingroup$

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

$\endgroup$

closed as off-topic by Franz Lemmermeyer, Mike Shulman, Wolfgang, Jan-Christoph Schlage-Puchta, Myshkin Oct 31 '16 at 3:25

This question appears to be off-topic. The users who voted to close gave this specific reason:

  • "This question does not appear to be about research level mathematics within the scope defined in the help center." – Franz Lemmermeyer, Mike Shulman, Wolfgang, Myshkin
If this question can be reworded to fit the rules in the help center, please edit the question.

  • $\begingroup$ 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.) $\endgroup$ – Kelley van Evert Oct 31 '16 at 10:00
4
$\begingroup$

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
$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Kelley van Evert Oct 30 '16 at 17:51

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