basic constructions:
strong axioms
further
The explicit formulation of the principles of category theory … is still in need of improved axiomatization. I will be overjoyed when some young person responds to that need. (Lawvere, 2016, p.1)
Elementary theory of the category of categories, or ETCC for short, is in a broad sense an appropriate name for any first order theory axiomatizing the metacategory CAT of categories that forms the intuitive background for naive category theory with a view to the categorical foundations of mathematics. This is in categorification of the analogous first-order axiomatization of the metacategory SET of sets, for which see at ETCS.
Historically, the first attempt to formulate such a system of axioms has been undertaken by F. W. Lawvere in his dissertation (Lawvere 63) and a subsequent publication (Lawvere 1966), and it is this system that is sometimes referred to as the ETCC. We will discuss it together with subsequent attempts to repair its technical flaws under this heading in the next section.
Taking into account that the intuitively given category of categories is a 2-category, from an n-categorical perspective one would prefer to axiomatize CAT directly as a 2-category, and the resulting elementary theory of the 2-category of categories, or ET2CC, is the subject of a subsequent section.
In 1964, F. W. Lawvere proposed to found mathematics on the category of categories. When he lectured on this at an international conference in Jerusalem, Alfred Tarski objected: “But what is a category if not a set of objects together with a set of morphisms?” Lawvere replied by pointing out that set theory axiomatized the binary relation of membership, while category theory axiomatized the ternary relation of composition. 1
W. Lawvere launched in the early 60s an ambitious long-term project to replace membership based mathematics by more invariant concepts in order to arrive at a renewal of analysis and geometry adapted for the needs of modern (continuum) physics.
His 1963 dissertation takes issue with set-theoretic notions at various levels, e.g. redefining adjoint functors via comma categories in order to avoid reference to Hom-sets, but the most radical step is the attempt at a first-order axiomatization of the category of categories that he proposes to bypass set theory completely at a foundational level.
The system of axioms that he published in a more elaborate form in 1966, is layered in three parts:
The elementary theory of abstract categories (ETAC) has besides equality three primitive predicates for domain, codomain, and composition and as axioms the usual axioms for identity, associativity etc. (See at theory of categories for a variant of such an axiomatisation!)
The basic theory (BT) adds axioms for e.g. 1, a one-morphism category, 2, a category with one non-identity morphism between two objects, 3, a category with a commutative triangle of morphisms, and various exactness properties among which is the existence of exponentials. This permits then to define e.g. sets as discrete objects with i.e. as categories whose morphisms are all identity morphisms. The final axiom of the basic theory tries to express the density-adequacy of the simple categories like 1 etc. within the metacategory.
The stronger theory (ST) then adds two further axioms to the basic theory concerning existence of completions and an ‘inaccessible’ category (p.18).
As pointed out by J. Isbell in 1967, one of Lawvere’s results (namely, the theorem on the ‘construction of categories by description’ on p.14) was mistaken, which left the axiomatics dangling with insufficient power to construct models for categories. Several ways to overcome these problems where suggested in the following but no system achieved univocal approval (cf. Blanc-Preller(1975), Blanc-Donnadieu(1976), Donnadieu(1975), McLarty(1991)).
As ETCC also lacked the simplicity of ETCS, it rarely played a role in the practice of category theory in the following and was soon eclipsed by topos theory in the attention of the research community that generally preferred to hedge their foundations with appeals to Gödel-Bernays set-theory or Grothendieck universes.
Nevertheless, the axiomatic treatment of 1963/66 contained also the seminal idea to internally define discrete set-theoretic ‘foundations’ within a bigger category, that will later on play a central role in Lawvere’s approach to cohesion. So when one can view the 1964 ETCS as a forerunner of the Lawvere-Tierney axioms for an elementary topos, one could view ETCC as an anticipation of the 2007 axioms for a cohesive topos.
For Lawvere ETCS and ETCC have a different status, the first provides abstract constant sets as convenient carriers for structured objects, whereas the latter provides the overall ontology of concepts, the intellectual working space.
Yet from an n-categorical perspective, the categories they axiomatize differ in level only and so it is tempting to think of the second as a sort of categorification of the first: this suggests to posit an abstract concept ‘foundation’ that at the level of ETCS shows up as set theory, gets refined to ‘category theory’ one step higher, then as 2-category theory, and so on.
Now what comes closest to such a vision at the moment is probably homotopy type theory but truncating such a tower of ‘foundations’ might be still relevant for applications where concepts of 2-toposes are considered. It would also provide an axiomatisation for the ‘familiar’ meta 2-category CAT suggestive for the generalization to n-CAT.
At the time no such axiomatisation is fully worked out, but in 2009 M. Shulman gave a rough sketch of what such an elementary theory of the 2-category of categories (ET2CC) should look like (see at at formal category theory):
Firstly, some exactness axioms amounting to its being a “2-pretopos” in the sense I described here:2-categorical logic . This gives you an “internal logic” like that of an ordinary (pre)topos.
Secondly, the existence of certain exponentials (this is optional).
Thirdly, the existence of a “classifying discrete opfibration” el→set in the sense introduced by Mark Weber (“Yoneda structures from 2-toposes”) which serves as “the category of sets,” and internally satisfies some suitable axioms.
Finally, a “well-pointedness” axiom saying that the terminal object is a generator, as is the case one level down with in ETCS. This is what says you have a 2-category of categories, rather than (for instance) a 2-category of stacks.
Once you have all this, you can use finite 2-categorical limits and the “internal logic” to construct all the usual concrete categories out of the object “set”. (Shulman 2009)
We can see here how at the end Lawvere’s idea of internal set-theoretic ‘foundations’ resurfaces. Such a level of discreteness seems to be pervasive in this context and e.g. the approach of Przybylek (2014) to the concept of internal 2-cartesian closure takes discreteness as a starting point.
Note that already R. F. C. Walters and R. Street conceived of their work on Yoneda structures in the early 1970s as a 2-dimensional version of ETCC (cf. Walters 1971).
A revised version of the axioms appears as
Important reviews of the paper pointing out technical problems appeared here
J. R. Isbell, Review of Lawvere 1966, Mathematical Reviews 34 (1967) #7332.
G. Blanc. A. Preller, Lawvere’s basic theory of the category of categories, JSL 40 (1975) pp.14-18.
A more recent view of Lawvere exposing in particular his ‘Münchhausen’ approach to set-theoretic ‘foundations’ is in
Lawvere briefly comments on his 1965 system 50 years later p.6 in
An insightful and non-partisan view of ETCC can be found in a section of:
Alternative or complementary approaches are
J. Bénabou, Fibered Categories and the foundations of naive category theory, JSL 50 (1985) pp.10-37. (preprint)
G. Blanc, Propriétés du Premier Ordre et Catégories, Cah. Top. Géom. Diff. Cat. 16 (1975) pp.222-224. (Colloque Amiens 1975 proceedings,6.81 MB)
G. Blanc, M. R. Donnadieu, Axiomatisation de la catégorie des catégories, Cah.Top.Géom.Diff.Cat. XVII no. 2 (1976) pp.1-35. (pdf)
M. W. Bunder, Category Theory Based on Combinatory Logic, Arch. Math. Logik 24 (1984) pp.1-15. (gdz)
N. C. A. da Costa, O. Bueno, A. Volkov, Outline of a Paraconsistent Category Theory, pp.95-114 in Weingartner (ed.), Alternative Logics. Do Science Need Them?, Springer Heidelberg 2004. (draft)
M. R. Donnadieu, Démonstration du théorème de construction de catégories d’après description de Lawvere sous certains axiomes, C. R. Acad. Sc. Paris 280 série A (1975) pp.307-308. (gallica)
E. Engeler, H. Röhrl, On the problem of foundations of category theory, Dialectica 23 (1969) pp.58-66.
C. McLarty, Axiomatizing a category of categories, JSL 56 (1991) pp.1243-1260. (preprint)
L. Oubiña, Teoría axiomatica de categorías, Cah. Top. Géom. Diff. Cat., X no. 3 (1968) pp.375-394. (numdam)
J. Sonner, On the formal definition of categories, Math. Zeitschr. 80 (1962) pp.163-176. (gdz)
H. Tsukuda, Category theory not based upon set theory, Sci. Papers College Gen. Ed. Univ. Tokyo 31 (1981) pp.1-24.
A critical view of purely categorical foundations can be found in a series of papers by S. Feferman e.g. :
The unattainability of all the formal desiderata proposed by Feferman is discussed in
The above remarks from M. Shulman come from the following MO discussion that also offers additional perspectives on ETCC and ET2CC:
A worked out ET2CSC where the “S” stands for “small” can be found in
See also
Andreas Blass, The interaction of category theory and set theory , Cont. Math. 30 (1984) pp.5-29. (draft)
Jim Lambek, Phil Scott, Reflections on Categorical Foundations of Mathematics, pp.171-185 in Sommaruga (ed.), Foundational Theories of Classical and Constructive Mathematics, Springer New York 2011. (draft)
C. McLarty, A. Rodin, A Discussion between Colin McLarty and Andrei Rodin about Structuralism and Categorical Foundations of Mathematics, n.d. (pdf)
M. R. Pryzbylek, Logical systems I: Lambda calculi through discreteness, arxiv:1306.3703v3 (2014). (pdf)
Bob Walters, Yoneda 2Categories , talk at the University of New South Wales December 1971. (manuscript)
Lambek&Scott 2009, pp.171-172. ↩
Last revised on May 18, 2024 at 21:23:25. See the history of this page for a list of all contributions to it.