Homotopy Type Theory semiadditive dagger category > history (Rev #4, changes)

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



A semiadditive dagger category is a cocartesian monoidal dagger category (C,,0,i A,i B,0 A)(C, \oplus, 0, i_A, i_B, 0_A) with

  • an identity m A:i A i A=id Am_A: i_A^\dagger \circ i_A = id_A for A:CA:C
  • an identity m B:i B i B=id Bm_B: i_B^\dagger \circ i_B = id_B for B:CB:C
  • an identity p:i b i A=0 B0 A p: i_b^\dagger \circ i_A = 0_B \circ 0_A^\dagger for A:CA:C and B:CB:C.

In a semiadditive dagger category, the coproduct is called a biproduct and the initial object is called a zero object.



See also


  • Martti Karvonen. Biproducts without pointedness (abs:1801.06488)
  • Chris Heunen and Martti Karvonen. Limits in dagger categories. Theory and Applications of Categories, 34(18):468–513, 2019.
  • Chris Heunen, Andre Kornell. Axioms for the category of Hilbert spaces (arXiv:2109.07418)

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