Enriched monoidal action of enriched cat over arbitrary cat

Stream: Is there code for X?

[nrs]

image.png

Am trying to find something analogous to the above definition, would anyone know if something like it is in mathlib? I'm trying to see maybe if I can arrive to it through some variation of Action maybe

[Joël Riou]

If we ignore the enriched aspect, it seems like a monoidal functor from M to the category of endofunctors of C (which is monoidal for the composition of functors).

[nrs]

Thanks! I've been tinkering around with variations on that idea, it seems to me we might not be able to lift the concept up to enriched categories without the notion of C-module categories as in https://ncatlab.org/nlab/show/action+of+a+monoidal+category

[nrs]

seems like we would need enrichment is preserved for category of endofunctors otherwise, which seems to only be true for enriched ordinary categories
edit: might have been mistaken, working on a proper encoding