LFCS Theory Seminar
Room 2511, JCMB, King's Buildings
4pm, Tuesday 4th November 1997

Title: Linear Bicategories

Speaker: Robin Cockett (Department of Computer Science, Calgary, Canada)

It is well-known that $*$-autonomous categories provide the categorical semantics for linear logic. It is also well-known that weakly distributive categories (or "linear categories") provide the semantics for the pure logic of the cut rule.

In the symmetric case the coherence problem for linear categories has been "solved" (in the sense that there is a decision problem for "proof equivalence"). In the non-symmetric case the problem is still open. However, the manipulation of these proofs is well-understood and, in many ways, is much simpler than in the symmetric case.

The main body of my talk will describe this system of manipulations. I shall use circuits which are (essentially) two-sided proof nets with additional structure to keep track of the units. There are (invertible) translations from circuits to proofs (and from circuits to categorical maps): there are some subtle points to be made about the "net condition" and the manipulation of the units.

If one wishes to understand the non-symmetric proof theory of cut, it is a small step to start working in a "bicategorical setting." When one works out what this setting actually is, one finds that it is a bicategory with TWO compatible 1-cell compositions -- a linear bicategory. The notion of (left and right) negation at this level of generality, rather nicely, turns out to be a notion of adjunction. If all 1-cells have left and right adjoints, in this sense, one obtains the generalization to the bicategorical level of a $*$-autonomous category.

This talk reports on joint work with Robert Seely and J\"urgen Koslowski.