Lawvere theory

In , a Lawvere theory (named after American mathematician William Lawvere) is a that can be considered a categorical counterpart of the notion of an equational theory. Let be a of the category FinSet of finite sets and functions. Formally, a Lawvere theory consists of a L with (strictly associative) finite s and a strict identity-on-objects preserving finite products. A model of a Lawvere theory in a category C with finite products is a finite-product preserving functor M : L → C. A morphism of models h : M → N where M and N are models of L is a natural transformation of functors. A map between Lawvere theories (L, I) and (L′, I′) is a finite-product preserving functor that commutes with I and I′. Such a map is commonly seen as an interpretation of (L, I) in (L′, I′). Lawvere theories together with maps between them form the category Law. Variations include multisorted (or multityped) Lawvere theory, infinitary Lawvere theory, and finite-product theory.