Homotopy Type Theory
compact closed dagger category > history (Rev #1)
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 February 14, 2022 at 16:18:59 by
Anonymous?.
See the history of this page for a list of all contributions to it.