Poly-bicategories
by
Jürgen Koslowski
ITI, TU Braunschweig
Coauthors: Robin Cockett (University of Calgary), Robert Seely (McGill University, Montreal)

The notion of ``cut'' is of prime importance in logic, especially in the sequent calculus. Here we wish to make precise the slogan, often heard from categorical logicians, that ``cut is composition''. A 1-sided sequent calculus for typed formulae leads to ``multi-bicategories'', where the 2-cells have strings of 1-cells as domains and single 1-cells as codomains. Related structures currently enjoy much attention by people studying weak n-categories. Here we take a symmetric sequent calculus as our starting point. Consequently, both the domains and the codomains of our 2-cells can be strings of 1-cells. Interestingly, the notion of adjunction already makes sense at this level. Requiring in addition that the domains and codomains of these 2-cells are representable, one recovers the notion of ``linear bicategory'', originally designed to capture the essence of the multiplicative fragment of non-commutative linear logic without negation, while adjunctions turn into ``linear adjunctions''.

Since morphisms between linear bicategories, so-called ``linear functors'', are well-understood, one has a good starting point for defining ``poly-functors''. The situation was less satisfactory for morphisms between linear functors. ``Linear natural transformations'' proved unsatisfactory. In fact, the quest for a replacement, called ``linear modules'', was a strong motivation for studying poly-bicategories. Here rather elegant notions of ``poly-module'' and of ``poly-module transformation'' are available. Fixing two poly-bicategories, one may ask if the poly functors, poly-modules and their transformations themselves can be organized into a poly-bicategory. This is indeed the case, provided the domain poly-bicategory is representable and closed, in the sense that every 1-cell has both a left and a right adjoint. Previously, only the case of the domain being terminal and the codomain being representable and locally having reflexive equalizers and reflexive coequalizers was well-understood.

Date received: June 7, 2000

Copyright © 2000 by the author(s). The author(s) of this document and the organizers of the conference have granted their consent to include this abstract in Atlas Conferences Inc. Document # caeq-42.