Semantics

A strict symmetric premonoidal category (proposed by Power and Robinson) is a category P together with:

A strict symmetric monoidal category C with the same objects as P (called the centre of P).
An identity on objects inclusion C P.
Two functors:
: C P P
: P C P
such that:
- the three functors , and coincide on objects,
- the three `obvious' functors from C C to P coincide, and
- the symmetry in C is a natural isomorphism X Y Y X in P.