nLab univalent dagger category




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 CC, with type of objects Ob(C)Ob(C) and hom-sets Hom:Ob(C)Ob(C)SetHom : Ob(C) \to Ob(C) \to Set.

  • For all A,B:Ob(C)A,B:Ob(C), a function () :Hom(A,B)Hom(B,A)(-)^\dagger : Hom(A,B) \to Hom(B,A)

  • For every AOb(C)A \in Ob(C), (1 A) =1 A(1_A)^\dagger = 1_A.

  • For every A,BOb(C)A,B \in Ob(C) and every fHom C(A,B)f \in Hom_C(A,B) and gHom C(B,C)g \in Hom_C(B,C), (gf) =f g (g \circ f)^\dagger = f^\dagger \circ g^\dagger.

  • For every A,BOb(C)A,B \in Ob(C) and every fHom C(A,B)f \in Hom_C(A,B), ((f) ) =f((f)^\dagger)^\dagger = f.

Note that as for any precategory, there is no h-level restriction on the type Ob(C)Ob(C). As usual in a \dagger-category, we define an isomorphism in a \dagger-precategory to be unitary if f 1=f f^{-1} = f^\dagger.

Let (a b)(a \cong^\dagger b) denote the type of unitary isomorphisms. The identity morphism is unitary, so there is a function

idtouiso:(a=b)(a b)idtouiso : (a=b) \to (a \cong^\dagger b)

defined by induction on identity.


A \dagger-precategory is univalent (or saturated) if idtouisoidtouiso is an equivalence for all a,b:Ob(C)a,b:Ob(C).

We may denote the inverse of idtouisoidtouiso by uisotoiduisotoid.


  • Every univalent groupoid is a univalent dagger category with f =f 1f^\dagger = f^{-1}.

  • There is a \dagger-precategory Rel of h-sets and relations (i.e. Prop-valued binary functions), where f f^\dagger is the opposite relation of a relation ff. 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 HilbHilb\mathbb{R} of Hilbert spaces over the real numbers and linear maps, where f f^\dagger is the adjoint linear map of ff. 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.

See also


Last revised on November 8, 2023 at 08:58:52. See the history of this page for a list of all contributions to it.