Reference request: Derived category of category with sufficiently many injectives I'm studying derived categories and have encountered problem with references I have. Namely, proof of the following theorem:

Theorem: Let $\mathcal A$ be Abelian category and $\mathcal I$ full subcategory of injective objects. Then, if $\mathcal A$ has sufficiently many injectives, $K^+(\mathcal I)$ is equivalent to
  $D^+(\mathcal A)$.

particularly, I can prove that $K^+(\mathcal I)$ is full subcategory of $D^+(\mathcal A)$, but can't finish the proof of:

Proposition: Let $K^\bullet$ be a complex in $K^+(\mathcal A)$. Then there exists quasi-isomorphism $f\colon K^\bullet \to I^\bullet$ where
  $I^\bullet$ is in $K^+(\mathcal I)$.

By following Gelfand, Manin: Methods of Homological Algebra I can easily construct both $f$ and $I^\bullet$ but in Gelfand, Manin proof that $f$ is really quasi-isomorphism is done by using elements, which is something I'd like to avoid. 


*

*Can this proof be reformulated using only universal properties and not categorical elements?

*Is there a reference to similar proof (not just the fact) of proposition?

 A: Not sure if you like this more, but the following is an alternative:

Fact. If ${\mathscr A}$ has enough injectives, then for any  $X\in\text{Ch}^{\geq 0}({\mathscr A})$ there exists an exact sequence $0\to X\to I^0\to\ldots$ in the abelian category $\text{Ch}^{\geq 0}({\mathscr A})$, with chain complexes of injectives  $I^0, I^1,\ldots$.

Indeed, you can even assume that the induced sequences on cycles, boundaries and cohomologies are injective resolutions, too. Then the resolution goes under the name Cartan-Eilenberg resolution and can be constructed by constructing simultaneous injective resolutions (see Horseshoe Lemma) for the short exact sequences $0\to \text{Z}^n X\to X^n\to \text{B}^{n+1} X\to 0$ and $0\to\text{B}^n X\to \text{Z}^n X\to \text{H}^n X\to 0$ and glueing these together afterwards. Let me know if you need details.

Corollary. If ${\mathscr A}$ has enough injectives, then any $X\in \text{Ch}^{\geq 0}({\mathscr A})$ admits a quasi-isomorphism $X\to I$ to a complex of injectives.

Given the sequence $I^0\to I^1\to\ldots$ from the fact, view it as a first quadrant bicomplex and consider its totalization $\text{Tot}(I^{\bullet})$. Its components are finite coproducts of injectives, hence injective, and the canonical morphism $X\to\text{Tot}(I^{\bullet})$ coming from the map $X\to I^0$ is a quasi-isomorphism: Its cone is the totalization of the bicomplex associated to the augmented resolution $0\to X\to I^0\to I^1\to\ldots$, which is acylic as the totalization of a first-quadrant bicomplex with acylic columns. The proof of this last statement can in turn be reduced to proving that the totalization of a short exact sequences of complexes is always acyclic, which follows from the long exact cohomology sequence associated to a short exact sequence of chain complexes.
It is also done this way in Weibel, An Introduction to Homological Algebra, Theorem 10.4.8. A very thorough treatment of derived categories is also contained in Kashiwara-Shapira, Categories and Sheaves, but it might be a tough and too general read to begin with - in particular, they consider unbounded complexes, which are considerably more difficult to deal with.
