8.8 Whitehead’s theorem and Whitehead’s principle

In classical homotopy theory, a map $f:A\to B$ which induces an isomorphism ${\pi }_n(A,a)\cong {\pi }_n(B,f(a))$ for all points $a$ in $A$ (and also an isomorphism ${\pi }_0(A)\cong {\pi }_0(B)$) is necessarily a homotopy equivalence, as long as the spaces $A$ and $B$ are well-behaved (e.g. have the homotopy types of CW-complexes). This is known as Whitehead’s theorem. In fact, the “ill-behaved” spaces for which Whitehead’s theorem fails are invisible to type theory. Roughly, the well-behaved topological spaces suffice to present $\mathrm{\infty }$-groupoids, and homotopy type theory deals with $\mathrm{\infty }$-groupoids directly rather than actual topological spaces. Thus, one might expect that Whitehead’s theorem would be true in univalent foundations.

However, this is not the case: Whitehead’s theorem is not provable. In fact, there are known models of type theory in which it fails to be true, although for entirely different reasons than its failure for ill-behaved topological spaces. These models are “non-hypercomplete $\mathrm{\infty }$-toposes” (see [lurie:higher-topoi]); roughly speaking, they consist of sheaves of $\mathrm{\infty }$-groupoids over $\mathrm{\infty }$-dimensional base spaces.

From a foundational point of view, therefore, we may speak of Whitehead’s principle as a “classicality axiom”, akin to $\mathrm{𝖫𝖤𝖬}$ and $\mathrm{𝖠𝖢}$. It may consistently be assumed, but it is not part of the computationally motivated type theory, nor does it hold in all natural models. But when working from set-theoretic foundations, this principle is invisible: it cannot fail to be true in a world where $\mathrm{\infty }$-groupoids are built up out of sets (using topological spaces, simplicial sets, or any other such model).

This may seem odd, but actually it should not be surprising. Homotopy type theory is the abstract theory of homotopy types, whereas the homotopy theory of topological spaces or simplicial sets in set theory is a concrete model of this theory, in the same way that the integers are a concrete model of the abstract theory of rings. It is to be expected that any concrete model will have special properties which are not intrinsic to the corresponding abstract theory, but which we might sometimes want to assume as additional axioms (e.g. the integers are a Principal Ideal Domain, but not all rings are).

It is beyond the scope of this book to describe any models of type theory, so we will not explain how Whitehead’s principle might fail in some of them. However, we can prove that it holds whenever the types involved are $n$-truncated for some finite $n$, by “downward” induction on $n$. In addition to being of interest in its own right (for instance, it implies the essential uniqueness of Eilenberg–Mac Lane spaces), the proof of this result will hopefully provide some intuitive explanation for why we cannot hope to prove an analogous theorem without truncation hypotheses.

We begin with the following modification of thm:mono-surj-equiv, which will eventually supply the induction step in the proof of the truncated Whitehead’s principle. It may be regarded as a type-theoretic, $\mathrm{\infty }$-groupoidal version of the classical statement that a fully faithful and essentially surjective functor is an equivalence of categories.

Theorem 8.8.1.

Suppose $f\mathrm{:}A\mathrm{\to }B$ is a function such that

1. $\parallel f{\parallel }_0:\parallel A{\parallel }_0\to \parallel B{\parallel }_0$ is surjective, and

2. for any $x,y:A$, the function ${\mathrm{𝖺𝗉}}_f:(x{=}_{A}y)\to (f(x){=}_{B}f(y))$ is an equivalence.

Then $f$ is an equivalence.

Proof.

Note that 2 is precisely the statement that $f$ is an embedding, c.f. sec:mono-surj. Thus, by thm:mono-surj-equiv, it suffices to show that $f$ is surjective, i.e. that for any $b:B$ we have ${\parallel {\mathrm{𝖿𝗂𝖻}}_f(b)\parallel }_{-1}$. Suppose given $b$; then since ${\parallel f\parallel }_0$ is surjective, there merely exists an $a:A$ such that $\parallel f{\parallel }_0(|a{|}_0)=|b{|}_0$. And since our goal is a mere proposition, we may assume given such an $a$. Then we have $|f(a){|}_0=\parallel f{\parallel }_0(|a{|}_0)=|b{|}_0$, hence $\parallel f(a)=b{\parallel }_{-1}$. Again, since our goal is still a mere proposition, we may assume $f(a)=b$. Hence ${\mathrm{𝖿𝗂𝖻}}_f(b)$ is inhabited, and thus merely inhabited. ∎

Since homotopy groups are truncations of loop spaces, rather than path spaces, we need to modify this theorem to speak about these instead.

Corollary 8.8.2.

Suppose $f\mathrm{:}A\mathrm{\to }B$ is a function such that

1. $\parallel f{\parallel }_0:\parallel A{\parallel }_0\to \parallel B{\parallel }_0$ is a bijection, and

