5
$\begingroup$

$\newcommand\base{\mathit{base}}\newcommand\unique{\mathit{unique}}\DeclareMathOperator\transport{transport}\newcommand\loop{\mathit{loop}}\DeclareMathOperator\refl{refl}$In the context of homotopy type theory, I am trying to prove that the only element of $S^1$ is $\base$ i.e. $\unique: \prod_{x:S^1} \base=x$ however by using the induction principle of the circle I reach a dead end:

$$P: S^1 \rightarrow \mathcal{U}; P \mathrel{:\equiv} x \Rightarrow \base=x.$$

For induction, it is required an element $a: P(\base)$ and a path $l: \transport^P(\loop, a) = a$ that by transport over path spaces results in $l: a \cdot \loop = a$.

Choosing $a \mathrel{:\equiv} \refl_{\base}$ or $a \mathrel{:\equiv} \loop$ results on impossible paths (assuming univalence) i.e. $l: \loop = \refl_{\base}$ and $l: \loop \cdot \loop = \loop$.

This made me think if $S^1$ have other elements other than base? or there is some other path $a: \base = \base$ that makes $l$ be derivable, but which ones?

Improve this question
$\endgroup$
11
  • 4
    $\begingroup$ The circle is connected, but not contractable. That is, everything of type $S^1$ is merely equal to base, but the statement you're trying to prove is false. $\endgroup$
    – Noah Snyder
    Commented Sep 14, 2023 at 0:49
  • 14
    $\begingroup$ Wow, I don't understand this question at all. $\endgroup$
    – Zach Teitler
    Commented Sep 14, 2023 at 0:53
  • 5
    $\begingroup$ Nor do I. (But at least the question has the correct spelling of "contractible".) $\endgroup$
    – Daniel Asimov
    Commented Sep 14, 2023 at 1:31
  • 5
    $\begingroup$ I would be curious to hear whether the close vote is the result of fear of the unknown, or a HoTT expert thinking this question is too basic for MO (which it is). $\endgroup$
    – Andrej Bauer
    Commented Sep 14, 2023 at 5:56
  • 13
    $\begingroup$ HoTT is well beyond the standard graduate syllabus which a mathematician should be expected to know; there are many many of us who don't understand it. I don't think we should be closing down questions about how to do basic things in HoTT on the grounds that they are obvious to people who know HoTT. $\endgroup$
    – David E Speyer
    Commented Sep 14, 2023 at 19:36

2 Answers 2

Reset to default
6
$\begingroup$

Perhaps this will help: in homotopy type theory, to say that $x$ and $y$ of type $A$ are different corresponds intuitively to the fact that they are in different connected components, i.e., there is no path between them.

Specifically, for the circle $S^1$:

  • The statement $\Pi(x, y: S^1).\, x = y$ ("All points are equal") should be understood geometrically as saying that there is a continuous map which to each pair of points assigns a path between them.

  • The statement $\Sigma(x, y : S^1).\, x \neq y$ ("There are two different points") should be understood as saying that there are points on the circle which are not connected by a path.

Neither of the above is the case. What is the case, though is that $\Pi (x, y : S^1) . \|x = y\|_{-1}$ ("Every two points are in the same connectedness component.")

Improve this answer
$\endgroup$
5
  • $\begingroup$ This answer brings me some ideas (correct me if I am misunderstanding): I cannot prove the first case, since the function itself could raise paths that will conflict in some way with univalence. By truncating it, we deny this possibility and make it consistent. Something similar as the case of LEM, where we can assume it consistently if we truncate it to only mere propositions. $\endgroup$
    – Daniel Murcia
    Commented Sep 14, 2023 at 23:19
  • $\begingroup$ Yes, it's a bit like that. $\endgroup$
    – Andrej Bauer
    Commented Sep 15, 2023 at 6:23
  • $\begingroup$ That should either be $\| x = y \|_{-1}$ or $\| x \|_0 = \| y \|_0$. $\endgroup$
    – Naïm Favier
    Commented Feb 2 at 9:01
  • $\begingroup$ @NaïmFavier: thanks, fixed. By the way, you can just edit people's answers around here. $\endgroup$
    – Andrej Bauer
    Commented Feb 2 at 9:24
  • $\begingroup$ I know, but I didn't know which one you meant precisely! (Not that it matters, as they are equivalent.) $\endgroup$
    – Naïm Favier
    Commented Feb 2 at 9:50
5
$\begingroup$

The question was answered by Noah Snyder in the comments: No, $S^1$ is not contractible.

It connected, so any point in $S^1$ is merely equal to $base$.

To prove that $S^1$ is not contractible, you might try proving that the identity type $base = base$ is equivalent to $\mathbb Z$, e.g. via the encode-decode method.

Improve this answer
$\endgroup$
5
  • $\begingroup$ I understand that the type $base=base$ is not contractible because different elements can be generated from loop and concatenation. But if $S^1$ is not contractible, I would expect something similar to its path space, i.e. building some sort of non-trivial points that are different from base. How the non-trivial path loop can affect the fact that there is only one point, i.e. base? $\endgroup$
    – Daniel Murcia
    Commented Sep 14, 2023 at 3:59
  • 1
    $\begingroup$ The nontrivial loop does not affect the fact that there merely is only one point. It's possible to merely have only one point and not be contractible. This is homotopy type theory, after all. $\endgroup$
    – Tim Campion
    Commented Sep 14, 2023 at 4:02
  • $\begingroup$ By "merely" you refer to propositional truncation? $\endgroup$
    – Daniel Murcia
    Commented Sep 14, 2023 at 4:11
  • 2
    $\begingroup$ Yes, "merely" is the terminology from the HoTT book. Speaking of which, have you not looked at it? Chapter 6 begins with a detailed explanation of what is going on with the circle, with pictures in color. $\endgroup$
    – Andrej Bauer
    Commented Sep 14, 2023 at 5:54
  • $\begingroup$ Yes, I have read it many times and this question comes as an attempt to understand it more. $\endgroup$
    – Daniel Murcia
    Commented Sep 14, 2023 at 23:02

You must log in to answer this question.

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