A Linear Category of Polynomial Functors (extensional part)Article
Authors: Hyvernat Pierre
NULL
Hyvernat Pierre
We construct a symmetric monoidal closed category of polynomial endofunctors
(as objects) and simulation cells (as morphisms). This structure is defined
using universal properties without reference to representing polynomial
diagrams and is reminiscent of Day's convolution on presheaves. We then make
this category into a model for intuitionistic linear logic by defining an
additive and exponential structure.