Homotopy Type Theory
monoidal dagger category > history (Rev #1)
Contents
Definition
A monoidal dagger category is a dagger category with
-
a functor from the product dagger category of to itself called the tensor product.
-
an object called the tensor unit.
-
a natural unitary isomorphism type family
called the associator, with dependent terms
- a natural unitary isomorphism type family
called the left unitor, with dependent terms
- a natural unitary isomorphism type family
called the right unitor, with dependent terms
called the triangle identity, with dependent terms
called the pentagon identity, with dependent terms
Examples
See also
Revision on February 14, 2022 at 09:17:39 by
Anonymous?.
See the history of this page for a list of all contributions to it.