The Note: All precategories given can become categories via the univalence Rezk axiom completion . implies immediately that$\mathcal{Set}$ is a category. One can also show that any precategory of set-level structures such as groups, rings topologicial spaces, etc. is a category.

There is a precategory $\mathit{Set}$, whose type of objects is $Set$, and with $hom_{\mathit{Set}}(A,B)\equiv (A \to B)$. Under univalence this becomes a category. One can also show that any precategory of set-level structures such as groups, rings topologicial spaces, etc. is also a category.

For any 1-type $X$, there is a category with $X$ as its type of objects and with $hom(x,y)\equiv(x=y)$. If $X$ is a set we call this the discrete category on $X$. In general, we call this a groupoid.

For any type $X$, there is a precategory with $X$ as its type of objects and with $hom(x,y)\equiv \| x= y \|_0$. The composition operation

$\|y=z\|_0 \to \|x=y\|_0 \to \|y=z\|_0$

is defined by induction on truncation? from concatenation of the identity type. We call this the fundamental pregroupoid of $X$.

There is a precategory whose type of objects is $\mathcal{U}$ and with $hom(X,Y)\equiv \| X \to Y\|_0$, and composition defined by induction on truncation from ordinary composition of functions. We call this the homotopy precategory of types.