Abstract:

∞-categories naturally occur in various areas of modern mathematics, such as homotopy theory and algebraic geometry. Intuitively, like ordinary categories, they consist of objects and morphisms, but the morphisms form spaces rather than discrete sets. As such, ∞-categories inherently are of homotopical flavor. In traditional set-theoretic foundations one builds up continuous structures (spaces) out of discrete ones (sets). This traditional development of topology can therefore be called analytic. In contrast, alternative foundations like homotopy type theory (HoTT) are synthetic in that their primal objects are spaces up-to-homotopy rather than discrete sets. In that setting, spaces like e.g. the spheres can be defined solely through their homotopical properties, without recourse to an ambient space. HoTT has served as a synthetic language well-suited for developing homotopy theory. As another feature it supports Voevodsky's univalence axiom which makes formally precise the principle of identifying isomorphic structures. Moreover, HoTT can be implemented as a programming language, making it possible for the computer to verify theorems from homotopy theory. However, HoTT has so far failed to capture ∞-categories in a satisfactory way. One possible solution is to augment HoTT by an interval, making it possible to reason about ∞-categories in the guise of (complete) Segal spaces. This program has been initiated by Riehl and Shulman under the name simplicial homotopy type theory (sHoTT).

I will present various advances in the developments of synthetic ∞-category in simplicial HoTT. This includes the treatment of functorial families of ∞-categories (aka fibrations), a directed univalence principle, a synthetic theory of ∞-presheaves, as well as computer formalizations of some of the results in Kudasov's proof assistant Rzk. A crucial role for some of the applications mentioned is being played by various modal operators, as known from modal logic, that are added to the type theory to model constructions like the opposite category or the groupoid core.

The talk includes joint work with Gratzer and Buchholtz. The formalizations are joint work with Kudasov and Riehl.