Linearly distributive functors

by J.R.B. Cockett, R.A.G. Seely

This paper introduces a notion of "linear functor" between linearly distributive categories that is general enough to account for common structure in linear logic, such as the exponentials (!, ?), and the additives (product, coproduct), and yet when interpreted in the doctrine of *-autonomous categories, gives the familiar notion of monoidal functor. We show that there is a bi-adjunction between the 2-categories of linearly distributive categories and linear functors, and of *-autonomous categories and monoidal functors, given by the construction of the "nucleus" of a linearly distributive category. We develop a calculus of proof nets for linear functors, and show how linearity accounts for the essential structure of the exponentials and the additives.
This paper was first presented at a conference held in Montreal in May 1997, in honour of Michael Barr's 60th birthday, and is dedicated to him in celebration of this occasion.