**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**

**natural deduction** metalanguage, practical foundations

**type theory** (dependent, intensional, observational type theory, homotopy type theory)

**computational trinitarianism** =

**propositions as types** +**programs as proofs** +**relation type theory/category theory**

A homotopy $1$-type is a space where we consider its properties with regard to the fundamental groups $\pi_1$ of its components.

A continuous map $X \to Y$ is a **homotopy $1$-equivalence** if it induces isomorphisms on $\pi_0$ and $\pi_1$ at each basepoint. Two spaces share the same **homotopy $1$-type** if they are linked by a zig-zag chain of homotopy $1$-equivalences.

For any 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 $1$-equivalence; up to (weak) homotopy equivalence, the result is the same for any space with the same homotopy $1$-type. Accordingly, a **homotopy $1$-type** may alternatively be defined as a space with trivial $\pi_i$ for $i \gt 1$, or as the unique (weak) homotopy type of such a space, or as its fundamental $\infty$-groupoid (which will be a $1$-groupoid).

See the general discussion in homotopy n-type.

A connected pointed homotopy 1-type is completely determined, up to (weak) homotopy equivalence, by the one group $\pi_1$. A connected homotopy 1-type with $\pi_1 = G$ is an Eilenberg-Mac Lane space and is often written $K(G,1)$. A general homotopy 1-type can then be written as a disjoint union of such $K(G,1)$s, and is completely determined by its fundamental groupoid.

In the other direction, for any (discrete) group $G$ one can construct its classifying space $\mathcal{B}G$, which is a $K(G,1)$. In fact, many versions of this construction (such as the geometric realization of the simplicial nerve $nerve(G)$; see Dold-Kan correspondence) apply just as well to any groupoid. We can obtain any 1-type in this way, since a groupoid is up to homotopy type (of groupoids!) a disjoint union of groups. However this description is not natural in the category of groupoids, and is analogous to choosing a basis for a vector space.

Moreover, every continuous map between $K(G,1)$s is induced by a group homomorphism, every map between 1-types is induced by a functor between groupoids, and every homotopy is induced by a conjugation (aka a natural transformation between groupoids). In fact, one can show that the $(\infty,1)$-category of homotopy 1-types is equivalent to the 2-category Grpd of groupoids, via the above-described correspondence..

There are further aspects to this relationship; for instance, the van Kampen theorem for the fundamental groupoid shows how the algebra of groupoids models the gluing of spaces. The general result for non-connected spaces is possible because groupoids model homotopy 1-types, having structure in dimensions 0 and 1. For the search for algebraic structures that play an analogous role to groupoids for $n$-types with $n\gt 1$, see the pages homotopy hypothesis, fundamental infinity-groupoid, cat-n-group, classifying space, crossed complex, and probably others.

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 July 27, 2018 at 23:27:34. See the history of this page for a list of all contributions to it.