Perhaps I'm just not understanding how the definitions are actually supposed to work. In particular, the definition of $\mathbb{S}^{1}$ confuses me.

So first, we have $\text{base}:\mathbb{S}^{1}$ and $\text{loop}:\text{base}=\text{base}$

We also have $isProp(A):\equiv \prod_{x:A}\prod_{y:A}x=y$ and $isSet(A):\equiv \prod_{x:A}\prod_{y:A}\prod_{p:x=y}\prod_{q:x=y}p=q$

And it is taken for granted that for any $A$, $isProp(A)\rightarrow isSet(A)$, via path induction.

But $\text{base}$ is the only element of $\mathbb{S}^{1}$, so $isProp(\mathbb{S}^{1})$ is clearly inhabited, by either $\lambda x.\lambda y.\text{loop}$ or $\lambda x. \lambda y.\text{refl}_{\text{base}}$ or concatenations thereof. But because we have to assume $\text{loop}=\text{refl}_{\text{base}}$ is uninhabited, it's clear that $isSet(\mathbb{S}^{1})$ is, at best, a partial function, which I don't believe HoTT allows.

And that's only the start of the problems that I'm having trouble with. In general, it seems that the theory sets up rules for paths that are both expected to be adhered to and ignored at the same time. Can someone simplify this? Should I be assuming there are points in $\mathbb{S}^{1}$ that aren't $\text{base}$? Or is there another answer?

  • 1
    $\begingroup$ I don't know about "assuming there are points in $\mathbb S^1$ that aren't base", but I'm pretty sure you should not be assuming that all points in $\mathbb S^1$ are base. (Remember that we don't have classical logic available here.) $\endgroup$ – Andreas Blass Feb 6 '18 at 0:49
  • $\begingroup$ Is $\mathrm{base}$ really the only element of $\mathbb{S}^1$? If $\prod_{x : \mathbb{S}^1} x = \mathrm{base}$ were inhabited then $\mathbb{S}^1$ would be contractible (and thus, a proposition), but can you really exhibit an element of this type? $\endgroup$ – Hurkyl Feb 6 '18 at 13:04

If $\mathsf{isProp}(\mathbb S^1)$ is "clearly inhabited", what's the inhabitant?

Let's try to write it. The induction principle for $\mathbb S^1$ is: given $P:\mathbb S^1\to\mathcal U$, $b : P(\mathsf{base})$, and $\ell : \mathsf{transport}^P(\mathsf{loop}, b)=b$ where $\mathsf{transport}^P(p,-):P(x)\to P(y)$ given $p : x=y$ there is a $f:\prod_{x:\mathbb S^1}P(x)$ such that $f(\mathsf{base})=b$ and $\mathsf{apd}_f(\mathsf{loop})=\ell$.

It's pretty clear that we will need to use this induction principle with $P(x):\equiv\prod_{y:\mathbb S^1}(x=y)$ to show $\mathsf{isProp}(\mathbb S^1)$. We need to then produce a value of type $P(\mathsf{base})$, i.e. $\prod_{y:\mathbb S^1}(\mathsf{base}=y)$.

Again, it is pretty clear that we will need to use the induction principle. This time with $P'(y):\equiv(\mathsf{base}=y)$. Again, we need $P'(\mathsf{base})$, i.e. $\mathsf{base}=\mathsf{base}$. Easy enough, we can pick $\mathsf{refl}_{\mathsf{base}}$ or $\mathsf{loop}$ (or $\mathsf{loop}\centerdot\mathsf{loop}$, etc.), call this $p$. But to apply the induction principle, we also need an $\ell:\mathsf{transport}^{P'}(\mathsf{loop},p)=p$. Generally, we have $\mathsf{transport}^{\lambda y.x=y}(p,q) = q\centerdot p$, so $\mathsf{transport}^{P'}(\mathsf{loop},p)=p$ is asking for $p\centerdot\mathsf{loop}=p$. There are no values of this type though. If $p\equiv\mathsf{refl}_{\mathsf{base}}$, then this is just asking for $\mathsf{loop}=\mathsf{refl}_{\mathsf{base}}$ which is explicitly not true, and if $p\equiv\mathsf{loop}$, then we have $\mathsf{loop}\centerdot\mathsf{loop}=\mathsf{loop}$ which also isn't true.

$\mathbb S^1$ is more than just a point. Indeed, it is the $\mathsf{loop}$ part of $\mathbb{S}^1$ that is the important part. $\mathsf{base}$ is only there so we can talk about $\mathsf{loop}$. A value of type $\prod_{x:\mathbb S^1}P(x)$ doesn't just send points to points, it sends paths to paths. This is the homotopical aspect of Homotopy Type Theory. From a logical perspective, $f:\prod_{x:\mathbb S^1}P(x)$ doesn't only need to map points to points, it needs to preserve equivalences between those points (and equivalences between the equivalences and so on).

  • $\begingroup$ So I've pretty much been thinking about it wrong. The need for the induction principle to also consider actions on paths, as opposed to "standard" inductive types where you only consider how the points behave, confused me, I suppose. Thank you for answering what was probably a stupid question! $\endgroup$ – sk8torchic1 Feb 6 '18 at 21:41
  • $\begingroup$ It definitely wasn't a stupid question. The intuitions for HoTT (and for other constructive/non-classical frameworks) are quite different than classical mathematics, and it takes some time to develop them. However, "truth" in a constructive type theory means having the proof term in hand, so whenever you believe something is true you should endeavor to produce the proof term. You can even use proof assistants like Coq, Agda, or LEAN to ensure you haven't made any mistakes or neglected any details. $\endgroup$ – Derek Elkins Feb 7 '18 at 1:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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