2

There is a mainstream definition of a contractible type and it goes like this: $\textrm{isContr} (A) = (x:A) \,\#\, (y:A) \to (x == y)$, where $\#$ means dependent pair (precedence and associativity same as $\to$) and $==$ is a path type.

Now, if I read this as "there is an x:A such that there's path between every y:A and x", then it sounds like path-connectedness, not contractibility.

The imho more intuitive definition, $\textrm{isContr} (A) = (x:A) \to (\textrm{loop}:x==x) \to (\textrm{loop} == \textrm{refl}\, x)$, was deemed impractical. Edit: By some text I don't recall the name of.

I ask why is it so? What makes the "canonical" definition define contractibility when it intuitively corresponds to path-connectedness? Why is it more convenient to use?

Explanation for both HoTT and/or CuTT are welcome.

PS: I'm not sure whether the "more intuitive" loop definition of contractibility requires dependent function (for all), or whether a dependent pair suffices.

DrunkCoder
  • 353

1 Answers1

9

For contractibility defined as $\text{isContr}(A) :\equiv \Sigma_{a:A} \Pi_{x:A} (a=x)$, (cf. page 124 of the HoTT book), the intuitive idea is that every point $x$ is the same point as $a$.

The way you are reading the definition is common, and says:

"there is an $a$ such that for each $x$ there is a path from $a$ to $x$"

I completely agree, this sounds like path-connected-ness. However we get this reading by mixing our interpretations of types. Here we forget the topological data in the $\Sigma$ and $\Pi$ types (by reducing them to mere quantifiers) but we remember the topological data in the identity type!

If you want to use the quantifier lingo, stick to it. Then the sentence says

"there is an $a$ such that for each $x$, $a=x$"

which DOES sound like contractibility.

Alternatively, if you want to use topological intuition, you have to remember what $\Sigma$ and $\Pi$ types mean -- there's a naturality condition in how we pick our paths. With path-connected-ness we can pick each path separately, however we need to. However, because of naturality, we are saying there is some uniform way to find a path from any point $x$ to $a$ -- that's exactly what it means to have a deformation retract to $a$.

In this interpretation, $\text{isContr}(A)$ is the type of pairs $(a,r)$ where $a$ is a point in $A$ and $r$ is a deformation retract to $a$, which also sounds like a good definition for contractibility.

There's a very good discussion of exactly this mistake (which everyone makes, by the way) here, as well as good background reading motivating why the definitions are what they are.

If a blind appeal to naturality isn't satisfying, by the way, I encourage you to actually prove the associated theorem. It isn't very difficult, and it's what finally convinced me that $\text{isContr}$ was correct:

If $(a,r) : \text{isContr}(A)$, then $r$ is (judgementally) equal to the type $\text{const}_a \sim \text{id}_A$. That is, $r$ witnesses the constant function at $a$ is homotopic to the identity function on $A$, and so it is actually a deformation retract, as claimed.

Hope this helped ^_^

Edit:

I realize I've left out part of your question, so let me try to remedy that now.

Why not take $\text{intuitiveContr}(A) = \Pi_{x:A} \Pi_{\alpha : x=x} (\alpha = \text{refl}_x)$ as a definition? Leaving aside the fact that it admits the empty type as contractible (which is easily fixed), what bad can really come of it?

The more pressing reason to not take $\text{intuitiveContr}(A)$ as a definition is that it doesn't capture contractibility. Instead, it captures the notion of Simply Connected (cf. this article).

$\text{intuitiveContr}$ insists that all loops can be contracted to refl, but it says nothing about higher homotopy. The 2-sphere, for instance, satisfies $\text{intuitiveContr}$, but is not contractible. Even though there is no 1-dimensional obstruction to contractibility (i.e. every loop contracts to a point), there is a 2-dimensional obstruction to contractibility (the sphere is not filled in with a ball). Unfortunately, $\text{intuitiveContr}(A)$ misses this.

Part of the magic of $\text{isContr}$ is that it avoids this problem. One can prove (using function extensionality) that $\text{isContr}(A) \to \text{isContr}(\text{isContr}(A))$, and using this we can inductively show that homotopy vanishes in all dimensions.

Said another way, it is an easy exercise to show that contractible types are equivalent to $\textbf{1}$, the singleton type (also on page 124 of the HoTT book), so it is the right definition.

HallaSurvivor
  • 38,115
  • 4
  • 46
  • 87
  • A couple additions. 1) The loop definition given actually defines the empty space as contractible, because it's missing the inhabitation part. 2) In a similar vein to this answer, if we read the standard isContr like "path connected", isn't the alternate definition read as, "the loop space is path connected?" But e.g. the loop space of the sphere is path connected, right? – Dan Doel Sep 04 '19 at 22:48
  • Also, since the loop definition is the same as saying the loop space is contractible (via the standard notion), any HSet qualifies, because the loop space is a proposition with point refl. I expect a better definition involves two points, but then the problem mentioned occurs that refl doesn't go between two arbitrary points, so you need additional complications to mediate between between the paths, or similar. But it will probably boil down to writing a more complicated type just to convince yourself not to read it the wrong way, even though you still could.
    • – Dan Doel Sep 04 '19 at 22:55
  • What do you mean by missing inhabitation? I've left the inhabitation requirement for the standard definition implicit as well. – DrunkCoder Sep 05 '19 at 10:11
  • Also, how is the loop space of a circle path-connected? I'm in fact just a high schooler and I know just some basic topology, abs. algebra, and category theory. But how do you connect a loop that winds two times around the circle to that which does so just once? – DrunkCoder Sep 05 '19 at 10:22
  • 1
    In the standard isContr, the $Σ$ provides a value of $A$, proving it's inhabited. But the loop version above doesn't require that any points exist. Also, I mean sphere as in the surface of a globe. You can shrink 1-dimensional loops on the surface of a sphere to a point, but it isn't contractible (because there is a non-trivial 2-dimensional sheet that can't be shrunk). – Dan Doel Sep 05 '19 at 12:14
  • I think in more generality, the n-spheres are each something that looks contractible until you get up to dimension n (and the 0-sphere actually is defined to be contractible, I guess, according to a table on wikipedia). My topology is not too strong either, though, even though I've been studying things much longer. :) – Dan Doel Sep 05 '19 at 12:37
  • Oh I see, I've just misread and was thinking of a circle instead of a sphere :) Then you're right, circles on a sphere are all contractible. Do you think the loop definition could be expanded so that it's equivalent to the "singleton" definition? I'm sure I've seen something similar to it... – DrunkCoder Sep 05 '19 at 16:56
  • I mean, you could use $Σ{x:A}Π{y:A}Σ{p : x≡y}Π{q:x≡y} p≡q$, but this is equivalent to the original. And you can keep expanding the type in this way, and all of them are equivalent, just more verbose. – Dan Doel Sep 06 '19 at 11:56
  • By "there is some uniform way to find a path from any point $x$ to $a$", do you mean that the choice of path is continuous in the point $x$, or a different condition? – Jules Sep 14 '19 at 12:14
  • 1
    Exactly! cf. this answer: https://math.stackexchange.com/a/25965/655547 – HallaSurvivor Sep 15 '19 at 01:05