Homotopy Type Theory
monoidal dagger category > history (Rev #3, changes)
Showing changes from revision #2 to #3:
Added | Removed | Changed
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
with dependent terms
for morphisms and ,
- a natural unitary isomorphism type family
called the associator, with dependent terms
for objects , , .
- a natural unitary isomorphism type family
called the left unitor, with dependent terms
for objects .
- a natural unitary isomorphism type family
called the right unitor, with dependent terms
for objects .
called the triangle identity, with dependent terms
for objects , .
called the pentagon identity, with dependent terms
for objects , , , .
Examples
See also
Revision on February 14, 2022 at 15:31:42 by
Anonymous?.
See the history of this page for a list of all contributions to it.