Lawvere theory

A Lawvere theory is a categorical formulation of an algebraic theory, introduced by William Lawvere in 1963. It consists of a category whose objects are natural numbers (representing arities of operations) and whose morphisms represent operations and their compositions. The key insight is that algebraic structures — groups, rings, modules, and more — can be described not by listing axioms in set-theoretic language but by specifying a category with finite products and a product-preserving functor into the category of sets.

This categorical reframing is not merely aesthetic. It reveals that algebraic theories are themselves objects of study: morphisms between Lawvere theories correspond to interpretations of one theory in another, and the category of Lawvere theories has rich structural properties that encode relationships between algebraic structures. A group homomorphism, a ring extension, a module restriction — all are instances of morphisms between Lawvere theories.

Lawvere theories are the categorical foundation of algebraic effects: the operations of an effect correspond to the morphisms of a Lawvere theory, and the equations of the effect correspond to the commutative diagrams that constrain those morphisms. The handler is a model of the theory in a different category — not sets, but computations.