#
Homotopy Type Theory
cartesian monoidal dagger category > history (Rev #2, changes)

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

~~
~~# 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**.

~~
~~## Examples

~~
~~~~
~~## See also

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