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, $Cat$, 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” $(\infty,1)$-category theory via axiomatization of the (very large) $(\infty,2)$-category of $(\infty,1)$-categories $Cat_{(\infty,1)}$ – the archetypical $(\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\big( Cat_{(\infty,1)}\big)$ – the homotopy 2-category of $(\infty,1)$-categories – retains much of the interesting structure of $(\infty,1)$-category theory. For example, formal 2-category theoretic adjunctions – as envisioned by Gray 1974 in $Cat$, but now interpreted in $2Ho\big( Cat_{(\infty,1)}\big)$ – turn out to encode the correct notion of adjoint $(\infty,1)$-functors (see there for more).
By analogy, this may be referred to as a formal theory of $(\infty,1)$-categories (Riehl 2021).
At least for presentable $(\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\big( PresCat_{(\infty,1)}\big) \,\simeq\,$ 2Ho(CombModCat) (Pavlov 2021).
Contexts for developing formal category theory:
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:
The undertaking of laying these foundations instead for the 2-category of all categories is famously associated with:
Review and further discussion:
Ivan Di Liberti, Simon Henry, Mike Lieberman, Fosco Loregian, Formal category theory, (course notes)
Ivan Di Liberti, Fosco Loregian, On the unicity of formal category theories (arXiv:1901.01594)
Discussion in double category-theory:
Seerp Roald Koudenburg, A double-dimensional approach to formal category theory (arXiv:1511.04070) 2015.
Seerp Roald Koudenburg, Augmented virtual double categories, Theory and Applications of Categories, Vol. 35, 2020, No. 10, pp 261-325 (arXiv:1910.11189, tac:35-10)
(On augmented virtual double categories, a expanded version of Sec. 1-3 of Koudenburg 15 )
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:
Emily Riehl, Dominic Verity, The 2-category theory of quasi-categories, Advances in Mathematics Volume 280, 6 August 2015, Pages 549-642 (arXiv:1306.5144, doi:10.1016/j.aim.2015.04.021)
Emily Riehl, Dominic Verity, Infinity category theory from scratch, Higher Structures Vol 4, No 1 (2020) (arXiv:1608.05314, pdf)
Emily Riehl, Dominic Verity, Elements of $\infty$-Category Theory, 2021- (pdf)
Emily Riehl, The formal theory of ∞-categories, talk at Categories and Companions Symposium June 8–12, 2021 (video)
Last revised on October 13, 2021 at 13:59:53. See the history of this page for a list of all contributions to it.