Groupoids more fundamental than categories, really? 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.
 A: 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.
A: 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.
A: 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.
