Constructing linear bicategories

Abstract Linearly distributive categories were introduced to model the tensor/par fragment of linear logic, without resorting to the use of negation. Linear bicategories are the bicategorical version of linearly distributive categories. Essentially, a linear bicategory has two forms of composition, each determining the structure of a bicategory, and the two compositions are related by a linear distribution. After the initial paper on the subject, there was little further work as there seemed to be a lack of examples. The main goal of this paper is to demonstrate that there are in fact a great many examples, which are obtained by considering quantales and quantaloids and by extending familiar constructions from the (ordinary) bicategorical setting. It is standard in the field of monoidal topology that the category of quantale-valued relations is a bicategory. Here, we begin by showing that a quantale is Girard if and only if the corresponding bicategory is a Girard quantaloid, which is an example of a linear bicategory. The tropical and arctic semiring structures fit together into a Girard quantale, so this construction is likely to have multiple applications. More generally, we define LD -quantales, which are suplattices with two quantale structures related by a linear distribution, and their bicategorical analog, linear quantaloids. We show that Q- Rel is a linear quantaloid if and only if Q is a LD -quantale. We then consider several standard constructions from enriched bicategory theory and show that these lift to the linear quantaloid setting and produce new examples of linear bicategories. In particular, we consider linear Q -categories, matrices in Q, and linear monads in Q, where Q is a linear quantaloid. We develop non-locally posetal examples as well: Quant, the bicategory of quantales, modules, and module homomorphisms; and Qtld, the bicategory of quantaloids, modules, and module homomorphisms. These turn out to be cyclic * -autonomous bicategories, which are in essence a closed version of linear bicategories.