Being contractible in homotopy theory vs. homotopy type theory I'm trying to clarify the notion of being contractible in homotopy theory vs. homotopy type theory. 


*

*Is the following right?


"In homotopy theory the real interval $[0,1]$, considered as a subset of $\mathbb R$, is contractible. In contrast, for a set in homotopy type theory, isContr is only inhabited if that the set (extensionally) is empty or a singleton."
Looking at the relevant definitions I reproduced below, the answer should be yes. Because as terms of identity types, those sort of paths the type theory speaks about are simply not there in a "setty" homotopy theory, where a path means moving through a set. This then leads me to ask: 


*

*Does isEquiv, which is defined in terms of isContr, directly capture homotopy equivalence in the traditional sense. How can this still be used to natively describe geometric kind of paths, which are not relations signifying equality of the end points?

*If we set up categories in homotopy type theory, what categories are contractible? For this last point, I ask a related question on theoreticalCS.SE. here.

I've added text to the definitions to make clear where my dissonance comes from.
$isProp(A) := \prod_{x\colon A} \prod_{y\colon A}\ \ x=y$
For all terms x,y in A we can show that they are equal. (Roughly, A has one unique term or none, just like truth and falsehood.)
$isSet(A) := \prod_{x\colon A} \prod_{y\colon A} isProp(x=y)$
For all terms x in A, we can for all terms y in A shown that the type x=y is a proposition and not a complicated path space. Either x and y are not equal or they are equal in a unique way.
$isContr(A) := \sum_{x\colon A} \prod_{y\colon A}\ \ y=x$
A collection of all x's in A together with the way to to show, for all terms y in A, that y is equal to x in some way. This type is the same as the direct product of A with isProp(A).
$isEquiv(f:A\to B) := \prod_{b\colon B} isContr\left( \sum_{x\colon A}\ \ f(x) = b \right)$
For all b in the base we can show that the fibres (the collection of x's which make up the kernel of f over b) is contractible.
 A: It's very important not to confuse the "topological" words used to describe the higher-groupoidal aspects of types in HoTT with the sets and topological spaces that can be defined internally to HoTT (just as they can in any sort of mathematics).  This problem of terminology arises because homotopy theory studies objects that are properly called ∞-groupoids, but it traditionally presents them as the fundamental ∞-groupoid of some topological space and then works with that space rather than the ∞-groupoid itself, and thereby uses topological terminology.
The real numbers, as defined in HoTT (or any sort of mathematics, really), are a set (any two real numbers are equal in at most one way) that can be equipped with a topology.  The interval [0,1] can be defined as a subset of the reals, so it is likewise a set equipped with a topology.  Of course, these sets have many unequal elements in them, but any two of their elements are related by a continuous path.
Now the fundamental ∞-groupoid of a topological space discards the topology, but remembers the paths, making them instead into equalities a.k.a. isomorphisms a.k.a. equivalences.  So in the fundamental ∞-groupoid of the real numbers or [0,1], it is true that any two elements are equal, and so these ∞-groupoids are contractible.
The types in HoTT behave like ∞-groupoids, not topological spaces, and their groupoidal structure is intrinsic and unrelated to any topology (in the usual sense) that we might choose to define on them (using open sets, etc.).  In particular, the higher inductive type called the "interval" is very different from the subset [0,1] of the set of real numbers.  The latter could be equipped with its usual Euclidean topology, or the discrete topology, or the indiscrete topology, or many others; but none of those topologies have anything to do with its intrinsic ∞-groupoid structure (according to which it is a set, having no higher groupoidal structure).
In principle, as Zhen says, one ought to be able to perform the "fundamental ∞-groupoid" construction inside HoTT to arrive at the former from the latter, but there are currently technical obstructions to making that precise.
