12
$\begingroup$

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.

$\endgroup$
15
  • 1
    $\begingroup$ I'm nervous to try to write up the answer myself because I'll mess up something about universes, but this is the sort of thing that should be pretty straightforward if you understand the HoTT book and ETCS. You want to do the same kind of translation that relates Martin-Löf type theory with Axiom K (i.e. all types are 0-truncated) to ETCS but instead applied to type theory with a 1-truncation axiom. $\endgroup$ Feb 3, 2021 at 20:23
  • 1
    $\begingroup$ And I'm reasonably certain that there are papers out there studying type theory with a 1-truncaction axiom. The analog of the issue in the last paragraph of my answer in this setting is that you have to figure out what form of univalence you'll have. $\endgroup$
    – Tim Campion
    Feb 3, 2021 at 20:48
  • 2
    $\begingroup$ @MadeleineBirchfield That's a good point. For that the canonical place to point you would be Makkai's FOLDS. $\endgroup$
    – Tim Campion
    Feb 4, 2021 at 1:49
  • 2
    $\begingroup$ In the $(2,1)$-case the situation is terminologically a little awkward. There is a strict notion of limit which still exists if you're working with strict (2,1)-categories (which it is often convenient to do) which is defined up to isomorphism, and there is also a weak notion of (2,1)-limit, which should really be defined only up to equivalence, but can also be given an up-to-isomorphism definition as a 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, 2021 at 3:18
  • 2
    $\begingroup$ But an often more convenient way to work with (2,1) limits is to construct them from products, iso-inserters, and equifiers -- so called PIE limits. The precise relationship to pseudolimits is not something I have at my fingertips, but they should be essentially equivalent. $\endgroup$
    – Tim Campion
    Feb 4, 2021 at 3:20

3 Answers 3

8
$\begingroup$

I'm showing up a bit late to this party, but maybe I still have something to add. As Andrej and others have pointed out, one can obtain a type theory for 1-groupoids by starting with any form of HoTT and adding a 1-truncation axiom. (It's amusing (and perhaps deep) that in the type-theoretic context, it's easier to start from a type theory for $\infty$-groupoids and then assert an extra axiom that cuts down to 1-groupoids.) The paper of Harper and Licata is about a version of such a theory that satisfies the nice technical property of "canonicity", but if all you want is a formal system you can just add the 1-truncation axiom to Book HoTT --- and modify the univalence axiom so it doesn't contradict that. Basically you should assert only that there is a univalent universe of sets (0-truncated types).

Now, it sounds from the question like you're more interested in a "category-theoretic" phrasing of this, looking more like the phrasing of ETCS as "the category of sets is an elementary topos such that blah". I don't think this has been written down as such; for higher values of $n$ it's more common to discuss Grothendieck $n$-toposes than elementary ones. But similar to the type-theoretic case, one could start from a proposed definition of elementary $(\infty,1)$-topos and cut it back down to a (2,1)-category. This would produce something like: an elementary (2,1)-topos is a (2,1)-category (i.e. a category enriched in groupoids, or a 2-category or bicategory whose hom-categories are groupoids) such that

  1. It has finite limits and colimits, in the bicategorical sense.
  2. It is locally cartesian closed, in a bicategorical sense: pullback along any morphism has a right bicategorical adjoint.
  3. It has a subobject classifier, i.e. the functor sending each object to the poset of fully faithful inclusions into it is representable.
  4. For any faithful morphism, there is a generic faithful morphism classifying it and such that the morphisms it classifies are closed under composition, finite fiberwise limits and colimits, and dependent products.

The last axiom is the "object classifier", and there's some room for discussion in how it should be phrased. The above phrasing will allow you to use it to reason about arbitrary 0-truncated objects, but it requires some large cardinals to model.

I expect that with the object classifier, one can prove that the category is "(2,1)-exact" in the sense that any "internal groupoid" in a suitable sense is the "kernel" of some quotient. A while ago I made some study of exactness conditions for 2-categories, the remnants of which can be found here. If one wants to avoid any universes, one could take this exactness as part of the definition instead, although exactness isn't the only purpose of the universe so this would impoverish the definition a bit.

