Homotopy Type Theory dagger category > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

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 HilbR of Hilbert spaces over the real numbers and linear maps is a dagger category with f f^\dagger representing the adjoint linear map of ff.

See also

References

Revision on June 7, 2022 at 20:40:33 by Anonymous?. See the history of this page for a list of all contributions to it.