2. for any $x:A$, the function ${\mathrm{𝖺𝗉}}_f:\mathrm{\Omega }(A,x)\to \mathrm{\Omega }(B,f(x))$ is an equivalence.

Then $f$ is an equivalence.

Proof.

By thm:whitehead0, it suffices to show that ${\mathrm{𝖺𝗉}}_f:(x{=}_{A}y)\to (f(x){=}_{B}f(y))$ is an equivalence for any $x,y:A$. And by thm:equiv-inhabcod, we may assume $f(x){=}_{B}f(y)$. In particular, $|f(x){|}_0=|f(y){|}_0$, so since ${\parallel f\parallel }_0$ is an equivalence, we have $|x{|}_0=|y{|}_0$, hence $|x=y{|}_{-1}$. Since we are trying to prove a mere proposition ($f$ being an equivalence), we may assume given $p:x=y$. But now the following square commutes up to homotopy:

The top and bottom maps are equivalences, and the left-hand map is so by assumption. Hence, by the 2-out-of-3 property, so is the right-hand map. ∎

Now we can prove the truncated Whitehead’s principle.

Theorem 8.8.3.

Suppose $A$ and $B$ are $n$-types and $f\mathrm{:}A\mathrm{\to }B$ is such that

1. $\parallel f{\parallel }_0:\parallel A{\parallel }_0\to \parallel B{\parallel }_0$ is an isomorphism, and

2. ${\pi }_k(f):{\pi }_k(A,x)\to {\pi }_k(B,f(x))$ is a bijection for all $k\ge 1$ and all $x:A$.

Then $f$ is an equivalence.

Condition 1 is almost the case of 2 when $k=0$, except that it makes no reference to any basepoint $x:A$.

Proof.

We proceed by induction on $n$. When $n=-2$, the statement is trivial. Thus, suppose it to be true for all functions between $n$-types, and let $A$ and $B$ be $(n+1)$-types and $f:A\to B$ as above. The first condition in thm:whitehead1 holds by assumption, so it will suffice to show that for any $x:A$, the function ${\mathrm{𝖺𝗉}}_f:\mathrm{\Omega }(A,x)\to \mathrm{\Omega }(B,f(x))$ is an equivalence. However, $\mathrm{\Omega }(A,x)$ and $\mathrm{\Omega }(B,f(x))$ are $n$-types, and ${\pi }_k({\mathrm{𝖺𝗉}}_f)={\pi }_{k+1}(f)$, so this follows from the inductive hypothesis. ∎

Note that if $A$ and $B$ are not $n$-types for any finite $n$, then there is no way for the induction to get started.

Corollary 8.8.4.

If $A$ is a $\mathrm{0}$-connected $n$-type and ${\pi }_k\mathit{}\mathrm{(}A\mathrm{,}a\mathrm{)}\mathrm{=}\mathrm{0}$ for all $k$ and $a\mathrm{:}A$, then $A$ is contractible.

Proof.

Apply thm:whiteheadn to the map $A\to \mathrm{𝟏}$. ∎

As an application, we can deduce the converse of thm:conn-pik.

Corollary 8.8.5.

For $n\mathrm{\ge }\mathrm{0}$, a map $f\mathrm{:}A\mathrm{\to }B$ is $n$-connected if and only if the following all hold:

1. $\parallel f{\parallel }_0:\parallel A{\parallel }_0\to \parallel B{\parallel }_0$ is an isomorphism.

2. For any $a:A$ and $k\le n$, the map ${\pi }_k(f):{\pi }_k(A,a)\to {\pi }_k(B,f(a))$ is an isomorphism.

3. For any $a:A$, the map ${\pi }_{n+1}(f):{\pi }_{n+1}(A,a)\to {\pi }_{n+1}(B,f(a))$ is surjective.

Proof.

The “only if” direction is thm:conn-pik. Conversely, by the long exact sequence of a fibration (thm:les), the hypotheses imply that ${\pi }_k({\mathrm{𝖿𝗂𝖻}}_f(f(a)))=0$ for all $k\le n$ and $a:A$, and that ${\parallel {\mathrm{𝖿𝗂𝖻}}_f(f(a))\parallel }_0$ is contractible. Since ${\pi }_k({\mathrm{𝖿𝗂𝖻}}_f(f(a)))={\pi }_k(\parallel {\mathrm{𝖿𝗂𝖻}}_f(f(a)){\parallel }_n)$ for $k\le n$, and ${\parallel {\mathrm{𝖿𝗂𝖻}}_f(f(a))\parallel }_n$ is $n$-connected, by thm:whitehead-contr it is contractible for any $a$.

