Let be a skeleton of the category FinSet of finite sets and functions. Formally, a Lawvere theory consists of a small category L with (strictly associative) 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 M : L → C. A morphism of models h : M → N where M and N are models of L is a natural transformation of functors.
Category of Lawvere theories
A map between Lawvere theories (L,I) and (L′,I′) is a finite-product preserving functor which 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.
- Hyland, Martin; Power, John (2007), The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads (PDF)
- Lawvere, William F. (1964), Functorial Semantics of Algebraic Theories (PhD Thesis)