**homotopy theory, (∞,1)-category theory, homotopy type theory**

flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed…

models: topological, simplicial, localic, …

see also **algebraic topology**

**Introductions**

**Definitions**

**Paths and cylinders**

**Homotopy groups**

**Basic facts**

**Theorems**

A homotopy $3$-type is a homotopy type where we consider its properties only up to the $3$nd homotopy group $\pi_3$, a homotopy n-type for $n = 3$

A continuous map $X \to Y$ is a **homotopy $3$-equivalence** if it induces isomorphisms on $\pi_i$ for $0 \leq i \leq 3$ at each basepoint. Two spaces share the same **homotopy $3$-type** if they are linked by a zig-zag chain of homotopy $3$-equivalences.

For any nice space $X$, you can kill its homotopy groups in higher dimensions by attaching cells, thus constructing a new space $Y$ so that the inclusion of $X$ into $Y$ is a homotopy $3$-equivalence; up to (weak) homotopy equivalence, the result is the same for any space with the same homotopy $3$-type. Accordingly, a **homotopy $3$-type** may alternatively be defined as a space with trivial $\pi_i$ for $i \gt 3$, or as the unique (weak) homotopy type of such a space, or as its fundamental $\infty$-groupoid (which should be a $3$-groupoid).

See the general discussion in homotopy n-type.

There are many useful algebraic models for a homotopy $3$-type. (Assume the homotopy type is connected for simplicity.)

- 2-crossed modules
- crossed squares
- cat-2-groups
- Gray-groups: one-object groupoidal Gray-categories

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.

Of course, any sufficient weak notion of $3$-groupoid ought to qualify, by the homotopy hypothesis.

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 | contractible-if-inhabited | (-1)-groupoid/truth value | (0,1)-sheaf/ideal | 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/2-stack | h-2-groupoid |

h-level 5 | 3-truncated | homotopy 3-type | 3-groupoid | (4,1)-sheaf/3-stack | h-3-groupoid |

h-level $n+2$ | $n$-truncated | homotopy n-type | n-groupoid | (n+1,1)-sheaf/n-stack | h-$n$-groupoid |

h-level $\infty$ | untruncated | homotopy type | ∞-groupoid | (∞,1)-sheaf/∞-stack | h-$\infty$-groupoid |

Last revised on April 25, 2013 at 21:39:46. See the history of this page for a list of all contributions to it.