@TimCampion I don't really remember to be honest! I'll need to think a little about it to be honest. There are a few places where they uses argument that involves cardinals and locally presentable categories (like prop 3.4 where they talk about accessible functors) as written this definitely is not constructively convincing, but it is also not clear the argument can't be made constructive...

Oh thanks! I hadn't noticed it. Johnstone's proof also looks a little simpler than mine.

@IngoBlechschmidt I might be answering to quickly, but I think the correct thing to say is "proper and surjective". Properness seems clear in each case, and unless I'm going to fast, "non empty" means surjective for proper maps.

You might want to clarify what kind of operads you are talking about. I'm somehow guessing you are talking about Batanin-Leinster globular operads, but that's really not so clear, you could also be referring to Trimble style definition of n-categories or even things like Dendroidal spaces/$\infty$-operads

The question doesn't make a lot of sense. This object "Coh(C)" you are talking about isn't well defined. Especially "Ordered by inclusion" doesn't mean anything: Coherence conditions aren't equations the composition operation need to satisfies, they are additional operation that need to exists. To some extend the first paragraph is roughly the idea of Maltsiniotis-Grothendieck definition of weak infinity categories, (if one remove the uniqueness of the morphism $S \to T$ that never holds) but they end up being very hard to relate to other more practical definition.

Yes, if you allow yourselve to take a Bousfield localization of the presheaves categories at some arrow this is much easier. I didn't mentioned that because it felt to me more different from what you asked (you are no longer working with a presheaves categories, but a localization of one), but if that suit your goal, great!

To be clear, the key point that you need for Z. M argument to work is that $Hom(K,Fun^{\otimes,L}(A,C) ) \simeq Fun^{\otimes,L}(A, Hom(K,C) )$, where $Hom(K,C)$ has the levelwise monoidal structure. This is definitely correct. But I'm not sure it is proved anywhere in the litterature,

Yes, that's what I'm alluding too in my second message: going all the way to a simplicially enriched category is possible, but not super easy or very explicit (as I say, look at the sort of thing you would have to do for the simplest case of sSet/X). Maybe it would be better to not try to do that and work with the simplicial category instead - but that's just an opinion.

To go from there to a simplicially enriched category, you should start by looking at the case of just sSet/X for X a simplicial sets. This is definitely possible, but the construction is not going to be very simple (nor very explicit). In the general case you want to do something similar applied to the simplicial set of object of your simplicial category but also take into account the morphism part... Given your motivation I feel like working with the simplicial category might be the best way to proceed.

Note that If "simplicial category" means categories objects in simplicial set ( so with both a simplicial set of objects and a simplicial set of morphism), then there is a simplicial category $\int_\Delta X$ such that you have a littleral equivalence of categories instead of just a Quillen equivalence.