Cone triangles satisfy the octahedral axiom

Let $\alpha :\mathrm{Cone}(f)⟶\mathrm{Cone}(gf),\beta :\mathrm{Cone}(gf)⟶\mathrm{Cone}(g)$ be the cone maps induced by the squares $(1_C,g)$ and $(f,1_E)$. In the coordinates of The three-cone calculation for a composite chain map, write an element of $\mathrm{Cone}(\alpha )$ as $(e,c,d,c^{\mathrm{\prime }})$ and define $r(e,c,d,c^{\mathrm{\prime }})=(e,d+f(c)),s(e,d)=(e,0,d,0)\mathrm{.}$ The displayed cone-differential calculation in that lemma shows that $r$ and $s$ are chain maps, $rs=1$, and $sr\simeq 1$: under its isomorphism $\mathrm{\Theta }$, $r$ is projection off the contractible $\mathrm{Cone}(1_{C[1]})$ summand and $s$ is inclusion of the $\mathrm{Cone}(g)$ summand.

If $j_{\alpha }$ and $q_{\alpha }$ are the canonical maps in the standard cone triangle of $\alpha$, then the formulas give $r{j}_{\alpha }=\beta ,q_{\alpha }s=j_f[1]\circ q_g\mathrm{.}$ Indeed, $j_{\alpha }(e,c)=(e,c,0,0)$ and $\beta (e,c)=(e,f(c))$, while $q_{\alpha }(e,c,d,c^{\mathrm{\prime }})=(d,c^{\mathrm{\prime }})$ and $j_f[1]q_g(e,d)=(d,0)$.

Thus the standard distinguished cone triangle of $\alpha$ is isomorphic in $K(\mathcal{A})$ to $\mathrm{Cone}(f)\stackrel{\alpha }{\to }\mathrm{Cone}(gf)\stackrel{\beta }{\to }\mathrm{Cone}(g)\stackrel{j_f[1]\circ q_g}{\to }\mathrm{Cone}(f)[1]\mathrm{.}$ The definitions of $\alpha$ and $\beta$ make the other two faces the required morphisms of cone triangles, and the displayed final map is precisely the typed fourth arrow in TR4.