A cartesian multicategory, or a Lawvere theory can be defined using faithful cartesian clubs. The internal language of cartesian multicategories is that of classical algebraic expressions.
A cartesian multicategory is equivalently a colored Lawvere theory. The opposite of a cartesian multicategory is a cocartesian comulticategory.
References.
- Universal Algebra (Cohn, 1981)
- Sequential multicategories (Pisani)
- Clones from Comonoids (Krahmer, Mahaman)
- Operads, Clones, and Distributive Laws (Curien)
- Universal Algebra and Effectful Computation (Rajesh, 2023)
Tags: Type theory, multicategory, cartesian category.