cartesian-multicategory

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.

theory-of-cartesian-multicategories

A cartesian multicategory is equivalently a colored Lawvere theory. The opposite of a cartesian multicategory is a cocartesian comulticategory.

References.

Tags: Type theory, multicategory, cartesian category.