Lawvere theories and Jf-relative monads

TL;DR

This paper constructs a fully constructive equivalence between Lawvere theories and Jf-relative monads, applicable within ZF set theory without choice or excluded middle, and suitable for formalization in UniMath.

Contribution

It provides a detailed, constructive proof of the equivalence between Lawvere theories and Jf-relative monads, expanding the categorical understanding of algebraic theories.

Findings

Established a constructive equivalence between Lawvere theories and Jf-relative monads.

Methods are formalizable in ZF set theory without choice or excluded middle.

Results are compatible with formal proof systems like UniMath.

Abstract

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 $Jf:F\rightarrow Sets$ where $F$ is the category with the set of objects ${\bf 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.