One axiomatisation of set theory, the Elementary Theory of the Category of Sets, or ETCS for short, comes from category theory and states that sets and functions form a locally cartesian-closed, finitely complete and co-complete Heyting pretopos with a subobject classifier and a natural numbers object, whose generating object is the terminal object and whose epimorphisms are split.

Is there a corresponding **axiomatic charactersation of the category of groupoids**, in which one could do groupoid theory in, that does not involve first defining the concept of $\infty$-groupoid or homotopy types or other infinity categorical structures, and if so, what are the axioms?

And just as ETCS could be considered as a foundation of mathematics that only require sets and propositions, could this Elementary Theory of the Category of Groupoids serve as a more general foundation of mathematics that includes everything that could be done in ETCS as well as providing proper foundations for $1$-category theory? The collection of objects $Ob(C)$ in a category $C$ tend to be a groupoid; when $Ob(C)$ is a set, the category is called strict, so category theory as defined in ETCS or another set theory like ZFC could only speak of strict categories rather than general categories.

Edit: In a finitely complete category, finite limits are saturated under the terminal object and pullbacks. Does this still remain true when one moves to (2,1)-terminal objects and (2,1)-pullbacks and (2,1)-limits in finitely (co)complete (2,1)-categories? For ($\infty$,1)-categories, it doesn't seem to be the case that finite ($\infty$,1)-limits are saturated under ($\infty$,1)-terminal objects and ($\infty$,1)-pullbacks, if I am reading the nLab article on Lurie's ($\infty$,1)-pretopos correctly. In a (2,2)-category, (2,2)-terminal objects and (2,2)-pullbacks are known not to be enough for all finite (2,2)-limits; (2,2)-powers with the interval category are also needed.

Edit 2: I commented somewhere below that this theory as a foundational theory should be expressed in first order logic with isomorphisms, rather than first order logic with equality. I don't think this is the case anymore; ETCS should be the theory expressed in first order logic with isomorphism, as sets in ETCS are only isomorphic rather than equal. Rather, ETCG should be expressed in first order logic with equivalence of groupoids. It is only models of ETCG internal to ETCG that are expressed in first order logic with isomorphism, in the same way that models of ETCS internal to ETCS are expeessed in first order logic with equality.

pseudolimit. The analog of the statement in question is that a (2,1)-category with a pseudoterminal object and pseudopullbacks has all finite pseudolimits up to equivalence. $\endgroup$ – Tim Campion Feb 4 at 3:189more comments