Derived functors are well defined relative to supplied resolution data

Assume the Axiom of Dependent Choice. Derived functors are well defined here in a specific seven-part sense, and each part is now on the page rather than being collapsed into one slogan:

1. supplied resolutions give the object assignments;
2. comparison maps or extensions exist for each morphism (A morphism has a comparison lift between the supplied projective resolutions, A morphism has a comparison extension between the supplied injective resolutions);
3. the induced map is independent of the chosen lift (The induced homology map is independent of the chosen comparison lift, The induced cohomology map is independent of the chosen injective comparison extension);
4. those maps preserve identities (Left derived functors relative to supplied data are additive functors, Right derived functors relative to supplied data are additive functors);
5. those maps preserve composition (Left derived functors relative to supplied data are additive functors, Right derived functors relative to supplied data are additive functors);
6. changing the supplied data yields a natural isomorphism (Two supplied projective resolution data define naturally isomorphic left derived functors, Two supplied injective resolution data define naturally isomorphic right derived functors); and
7. those change-of-data isomorphisms satisfy identity and cocycle laws (Change-of-projective-resolution isomorphisms satisfy identity and cocycle laws, Change-of-injective-resolution isomorphisms satisfy identity and cocycle laws).

What this remark does not claim is a global theorem saying that enough projectives or enough injectives canonically choose one resolution for every object. The present conclusions are relative to displayed supplied data, and two different data are compared by natural isomorphism rather than by an unstated class-sized choice.