nLab univalent dagger category

Contents

Contents

Definition

In homotopy type theory, given a dagger category AA and objects a,b:Aa,b:A, then by induction on identity, there is a function

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

as we may assume aa and bb are the same, which means 1 a:hom A(a,a)1_a:hom_A(a,a), which is a unitary isomorphism.

AA is a univalent dagger category or a saturated dagger category if for all a,b:Aa,b:A, idtouiso a,bidtouiso_{a,b} is an equivalence.

The inverse of idtouisoidtouiso is denoted uisotoiduisotoid.

Examples

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

  • The dagger category RelRel of sets and relations is a univalent dagger category with f f^\dagger representing the opposite relation of a relation ff.

  • The dagger category HilbHilb\mathbb{R} of Hilbert spaces over the real numbers and linear maps is a univalent dagger category with f f^\dagger representing the adjoint linear map of ff.

See also

References

Last revised on June 6, 2022 at 15:27:40. See the history of this page for a list of all contributions to it.