nLab second order algebraic theory



Categorical algebra

Higher algebra



A second-order algebraic theory is a generalization of the notion of Lawvere theory to describe algebraic structures with variable binding.

While single-sorted Lawvere theories are cartesian monoidal categories generated from a single object, single-sorted second-order algebraic theories are cartesian monoidal categories generated from a single exponentiable object.


A second-order algebraic theory is a category TT with cartesian products and an exponentiable object oo such that every object of TT is isomorphic to a finite cartesian product of objects of the form o noo^n \Rightarrow o.

A model of a theory TT is given by a functor M:TSetM : T \to \Set that preserves cartesian products (not necessarily exponentials). On objects, such a functor must give for each o noo^n \Rightarrow o a set M(n)M(n) and the functoriality determines a first-order Lawvere theory/cartesian multicategory structure on MM. So models of second order algebraic theories are first order algebraic theories with additional structure.


Just as Lawvere theories can be identified with cartesian multicategories, there should be a similar correspondence between second-order theories and some notion of second-order cartesian multicategory.



A formalization in Agda by Marcelo Fiore and Dmitrij Szamozvancev: webpage with an accompanying talk.

Last revised on January 5, 2023 at 17:31:41. See the history of this page for a list of all contributions to it.