The concept of initial functor provides a categorical and operational semantics for equational reasoning with diagrams. So far, we have explored this thesis in the simplest possible setting, that of a bare category, or, in logical terms, of an equational theory with unary function symbols. This is rather restrictive. The standard setting for equational reasoning was historically the starting point of both categorical logic (Lawvere 1963) and e-graphs (Nelson 1980; Nelson and Oppen 1980): a category with finite products, viewed as an algebraic theory.