8.8 Whiteheadâs theorem and Whiteheadâs principle
In classical homotopy theory, a map which induces an isomorphism for all points in (and also an isomorphism ) is necessarily a homotopy equivalence, as long as the spaces and 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 -groupoids, 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 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 -truncated for some finite , by “downward” induction on . 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.
Note that 2 is precisely the statement that is an embedding, c.f. \autorefsec:mono-surj. Thus, by \autorefthm:mono-surj-equiv, it suffices to show that is surjective, i.e. that for any we have . Suppose given ; then since is surjective, there merely exists an such that . And since our goal is a mere proposition, we may assume given such an . Then we have , hence . Again, since our goal is still a mere proposition, we may assume . Hence is inhabited, and thus merely inhabited. ∎
Suppose is a function such that
is a bijection, and
for any , the function is an equivalence.
Then is an equivalence.
By \autorefthm:whitehead0, it suffices to show that is an equivalence for any . And by \autorefthm:equiv-inhabcod, we may assume . In particular, , so since is an equivalence, we have , hence . Since we are trying to prove a mere proposition ( being an equivalence), we may assume given . 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.
Suppose and are -types and is such that
is an isomorphism, and
is a bijection for all and all .
Then is an equivalence.
We proceed by induction on . When , the statement is trivial. Thus, suppose it to be true for all functions between -types, and let and be -types and as above. The first condition in \autorefthm:whitehead1 holds by assumption, so it will suffice to show that for any , the function is an equivalence. However, and are -types, and , so this follows from the inductive hypothesis. ∎
Note that if and are not -types for any finite , then there is no way for the induction to get started.
Apply \autorefthm:whiteheadn to the map . ∎
As an application, we can deduce the converse of \autorefthm:conn-pik.
For , a map is -connected if and only if the following all hold:
is an isomorphism.
For any and , the map is an isomorphism.
For any , the map is surjective.
The “only if” direction is \autorefthm:conn-pik. Conversely, by the long exact sequence of a fibration (\autorefthm:les), the hypotheses imply that for all and , and that is contractible. Since for , and is -connected, by \autorefthm:whitehead-contr it is contractible for any .
It remains to show that is contractible for not necessarily of the form . However, by assumption, there is with . Since contractibility is a mere proposition, we may assume is of the form for , in which case , and therefore . Again since contractibility is a mere proposition, we may assume , and the result follows. ∎
A map such that is a bijection and is a bijection for all is called -connected or a weak equivalence. This is equivalent to asking that be -connected for all . A type is called -truncated or hypercomplete if the induced map
is an equivalence whenever is -connected — that is, if 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 -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 -types for any , but in fact there are. Indeed, in classical homotopy theory, has this property for any . 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”.
Suppose we have such that for each , the type contains an -loop which is not equal to -fold reflexivity, say with . (For instance, we could define , with the image of under the isomorphism .) Consider , with the point defined by . Since loop spaces commute with products, for any we have
Under this equivalence, corresponds to the function . Now define in the right-hand type by
If we had , then we would have , which is not the case. Thus, , and so there is a point of which is unequal to . Hence is not an -type, for any .
We expect it should also be possible to show that a universe itself is not an -type for any , using the fact that it contains higher inductive types such as for all . However, this has not yet been done.
|Title||8.8 Whiteheadâs theorem and Whiteheadâs principle|