It remains to show that ${\parallel {\mathrm{𝖿𝗂𝖻}}_f(b)\parallel }_n$ is contractible for $b:B$ not necessarily of the form $f(a)$. However, by assumption, there is $x:\parallel A{\parallel }_0$ with $|b{|}_0=\parallel f{\parallel }_0(x)$. Since contractibility is a mere proposition, we may assume $x$ is of the form ${\left|a\right|}_0$ for $a:A$, in which case $|b{|}_0=\parallel f{\parallel }_0(|a{|}_0)=|f(a){|}_0$, and therefore $\parallel b=f(a){\parallel }_{-1}$. Again since contractibility is a mere proposition, we may assume $b=f(a)$, and the result follows. ∎

A map $f$ such that ${\parallel f\parallel }_0$ is a bijection and ${\pi }_k(f)$ is a bijection for all $k$ is called $\mathrm{\infty }$-connected or a weak equivalence. This is equivalent to asking that $f$ be $n$-connected for all $n$. A type $Z$ is called $\mathrm{\infty }$-truncated or hypercomplete if the induced map

$$(\text{–}\circ f):(B\to Z)\to (A\to Z)$$

is an equivalence whenever $f$ is $\mathrm{\infty }$-connected — that is, if $Z$ thinks every $\mathrm{\infty }$-connected map is an equivalence. Then if we want to assume Whitehead’s principle as an axiom, we may use either of the following equivalent forms.

• Every $\mathrm{\infty }$-connected function is an equivalence.

• Every type is $\mathrm{\infty }$-truncated.

In higher topos models, the $\mathrm{\infty }$-truncated types form a reflective subuniverse in the sense of sec:modalities (the “hypercompletion” of an $(\mathrm{\infty },1)$-topos), but we do not know whether this is true in general.

It may not be obvious that there are any types which are not $n$-types for any $n$, but in fact there are. Indeed, in classical homotopy theory, ${𝕊}^n$ has this property for any $n\ge 2$. We have not proven this fact in homotopy type theory yet, but there are other types which we can prove to have “infinite truncation level”.

Example 8.8.6.

Suppose we have $B\mathrm{:}\mathrm{N}\mathrm{\to }\mathrm{U}$ such that for each $n$, the type $B\mathit{}\mathrm{(}n\mathrm{)}$ contains an $n$-loop which is not equal to $n$-fold reflexivity, say $p_n\mathrm{:}{\mathrm{\Omega }}^n\mathit{}\mathrm{(}B\mathit{}\mathrm{(}n\mathrm{)}\mathrm{,}{b}_n\mathrm{)}$ with $p_n\mathrm{\ne }{\mathrm{refl}}_{b_n}^n$. (For instance, we could define $B\mathrm{(}n\mathrm{)}\mathrm{:}\mathrm{\equiv }{\mathrm{S}}^n$, with $p_n$ the image of $\mathrm{1}\mathrm{:}\mathrm{Z}$ under the isomorphism ${\pi }_n\mathit{}\mathrm{(}{\mathrm{S}}^n\mathrm{)}\mathrm{\cong }\mathrm{Z}$.) Consider $C\mathrm{:}\mathrm{\equiv }{\mathrm{\prod }}_{\mathrm{(}n\mathrm{:}\mathrm{N}\mathrm{)}}B\mathrm{(}n\mathrm{)}$, with the point $c\mathrm{:}C$ defined by $c\mathrm{(}n\mathrm{)}\mathrm{:}\mathrm{\equiv }{b}_n$. Since loop spaces commute with products, for any $m$ we have

$${\mathrm{\Omega }}^m(C,c)\simeq \prod _{n:\mathbb{N}}{\mathrm{\Omega }}^m(B(n),b_n).$$

Under this equivalence, ${\mathrm{refl}}_c^m$ corresponds to the function $\mathrm{(}n\mathrm{\mapsto }{\mathrm{refl}}_{b_n}^m\mathrm{)}$. Now define $q_m$ in the right-hand type by

If we had $q_m\mathrm{=}\mathrm{(}n\mathrm{\mapsto }{\mathrm{refl}}_{b_n}^m\mathrm{)}$, then we would have $p_n\mathrm{=}{\mathrm{refl}}_{b_n}^n$, which is not the case. Thus, $q_m\mathrm{\ne }\mathrm{(}n\mathrm{\mapsto }{\mathrm{refl}}_{b_n}^m\mathrm{)}$, and so there is a point of ${\mathrm{\Omega }}^m\mathit{}\mathrm{(}C\mathrm{,}c\mathrm{)}$ which is unequal to ${\mathrm{refl}}_c^m$. Hence $C$ is not an $m$-type, for any $m\mathrm{:}\mathrm{N}$.

We expect it should also be possible to show that a universe $𝒰$ itself is not an $n$-type for any $n$, using the fact that it contains higher inductive types such as ${𝕊}^n$ for all $n$. However, this has not yet been done.

Title	8.8 Whitehead’s theorem and Whitehead’s principle