@JonathanBeardsley i'd guess you can prove this by embedding O-algebras into the category of left O-modules in symmetric sequences, and then using the usual eilenberg--watts theorem for associative algebras. would that recover the version of the theorem you're after?

actually, this reminds me of a more general question i've been wondering: is there a generalization of "symmetric sequences" such that associative algebras in it recover arbitrary (colored $\infty$-)operads? (maybe this is worked out in one of @RuneHaugseng's recent papers?)

@AaronMazel-Gee There are analogues of symmetric sequences and the composition product for any fixed set/space of objects, and the current version of my paper describes infinity-versions of these. But you can also combine these into a double category such that the category of associative algebras in it is the category of operads with varying objects (more precisely the "algebraic" category, where FFES morphisms have not been inverted).

1-categorically I believe this is due to Gambino-Joyal and Fiore-Gambino-Hyland-Winskel. I now know how to define an infinity-version of this, hopefully it won't take too long to finish revising the paper accordingly...

@user170039 For what it's worth, I always found the description as "conceptual inverses" more trouble than benefit. I'd recommend just ignoring it, and concentrate on looking at many examples of adjoint functors to get an intuitive feeling for them

@DenisNardin @user170039 I second this. I've never quite grokked the idea of adjoints being "almost inverses" or something, though that was the way they were first explained to me. Understanding them in terms of free/forgetful pairs is what really helped solidify them in my mind.

Does anyone know, if I have a cocartesian fibration of ∞-categories p:C→D, and an ∞-category K, do I get a new cocartesian fibration Fun(K,C)→Fun(K,D)?

@JonathanBeardsley Yes. The lifting condition for cocartesian arrows adjoins it over without many problems (so an arrow in Fun(K,C) is cocartesian iff when evaluated at all points it is cocartesian)

You're going to need some of the pushout-product properties for marked anodyne morphisms at the beginning of chapter 4 of HTT, ofc

@DenisNardin oh ok good. I think that maybe then the monoidal structure on T_C described at the end of HA 7.3.1 is actually kind of understandable then