Is there anything special about types such that it makes the Whitehead Theorem true for any type?

[Yiming Xu]

On section 8.8, for the discussion of Whitehead's theorem, it says that types that Whitehead theorem fails does not exists. In usual algebraic topology, Whitehead state a result only on CW complexes. We have CW complexes in HoTT, as discussed in Chapter 6. So what is special for types that make the Whitehead's theorem works for every type? Is it the fact that every type has a CW-structure?

[Michael Shulman]

Whitehead's theorem in HoTT is *not* provable about all types unless
we assert it as an axiom. Confusingly, however, this has nothing to
do with the classical restriction to CW complexes, because the way
HoTT is modeled in classical homotopy theory is using Kan complexes,
whose homotopy theory is equivalent to that of CW complexes. The
non-CW-complex topological spaces are invisible to HoTT. The reason
Whitehead's theorem can fail in HoTT is instead due to the existence
of other "nonclassical" models that violate it, called
"non-hypercomplete infinity-topoi". (Similarly, although the
"classical" model of HoTT sees only CW-complexes, we cannot prove in
HoTT that every type has a CW structure, because there are other
models in which this fails.)

On Tue, Mar 19, 2019 at 3:58 AM Yiming Xu <u594...@gmail.com> wrote:
>
> On section 8.8, for the discussion of Whitehead's theorem, it says that types that Whitehead theorem fails does not exists. In usual algebraic topology, Whitehead state a result only on CW complexes. We have CW complexes in HoTT, as discussed in Chapter 6. So what is special for types that make the Whitehead's theorem works for every type? Is it the fact that every type has a CW-structure?
>

> --
> You received this message because you are subscribed to the Google Groups "HoTT Cafe" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to hott-cafe+...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.