A continuous map is a homotopy -equivalence if it induces isomorphisms on for at each basepoint. Two spaces share the same homotopy -type if they are linked by a zig-zag chain of homotopy -equivalences.
For any nice space , you can kill its homotopy groups in higher dimensions by attaching cells, thus constructing a new space so that the inclusion of into is a homotopy -equivalence; up to (weak) homotopy equivalence, the result is the same for any space with the same homotopy -type. Accordingly, a homotopy -type may alternatively be defined as a space with trivial for , or as the unique (weak) homotopy type of such a space, or as its fundamental -groupoid (which should be a -groupoid).
See the general discussion in homotopy n-type.
There are many useful algebraic models for a homotopy -type. (Assume the homotopy type is connected for simplicity.)
One measure of the usefulness of a given model may be its ease of calculation (e.g., with a generalised van Kampen theorem) and of extraction of topologically significant invariants. In the above a lot more is known, from this viewpoint, about the second and third model than for the first.
|homotopy level||n-truncation||homotopy theory||higher category theory||higher topos theory||homotopy type theory|
|h-level 0||(-2)-truncated||contractible space||(-2)-groupoid||true/unit type/contractible type|
|h-level 1||(-1)-truncated||(-1)-groupoid/truth value||(0,1)-sheaf||mere proposition, h-proposition|
|h-level 2||0-truncated||homotopy 0-type||0-groupoid/set||sheaf||h-set|
|h-level 3||1-truncated||homotopy 1-type||1-groupoid/groupoid||(2,1)-sheaf/stack||h-groupoid|
|h-level 4||2-truncated||homotopy 2-type||2-groupoid||(3,1)-sheaf||h-2-groupoid|
|h-level 5||3-truncated||homotopy 3-type||3-groupoid||(4,1)-sheaf||h-3-groupoid|