Algebraic theory

A finitary algebraic theory specifies sorts, finite-arity operations and equations between terms. Its internal models can be interpreted in any category with finite products. Finitely presented set-based models generate arbitrary models under filtered colimits and determine its classifying topos.

A finitely presented model is described by finitely many generators and finitely many equations. Model homomorphisms from it commute with filtered colimits. A small skeleton of these models is equivalent to the opposite of the finite-equation part of the algebraic syntactic category.