Finally one would want to add some axioms analogous to the blah in ETCS. A (2,1)-category should be "well-pointed" if the terminal object is a "generator" in a suitable sense. Certainly the functor $E(1,-) : E \to Gpd$ should be locally faithful. Probably it's too much to ask it to be locally fully faithful. One might need to add some more "projectivity and indecomposablity" conditions analogous to the constructive notion of well-pointedness for 1-categories, if they don't follow automatically the way they do for classical 1-categories; I haven't thought too much about this.

Then if one wants a "classical" version analogous to ETCS, one can add the axiom of choice. The only thing to be aware of here is that it can pertain only to 0-truncated objects, as discussed in type theory in the HoTT Book. In a (2,1)-category, one way to state the internal axiom of choice is that for any (not necessarily truncated) object $U$ and 0-truncated (i.e. representably faithful) morphisms $Y\to X\to U$ such that $Y\to X$ is surjective, there exists a surjective map $V\to U$ such that the pullback of $Y\to X$ to $V$ has a section. Note that $V$ need not be 0-truncated either. In the presence of well-pointedness, this might simplify to a more "external" axiom of choice analogous to ETCS's "all epimorphisms split", but I haven't thought much about that either.

$\endgroup$
9
$\begingroup$

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.

$\endgroup$
3
  • $\begingroup$ An extremely lazy search of the slides did not reveal use of the word "univalence". Was I off-base in asserting above that formulating a correct (weak) version of univalence is essentially equivalent to understanding the analog of a (sub)object classifier and hence to getting a good theory? $\endgroup$
    – Tim Campion
    Feb 4, 2021 at 16:37
  • 1
    $\begingroup$ The paper explains that their type theory is suitably univalent. $\endgroup$ Feb 4, 2021 at 16:56
  • 1
    $\begingroup$ But yes, understanding the univalent universe is always the hard and illuminating. $\endgroup$ Feb 4, 2021 at 17:04
2
$\begingroup$

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

  1. 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".

  1. 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.

  2. 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.

$\endgroup$
5
  • $\begingroup$ Since a subobject classifier is simply an object that classifies $-1$-morphisms; i.e. internal trith values; I would think that the corresponding classifier would be something that could classify $0$-morphisms, or the discrete objects of the groupoid. This might be some internal notion of a groupoid of sets. $\endgroup$
    – user173426
    Feb 3, 2021 at 20:11
  • $\begingroup$ Yes. I should also mention that there has been work on 2-topoi (i.e. (2,2)-topoi in the terminology from above. In this terminology, what is normally called an $\infty$-topos should be called an $(\infty,1)$-topos, and what is normally called a topos or 1-topos should be called a (1,1)-topos).Just as the canonical 1-topos is $Set$, and the canonical $(2,1)$-topos is $Gpd$, the canonical $(2,2)$-topos is $Cat$.The "subobject classifier" of the 2-topos$Cat$ is $Set$. The "subobject classifier" of the (2,1)-topos of groupoids, would be the groupoid of sets $\endgroup$
    – Tim Campion
    Feb 3, 2021 at 20:17
  • $\begingroup$ However, the notion of the groupoid of sets in a category of groupoids has size issues, similar to the case in infinity topos theory, so it probably would make more sense to talk about internal groupoid of $\kappa$-small sets. $\endgroup$
    – user173426
    Feb 3, 2021 at 20:26
  • $\begingroup$ Yes. I believe in Weber's theory of 2-topoi, two universes are used. Size issues are important to think about here, and potentially very delicate. This is especially so if one is trying to work foundationally, because a lot of the ways we're used to thinking about size are potentially quite tied up with the details of the metatheory, which is usually ZFC (but if we're trying to build a foundational theory, we're probably trying to avoid using something like ZFC in any kind of metatheory). As Noah Snyder indicates, thinking about this from a type-theoretic perspective would at least mean no ZFC $\endgroup$
    – Tim Campion
    Feb 3, 2021 at 20:29
  • $\begingroup$ In the (Grothendieck) $\infty$-topos case, Lurie formally uses universes in the metatheory. That's not really relevant to the issue of thinking about size inside an $\infty$-topos, where he ends up with $\kappa$-object classifiers for every regular cardinal $\kappa$ or something. (I'm trying to say that your $\kappa$-small sets need not technically form a "universe" but just some sort of "weak universe"...) Anyway, the existing stuff outside of type theory is foundationally complicated. But type theorists do think carefully about these sorts of things. $\endgroup$
    – Tim Campion
    Feb 3, 2021 at 20:34

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.