Quasi isomorphisms admit the roof calculus in the homotopy category

Cohomology is defined on homotopy classes. Identities, composites, and shifts preserve quasi-isomorphisms, and homotopy equivalences are quasi-isomorphisms. These assertions include the zero complex.

For $s:X\to X^{\mathrm{\prime }}$ a quasi-isomorphism and $f:X\to Y$, take the triangle $X\stackrel{f}{\to }Y\to C\stackrel{h}{\to }X[1]$. Complete $s[1]h:C\to X^{\mathrm{\prime }}[1]$ to a triangle $X^{\mathrm{\prime }}\stackrel{f^{\mathrm{\prime }}}{\to }{Y}^{\mathrm{\prime }}\to C\stackrel{s[1]h}{\to }{X}^{\mathrm{\prime }}[1]$. Rotated TR3 gives $t:Y\to Y^{\mathrm{\prime }}$ with $tf=f^{\mathrm{\prime }}s$ and a morphism of triangles whose other components are $s,1_C$. The two long cohomology sequences show $H^n(t)$ invertible: exactness identifies its kernel and cokernel with zero by the adjacent isomorphisms. Thus $t$ is a quasi-isomorphism, giving the outgoing Ore square. Reversing arrows and rotating gives the incoming Ore square.

If $a=f-g:X\to Y$ satisfies $at=0$ for a quasi-isomorphism $t:Z\to X$, the triangle $Z\stackrel{t}{\to }X\stackrel{d}{\to }C\to Z[1]$ has acyclic $C$. Hom exactness gives $a=i\circ d$ for some $i:C\to Y$. Complete $i$ to $C\stackrel{i}{\to }Y\stackrel{j}{\to }W\to C[1]$. Cohomology exactness makes $j$ a quasi-isomorphism and $ja=jid=0$. Reversing arrows gives the converse cancellation direction.

All constructions used only finitely many shifts, sums and cones. These preserve each of termwise upper, lower, and two-sided boundedness (with possibly changed finite bounds). Thus both Ore and cancellation constructions stay in each bounded homotopy category and establish exactly the multiplicative-system axioms there.