## Idea $Hilb_\mathbb{R}$ is the category of Hilbert spaces over the real numbers, with morphisms the linear maps between Hilbert spaces over the real numbers. ## Definition (Todo: address size issues with regards to universes, as well as the non-constructive nature of the proof...) Assuming propositional excluded middle in the type theory, $Hilb_\mathbb{R}$ is a [[dagger category]] with * a tensor product $\otimes$ and tensor unit $\Iota$, such that $(Hilb_\mathbb{R},\otimes,\Iota)$ is a [[symmetric monoidal dagger category]] and $\Iota$ is a [[simple object]] and a monoidal [[separator]], * a biproduct $\oplus$ and zero object $0$ such that $(Hilb_\mathbb{R},\oplus,0)$ is a [[semiadditive dagger category]] * a [[dagger equaliser]] $eq$ such that $(Hilb_\mathbb{R},\oplus,0,eq)$ is a [[finitely complete dagger category]] * a [[directed colimit]] $\underrightarrow{lim} F$ for any inductive system $F$ in the wide sub-dagger category of objects and [[dagger monomorphisms]]. * a morphism $g:B \to C$ for any [[dagger monomorphism]] $f:A \to B$ such that $g = eq(f,0_B \circ 0_A^\dagger)$ * an identity $t:f^\dagger = f$ for any $f:hom(\Iota,\Iota)$. ## References * Chris Heunen, Andre Kornell. Axioms for the category of Hilbert spaces ([arXiv:2109.07418](https://arxiv.org/abs/2109.07418))