Homotopy Type Theory
unitary isomorphism in a dagger precategory > history (Rev #1)
Definition
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 February 14, 2022 at 08:09:42 by
Anonymous?.
See the history of this page for a list of all contributions to it.