arXiv · 1601.02158
Lawvere theories and Jf-relative monads
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.
Explore related subjects
Keep this discovery
Vladimir Voevodsky. 2016-01-09. Lawvere theories and Jf-relative monads. https://arxiv.org/abs/1601.02158
Cite the original work for its findings. Save a collection to share your selection of sources.