search

jwiegley / category-theory

An axiom-free formalization of category theory in Coq for personal study and practical work
BSD 3-Clause "New" or "Revised" License
748 stars 69 forks source link

CartesianMonoidal cleanup #139

Open patrick-nicodemus opened 8 months ago

patrick-nicodemus commented 8 months ago

I suggest some reorganization and renaming in Structure/Monoidal/Cartesian.v and Structure/Monoidal/Cartesian/Cartesian.v.

There are two relations between monoidal products and Cartesian products:

  1. Every Cartesian product is a monoidal product.
  2. A monoidal product which is both semicartesian and relevant is a Cartesian product, this is the result by by Heunen and Vicary proven in Structure/Monoidal/Cartesian.v.

The second theorem is important and interesting, but I don't expect it to be actually heavily used by users of the library. Instead, I suspect that if a user wants to prove that their category is Cartesian, they will show that for each pair of objects x, y there is an object z with the universal property of the Cartesian product. I have never personally needed or used theorem 2 to prove that a concrete category has a Cartesian product.

On the other hand, 1. is obviously very important, because it allows us to prove theorems about general monoidal products which automatically hold for Cartesian products. I'm not aware of a proof of 1. in the library at this moment. It should be added. I can try to do this when I get a chance.

I also suggest reorganizing things to deemphasize the proof of theorem 2 in order to make it easier to find the proof of theorem 1. I think a file named Monoidal/Cartesian.v which contains a typeclass called "CartesianMonoidal" and proves that a "CartesianMonoidal" product is Cartesian is likely to be misleading to readers who are looking for a proof that a Cartesian category is also a monoidal category. Furthermore it is defined as a typeclass which is probably unnecessary as, realistically, this theorem is applied rarely enough that it doesn't need typeclass resolution.

I would suggest we simply delete the typeclass CartesianMonoidal and just prove the result by separately assuming the two typeclasses RelevantMonoidal and Semicartesian. A pair of only two assumptions does not need to be bundled together, and the choice of bundle name pollutes the library namespace. We should also rename the files "Monoidal/Cartesian.v" and "Monoidal/Cartesian/Cartesian.v" to something that does less overloading of the heavily used terms "Monoidal" and "Cartesian" such as, for example, "Heunen_Vicary.v".

jwiegley commented 2 weeks ago

All of this sounds entirely reasonable to me.