Consider the first-order language $L_{\omega\omega}$ of the signature $L:=\{\mathrm{dom}, \mathrm{cod}, \mathrm{comp}\}$, where $\mathrm{dom}$ and $\mathrm{cod}$ are unary function symbols and $\mathrm{comp}$ is a ternary relation symbol. This is intended to be thought of as the language of a single category: $\mathrm{dom}$ resp. $\mathrm{cod}$ are interpreted as functions yielding the *domain* resp. *codomain* of a given morphism; $\mathrm{comp}(h, g, f)$ is interpreted as $h=g\circ f$. One can formally write down the axioms of a category (associativity of composition, identity morphisms for composition) as first-order $L$-sentences. If we call the collection of these axioms $T_\text{Cat}$, then an $L$-structure $C$ with $C\models T_\text{Cat}$ is essentially the same as a category. (Okay, one can argue about size issues or whether specific decisions concerning the design of the formal language are natural, for example, whether it would be better to use a two-sorted language with the sorts "objects" and "morphisms" rather than a one-sorted language where everything is a morphism, but let us ignore these issues for now.)

Lawvere famously gave an axiomatization $\mathsf{ETCS}\supseteq T_{\mathrm{Cat}}$ of the category of sets in the language $L_{\omega\omega}$ and showed that a great deal of set theory can be carried out in this theory. I think it is quite remarkable that all the usual concepts of set theory (such as elements, the set of natural numbers, and the cartesian product) can be formulated categorically in the language $L_{\omega\omega}$ of morphisms. Here are some links for further reading for people not familiar with $\mathsf{ETCS}$: nLab, Lawvere's original paper, fully formal presentation of ETCS on the nLab, Tom Leinster's "Rethinking set theory". Lawvere also gave an axiomatization $\mathsf{ETCC}$ of the category of categories (nLab). (To me, this theory seems to be not as established as $\mathsf{ETCS}$ and I don't know to what extent this theory can be used to carry out doing category theory.)

**Question:** Is it also possible to axiomatize the category of topological spaces (and continuous maps) in the language $L_{\omega\omega}$? Is it then possible to really carry out some topology in this theory? Also, is it possible to axiomatize the category of groups resp. rings in $L_{\omega\omega}$ and then really do some group resp. ring theory? (You can really interpret my question as a question schema: for each theory, you can ask this question.) This would be interesting, because it would show that one can do topology, group theory, ring theory, ... *without presupposing some form of set theory*. Also, it would show that one can express all (or a great deal of) the theorems of topology, group theory, ring theory, ... *just in terms of morphisms, domain, codomain, and composition*.

doesn'taxiomatize the category of sets fully - there are lots of statements about the category of sets, in the language above, which are independent of ETCS. This is relevant because when you ask "is it possible to axiomatize ---?," it's not clear what you mean by "axiomatize" - if you just mean "write some true statements about," then that's trivially true ($\emptyset$), while if you mean "give a complete axiomatization of" then that's false even for the category of sets. (cont'd) $\endgroup$computableaxiomatization at all (the category of sets is complicated enough for Godel's incompleteness theorem to apply to its theory). As to "it would show that one can express all (or a great deal of) the theorems of topology, group theory, ring theory, ... just in terms of morphisms, domain, codomain, and composition," this is already well-known and one of the whole points of category theory in the first place. (cont'd) $\endgroup$in such a way that a great deal of the theory can be done in the axiomatization. Note that my question is a soft question. Basically, I just wonder: if one studies ETCS, why don't consider similar theories for topology, group theory, ring theory, ... $\endgroup$isrich enough to talk about a huge amount of the stuff we care about. $\endgroup$17more comments