internalization and categorical algebra
algebra object (associative, Lie, …)
symmetric monoidal (∞,1)-category of spectra
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 with cartesian products and an exponentiable object such that every object of is isomorphic to a finite cartesian product of objects of the form .
A model of a theory is given by a functor that preserves cartesian products (not necessarily exponentials). On objects, such a functor must give for each a set and the functoriality determines a first-order Lawvere theory/cartesian multicategory structure on . 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.
The untyped lambda calculus can be described as a second-order algebraic theory, and simply typed lambda calculus as a multi-sorted second-order theory.
The calculus of derivatives or more generally partial derivatives.
Marcelo Fiore and Chung-Kil Hur, Term Equational Systems and Logics, MFPS XXIV, doi
Marcelo Fiore and Ola Mahmoud, Second-order Algebraic Theories, MFCS 2010, arxiv
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.