8.8 Whitehead’s theorem and Whitehead’s principle

In classical homotopy theory, a map f:AB which induces an isomorphismMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath πn(A,a)πn(B,f(a)) for all points a in A (and also an isomorphism π0(A)π0(B)) is necessarily a homotopy equivalenceMathworldPlanetmathPlanetmath, as long as the spaces A and B are well-behaved (e.g. have the homotopy types of CW-complexesMathworldPlanetmath). This is known as Whitehead’s theorem. In fact, the “ill-behaved” spaces for which Whitehead’s theorem fails are invisible to type theoryPlanetmathPlanetmath. Roughly, the well-behaved topological spacesMathworldPlanetmath suffice to present -groupoidsPlanetmathPlanetmathPlanetmathPlanetmath, and homotopy type theory deals with -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 -toposes” (see [lurie:higher-topoi]); roughly speaking, they consist of sheaves of -groupoids over -dimensional base spaces.

From a foundational point of view, therefore, we may speak of Whitehead’s principle as a “classicality axiom”, akin to 𝖫𝖤𝖬 and 𝖠𝖢. 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 -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 theoryMathworldPlanetmath 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 DomainMathworldPlanetmath, 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” inductionMathworldPlanetmath 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 \autorefthm: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, -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:AB is a function such that

  1. 1.

    f0:A0B0 is surjectivePlanetmathPlanetmath, and

  2. 2.

    for any x,y:A, the function 𝖺𝗉f:(x=Ay)(f(x)=Bf(y)) is an equivalence.

Then f is an equivalence.


Note that 2 is precisely the statement that f is an embeddingMathworldPlanetmath, c.f. \autorefsec:mono-surj. Thus, by \autorefthm:mono-surj-equiv, it suffices to show that f is surjective, i.e. that for any b:B we have 𝖿𝗂𝖻f(b)-1. Suppose given b; then since f0 is surjective, there merely exists an a:A such that f0(|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=f0(|a|0)=|b|0, hence f(a)=b-1. Again, since our goal is still a mere proposition, we may assume f(a)=b. Hence 𝖿𝗂𝖻f(b) is inhabited, and thus merely inhabited. ∎

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

Corollary 8.8.2.

Suppose f:AB is a function such that

  1. 1.

    f0:A0B0 is a bijection, and

  2. 2.

    for any x:A, the function 𝖺𝗉f:Ω(A,x)Ω(B,f(x)) is an equivalence.

Then f is an equivalence.


By \autorefthm:whitehead0, it suffices to show that 𝖺𝗉f:(x=Ay)(f(x)=Bf(y)) is an equivalence for any x,y:A. And by \autorefthm:equiv-inhabcod, we may assume f(x)=Bf(y). In particular, |f(x)|0=|f(y)|0, so since f0 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 homotopyMathworldPlanetmath:

\xymatrix @C=3pc Ω(A,x)\ar[r]^-– \centerdotp\ar[d]_𝖺𝗉f & (x=Ay\ar[d]^𝖺𝗉f
Ω(B,f(x))\ar[r]_-– \centerdotf(p) & (f(x)=Bf(y)). 

The top and bottom maps are equivalences, and the left-hand map is so by assumptionPlanetmathPlanetmath. 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:AB is such that

  1. 1.

    f0:A0B0 is an isomorphism, and

  2. 2.

    πk(f):πk(A,x)πk(B,f(x)) is a bijection for all k1 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.


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:AB as above. The first condition in \autorefthm:whitehead1 holds by assumption, so it will suffice to show that for any x:A, the function 𝖺𝗉f:Ω(A,x)Ω(B,f(x)) is an equivalence. However, Ω(A,x) and Ω(B,f(x)) are n-types, and πk(𝖺𝗉f)=π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 0-connected n-type and πk(A,a)=0 for all k and a:A, then A is contractibleMathworldPlanetmath.


Apply \autorefthm:whiteheadn to the map A𝟏. ∎

As an application, we can deduce the converseMathworldPlanetmath of \autorefthm:conn-pik.

Corollary 8.8.5.

For n0, a map f:AB is n-connected if and only if the following all hold:

  1. 1.

    f0:A0B0 is an isomorphism.

  2. 2.

    For any a:A and kn, the map πk(f):πk(A,a)πk(B,f(a)) is an isomorphism.

  3. 3.

    For any a:A, the map πn+1(f):πn+1(A,a)πn+1(B,f(a)) is surjective.


The “only if” direction is \autorefthm:conn-pik. Conversely, by the long exact sequence of a fibrationMathworldPlanetmath (\autorefthm:les), the hypotheses imply that πk(𝖿𝗂𝖻f(f(a)))=0 for all kn and a:A, and that 𝖿𝗂𝖻f(f(a))0 is contractible. Since πk(𝖿𝗂𝖻f(f(a)))=πk(𝖿𝗂𝖻f(f(a))n) for kn, and 𝖿𝗂𝖻f(f(a))n is n-connected, by \autorefthm:whitehead-contr it is contractible for any a.

It remains to show that 𝖿𝗂𝖻f(b)n is contractible for b:B not necessarily of the form f(a). However, by assumption, there is x:A0 with |b|0=f0(x). Since contractibility is a mere proposition, we may assume x is of the form |a|0 for a:A, in which case |b|0=f0(|a|0)=|f(a)|0, and therefore b=f(a)-1. Again since contractibility is a mere proposition, we may assume b=f(a), and the result follows. ∎

A map f such that f0 is a bijection and πk(f) is a bijection for all k is called -connected or a weak equivalenceMathworldPlanetmath. This is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath to asking that f be n-connected for all n. A type Z is called -truncated or hypercomplete if the induced map


is an equivalence whenever f is -connected — that is, if Z thinks every -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 -connected function is an equivalence.

  • Every type is -truncated.

In higher topos models, the -truncated types form a reflective subuniverse in the sense of \autorefsec:modalities (the “hypercompletion” of an (,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 n2. We have not proven this fact in homotopy type theory yet, but there are other types which we can prove to have “infiniteMathworldPlanetmath truncation level”.

Example 8.8.6.

Suppose we have B:NU such that for each n, the type B(n) contains an n-loop which is not equal to n-fold reflexivityMathworldPlanetmath, say pn:Ωn(B(n),bn) with pnreflbnn. (For instance, we could define B(n):Sn, with pn the image of 1:Z under the isomorphism πn(Sn)Z.) Consider C:(n:N)B(n), with the point c:C defined by c(n):bn. Since loop spaces commute with productsPlanetmathPlanetmathPlanetmath, for any m we have


Under this equivalence, reflcm corresponds to the function (nreflbnm). Now define qm in the right-hand type by


If we had qm=(nreflbnm), then we would have pn=reflbnn, which is not the case. Thus, qm(nreflbnm), and so there is a point of Ωm(C,c) which is unequal to reflcm. Hence C is not an m-type, for any m:N.

We expect it should also be possible to show that a universePlanetmathPlanetmath 𝒰 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