Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorcwil124
    • CommentTimeAug 14th 2018
    Hello, my name is Christian Williams; I am a new student of John Baez. We are working on a paper which uses enriched Lawvere theories, and we would like these to be multisorted for applications to computer science. However, all of the enriched theory literature we've seen is one-sorted. Does anyone know a definition of multisorted enriched theory - hopefully one which fulfils enriched monadicity? Thank you.
    • CommentRowNumber2.
    • CommentAuthorDmitri Pavlov
    • CommentTimeAug 14th 2018

    The definition in the nLab article enriched Lawvere theory works just fine for S-sorted theories if one takes A=Set^S. Further details can be found in the references there, e.g., the Nishizawa-Power article.

    • CommentRowNumber3.
    • CommentAuthorcwil124
    • CommentTimeAug 14th 2018
    Ah, of course. Thank you!
    • CommentRowNumber4.
    • CommentAuthorSam Staton
    • CommentTimeAug 15th 2018
    • (edited Aug 15th 2018)

    Not sure whether this is very explicit in the Nishizawa-Power article. I learnt it from Gil Hur’s thesis work with Marcelo Fiore, e.g. Term equational systems and logics, which treats the enriched case too. If I recall correctly, the idea is to put A=V SA=V^S. So in particular VAV\neq A.

    • CommentRowNumber5.
    • CommentAuthorcwil124
    • CommentTimeAug 25th 2018
    • (edited Aug 25th 2018)

    Thank you for your response; apologies for the late reply. I appreciate your help - although it is not clear to me how the “generalized theory” of TESL would translate to an enriched Lawvere theory (probably just that I don’t yet have the intuition to see it).

    We need both the structure of the enrichment and the simplicity of natural-number arities, as opposed to all of V; this is why we chose a definition which allows for parametrization of the theory by a monoidal subcategory of arities (Lucyshyn-Wright’s Enriched Algebraic Theories and Monads for a System of Arities).

    I should have explained why my question was answered, even though it was not apparent. This paper characterizes conditions for such “systems of arities” to give the V-monadicity. In our case, we simply want N_V arities, the subcategory of finite copowers of the unit object of V. I realized that finite powers of this category, (N_V)^n would still be a viable system of arities, so there is no problem.

    • CommentRowNumber6.
    • CommentAuthorSam Staton
    • CommentTimeAug 30th 2018

    Thanks. It sounds like you’re on a good track now.

    Incidentally, I’ve found arities other than N VN_V to be very useful for variable-binding (as in lambda calculus or predicate logic). But perhaps you don’t need this.