You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Tim Hosgood (Mar 21 2022 at 12:57):Thursday the 24th of March at the unusual time of 20:00 UTC (n.b. if you live in the USA, then this is doubly confusing, since your clocks have changed for summer time, whereas those in e.g. Europe have not done so yet)
Tim Hosgood (Mar 21 2022 at 12:57):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
[1] E. Riehl, M. Shulman, A type theory for synthetic ∞-categories, High. Struct. 1 (2017) 147224.
[2] E. Riehl, D. Verity, Elements of ∞-category theory, Cambridge University Press, 2022.
[3] J. Weinberger, A synthetic perspective on (∞,1)-category theory: Fibrational and semantic aspects, arXiv Preprint arXiv:2202.13132. (2022).
Zoom: https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhTdGhvZ3pUdz09
YouTube: https://youtu.be/qLkRhKaw5DA
Tim Hosgood (Mar 24 2022 at 19:49):starting in 10 minutes!