Bifibrations of polycategories and classical linear logic

Résumé

Ceci est un article présenté à la conférence MFPS 2020. Il a aussi donné lieu à une présentation principale à la conférence ACT 2020. Cette page contient une (future) version étendue de l’article, ainsi que la version publiée dans le compte-rendu de MFPS et l’abstract étendu proposé à ACT. La version étendue est en cours d’écriture. The main goal of this article is to expose and relate different ways of interpreting the multiplicative fragment of classical linear logic in polycategories. Polycategories are known to give rise to models of classical linear logic in so-called representable *-polycategories, which ask for the existence of various polymaps satisfying the different universal properties needed to define tensor, par, and negation. We begin by explaining how these different universal properties can all be seen as instances of a single notion of universality of a polymap parametrised by an input or output object, which also generalises the classical notion of universal multimaps in a multicategory. We then proceed to introduce a definition of in-cartesian and out-cartesian polymap relative to a refinement system (= strict functor) of polycategoriesm in such a way that universal polymaps can be understood as a special case. In particular, we obtain that a polycategory is a representable *-polycategory if and only if it is bifibred over the terminal polycategory. Finally, we present a Grothendieck correspondence between bifibrations of polycategories and pseudofunctors into MAdj, the 2-polycategory of multivariable adjunctions. When restricted to bifibrations over the terminal polycategory we get back the correspondence between *-autonomous categories and Frobenius pseudomonoids in MAdj that was recently observed by Shulman.