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 $\mathrm{†}$-precategory is a precategory $A$ together with the following.

1. For each $x,y:A$, a function ${(-)}^{†}:{\mathrm{hom}}_A(x,y)\to {\mathrm{hom}}_A(y,x)$.

2. For all $x:A$, we have ${(1_x)}^{†}=1_x$.

3. For all $f,g$ we have ${(g\circ f)}^{†}=f^{†}\circ g^{†}$.

4. For all $f$ we have ${(f^{†})}^{†}=f$.

Definition 9.7.2.

A morphism $f\mathrm{:}{\mathrm{hom}}_A\mathit{}\mathrm{(}x\mathrm{,}y\mathrm{)}$ in a $\mathrm{†}$-precategory is unitary if $f^{\mathrm{†}}\mathrm{\circ }f\mathrm{=}{\mathrm{1}}_x$ and $f\mathrm{\circ }{f}^{\mathrm{†}}\mathrm{=}{\mathrm{1}}_y$.

Of course, every unitary morphism is an isomorphism, 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 $(x{\cong }^{†}y)$.

Lemma 9.7.3.

If $p\mathrm{:}\mathrm{(}x\mathrm{=}y\mathrm{)}$, then $\mathrm{idtoiso}\mathit{}\mathrm{(}p\mathrm{)}$ is unitary.

Proof.

By induction, we may assume $p$ is ${\mathrm{𝗋𝖾𝖿𝗅}}_x$. But then ${(1_x)}^{†}\circ 1_x=1_x\circ 1_x=1_x$ and similarly. ∎

Definition 9.7.4.

A $\mathrm{†}$-category is a $\mathrm{†}$-precategory such that for all $x\mathrm{,}y\mathrm{:}A$, the function

$$(x=y)\to (x{\cong }^{†}y)$$

from ct:idtounitary is an equivalence.

Example 9.7.5.

The category $\mathrm{R}\mathit{}e\mathit{}l$ from ct:rel becomes a $\mathrm{†}$-precategory if we define $\mathrm{(}{R}^{\mathrm{†}}\mathrm{)}\mathrm{(}y\mathrm{,}x\mathrm{)}\mathrm{:}\mathrm{\equiv }R\mathrm{(}x\mathrm{,}y\mathrm{)}$. The proof that $\mathrm{R}\mathit{}e\mathit{}l$ is a category actually shows that every isomorphism is unitary; hence $\mathrm{R}\mathit{}e\mathit{}l$ is also a $\mathrm{†}$-category.

Example 9.7.6.

Any groupoid becomes a $\mathrm{†}$-category if we define $f^{\mathrm{†}}\mathrm{:}\mathrm{\equiv }{f}^{\mathrm{-}\mathrm{1}}$.

Example 9.7.7.

Let $\mathrm{H}\mathit{}i\mathit{}l\mathit{}b$ be the following precategory.

• Its objects are finite-dimensional vector spaces equipped with an inner product $⟨\mathit{\text{–}},\mathit{\text{–}}⟩$.

• Its morphisms are arbitrary linear maps.

By standard linear algebra, any linear map $f\mathrm{:}V\mathrm{\to }W$ between finite dimensional inner product spaces has a uniquely defined adjoint $f^{\mathrm{†}}\mathrm{:}W\mathrm{\to }V$, characterized by $\mathrm{⟨}f\mathit{}v\mathrm{,}w\mathrm{⟩}\mathrm{=}\mathrm{⟨}v\mathrm{,}{f}^{\mathrm{†}}\mathit{}w\mathrm{⟩}$. In this way, $\mathrm{H}\mathit{}i\mathit{}l\mathit{}b$ becomes a $\mathrm{†}$-precategory. Moreover, a linear isomorphism is unitary precisely when it is an isometry, i.e. $\mathrm{⟨}f\mathit{}v\mathrm{,}f\mathit{}w\mathrm{⟩}\mathrm{=}\mathrm{⟨}v\mathrm{,}w\mathrm{⟩}$. It follows from this that $\mathrm{H}\mathit{}i\mathit{}l\mathit{}b$ is a $\mathrm{†}$-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