Kerodon

I think one needs to use Corollary 4.4.5.9 instead of Proposition 4.4.5.8 here.

Also, though it is not a big deal, I think (unless I got confused in the indices) that in the current proof when using Proposition 4.4.5.8 one has a lifting of $\Delta^1 \times \{1\} \sqcup_{\{0\}\times \{1\}} \{0\} \times \Delta^1$ instead of $\Delta^1 \times \{1\} \sqcup_{\{1\}\times \{1\}} \{1\} \times \Delta^1$ as in the formulation of Proposition 4.4.5.8 (or Corollary 4.4.5.9).

I think you should use Proposition 5.1.6.6 instead of Proposition 5.1.6.7 when trying to prove the fact that $F$ being an equivalence of $\infty$-categories implies condition (2) of the proposition.