Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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.
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$.
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.
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.
1 to 6 of 6