# Axioms for category theory

I'm confused of background logic on category theory.

In ZFC set theory, we can construct new sets from existing sets by axioms, such as power set axiom, axiom of pairing etx.

I read first few pages of MacLane's category theory text and now I'm reading Tom Leinster's category theory text. Neither of these texts say whether we need some axioms or not, however, they are using some axioms in some sense without saying. I want to know what are the standard axioms for category theory.

Here are examples:

Firstly, how do we construct $$A\times B$$ where $$A,B$$ are categories? It is written in texts that "if we define $$\operatorname{Obj}(A\times B)=\operatorname{Obj}(A)\times \operatorname{Obj}(B)$$ and $$\operatorname{Mor}((A_1,B_1),(A_2,B_2))=(\operatorname{Mor}(A_1,A_2),\operatorname{Mor}(B_1,B_2))$$, then $$A\times B$$ forms a category". What kind of axiom would make this collecting possible?

Secondly, how do we construct a functor category $$[A,B]$$? How do we make "Collecting functors" process possible?

Thirdly, it is a theorem in text that "fully faith and essenially surjective functors are equivalences". However, to prove this, we need some kind of axiom of choice for category theory.

What would be the standard axioms?

• I suggest you read this Rubertos math.stackexchange.com/questions/724302/what-is-category-theory Sep 11, 2016 at 2:16
• Somewhere early on, MacLane talks about this and makes a choice of what foundations to use in his book. IIRC, he decides to work in ZFC + a large cardinal. Set is then the category whose objects are sets of the corresponding inner model (called "small sets"), and the few times it comes up he uses Ens for the category of all sets.
– user14972
Sep 12, 2016 at 4:50

The standard axioms vary: they're either ZFC with an axiom of choice for proper classes, some set theory such as NBG that axiomatizes classes more thoroughly, or ZFC with Grothendieck universes, so that "large" categories are interpreted as still being small, but relative to a larger "universe" of sets. There have been efforts to axiomatize category theory without set theory, most notably ETCC, the elementary theory of the category of categories, but these have not proven to be sufficient as a foundation.

• Could you elaborate on what "not proven to be sufficient as a foundation" means? Mar 9, 2022 at 22:35
• @hasManyStupidQuestions The axiomatization was actually wrong, and has not yet been successfully correct, see the nLab page: ncatlab.org/nlab/show/ETCC Mar 9, 2022 at 22:38
• Is "ET2CC" wrong? And is ETCC wrong related to whether ETCS is correct or not? I thought ETCS was known to be equivalent to a certain fragment of ZFC. Mar 9, 2022 at 23:16
• ETCS and ETCC are totally different theories. “ET2CC” is the content of a MathOverflow answer and has not been proposed as a foundation for mathematics. It seems to me that anybody who might have wanted to do such a thing is more excited by HoTT these days. Mar 10, 2022 at 4:53

Freyd gives as his axioms of categories (in his Amplifications to Categories, Allegories)

where src x expresses his box notation and x is a morphism.

1 xy is defined iff tar x = src y

2 (Src x) x = x and x (tar x) = x

and 3 associativity.