# nLab second order algebraic theory

Contents

### Context

#### Categorical algebra

internalization and categorical algebra

universal algebra

categorical semantics

#### Higher algebra

higher algebra

universal 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 $T$ with cartesian products and an exponentiable object $o$ such that every object of $T$ is isomorphic to a finite cartesian product of objects of the form $o^n \Rightarrow o$.

A model of a theory $T$ is given by a functor $M : T \to \Set$ that preserves cartesian products (not necessarily exponentials). On objects, such a functor must give for each $o^n \Rightarrow o$ a set $M(n)$ and the functoriality determines a first-order Lawvere theory/cartesian multicategory structure on $M$. 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.

## References

A formalization in Agda: