nLab second order algebraic theory

Contents

Context

Categorical algebra

Higher algebra

Contents

Idea

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.

Definition

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.

Multicategory

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.

Examples

References

A formalization in Agda:

Discussion via monads:

Last revised on March 4, 2024 at 22:48:32. See the history of this page for a list of all contributions to it.