nLab formal category theory




The idea of formal category theory is to handle the fundamental notions and constructions of category theory – such as adjoint functors, monads, limits, etc. – axiomatically via abstract properties enjoyed by the (very large) 2-category Cat of all categories, which is the archetypical 2-topos.

In the words of Gray 1974, p. VII:

The purpose of category theory is to try to describe certain general aspects of the structure of mathematics. Since category theory is also part of mathematics, this categorical type of description should apply to it as well as to other parts of mathematics. [][\dots]

The basic idea is that the category of small categories, CatCat, is a 2-category with properties and that one should attempt to identify those properties that enable one to do the “structural parts of category theory”.

This is analogous to – in fact is a categorification of – how (structural) set theory may be understood as the study of the 1-category Set of all sets, whose good abstract properties are largely captured by understanding it as being the archetypical topos (“1-topos”).

In the other direction of higher category theory there would be room for “formal” ( , 1 ) (\infty,1) -category theory via axiomatization of the (very large) ( , 2 ) (\infty,2) -category of ( , 1 ) (\infty,1) -categories Cat (,1)Cat_{(\infty,1)} – the archetypical ( , 2 ) (\infty,2) -topos.

While this has not been developed, it is interesting to observe (Riehl & Verity 13, following Joyal 08 p. 158) that already its truncation down to a plain 2-category 2Ho(Cat (,1))2Ho\big( Cat_{(\infty,1)}\big) – the homotopy 2-category of ( , 1 ) (\infty,1) -categories – retains much of the interesting structure of ( , 1 ) (\infty,1) -category theory. For example, formal 2-category theoretic adjunctions – as envisioned by Gray 1974 in CatCat, but now interpreted in 2Ho(Cat (,1))2Ho\big( Cat_{(\infty,1)}\big) – turn out to encode the correct notion of adjoint ( , 1 ) (\infty,1) -functors (see there for more).

By analogy, this may be referred to as a formal theory of (,1)(\infty,1)-categories (Riehl 2021).

At least for presentable ( , 1 ) (\infty,1) -categories this formal \infty-category theory is directly accessible from “abstract homotopy theory” in the sense of combinatorial model category-theory, in that 2Ho(PresCat (,1))2Ho\big( PresCat_{(\infty,1)}\big) \,\simeq\, 2Ho(CombModCat) (Pavlov 2021).


Contexts for developing formal category theory:


For 1-categories

An axiomatization of (just) the (very large) 1-category of all categories, but fully in formal logic is the elementary theory of the category of categories (ETCC) due to:

  • William Lawvere, The Category of Categories as a Foundation for Mathematics, pp.1-20 in Eilenberg, Harrison, MacLane, Röhrl (eds.), Proceedings of the Conference on Categorical Algebra - La Jolla 1965, Springer Heidelberg 1966 (doi:10.1007/978-3-642-99902-4_1)

The undertaking of laying these foundations instead for the 2-category of all categories is famously associated with:

Review and further discussion:

Discussion in double category-theory:

For (,1)(\infty,1)-categories

With (small) (∞,1)-categories modeled as quasi-categories, their their homotopy 2-category was considered first in

and then developed further (in the generality of homotopy 2-categories of ∞-cosmoi) in:

Last revised on May 8, 2022 at 09:48:23. See the history of this page for a list of all contributions to it.