## § Why is product in Rel not cartesian product?

#### § Monoidal category

- Intuitively, category can be equipped with $\otimes, I$ that makes it a monoid.

#### § Cartesian Monoidal category

- A category where the monoidal structure is given by the categorical product (universal property...).

#### § Fox's theorem: Any Symmetric Monoidal Category with Comonoid is Cartesian.

- Let
`C`

be symmetric monoidal under $(I, \otimes)$.

- A monoid has signature
`e: () -> C`

and `.: C x C -> C`

. - A comonoidal structure flips this, and gives us
`copy: C -> C x C`

, and `delete: C -> ()`

. - Fox's theorem tells us that if the category is symmetric monoidal, and has morphisms $copy: C \to C \otimes C$, and $delete: C \to I$ which obey some obvious conditions, then the monoidal product is the categorical product.

#### § Rel doesn't have the correct cartesian product

- This is because the naive product on Rel produces a monoidal structure on Rel.
- However, this does not validate the
`delete`

rule, because we can have a relation that does not relate a set to *anything *in the image. Thus, `A -R-> B -!-> 1`

need not be the same as `A -!-> 1`

if `R`

does not relate `A`

to ANYTHING. - Similarly, it does not validate the
`copy`

rule, because first relating and then copying is not the same as relating to two different copies, because `Rel`

represents nondeterminisim.

#### § Locally Caretesian Categories

- A category is locally cartesian if each of the slice categories are cartesian.
- That is, all $n$-ary categorical products (including $0$-ary) exist in the slice category of each object.
- MLTT corresponds to locally cartesian categories