Homotopy Type Theory HilbR > history (Rev #1)

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…)

$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)