Homotopy Type Theory
monoidal dagger category > history (Rev #5)
Contents
Definition
A monoidal dagger category is a dagger category with
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 20:28:18 by
Anonymous?.
See the history of this page for a list of all contributions to it.