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

Showing changes from revision #2 to #3:
Added | ~~Removed~~ | ~~Chan~~ged

~~
~~# Contents

~~
~~~~
~~## Definition

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

~~
~~
- a morphism $i_A: hom(A,A + B)$ for $A:C$ and $B:C$.
- a morphism $i_B: hom(B,A + B)$ for $A:C$ and $B:C$.
- a morphism $d_{A + B}: hom(A + B,D)$ for an object $D:C$ and morphisms $d_A: hom(A,D)$ and $d_B: hom(B,D)$
- an identity $u_A: d_{A + B} \circ i_A = d_A$ for an object $D:C$ and morphisms $d_A: hom(A,D)$ and $d_B: hom(B,D)$
- an identity $u_B: d_{A + B} \circ i_B = d_B$ for an object $D:C$ and morphisms $d_A: hom(A,D)$ and $d_B: hom(B,D)$
- a morphism $0_a: hom(0,A)$ for every object $A:C$
- an identity $u_0: f \circ 0_A = 0_B$ for for $A:C$ and $B:C$ and $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.