For 𝔼ₖ-monoidal things you can do the same, you just can't use discrete categories like Δ^{op} and Fin_* to index the structure.

I don't think this stuff is really written down anywhere, but you can get at some of it relatively quickly from existing definitions, at least for the case of monoidal and symmetric monoidal ∞-categories. These should be functors out of N(Δ^{op}) and N(Fin_*) respectively satisfying a Segal condition which can be written down in any ∞-cosmos, since it's purely in terms of products and equivalences.

Right, I think one issue here is that for an ∞-topos, ||f||₀ is not necessarily a set at all, which makes the idea of "injective" a bit complicated. But maybe that's handled by correctly "internalizing" the language.

Great! Does he show that, e.g., being (-1)-truncated in the HoTT sense agrees with being (-1)-truncated in the HTT sense?

Sure, sure, I know that it's supposed to be that, I just don't see it in, e.g. the HoTT book.

I see, that sounds correct then. But this would need to happen in an arbitrary $\infty$-topos though. Does homotopy type theory work in the same way there?

@NaïmFavier I don't know. What's an embedding in homotopy type theory?

Another possibly useful keyword is "descent cohomology." Ultimately these are all special cases of monadic descent.