Николай Иваныч (nivanych) wrote in category_theory,
Николай Иваныч

Lawvere theories and Jf-relative monads

[by oskar_808]
Lawvere theories and Jf-relative monads
Vladimir Voevodsky
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.
  • Post a new comment


    default userpic

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.