[[!redirects dagger precategories]] ## Contents ## * table of contents {:toc} ## 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 in a dagger precategory|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 $$idtouiso : (a=b) \to (a \cong^\dagger b)$$ *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]] category: category theory