1.1 Overview
Following [ RV22 ] , from which this document was excerpted, we aim to develop the basic theory of \(\infty \)-categories in a model independent fashion using a common axiomatic framework that is satisfied by a variety of models. In contrast with prior “analytic” treatments of the theory of \(\infty \)-categories — in which the central categorical notions are defined in reference to the coordinates of a particular model — our approach is “synthetic,” proceeding from definitions that can be interpreted simultaneously in many models to which our proofs then apply.
To achieve this, our strategy is not to axiomatize what infinite-dimensional categories are, but rather to axiomatize the categorical “universe” in which they live. This motivates the notion of an \(\infty \)-cosmos, which axiomatizes the universe in which \(\infty \)-categories live as objects. 1 So that theorem statement about \(\infty \)-cosmoi suggest their natural interpretation, we recast \(\infty \)-category as a technical term, to mean an object in some (typically fixed) \(\infty \)-cosmos. Several common models of \((\infty ,1)\)-categories 2 are \(\infty \)-categories in this sense, but our \(\infty \)-categories also include certain models of \((\infty ,n)\)-categories 3 as well as fibered versions of all of the above. Thus each of these objects are \(\infty \)-categories in our sense and our theorems apply to all of them. 4 This usage of the term “\(\infty \)-categories” is meant to interpolate between the classical one, which refers to any variety of weak infinite-dimensional categories, and the common one, which is often taken to mean quasi-categories or complete Segal spaces.
Much of the development of the theory of \(\infty \)-categories takes place not in the full \(\infty \)-cosmos but in a quotient that we call the homotopy 2-category, the name chosen because an \(\infty \)-cosmos is something like a category of fibrant objects in an enriched model category and the homotopy 2-category is then a categorification of its homotopy category. The homotopy 2-category is a strict 2-category — like the 2-category of categories, functors, and natural transformations 5 — and in this way the foundational proofs in the theory of \(\infty \)-categories closely resemble the classical foundations of ordinary category theory except that the universal properties they characterize, e.g., when a functor between \(\infty \)-categories defines a cartesian fibration, are slightly weaker than in the familiar case of strict 1-categories.
There are many alternate choices we could have made in selecting the axioms of an \(\infty \)-cosmos. One of our guiding principles, admittedly somewhat contrary to the setting of homotopical higher category theory, was to allow us to work as strictly as possible, with the aim of shortening and simplifying proofs. As a consequence of these choices, the \(\infty \)-categories in an \(\infty \)-cosmos and the functors and natural transformations between them assemble into a 2-category rather than a bicategory. To help us achieve this counterintuitive strictness, each \(\infty \)-cosmos comes with a specified class of maps between \(\infty \)-categories called isofibrations. The isofibrations have no homotopy-theoretic meaning, as any functor between \(\infty \)-categories is equivalent to an isofibration with the same codomain. However, isofibrations permit us to consider strictly commutative diagrams between \(\infty \)-categories and allow us to require that the limits of such diagrams satisfy a universal property up to simplicially enriched isomorphism. Neither feature is essential for the development of \(\infty \)-category theory. Similar proofs carry through to a weaker setting, at the cost of more time spent considering coherence of higher cells.
An \(\infty \)-cosmos is a particular sort of simplicially enriched category with certain simplicially enriched limits. In §1.2, we first review some prerequisites from the theory of simplicial sets, most of which are either currently in Mathlib or on their way. While the notion of simplicially enriched category currently exists in Mathlib, simplicially enriched limits do not, so in §1.3 we first introduce the prerequisite notions of simplicially enriched limits that will be required to state the definition of an \(\infty \)-cosmos in §1.4. The homotopy 2-category of an \(\infty \)-cosmos is then obtained by applying the general theory of change-of-base from enriched category, which is also currently missing from Mathlib. This theory is described in §1.5 and then used to define the homotopy 2-category in §1.6.
Additional chapters will be added to this blueprint in the future, containing excerpts of the material that can be found in [ RV22 , Chapters 2-5 ] . The broader aim of this project is to formalize the core basic theory of \(\infty \)-categories, covering those aspects that can be defined in the homotopy 2-category of an \(\infty \)-cosmos.
The authors of this blueprint are particularly indebted to:
Mario Carneiro, who contributed greatly to the original Lean formalization of \(\infty \)-cosmoi and prerequisite results about the homotopy category functor;
Johan Commelin, who suggested restructuring this as a blueprint project; and
Pietro Monticone, who created a template for blueprint-driven formalization projects in Lean, from which this repository was forked.
Special thanks are also due to the Hausdorff Research Institute for Mathematics and the organizers of the Trimester Program “Prospects of Formal Mathematics,” where the genesis of this project took place.