Homotopy Type Theory dagger category > history (Rev #1)

Contents

Definition

A dagger category is a dagger precategory such that for all a,b:Aa,b:A, the function idtouiso a,bidtouiso_{a,b}, as defined in the dagger precategory article, is an equivalence.

The inverse of idtouisoidtouiso is denoted uisotoiduisotoid.

Examples

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

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

  • The dagger category HilbHilb of Hilbert spaces and linear functions is a dagger category with f f^\dagger representing the adjoint linear function of ff.

See also

References

Revision on February 14, 2022 at 08:06:56 by Anonymous?. See the history of this page for a list of all contributions to it.