I would also recommend Equivariant homotopy and cohomology theory available off of Peter's website here: math.uchicago.edu/~may/BOOKS/alaska.pdf as well as the course notes of Stefan Schwede which I linked to above.

This works if $Y$ is a simply connected product of Eilenberg-Maclane spaces. Using this and the 'fibre lemmas' of Bousfield-Kan we see that it works more generally, by induction up the Postnikov tower, for $Y$ $p$-nilpotent. I was thinking of these fibre lemmas as requiring this sort of hands on data.

Mike: I was thinking of the EMSS and the UASS. These two spectral sequences are associated to the Tot filtration on a cosimplicial space, where you want the totalization to be identified with something else. For example, in the UASS we try to compute the homotopy groups of $Tot(Top(X,\mathbb{F}_p^{\bullet} X))$ where $\pi_*\mathbb{F}_p X\cong \tilde{H}_*(X,\mathbb{F}_p)$. Our interest in this spectral sequence lies in the cases where this Tot has the homotopy type of the space of maps from $X$ to the $p$-completion of $Y$.

@Tom, Giorgio: I answered the question under the presumption that the Giorgio is interested in the homotopical invariants of the spaces of maps in an $\infty$-category, including what happens to these invariants under the composition product.

Since there is now a paper on this, I would like to add that one can read about the universal characterization of higher K-theory that Tyler is discussing here: arxiv.org/abs/1001.2282

You could also use the A.1.1.6(b) if you know that all of your graded Hopf algebras are finite dimensional in each fixed degree (this is often the case in topology). This gives you the useful formula [ Ext^i_\Gamma( M^*, N)\cong Cotor^i(M^{**},N)\cong Cotor^i(M,N). ]

Now let's be specific. Let $C\rightarrow D\rightarrow E$ be a short exact sequence of $A//B$-comodules. Apply $-\square_{A//B} A$ to obtain a long exact sequence: [ 0\rightarrow C\square_{A//B} A\rightarrow D\square{A//B} A\rightarrow E\square_{A//B} A \rightarrow Cotor^1_{A//B}(C,A)\rightarrow Cotor^1_{A//B}(D,A)\rightarrow \cdots ] Since $A$ is injective the higher derived functors $Cotor^i_{A//B}(-,A)$ for $i>0$ are all zero. This shows that $-\square_{A//B} A$ is exact if $A$ is an injective $A//B$ comodule.

At this point I think everything is homological algebra: Fixing either one of the terms, the box product is left exact, at least over a field (or more generally if all of the tensor products used in the definition of the box product involve flat modules). Formally, this is because it is defined as a kernel of a map of modules. Since we have enough injectives we can compute the right derived functors of the box product using an injective resolution of one of the variables. If one of those variables is injective there are no higher derived functors.

Should we always expect that we can take strictly functorial replacements with respect to a class of objects adapted to $F$?