# 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 $C$ with

• a morphism $p_A: hom(A \otimes B,A)$ for $A:C$ and $B:C$.
• a morphism $p_B: hom(A \otimes B,B)$ for $A:C$ and $B:C$.
• a morphism $d_{A \otimes B}: hom(D,A \otimes B)$ for an object $D:C$ and morphisms $d_A: hom(D,A)$ and $d_B: hom(D,B)$
• an identity $u_A: p_A \circ d_{A \otimes B} = d_A$ for an object $D:C$ and morphisms $d_A: hom(D,A)$ and $d_B: hom(D,B)$
• an identity $u_B: p_B \circ d_{A \otimes B} = d_B$ for an object $D:C$ and morphisms $d_A: hom(D,A)$ and $d_B: hom(D,B)$
• a morphism $a_!: hom(A,\Iota)$ for every object $A:C$

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