5.1 Lawvere’s functorial semantics

A one-sorted Lawvere theory may be described as a small category \(\mathbb L\) with finite products whose objects are the finite powers

of a distinguished object \(X\). A morphism \(X^n\to X^m\) is an abstract \(m\)-tuple of \(n\)-ary operations. Composition performs substitution, and equality of morphisms records equational laws.

Let \(\mathcal C\) be a category with finite products. A model of \(\mathbb L\) in \(\mathcal C\) is a finite-product-preserving functor

Natural transformations between such functors are homomorphisms of models. We write

for the resulting model category.

For the theory of monoids, for example, \(\mathbb L\) contains abstract maps

and equations expressing associativity and the two unit laws. A product- preserving model in \(\mathsf{Set}\) chooses a set \(M(X)\), a multiplication, and a unit satisfying those equations. A model in another Cartesian category interprets the same formal operations using that category’s products.

The theory and its models must not be conflated. A theory is not one favored implementation, dataset, or neural parameterization. It is the invariant compositional specification shared by a category of realizations. This makes Lawvere semantics a natural target for persistent creativity: the constructed concept can travel between models.

Many-sorted theories replace the single generator \(X\) by a family of sorts. This is usually the appropriate form for scientific domains: particles, fields, observations, interventions, and experimental contexts need not have the same type.