Not signed in

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

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorcwil124
   • CommentTimeAug 14th 2018
   • PermaLink
   Author: cwil124
   Format: TextHello, 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.

   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.
2. • CommentRowNumber2.
   • CommentAuthorDmitri Pavlov
   • CommentTimeAug 14th 2018
   • PermaLink
   Author: Dmitri Pavlov
   Format: MarkdownItexThe 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.

   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.

3. • CommentRowNumber3.
   • CommentAuthorcwil124
   • CommentTimeAug 14th 2018
   • PermaLink
   Author: cwil124
   Format: TextAh, of course. Thank you!

   Ah, of course. Thank you!
4. • CommentRowNumber4.
   • CommentAuthorSam Staton
   • CommentTimeAug 15th 2018
   • (edited Aug 15th 2018)
   • PermaLink
   Author: Sam Staton
   Format: MarkdownItexNot 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](https://www.cl.cam.ac.uk/~mpf23/papers/Categories/TESL.pdf), which treats the enriched case too. If I recall correctly, the idea is to put $A=V^S$. So in particular $V\neq A$.

   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^S$. So in particular $V\neq A$.

5. • CommentRowNumber5.
   • CommentAuthorcwil124
   • CommentTimeAug 25th 2018
   • (edited Aug 25th 2018)
   • PermaLink
   Author: cwil124
   Format: MarkdownItexThank 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](https://arxiv.org/pdf/1511.02920.pdf)). 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.

   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.

6. • CommentRowNumber6.
   • CommentAuthorSam Staton
   • CommentTimeAug 30th 2018
   • PermaLink
   Author: Sam Staton
   Format: MarkdownItexThanks. It sounds like you're on a good track now. Incidentally, I've found arities other than $N_V$ to be very useful for variable-binding (as in lambda calculus or predicate logic). But perhaps you don't need this.

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

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