14
$\begingroup$

I've skimmed through a survey by Thierry Coquand on univalent foundations. It is claimed that "groupoids are more fundamental than categories". And that categories can be seen as groupoids equipped with a kind of preordered structure. See here, pp. 41-45. But I don't really understand the details of this construction. Is it possible to explain this in classical mathematics? That is, is there a definition of a category (in the classical sense) in terms of a groupoid with additional structure? The HoTT book defines categories directly without using groupoids.

$\endgroup$
4
  • 2
    $\begingroup$ What survey? Can you link to or quote the construction? $\endgroup$ Mar 2, 2015 at 6:20
  • $\begingroup$ @QiaochuYuan: I've added the link. $\endgroup$ Mar 2, 2015 at 9:09
  • 7
    $\begingroup$ Well, of course groupoids are more fundamental in univalent foundations – the whole point is that every type is an $\infty$-groupoid. In much the same way, sets are more fundamental than (say) posets in set theory. $\endgroup$
    – Zhen Lin
    Mar 2, 2015 at 9:12
  • 3
    $\begingroup$ I'm not sure about groupoids and categories, but for $\infty$-groupoids and $\infty$-categories (which seems to be what this survey is actually about), an $\infty$-category "is" a category enriched in $\infty$-groupoids, up to correct definition of these terms. So at least from this point of view, groupoids are "more fundamental" than categories, since $\infty$-categories are defined using $\infty$-groupoids. (I know nothing about univalent foundations, so that may not be what the author had in mind...) $\endgroup$ Mar 2, 2015 at 14:31

3 Answers 3

7
$\begingroup$

The definition of category in the HoTT book is exactly what you are looking for: just read "groupoid" for "1-type". But it can also be said in more traditional language: categories can be identified with internal categories in groupoids that satisfy a saturation condition.

$\endgroup$
8
  • $\begingroup$ Thank you. But does this justify the phrase that groupoids are more fundamental than categories? $\endgroup$ Mar 2, 2015 at 17:43
  • $\begingroup$ @Mike Something I wondered about recently: Rezk-completeness of a precategory in 1-groupoids more or less means that the space of equivalences between two objects is 0-truncated, but how do we know that the space of morphisms is 0-truncated? $\endgroup$
    – Zhen Lin
    Mar 2, 2015 at 19:06
  • $\begingroup$ @ZhenLin that has to be assumed separately. In the HoTT book definition, the space of morphisms being 0-truncated is part of what it means to be a precategory. $\endgroup$ Mar 3, 2015 at 21:00
  • 2
    $\begingroup$ @MartinBrandenburg I wouldn't personally claim that "groupoids are more fundamental than categories", at least not without making the context clear. In HoTT, groupoids are basic objects out of which other things are built, so in that sense they are more fundamental. In a foundation where categories are the basic objects, like Lawvere's ETCC, the opposite would be true. In set theory, where both groupoids and categories are built out of sets, it's less clear; usually groupoids are defined as particular categories, but this shows that categories can also be built out of groupoids. (cont.) $\endgroup$ Mar 3, 2015 at 21:09
  • 1
    $\begingroup$ So the question is really, what does "more fundamental" mean? Does it involve a normative judgment about which definition is better, or which foundational theory is better? In that case it's eventually going to reduce to opinion; one can make arguments one way or the other, but this isn't the place for them. So the short answer is, this construction by itself doesn't "justify" such a claim, although perhaps one might say that it makes it possible to make such a claim (after which one would then have to justify it). $\endgroup$ Mar 3, 2015 at 21:12
3
$\begingroup$

I'm not sure if this is what you are looking for, or if this is basic knowledge to you. But, in Type Theory every type has the structure of an $\infty$-groupoid. Given two elements of a type $a,b:A$, we have an identity type $a=_Ab$ that expresses the fact that $a$ and $b$ are equal. If $a=_Ab$ has an element, then $a$ and $b$ are equal. Since $a=_Ab$ is a type, we can also get a type $p=_{a=_Ab}q$. We can iterate this process indefinitely. The various coherence laws make this into an $\infty$-groupoid structure.

A set in type theory is a type such that any two elements of an identity type are equal. Then a precategory is a type of objects and, for any two objects, a set type of morphisms. A category is a precategory where isomorphisms of objects are equivalent as equality. Since all types have an $\infty$-groupoid structure, the type of objects is an $\infty$-groupoid and so are all the morphism sets.

$\endgroup$
1
  • 1
    $\begingroup$ Well, this is all contained in the survey article. I wanted to understand the phrase "groupoids are more fundamental than categories" in classical mathematics, without type theory, if this is possible at all. $\endgroup$ Mar 2, 2015 at 13:59
1
$\begingroup$

You should look at http://www.springer.com/us/book/9781441915238, specially "Lectures on n-categories and cohomology, Baez and Shulman".

A set can then be regarded as a discrete poset, or equivalently a poset in which every morphism is invertible; that is, a '0-groupoid'.

The moral then should be (paraphrasing Voevodsky) that categories are partially ordered sets in the next dimension and groupoids are sets in the next dimension.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .