§ 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