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?
Best Answer
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}$.