MathOverflow Asked by Madeleine Birchfield on February 21, 2021

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.

Robert Harper and Dan Licata studied the topic under the name *2-dimensional type theory*, see their Canonicity for 2-Dimensional Type Theory and possibly these
slides. As they are computer scientists there is a lot of talk about the syntactic properties of such theories, but underneath it really is just groupoids (and they make the connection explicit). If you stare long enough at their rules, they can all be understood in terms of groupiod structures.

In the context of homotopy type theory one can formulate an axiom stating that all types are groupoids: $$Pi(A : mathsf{Type}) (x, y : A) (p, q : x = y) (alpha, beta : p = q),., alpha = beta.$$ It states that for any type $A$, points $x, y : A$, parallel paths $p, q$ from $x$ to $y$, any 2-cells between $p$ and $q$ are equal. This is a straightforward modification of Streicher's axiom $K$ which states that all types are sets. This may look simpler than Harper's and Licata's 2-dimensional type theory, but is actually not capturing groupoids directly – it's more like 2-truncated $infty$-groupoids, where all the higher structure is still around, but is declared to be contractible.

Answered by Andrej Bauer on February 21, 2021

My rambling comments are starting to cohere into a quasi-answer, though not a definitive one:

- In addition to ETCS, Lawvere also formulated ETCC, the elementary theory of the category of categories.

One could very likely arrive at a similar axiomatization of groupiods, either by adapting Lawvere's ETCC axioms, or by directly using the fact that groupoids form a full subcategory of categories.

Of course, the way you formulate the axioms of ETCS reflects a great deal of conceptual development which has happened since Lawvere originally wrote down the theory. I don't know of a similar modernized, sleek way to package Lawvere's axioms for the category of categories, and I think that's partly because it would be harder to do / the necessary concepts may not have been studied (yet?). So if one were to groupoid-ify ETCC, there would still be more work to make the theory more "palatable".

You might also be interested in groupoid models of type theory, where groupoids are thought of in a similar way to what you suggest, lying somewhere between sets and homotopy types and undelrying a theory which can be used foundationally.

I'll also point out that your idea of thinking of the underlying groupoid of a category as a sort of "improved version" of the set of objects of the category does come up. For example, this way of thinking leads to the idea of a complete Segal space as opposed to a Segal category.

Because of the difficulties I alluded to above in groupoid-ifying ETCC, it may be better to return to the comparison to ETCS. The formulation you give, though it doesn't directly invoke the notion of an elementary topos, is closely related to it. A groupoid version of this axiomatization, then, would be talking about something close in spirit to a higher theory of elementary topoi. There has been a great deal of interest in formulating such a theory for a long time.

Going beyond ordinary topoi, the most famous development is Lurie's theory of (Grothendieck) $infty$-topoi. Nima Rasekh has given a theory of elementary $infty$-topoi, but the theory is very much in its infancy.

You want something in the middle -- a (2,1)-topos. (The "2" means that you want your topos to be a 2-category; the "1" means that only 1-morphisms and not 2-morphisms will be non-invertible in your category.) I believe that people like Mike Shulman have thought about notions in this area, but I don't know if anything is published.

I haven't thought carefully about this, but the main thing I'd think needs to be straightened out is the following. In ordinary topoi, the subobject classifier does a great deal of work, but in in $infty$-topoi the concept needs to be strengthened to an object classifier, and size issues cause technical annoyances. The other way of thinking about what the object classifier encodes is in terms of *descent* (a scary category-theoretic word which means different things to different people, but which in each individual case turns out to be not scary). Thinking in these terms, the theory of $infty$-topoi actually turns out to be in some sense *cleaner* than the theory of ordinary topoi. In fact the following is true in $infty$-topoi but (its corresponding version) is false in ordinary topoi: if $mathcal E$ is an $infty$-topos, the "slice" functor $mathcal E^{op} to CAT_infty$, $X mapsto mathcal E/X$ preserves limits. I'm not sure whether a (2,1)-topos is expected to be more like $infty$-topoi or 1-topoi in this regard.

Answered by Tim Campion on February 21, 2021

Since groupoids are categories then Maclane's axiomatisation of categories, which he covers in his book, *Categories for the Working Mathematician* might be a possibility. I don't recall whether he stated this was a first-order axiomatisation but it shows that the sense that category theory could itself be a foundation for mathematics came early in it's development. And I think importantly, given the hegemony of ZFC in foundational thinking.

He expresses the axioms in terms of what he calls meta-categories, and in fact, of a simpler notion, meta-graphs. He does without objects, noting that these can be recovered from the arrows. I've checked, and he doesn't mention whether or not it's first order.

There's also Makkai's FOLDS, which is first order logic with dependent types. It has a weakened law of equality where it's impossible to say two objects are equal to each other and according to NLab it can even be used to formulate higher category theory.

Answered by Mozibur Ullah on February 21, 2021

Get help from others!

Recent Questions

- How can I transform graph image into a tikzpicture LaTeX code?
- How Do I Get The Ifruit App Off Of Gta 5 / Grand Theft Auto 5
- Iv’e designed a space elevator using a series of lasers. do you know anybody i could submit the designs too that could manufacture the concept and put it to use
- Need help finding a book. Female OP protagonist, magic
- Why is the WWF pending games (“Your turn”) area replaced w/ a column of “Bonus & Reward”gift boxes?

Recent Answers

- Jon Church on Why fry rice before boiling?
- haakon.io on Why fry rice before boiling?
- Lex on Does Google Analytics track 404 page responses as valid page views?
- Joshua Engel on Why fry rice before boiling?
- Peter Machado on Why fry rice before boiling?

© 2024 TransWikia.com. All rights reserved. Sites we Love: PCI Database, UKBizDB, Menu Kuliner, Sharing RPP