# 9.7 $\dagger$-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 $\dagger$-precategory is a precategory $A$ together with the following.

1. 1.

For each $x,y:A$, a function ${(-)}^{\dagger}:\hom_{A}(x,y)\to\hom_{A}(y,x)$.

2. 2.

For all $x:A$, we have ${(1_{x})}^{\dagger}=1_{x}$.

3. 3.

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

4. 4.

For all $f$ we have ${({f}^{\dagger})}^{\dagger}=f$.

###### Definition 9.7.2.

A morphism $f:\hom_{A}(x,y)$ in a $\dagger$-precategory is unitary if ${f}^{\dagger}\circ f=1_{x}$ and $f\circ{f}^{\dagger}=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\mathrel{\cong^{\dagger}}y)$.

###### Lemma 9.7.3.

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

###### Proof.

By induction, we may assume $p$ is $\mathsf{refl}_{x}$. But then ${(1_{x})}^{\dagger}\circ 1_{x}=1_{x}\circ 1_{x}=1_{x}$ and similarly. ∎

###### Definition 9.7.4.

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

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

from \autorefct:idtounitary is an equivalence.

###### Example 9.7.5.

The category $\mathcal{R}el$ from \autorefct:rel becomes a $\dagger$-precategory if we define $({R}^{\dagger})(y,x):\!\!\equiv R(x,y)$. The proof that $\mathcal{R}el$ is a category actually shows that every isomorphism is unitary; hence $\mathcal{R}el$ is also a $\dagger$-category.

###### Example 9.7.6.

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

###### Example 9.7.7.

Let $\mathcal{H}ilb$ be the following precategory.

• Its objects are finite-dimensional vector spaces equipped with an inner product $\langle\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt},\mathord{\hskip 1.0pt\text{% --}\hskip 1.0pt}\rangle$.

• Its morphisms are arbitrary linear maps.

By standard linear algebra, any linear map $f:V\to W$ between finite dimensional inner product spaces has a uniquely defined adjoint ${f}^{\dagger}:W\to V$, characterized by $\langle fv,w\rangle=\langle v,{f}^{\dagger}w\rangle$. In this way, $\mathcal{H}ilb$ becomes a $\dagger$-precategory. Moreover, a linear isomorphism is unitary precisely when it is an isometry, i.e. $\langle fv,fw\rangle=\langle v,w\rangle$. It follows from this that $\mathcal{H}ilb$ is a $\dagger$-category, though it is not a category (not every linear isomorphism is unitary).

There has been a good deal of general theory developed for $\dagger$-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 $\dagger$-category, which has caused some consternation among category theorists. Homotopy type theory resolves this issue by identifying $\dagger$-categories, like strict categories, as simply a different kind of precategory.

 Title 9.7 $\dagger$-categories \metatable