Homotopy Type Theory cartesian monoidal dagger category > history (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

Contents

Definition

A cartesian monoidal dagger category is a monoidal dagger category CC with

  • a morphism p A:hom(AB,A)p_A: hom(A \otimes B,A) for A:CA:C and B:CB:C.
  • a morphism p B:hom(AB,B)p_B: hom(A \otimes B,B) for A:CA:C and B:CB:C.
  • a morphism d AB:hom(D,AB)d_{A \otimes B}: hom(D,A \otimes B) for an object D:CD:C and morphisms d A:hom(D,A)d_A: hom(D,A) and d B:hom(D,B)d_B: hom(D,B)
  • an identity u A:p Ad AB=d Au_A: p_A \circ d_{A \otimes B} = d_A for an object D:CD:C and morphisms d A:hom(D,A)d_A: hom(D,A) and d B:hom(D,B)d_B: hom(D,B)
  • an identity u B:p Bd AB=d Bu_B: p_B \circ d_{A \otimes B} = d_B for an object D:CD:C and morphisms d A:hom(D,A)d_A: hom(D,A) and d B:hom(D,B)d_B: hom(D,B)
  • a morphism a !:hom(A,Ι)a_!: hom(A,\Iota) for every object A:CA:C

In a cartesian monoidal dagger category, the tensor product is called a cartesian product and the tensor unit is called a terminal object.

Examples

See also

Revision on June 7, 2022 at 15:22:20 by Anonymous?. See the history of this page for a list of all contributions to it.