nLab
Whitehead theorem

Classical case

The classical Whitehead theorem asserts that

Theorem (Whitehead)

Every weak homotopy equivalence between CW-complexes is a homotopy equivalence.

(See also the discussion at m-cofibrant space).

Using the homotopy hypothesis-theorem this may be reformulated:

Corollary

In the (∞,1)-category ∞ Grpd every weak homotopy equivalence is a homotopy equivalence.

In general $(\mathrm{\infty },1)$-toposes

There is a notion of homotopy groups for objects in every ∞-stack (∞,1)-topos, as described at homotopy group (of an ∞-stack). Accordingly, there is a notion of weak homotopy equivalence in every ∞-stack (∞,1)-topos and hence an analog of the statement of Whiteheads theorem. One finds that

Warning Whitehead’s theorem fails for general (∞,1)-toposes and non-truncated objects.

The ∞-stack (∞,1)-toposes in which the Whitehead theorem does hold are the hypercomplete (∞,1)-toposes. These are precisely the ones that are presented by a local model structure on simplicial presheaves.

For instance the hypercomplete $(\mathrm{\infty },1)$-topos Top is presented by the model structure on simplicial presheaves on the point, namely the model structure on simplicial sets.

References

The $(\mathrm{\infty },1)$-topos version is in section 6.5 of

• Jacob Lurie, Higher Topos Theory

A formalization in homotopy type theory written in Agda is in

• Dan Licata, Whitehead.agda