Bar/Cobar Adjunction Between Modules and Comodules There is a pretty well known, and widely written about, adjunction between augmented algebras and coaugmented coalgebras given by taking the bar construction on algebras and the cobar construction on coalgebras. Sometimes, under certain circumstances (for instance, if your algebras are group-like loop spaces), this adjunction is an equivalence (e.g. the equivalence between group-like loop spaces and connected spaces)
My question is: when does this lift to categories of modules and comodules? In other words, given an augmented monoid $A$ (augmented, let's say, over $k$) and an $A$-module $X$, we can produce a $BA$-comodule $BX$ by taking a bar construction $Bar(X,A,k)$, which is effectively a kind of ``quotient" by the $A$-action. There should, I feel, be a right adjoint going from $BA$-comodules to $A$-modules, given by $Cobar(C,BA,k)$ ($C$ being a comodule). 
A good example is the case of $G$-spaces for a discrete group $G$. If we have a group action of $G$ on a space $X$, then we have an "action groupoid" which is basically a simplicial diagram whose bottom part looks like $G\times X\rightrightarrows X$ and whose colimit is $X//G$. In particular, we now also have a map $X//G\to BG=\ast//G$ endowing $X//G$ with a $BG$-comodule structure (using the diagonal map of $X//G$). On the other hand, given a map $Y\to BG$, we can perform a cobar construction whose effect is to take the fiber of $Y$ over the base point, which is, by elementary topological considerations, once again a $G$-space. 
I'm skipping a lot of the technicalities of describing this kind of structure, but I'm really interested in knowing how general this structure is. In particular, I'd really like to be able to go between modules and comodules, and I'd really like to do this in some homotopical-enough setting (e.g. quasicategories or simplicial model categories). Are there well known references for this? 
Note: There are TONS of references for this kind of thing for going between algebras and coalgebras. I'm very specifically interested in doing this for modules and comodules. 
 A: The topological picture is the following. Suppose $(X, x)$ is a based connected space. There's an equivalence of $\infty$-categories between spaces $Y \to X$ over $X$ ("$X$-comodules") and spaces with an action of $\Omega X$ ("$\Omega X$-modules"). The special case of $G$-spaces occurs when $X = BG$ as you say. You might call this, together with the equivalence between based connected spaces and grouplike $E_1$ spaces, "topological Koszul duality." 
One way of thinking about where this equivalence comes from is to notice that starting with a space $Y \to X$, taking the homotopy fiber at $x$ is the right adjoint of an adjunction between $\text{Space}_{/x} \cong \text{Space}$ and $\text{Space}_{/X}$, where the left adjoint is just given by composition with the inclusion of $x$ into $X$. This adjunction induces a monad on $\text{Space}$ whose functor part is $\Omega X \times (-)$, and you can hope that 1) an algebra over this monad is precisely a space with an action of $\Omega X$, and 2) this adjunction is monadic via Barr-Beck-Lurie.
Dually, starting with a space $F$ equipped with an action of $\Omega X$, taking the homotopy quotient is the left adjoint of an adjunction between $\Omega X\text{-Space}$ and $\text{Space}$, where the right adjoint equips a space with the trivial action. This adjunction induces a comonad on $\text{Space}$ whose functor part is $X \times (-)$, and you can hope that 1) a coalgebra over this comonad is precisely a space over $X$, and 2) this adjunction is comonadic via Barr-Beck-Lurie. 
Now you can hope for the same sorts of things to be true in a more algebraic setting. For example, let $f : R \to S$ be a morphism of algebras (e.g. ring spectra). To match up with the topological picture (which you can hope is reasonable if $R, S$ are $E_{\infty}$), $\text{Spec } R$ is $X$ and $\text{Spec } S$ is $x$. Taking the (derived) tensor product $(-) \otimes_R S$ is the left adjoint of an adjunction between $\text{Mod}(R)$ and $\text{Mod}(S)$, where the right adjoint is restriction. This adjunction induces a comonad on $\text{Mod}(S)$ whose functor part is $(-) \otimes_S (S \otimes_R S)$ (again matching up with the topological picture, $\text{Spec } S \otimes_R S$ is $\Omega X$), and you can hope that this adjunction is comonadic via Barr-Beck-Lurie. 
$S \otimes_R S$ is a priori only a coalgebra in $(S, S)$-bimodules, but if moreover $S$ is $E_{\infty}$, $R$ is an $S$-algebra, and $f$ is a morphism of $S$-algebras (so $f$ is an augmentation), then I believe the left and right actions should match and make $S \otimes_R S$ a coalgebra in $S$-modules. Beyond this I don't have details or references but my impression is that Barr-Beck-Lurie is your friend. 
