Categories axiomatize the concept of composition of functions or homomorphisms. This admits "higher-order" generalizations studying morphisms between morphisms, morphisms between morphisms between morphisms etc., giving rise to higher-dimensional or ∞-categories.

The composition data in an ∞-category is inherently complex making them challenging to handle both as an abstract concept as well as when it comes to constructing concrete examples. Based on homotopy type theory (HoTT), Riehl--Shulman constructed a language that significantly simplifies the abstract treatment of ∞-categories, and which is amenable to formalization in proof assistants which I will briefly discuss.

However, the construction of nontrivial instances of ∞-categories in this setting still remained elusive for a long time. In a modal extension of Riehl--Shulman's simplicial HoTT, I will show how to construct the ∞-category of ∞-groupoids and ∞-categories as concrete ∞-categories of central importance. Moreover, I will sketch how these universes satisfy a directed version of the univalence axiom which has several interesting consequences such as parametricity and structure homomorphism principles.

The formalization is joint work with Nikolai Kudasov and Emily Riehl in Kudasov's proof assistant Rzk, and the results on universes are joint work with Daniel Gratzer and Ulrik Buchholtz.

Jonathan Weinberger is an assistant professor in computer science and a Fletcher Jones Foundation Faculty Fellow '25-'28 at the Fowler School of Engineering at Chapman University, Orange, CA, USA. He works in theoretical computer science and mathematical logic, in particular category theory and type theory. Jonathan Weinberger obtained his PhD in mathematics at TU Darmstadt in 2021 advised by Thomas Streicher. After two short postdoctoral fellowships at the University of Birmingham, UK, and the Max Planck Institute for Mathematics in Bonn, Germany, he joined Johns Hopkins University in Baltimore, MD, USA from 2022-2024 as a postdoctoral fellow with Emily Riehl.