Kerodon

I believe the reference to Remark 7.3.1.10 is inaccurate in this proof: this Remark allows us to change out $F_0$ for something isomorphic, but we are really attempting to change $\delta$ for something isomorphic. While not directly stated, I believe this follows from 7.1.3.13: passing from $\delta^0 : K \to \mathcal{C}_0$ to a homotopy out of a cylinder object $K'$ of $K$ witnessing $\delta \circ H \simeq \delta^0$ and then applying 7.1.3.13 once more to pass back to a map out of $K$ "on the other side" of $K'$. For symmetry, however, perhaps this should be recorded more directly.

Yep. Thanks!

“we see that the natural map [...] is an equivalence of left fibrations over $\mathcal C^{0}$”

In the proof of (2), the roles of “$H\circ G\circ \delta^0$” and “$F\circ G$” seem to be confused, and similarly for the roles of “$\delta$” and “$F\circ G\circ H$”.

Yep. Thanks!