1
$\begingroup$

I know that the circle type is not supposed to be contractible in homotopy type theory. But by the definition of contractible, it seems like it is.

Define the circle type $S^1$ as the higher inductive type with two constructors, $\mathrm{pt} : S^1$ and $\mathrm{loop} : \mathrm{pt} = \mathrm{pt}$.

Define the modality $\mathrm{isContr}$ as $\mathrm{isContr}(X) := \sum_{x : X} \prod_{y : X} x = y$.

Now we want to construct an $f$ such that $(\mathrm{pt}, f) : \mathrm{isContr}(S^1)$. This means $f : \prod_{y : S^1} \mathrm{pt} = y$. Now we can use the induction principle of $S^1$ to construct $f$. Define $f(\mathrm{pt}) := \mathrm{refl}_{\mathrm{pt}}$ and $\mathrm{apd}_f(\mathrm{loop}) := \mathrm{refl}_{\mathrm{refl}_{\mathrm{pt}}}$.

This seems to complete the proof that $\mathrm{isContr}(S^1)$ is inhabited. What is wrong with the above?

$\endgroup$

1 Answer 1

3
$\begingroup$

When doing induction on $y$, the type you're trying to inhabit, $\mathrm{pt} = y$, depends on $y$. That means that you need to use the dependent induction principle, which is what makes your argument not work.

Dependent induction for the circle (see here) says that for a dependent type $P : S^1 \to \mathrm{Type}$, to prove $\prod_{s : S^1}P(s)$, we need to provide $p_\mathrm{pt} : P(\mathrm{pt})$ and $p_{\mathrm{loop}} : \mathrm{transport}_P(\mathrm{loop}, p_\mathrm{pt}) = p_\mathrm{pt}$. This transport is what causes problems.

For you, $p_\mathrm{base} := \mathrm{refl}_\mathrm{pt}$, so $p_{\mathrm{loop}}$ should be in $\mathrm{transport}_P(\mathrm{loop}, \mathrm{refl}_\mathrm{pt}) = \mathrm{refl}_\mathrm{pt}$. But the left side is $\mathrm{loop}$ and the right side is is not. That makes your proposal of $p_{\mathrm{loop}} := \mathrm{refl}_{\mathrm{refl}_\mathrm{pt}}$ ill-typed.


Addendum: proving that $\mathrm{transport}_P(\mathrm{loop}, \mathrm{refl}_\mathrm{pt})$ is $\mathrm{loop}$ for $P(y) := \mathrm{pt} = y$ is done by generalizing. This is a typical situation when doing proofs with induction, since induction proves statements of the form "for all ...". Specifically, we can prove in generality that for any type $A$, any points $a, b : A$, $P(x) := a = x$ and $p: a = b$, $\mathrm{transport}_P(p, \mathrm{refl}_a) = p$. We can use induction on $p$. For $p \equiv \mathrm{refl}_a$, our statement reduces to $\mathrm{transport}_P(\mathrm{refl}_a, \mathrm{refl}_a) = \mathrm{refl}_a$, which is trivially true due to the definition of transport.

The statement we needed is a particular case of this with $A = S^1$, $a = b = \mathrm{pt}$ and $p = \mathrm{loop}$.

$\endgroup$
2
  • $\begingroup$ Thanks for your answer. Does that mean that this paragraph from ncatlab.org is wrong? i.stack.imgur.com/12GqZ.png Should it instead say $\mathrm{loop' : transport(loop, base') = base'}$? $\endgroup$
    – Adrian
    Mar 1, 2023 at 3:35
  • $\begingroup$ I think it should say that. I think the author meant that based on the phrase "dependent path", since without it, it's just a regular path. $\endgroup$
    – S.C.
    Mar 1, 2023 at 5:27

You must log in to answer this question.

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