by J.R.B. Cockett, R.A.G. Seely
ABSTRACT
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.