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.
Best Answer
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.