### Synthetic ∞-Groupoid Theory

#### Posted by Mike Shulman

This week I’m at the 2013 International Category Theory conference in Syndey, Australia, along with our co-hosts Tom and Emily (and a bunch of other people (-: ). There’s a lot of interesting stuff being said that I don’t have time to write about right now, but I thought I would go ahead and post the slides for my own talk that I gave yesterday, since I’ve had one or two requests:

- Homotopy type theory: towards Grothendieck’s dream (pdf slides)

I’m not sure how comprehensible the slides will be on their own, but you can probably get the general idea. The point I was trying to make was that if you want to, you can ignore all the business about computation, proof assistants, etc. and view homotopy type theory as a *synthetic theory of $\infty$-groupoids* — which happens to use slightly odd notation and terminology. The meaning of “synthetic” is by contrast with “analytic”, as in Euclid’s synthetic geometry (with undefined notions of points, lines, etc. satisfying axioms) versus cartesian analytic geometry (where points and lines are *defined* using pairs of real numbers).

Moreover, from this point of view, we can think of homotopy type theory as a solution to the homotopy hypothesis: its $\infty$-groupoids are algebraic and globular (in fact, as Guillaume Brunerie realized this past year, they’re very close to *Grothendieck’s* original definition of $\infty$-groupoid!), and via the model of homotopy type theory in “analytic” Kan complexes, we can use them to do homotopy theory. The classical homotopy hypothesis asks for an *equivalence* between $\infty$-groupoids and homotopy theory, but having the former be simply a *model* of the latter seems good enough for many purposes, and has the additional advantage that there are many other useful models (e.g. higher toposes).

## Re: Synthetic ∞-Groupoid Theory

To kick things off, here’s one thing I learned from Mike’s really excellent talk: the univalence axiom is what allows us to form the (synthetic) $\infty$-groupoid of (synthetic) $\infty$-groupoids.