In Lurie's `Higher Algebra`, construction 4.4.2.7 presents a Bar construction in the setting of $\infty$-categories. The construction in 4.4.2.7 takes as input an $\mathcal{O}$-monoidal $\infty$-category $\mathcal{C}^\otimes \to \mathcal{O}^\otimes$ and a suitable pair of bi-modules in $\mathcal{C}^\otimes$ and gives a simplicial object in $\mathcal{C}$.


In the proof of the Barr-Beck theorem, this construction is used in lemma 4.7.3.13, where Lurie uses a simplicial object $\mathrm{Bar}\_T(T, M)\_\bullet$ with values in $\mathrm{LMod}\_T(\mathcal{C})$. All of the Bar constructions previously used in Higher-algebra are only defined as taking value in the underlying $\infty$-category.


Looking at the construction, it *feels* obvious that the $\mathcal{C}$-valued simplicial object $\mathrm{Bar}\_T(T, M)\_\bullet$ should lift to a $\mathrm{LMod}\_T(\mathcal{C})$-valued simplicial object, since the bar construction essentially comes from some functor $\mathbf{\Delta}^{op} \to \mathrm{Tens}\_{\succ}$ in which the objects should have structure of modules and the maps should be linear, but I am unable to formally write down a lift along the forgetful functor $\mathrm{LMod}\_T(\mathcal{C}) \to \mathcal{C}$ from this definition.


Is there a way to see how to to produce such a lift? More generally, given an $(A,B)$-bimodule $M$ in $\mathcal{C}$ and a $(B,C)$-bimodule $N$ in $\mathcal{C}$, the simplicial object $\mathrm{Bar}(M,N)\_\bullet$ should take value in the $\infty$-category of $(A,C)$-bimodules, rather than in $\mathcal{C}$. This extension to the bimodule case is also used without proof in HA 5.2.2.6.


[This question](https://mathoverflow.net/questions/290035/bar-construction-and-the-infty-categorical-barr-beck-theorem) asks about the definition of $\mathrm{Bar}\_T(T, M)\_\bullet$ but seems to be only about it as a $\mathcal{C}$-valued object (that's what the answer in the commens gives), and do not address the issue of making it $\mathrm{LMod}\_T(\mathcal{C})$-valued.



Making the ($\infty$-categorical) Bar construction valued in (bi)-modules
In Lurie's construction of the relative tensor product, there's an $\infty$-operad $\mathrm{Tens}\_{[2]}^{\otimes}$ whose algebras in a monoidal $\infty$-category $\mathcal{C}$ are given by 3 associative algebras (say A,B,C) and two bimodules (say M for (A,B) and N for (B,C)). The simplicial bar construction is obtained by first restricting an algebra for this $\infty$-operad along a certain functor $\Delta^{\mathrm{op}} \to \mathrm{Tens}\_{[2]}^{\otimes}$, so that the composite to $\mathcal{C}^\otimes$ takes $[n]$ to $(M, B,\ldots,B,N)$ (with $n$ copies of $B$), and then taking the cocartesian pushforward to the fibre $\mathcal{C}$ over $\langle 1 \rangle$ (to get the simplicial diagram in $\mathcal{C}$ that takes $[n]$ to $M \otimes B^{\otimes n} \otimes N$).


To extend this to a simplicial diagram of bimodules, you want to first define a functor $\mathrm{Tens}\_{[1]}^{\otimes} \times \Delta^{\mathrm{op}} \to \mathrm{Tens}\_{[2]}^{\otimes}$ (where $\mathrm{Tens}\_{[1]}^{\otimes}$ is just the operad for bimodules). If we call the 3 objects of the bimodule operad $a,b$ (the two algebras) and $m$, then the composite with our algebra in $\mathcal{C}^\otimes$ should take $((a,\ldots,a,m,b,\ldots,b), [n])$ (with $i$ $a$'s and $j$ $b$'s) to
$(A,\ldots,A,M,B,\ldots,B,N,C,\ldots,C)$ with $i$ $A$'s, $n$ $B$'s and $j$ $C$'s.
Next you again take a cocartesian pushforward, so that you get a diagram in $\mathcal{C}^\otimes$ of the same shape, but which now takes this object in the source to $(A,\ldots,A,M \otimes B^{\otimes n} \otimes N,C,\ldots,C)$. This new diagram is then adjoint to a simplicial object in algebras for the bimodule operad, and indeed factors through the fibre of $(A,C)$-bimodules.


