How to define par-operations for given tensors

Jürgen Koslowski

Abstract

We present two construction principles that allow a large class of bicategories to be equipped with new associative 1-cell compositions. Each of these so-called par-operations together with the original 1-cell composition as tensor constitutes the structure of a linear bicategory, except possibly for the existence of par-units. This allows the interpretation of most of the positive fragment of non-symmetric linear logic in these bicategories. Both construction principles utilize local pushouts and are parametrized, either by ``oplaxly pointed lax endo-functors'', or by modules on the identity functor. In the first case one always obtains linear structures satisfying the MIX-rule. In particular, a given bicategory may carry several linear structures with the same tensor.

Already for the category of sets with cartesian product as tensor several non-trivial par operations with unit exist that yield a linearly distributive category (that is, a linear bicategory with one object). By means of a matrix construction, one then also obtains several linear structures on the bicategory of spans with ordinary span-composition as tensor.