Homotopy Type Theory cartesian monoidal dagger category > history (Rev #1)

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 February 14, 2022 at 20:29:01 by Anonymous?. See the history of this page for a list of all contributions to it.