The language of synthetic category theory

Chapter 1
The language of synthetic category theory

At the heart of mathematics lies the concept of a set, a collection of mathematical objects. In modern mathematics, sets serve as the building blocks for defining everything from numbers and relations to more complex structures like groups, rings, and topological spaces. Sets are manipulated using basic operations like forming unions, intersections, and complements, and are compared using functions between sets. It is fair to say that the language of set theory forms an essential toolkit for mathematicians.

Although formal axiomatizations of set theory exist, such as those by Zermelo and Fraenkel, they often diverge from the working mathematician’s intuitive understanding of sets. For instance, in formal set theory, every natural number needs to be defined as a set, and in particular one is allowed to speak of the elements of a natural number. Similarly, every function between sets needs to be defined as a set. While this approach is formally valid, it can seem disconnected from everyday mathematical discourse.

In practice, mathematicians often use a more pragmatic approach known as naive set theory. In naive set theory, one works with sets based on intuitive understanding, without invoking formal logical or axiomatic implementations. For example, the set of natural numbers is simply the set containing the numbers \(0, 1, 2,\) etcetera, and functions between sets \(X\) and \(Y\) are simply ‘specifications’ that assign to every element of \(X\) an element of \(Y\). The simplicity and accessibility of naive set theory make it relatively easy for students to learn, and indeed in many introductory mathematics textbooks sets are used in the naive way without being rigorously introduced.

A similar trend is occurring in the field of higher category theory. In recent decades, higher category theory has seen rapid growth, in large part thanks to contributions from people like Joyal, Lurie, and others. Their work provides solid foundations for the field, and the language of higher categories is now extending beyond its origins in algebraic topology to fields like algebraic geometry and representation theory. But while the original works of Joyal and Lurie are based on explicit set-theoretical models for higher categories called ‘quasicategories’, more and more research papers are written in a ‘model-independent’ way in which the usage of details about the specific choice of implementations is avoided. We refer to this as the language of naive category theory.

The goal of this chapter is to provide a structured form of this language, with explicit rules and axioms for how to manipulate categories and functors. Our approach is synthetic in nature rather than analytic: constructions of categories, like products or functor categories, are not defined in terms of set-level constructions, but are axiomatized to exist and satisfy the expected properties. Our rules are deliberately model-agnostic: we expect them to be satisfied in any reasonable foundational system for (higher) category theory. For example, we wish to cover the following three examples:

(1)

The standard theory of quasicategories;

(2)

Type-theoretic approaches like simplicial type theory [RS17; GWB24];

(3)

The internal theory of the (synthetic) category of small categories \(\Cat \).

While the first two examples satisfy various strictness conditions, like strict unitality or associativity for functor composition, the third example forces us to work in a fully ‘homotopical’ setting, where no strictness conditions are imposed.

The chapter is organized as follows. The foundational language is introduced in Section 1.1, and its layer of coherences in Section 1.2. These are used in Section 1.3 to study equivalences of categories. We then introduce a variety of category constructors via their universal properties.

Epistemic status: This chapter started off giving a natural language description of ‘naive category theory’, capturing the model-independent language used in modern papers in higher category theory. Over time, more explicit coherences have been added to the list of axioms when it became clear that some natural language proofs were implicitly using them. We expect the present list to cover most of the required coherences, but it may be the case that we missed some. We hope to eventually settle the complete list of coherences by formalizing everything in a proof assistant.