When working in intensional type theory such as homotopy type theory, the notion of category has both a precategory version and a univalent category version. The same is true for other categorical structures, in particular for dagger-categories we have $\dagger$-precategories and univalent $\dagger$-categories.
A $\dagger$-precategory is defined in type theory using the “family of functions” definition of dagger-category. Thus, it consists of
A precategory $C$, with type of objects $Ob(C)$ and hom-sets $Hom : Ob(C) \to Ob(C) \to Set$.
For all $A,B:Ob(C)$, a function $(-)^\dagger : Hom(A,B) \to Hom(B,A)$
For every $A \in Ob(C)$, $(1_A)^\dagger = 1_A$.
For every $A,B \in Ob(C)$ and every $f \in Hom_C(A,B)$ and $g \in Hom_C(B,C)$, $(g \circ f)^\dagger = f^\dagger \circ g^\dagger$.
For every $A,B \in Ob(C)$ and every $f \in Hom_C(A,B)$, $((f)^\dagger)^\dagger = f$.
Note that as for any precategory, there is no h-level restriction on the type $Ob(C)$. As usual in a $\dagger$-category, we define an isomorphism in a $\dagger$-precategory to be unitary if $f^{-1} = f^\dagger$.
Let $(a \cong^\dagger b)$ denote the type of unitary isomorphisms. The identity morphism is unitary, so there is a function
defined by induction on identity.
A $\dagger$-precategory is univalent (or saturated) if $idtouiso$ is an equivalence for all $a,b:Ob(C)$.
We may denote the inverse of $idtouiso$ by $uisotoid$.
Every univalent groupoid is a univalent dagger category with $f^\dagger = f^{-1}$.
There is a $\dagger$-precategory Rel of h-sets and relations (i.e. Prop-valued binary functions), where $f^\dagger$ is the opposite relation of a relation $f$. Assuming the global univalence axiom, this $\dagger$-category is univalent because an invertible relation is necessarily a function, and hence a bijection.
There is a $\dagger$-category $Hilb\mathbb{R}$ of Hilbert spaces over the real numbers and linear maps, where $f^\dagger$ is the adjoint linear map of $f$. This is also univalent, assuming the univalence axiom.
Indeed, if the univalence axiom holds, then most naturally-occurring $\dagger$-categories can be proven to be univalent.
Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013): Section 9.7.
Benedikt Ahrens, Paige North, Mike Shulman, and Dimitris Tsementzis, The Univalence Principle, arxiv (2021): Example 12.1.
Last revised on November 8, 2023 at 08:58:52. See the history of this page for a list of all contributions to it.