Groupoids more fundamental than categories, really?

Question

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.

Answer 1

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.

Answer 2

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.

Answer 3

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.