2016/01/09 by Vladimir Voevodsky, Voevodsky, Vladimir
Mathematics · #18C10 #18C99 #Category Theory (math.CT) #FOS: Mathematics #math.CT #msc:18C10 #msc:18C99
paper · pdf · doi:10.48550/arxiv.1601.02158
arxiv created 2016/01/09 · arxiv updated 2016/01/12
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→ 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.