Homotopy Type Theory cocartesian monoidal dagger category > history (Rev #3, changes)

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

Contents

Definition

A cocartesian monoidal dagger category is a monoidal dagger category (C,+,0)(C, +, 0) with

  • a morphism i A:hom(A,A+B)i_A: hom(A,A + B) for A:CA:C and B:CB:C.
  • a morphism i B:hom(B,A+B)i_B: hom(B,A + B) for A:CA:C and B:CB:C.
  • a morphism d A+B:hom(A+B,D)d_{A + B}: hom(A + B,D) for an object D:CD:C and morphisms d A:hom(A,D)d_A: hom(A,D) and d B:hom(B,D)d_B: hom(B,D)
  • an identity u A:d A+Bi A=d Au_A: d_{A + B} \circ i_A = d_A for an object D:CD:C and morphisms d A:hom(A,D)d_A: hom(A,D) and d B:hom(B,D)d_B: hom(B,D)
  • an identity u B:d A+Bi B=d Bu_B: d_{A + B} \circ i_B = d_B for an object D:CD:C and morphisms d A:hom(A,D)d_A: hom(A,D) and d B:hom(B,D)d_B: hom(B,D)
  • a morphism 0 a:hom(0,A)0_a: hom(0,A) for every object A:CA:C
  • an identity u 0:f0 A=0 Bu_0: f \circ 0_A = 0_B for for A:CA:C and B:CB:C and f:hom(A,B)f:hom(A,B).

In a cocartesian monoidal dagger category, the tensor product is called a coproduct and the tensor unit is called an initial object.

Examples

See also

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