Homotopy Type Theory
unitary isomorphism in a dagger precategory > history (Rev #2, changes)
Showing changes from revision #1 to #2:
Added | Removed | Changed
Definition
< unitary isomorphism
A morphism of a dagger precategory is a unitary isomorphism or dagger isomorphism if and . We write for the type of unitary isomorphisms.
Properties
For any the type “ is a unitary isomorphism” is a proposition. Therefore, for any the type is a set.
For , if , then (as defined in precategory) is a unitary isomorphism.
See also
Category theory
References
Revision on June 7, 2022 at 19:55:32 by
Anonymous?.
See the history of this page for a list of all contributions to it.