nLab Freyd multicategory

Idea

A Freyd multicategory is to a multicategory as a Freyd category is to a monoidal category.

Definition

A Freyd multicategory consists of

• A multicategory $\mathcal{V}$ (usually cartesian)
• A premulticategory $\mathcal{C}$
• A functor $return : \mathcal{V}\to\mathcal{C}$ that is the identity on objects and preserves central morphisms.

Relation to Freyd categories

A Freyd multicategory that has all tensor products and units, in a usual multicategorical sense that are preserved by $return$, is equivalent to a Freyd category.

References

• Sam Staton and Paul Blain Levy, Universal properties of impure programing languages. POPL ‘13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 2013, doi