A dagger precategory is a precategory with the following:
There are two notions of “sameness” for objects of a dagger precategory. On one hand we have a unitary isomorphism between objects and on the other hand we have equality of objects and .
There is a special kind of dagger precategory called a dagger category where these two notions of equality coincide and some very nice properties arise:
If is a dagger precategory and , then there is a map
Proof. By induction on identity, we may assume and are the same. But then we have , which is a unitary isomorphism.
Every dagger category is a dagger precategory.
For any type , there is a dagger precategory with as its type of objects and with . The composition operation
is defined by induction on truncation? from concatenation of the identity type, and the dagger is defined by induction on truncation? from inversion of the identity type. We call this the fundamental pregroupoid of .