查看文章

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 coherence structure of the exponentials and the additives.