Linear Logic without Units

Understand

We study categorical models for the unitless fragment of multiplicative linear logic.

• We find that the appropriate notion of model is a special kind of promonoidal category.
• Since the theory of promonoidal categories has not been developed very thoroughly, at least in the published literature, we need to develop it here.
• The most natural way to do this - and the simplest, once the (substantial) groundwork has been laid - is to consider promonoidal categories as an instance of the general theory of pseudomonoids in a monoidal bicategory.