Polycategory

14 Amazing Facts about Polycategories and their Fibrations

A quick compilation of facts about polycategories together with links to the appropriate litterature. Some are original work. Polycategories have been introduced by Szabo in 1975 in Polycategories. Polycategories are “categories with many-to-many morphisms”, i.e. polymaps have many inputs and many outputs. Polycategories correspond to Gentzen classical sequent calculus. Polycategories compose on one object. Composition of Polycategories is the cut rule. Representable polycategories, a.k.a. two-tensor polycategories, are linearly distributive categories, see Weakly distributive categories.

Classical linear logic via bifibrations of polycategories

Linearly distributives categories correspond to polycategories bifibred over the terminal polycategory.