Lawvere theories and Jf-relative monads
In this paper we provide a detailed construction of an equivalence between the category of Lawvere theories and the category of relative monads on the obvious functor
J f : F → Sets
where F is the category with the set of objects N and morphisms being the functions between the standard finite sets of the corresponding cardinalities.
The methods of this paper are fully constructive and it should be formalizable in the Zermelo-Fraenkel theory without the axiom of choice and the excluded middle.
It is also easily formalizable in the UniMath.