Lawvere theory
In category theory, a Lawvere theory is a category that can be considered a categorical counterpart of the notion of an equational theory.
Definition
Let be a skeleton of the category FinSet of finite sets and functions. Formally, a Lawvere theory consists of a small category L with finite products and a strict identity-on-objects functor preserving finite products.A model of a Lawvere theory in a category C with finite products is a finite-product preserving functor. A morphism of models where M and N are models of L is a natural transformation of functors.
Category of Lawvere theories
A map between Lawvere theories and is a finite-product preserving functor that commutes with I and I′. Such a map is commonly seen as an interpretation of in.Lawvere theories together with maps between them form the category Law.