9.7 -categories

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.

Definition 9.7.1.

A -precategory is a precategory A together with the following.

  1. 1.

    For each x,y:A, a function (-):homA(x,y)homA(y,x).

  2. 2.

    For all x:A, we have (1x)=1x.

  3. 3.

    For all f,g we have (gf)=fg.

  4. 4.

    For all f we have (f)=f.

Definition 9.7.2.

A morphism f:homA(x,y) in a -precategory is unitary if ff=1x and ff=1y.

Of course, every unitary morphism is an isomorphismPlanetmathPlanetmathPlanetmathPlanetmath, and being unitary is a mere proposition. Thus for each x,y:A we have a set of unitary isomorphisms from x to y, which we denote (xy).

Lemma 9.7.3.

If p:(x=y), then idtoiso(p) is unitary.


By inductionMathworldPlanetmath, we may assume p is 𝗋𝖾𝖿𝗅x. But then (1x)1x=1x1x=1x and similarly. ∎

Definition 9.7.4.

A -category is a -precategory such that for all x,y:A, the function


from \autorefct:idtounitary is an equivalence.

Example 9.7.5.

The category Rel from \autorefct:rel becomes a -precategory if we define (R)(y,x):R(x,y). The proof that Rel is a category actually shows that every isomorphism is unitary; hence Rel is also a -category.

Example 9.7.6.

Any groupoid becomes a -category if we define f:f-1.

Example 9.7.7.

Let Hilb be the following precategory.

By standard linear algebraMathworldPlanetmath, any linear map f:VW between finite dimensional inner product spacesMathworldPlanetmath has a uniquely defined adjointPlanetmathPlanetmathPlanetmath f:WV, characterized by fv,w=v,fw. In this way, Hilb becomes a -precategory. Moreover, a linear isomorphism is unitary precisely when it is an isometry, i.e. fv,fw=v,w. It follows from this that Hilb 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.

Title 9.7 -categories