Commit 2025-11-04 20:27 dec45e96

feat(CategoryTheory): semicartesian monoidal categories (#31064) This PR refactors Cartesian Monoidal Categories through Semicartesian Monoidal Categories. There are interesting weaker settings where it is too much to ask the full monoidal structure to be given by the cartesian structure, but reasonable for the monoidal unit to be terminal. A category like this is usually referred to as "Semicartesian". In semicartesian setting we have fst (X Y : C) : X ⊗ Y ⟶ X and snd (X Y : C) : X ⊗ Y ⟶ Y for free, but without their universal property. https://ncatlab.org/nlab/show/semicartesian+monoidal+category This PR makesCartesianMonoidalCategory an extension of SemiCartesianMonoidalCategory Some examples of semicartesian but not cartesian monoidal categories:

• The opposite of the category FinInj of finite sets with injections.
• The category of nominal sets.
• The category of commutative (semi-) rings. Personally, I need semicartesian structure for two other downstream projects where the use cases are natural number objects in semicartesian monoidal categories and the category of context of certain type theories.