Homotopy Type Theory
compact closed dagger category > history (Rev #2, changes)
Showing changes from revision #1 to #2:
Added | Removed | Changed
Contents
Definition
A compact closed dagger category is a symmetric monoidal dagger category with
-
an object called the dual for every object
-
for every object , a morphism called the right unit
-
for every object , a morphism called the left unit
-
for every object , a morphism called the left counit
-
for every object , a morphism called the right counit
-
a type family with dependent terms for
-
a type family with dependent terms for
-
a type family with dependent terms for
-
a type family with dependent terms for
-
a type family with dependent terms for
-
a type family with dependent terms for
Examples
(…)
See also
Revision on June 7, 2022 at 15:16:07 by
Anonymous?.
See the history of this page for a list of all contributions to it.