It is also worth mentioning a useful kind of precategory whose type of objects is not a set, but which is not a category either.
A -precategory is a precategory together with the following.
For each , a function .
For all , we have .
For all we have .
For all we have .
Of course, every unitary morphism is an isomorphism, and being unitary is a mere proposition. Thus for each we have a set of unitary isomorphisms from to , which we denote .
If , then is unitary.
By induction, we may assume is . But then and similarly. ∎
A -category is a -precategory such that for all , the function
from \autorefct:idtounitary is an equivalence.
The category from \autorefct:rel becomes a -precategory if we define . The proof that is a category actually shows that every isomorphism is unitary; hence is also a -category.
Any groupoid becomes a -category if we define .
Let be the following precategory.
Its morphisms are arbitrary linear maps.
By standard linear algebra, any linear map between finite dimensional inner product spaces has a uniquely defined adjoint , characterized by . In this way, becomes a -precategory. Moreover, a linear isomorphism is unitary precisely when it is an isometry, i.e. . It follows from this that is a -category, though it is not a category (not every linear isomorphism is unitary).
There has been a good deal of general theory developed for -categories under classical foundations. It was observed early on that the unitary isomorphisms, not arbitrary isomorphisms, are the correct notion of “sameness” for objects of a -category, which has caused some consternation among category theorists. Homotopy type theory resolves this issue by identifying -categories, like strict categories, as simply a different kind of precategory.