Homotopy Type Theory dagger precategory > history (Rev #1)

Contents

Definition

A dagger precategory $A$ is a precategory with the following:

• For every $a,b:A$, a function $(-)^\dagger: hom_A(a,b) \to hom_A(b,a)$
• For every $a:A$, an identity $(1_a)^\dagger = 1_a$
• For every $a,b:A$ and every $f:hom_A(a,b)$ and $g:hom_A(b,c)$, an identity $(g \circ f)^\dagger = f^\dagger \circ g^\dagger$
• For every $a,b:A$ and every $f:hom_A(a,b)$, an identity $((f)^\dagger)^\dagger = f$.

Properties

There are two notions of “sameness” for objects of a dagger precategory. On one hand we have a unitary isomorphism between objects $a$ and $b$ on the other hand we have equality of objects $a$ and $b$.

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 $A$ is a dagger precategory and $a,b:A$, then there is a map

Proof. By induction on identity, we may assume $a$ and $b$ are the same. But then we have $1_a:hom_A(a,a)$, which is a unitary isomorphism. $\square$

Examples

• Every dagger category is a dagger precategory.

• For any type $X$, there is a dagger precategory with $X$ as its type of objects and with $hom(x,y)\equiv \| x= y \|_0$. The composition operation

  $$\|y=z\|_0 \to \|x=y\|_0 \to \|y=z\|_0$$

  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 $X$.

See also

• Category theory
• precategory

References

HoTT Book