Linearly distributive functors (Q1818630)

From MaRDI portal
scientific article
Language Label Description Also known as
English
Linearly distributive functors
scientific article

    Statements

    Linearly distributive functors (English)
    0 references
    0 references
    0 references
    10 October 2000
    0 references
    A linearly distributive category (called a weakly distributive category in earlier work by the same authors; the present name was suggested by \textit{M.~Barr,} to whom the paper is dedicated) is a category with two monoidal structures \(\otimes\) and \(\oplus\), together with a pair of natural transformations making each tensor strong with respect to the other. Such categories arise naturally in the construction of categorical models for the multiplicative fragment of linear logic, the two tensors being used to model the `tensor' and `par' of the latter. In the present paper, the authors argue that the appropriate notion of morphism between such categories is not a single functor but a pair of functors, each monoidal with respect to one of the tensors, and equipped with a number of natural transformations satisfying coherence conditions which are too complicated to repeat here. As evidence in support of this, they show that the exponentials and the additive connectives of linear logic can be regarded as examples of such `linearly distributive functors'; they also show that linearly distributive functors between {\(^*\)-autonomous} categories are essentially the same thing as (dual pairs of) monoidal functors, and in fact the \(2\)-category of \(^*\)-autonomous categories is coreflective in that of linearly distributive categories.
    0 references
    distributive category
    0 references
    multiplicative fragment of linear logic
    0 references
    coherence conditions
    0 references
    \(^*\)-autonomous categories
    0 references

    Identifiers

    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references