Zen and the art of ∞-categories

Last Friday morning I spoke in the Topos Institute Colloquium on the topic of model independent and synthetic approaches to ∞-category theory. This might be considered part of our virtual book tour for The Elements.

You can view the video of this talk and play along with my slides.

Abstract

You may well have heard the rumour that ∞-category theory is “really just like category theory with a little homotopy theory thrown in”. Inspired by that comment, you might even have headed to a book on ∞-categories or to the nLab to find out more, only to find that things in the ∞-world are far from that simple.

Firstly you will have discovered that there is no universal agreement on what an ∞-category actually is. Instead, you’ve been met with a proliferation of ∞-categorical models; simplicially enriched categories, quasi-categories, (iterated) complete Segal spaces, complicial sets, Θ-spaces and so on. Then you discover, to your horror, that each one of these models supports its own particular interpretations of common categorical concepts, some of which appear far more familiar than others. Finally, you realise that the relationships between the category theories developed for each model are also much less than clear.

If this weren’t enough to leave anyone reaching for the Aspirin bottle, there is more bad news to come. It quickly becomes clear that there exists quite a large gap between the informal language used to describe ∞-categorical arguments, in blog posts and wiki articles, and the corresponding formal arguments expressed in any particular model of ∞-categories. Most of these are given either as concrete constructions with simplicial (or increasingly cubical) objects or as abstract model category theoretic arguments. Now I have no doubt that we “all” love a good simplicial argument, but encoding things in this way does very little to aid our categorical intuition.

There must be a better way!

In this talk we discuss recent developments in ∞-technology that seek to address these issues. Specifically, we review the current state of the art in model agnostic ∞-category theory [2], which seeks to provide a unified account of ∞-category theory freed from the straight jacket of a specific model. This allows both for the model independent, synthetic development of ∞-categorical results and for the transport of analytically derived such results from one model to another. We shall also see how these techniques are rapidly being reframed in type theoretic terms, through the development of directed type theory [1,3], thereby promising a more natural language for the formal development of ∞-categorical concepts and results.

References