§ Why is product in Rel not cartesian product?
§ Monoidal category
- Intuitively, category can be equipped with 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.
C be symmetric monoidal under .
- 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 , and 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 -ary categorical products (including -ary) exist in the slice category of each object.
- MLTT corresponds to locally cartesian categories