# Why is the circle not contractible in homotopy type theory?

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?

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}$$.

• 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'}$? Mar 1, 2023 at 3:35
• 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.
– S.C.
Mar 1, 2023 at 5:27