Homotopy types as $\infty$-groupoids

For zoom details contact: Barthel, Ozornova, Ray, Teichner.

In his very influential manuscript Pursuing Stacks from 1983, Grothendieck proposed a definition of weak $n$-groupoids, for $n\in \mathbb{N}\cup{\infty}$, and formulated his famous Homotopy Hypothesis, which conjectures that weak $n$-groupoids model homotopy $n$-types. The definition of weak $n$-groupoids he gave perfectly captures the platonic vision of these objects that category theorists and homotopy theorists usually have and thus is very different in nature from other standard accepted definitions of weak higher groupoids (e.g. Kan complexes). While the Homotopy Hypothesis has been accepted as a guiding principle of higher category theory, as of today the actual conjecture concerning Grothendieck's weak $n$-groupoids
has only been proved for the values $n=0,1,2$ and very recently $3$.

The main goal of this talk is to give a gentle introduction to some work of Brunerie, later refined by Finster and Mimram, which shows how to express Grothendieck's definition of weak $\infty$-groupoids using the language of type theory. I will then present Brunerie's result that the types of HoTT can be equipped with such a structure of weak $\infty$-groupoids. In particular, this sheds a new light on Grothendieck's Homotopy Hypothesis, and if we are to believe that HoTT is indeed a formal language that captures (a synthetic version) of the homotopy theory of spaces, this seems to indicate that the weak $\infty$-groupoids structure of homotopy types appears at a very fundamental level.