Commit 2026-03-07 22:58 401ee042

chore: refactor CartesianMonoidalCategory instance on functors (#36331) The CartesianMonoidalCategory instance on functors categories to a cartesian monoidal category is bad: it is defined using ofChosenFiniteProduct, which redefines a whole MonoidalCategoryStruct on the category, instead of using the already existing pointwise monoidal structure from the file CategoryTheory.Monoidal.FunctorCategory. The two structures end up being defeq, as Functor.chosenProd is defeq to the pointwise tensor product, but this defeq requires unfolding a few defs to be seen. This PR deprecates the Functor.chosenProd and Functor.chosenTerminal and use the underlying pointwise monoidal structure for the instance underlying the cartesian monoidal category instance.