Semicartesian Monoidal Categories?

Stream: mathlib4

[Sina Hazratpour]

We have Cartesian Monoidal Categories in Mathlib. I am working in a weaker setting where it is too much to ask the monoidal structure to be given by the cartesian structure. However it is OK for the monoidal unit to be terminal. A category like this is usually referred to as "Semicartesian". Maybe the most famous example of a semicartesian monoidal – but not cartesian monoidal – category is the opposite of the category FinInj of finite sets with injections. Another related example is the category of nominal sets.

Semicartesian Monoidal is not on mathlib, and it seems not on any branch either. I have some basic development including he example of <finite sets and injections>^op , but it would be nice to know if someone has already developed this stuff somewhere else.

A design proposal: once we have SemiCartesianMonoidalCategory, I think CartesianMonoidalCategory should be an extension of this structure. 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.

[Sina Hazratpour]

I made a PR in #31064. @Joël Riou suggested discussing this PR over Zulip.

[Kim Morrison]

It doesn't seem particularly problematic. @Sina Hazratpour, could you provide links to the downstream developments you referred to?