internalization and categorical algebra
algebra object (associative, Lie, …)
internal category ($\to$ more)
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 $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.
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.