Groupoids more fundamental than categories, really?

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.


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.


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.