(Re)Reading [Lawvere theories versus classical universal algebra](https://mathoverflow.net/questions/69086/lawvere-theories-versus-classical-universal-algebra), I was reminded of a question I have had for quite some time:



> 
> What is the best way to **present** Lawvere theories?
> 
> 
> 


By *present*, I mean give a (mathematical) description of the theory, by means of **syntax**. The Lawvere theory will be the denotation of that syntax.


I believe I understand the technical advantages that they provide over classical universal algebra (basically in terms of proving theorems over the models). My 'problem' is that I am trying to mechanize (parts of) mathematics. And to do that, one needs examples, which means constructing particular theories; more precisely, that means *writing something down, in finite terms* which denotes a theory.


Lawvere theories seems to largely abstract this away, unlike classical universal algebra, which gives quite explicit tools for writing things down explicitly. With Lawvere theories, I am reduced to figuring out how to present `a small category with finite products such that every object is isomorphic to a finite product of copies of a distinguished object x`. I have read quite a bit of CT, and I have yet to find a book which gives me tools as convenient as those of universal algebra for that purpose.



Presenting Lawvere theories?
Developing @AndrejBauer's suggestion to present them as single-sorted equational theories, you could write something like:



> 
> Let $\mathsf{Grp}$ denote the Lawvere theory with the following
>  presentation.
> 
> 
> Generators:
> 
> 
> 1. $c : 2 \rightarrow 1$
> 2. $e : 0 \rightarrow 1$
> 3. $i : 1 \rightarrow 1$
> 
> 
> Relations:
> 
> 
> 1. $c(c(x,y),z) \equiv (x,c(y,z))$
> 2. $c(e,x) \equiv x,\;\; c(x,e) \equiv x$
> 3. $c(i(x),x) \equiv e, \;\; c(x,i(x)) \equiv e$
> 
> 
> 


But, perhaps you were looking for something a little deeper.


