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.

• First thought: both categories $\mathbf{Top}$ and $\mathbf{hTop}$ have topological spaces as objects. A space $X$ is contractible in $\mathbf{Top}$ iff it is terminal in $\mathbf{hTop}$. – drhab Oct 31 '14 at 10:02
• @NikolajK: I am not sure if I understand your first question correctly, but in classical topology, a map $f: X\to Y$ between topological spaces is a weak equivalence if and only if for all $y\in Y$ the homotopy fiber of $f$ over $y$ is weakly trivial, and this is what is captured by the definition of $\text{isEquiv}$. – Hanno Oct 31 '14 at 10:12
• @ZhenLin: If I define the real numbers in homotpopy type theory and then $[0,1]$ with the numbers $0.2$ and $2.5$ and $\pi/7$ three terms of it, which of the following is inhabited: $isSet([0,1])$, $isProp([0,1])$, $isContr([0,1])$. The first should be, the second one shouldn't and now I'm confused about the last. – Nikolaj-K Oct 31 '14 at 10:27
• The *****set***** $[0, 1]$ is not contractible, of course. – Zhen Lin Oct 31 '14 at 10:32
• The machinery needed to convert topological spaces into actual homotopy types does not yet exist in homotopy type theory (due to some technical difficulties). – Zhen Lin Oct 31 '14 at 11:29