Hyperderived functors are independent of the supplied resolution

Under DC apply the K-injective theorem to $T$ and $T^{\mathrm{\prime }}$. In the derived category the isomorphism $Q(e^{\mathrm{\prime }})Q(e{)}^{-1}:T\to T^{\mathrm{\prime }}$ is represented by a unique homotopy class of maps $a:T\to T^{\mathrm{\prime }}$. Its inverse is represented by $a^{\mathrm{\prime }}:T^{\mathrm{\prime }}\to T$. The bijection for maps into $T$ and $T^{\mathrm{\prime }}$ gives $a^{\mathrm{\prime }}a\simeq 1_T$, $a{a}^{\mathrm{\prime }}\simeq 1_{T^{\mathrm{\prime }}}$ and $ae\simeq e^{\mathrm{\prime }}$. In the supplied-data branch these are exactly the comparison maps and homotopies required in the statement.

Additivity of $F$ sends $a^{\mathrm{\prime }}a-1=dH+Hd$ to $F(a^{\mathrm{\prime }})F(a)-1=F(d)F(H)+F(H)F(d)$, and likewise for the other composite. Homotopic maps induce the same map on cohomology because their difference factors through a differential on cycles. Thus $H^n(F(a))$ and $H^n(F(a^{\mathrm{\prime }}))$ are inverse. Any other comparison over $K$ has the same class by the bijection in step 1.1 and hence gives the same cohomology map.

For $f:K\to L$ with total models $T_K,T_L$, represent $Q(e_L)Q(f)Q(e_K{)}^{-1}$ by a cochain map into $T_L$. The representative for a composite and the composite of representatives have identical images in the derived category; the no-roof bijection makes them homotopic. The same holds for identities and for changes of total models. Apply step 2.1 to obtain functorial maps and the natural comparison isomorphism. Zero maps and zero complexes obey these identities, and no uniform choice of representatives for all maps is needed to define their unique homotopy classes.