nLab LNL polycategory

Idea

A linear-non-linear polycategory or simply LNL polycategory is a generalization of a symmetric polycategory to include “non-linear” objects in the same way that linear-non-linear logic generalizes symmetric multicategories. Just as linear-non-linear logic provides a setting in which the exponential comonad ! in intuitionistic linear logic can be decomposed into an adjunction, LNL polycategories provide a setting in which the exponential comonad ! and the monad ? in classical linear logic can each be decomposed into adjunctions.

In addition to the study of classical linear-logic, LNL polycategories can be used as a unified setting in which to study multicategory and polycategory-like structures as “LNL doctrines”.

Doctrines

See the original paper for a definition of LNL doctrine.

The following is an incomplete list of structures that can be defined as LNL doctrines:

• cartesian multicategories
• symmetric multicategories
• symmetric polycategories?
• linear-non-linear logic
• skew-multicategories?
• call-by-push-value
• Freyd multicategories
• adjunctions
• models of classical linear logic

References

Introduced in

• Michael Shulman, LNL polycategories and doctrines of linear logic, arxiv