structures in a cohesive (∞,1)-topos
The classical Whitehead theorem asserts that
(See also the discussion at m-cofibrant space).
Using the homotopy hypothesis-theorem this may be reformulated:
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
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.
Since homotopy type theory admits models in (∞,1)-toposes (and in particular in non-hypercomplete ones), Whitehead’s theorem is not provable when regarded as a statement about types in homotopy type theory. From this perspective, the truth of Whitehead’s theorem is a foundational axiom that may be regarded as a “classicality” property, akin to excluded middle or the axiom of choice — we call it Whitehead’s principle (not to be confused with Whitehead's problem?, another statement that is independent of the usual axioms of set theory).
The -topos version is in section 6.5 of