Kerodon

In the proof that 1 implies 2, I do not believe that 4.6.4.18 is the correct reference (this refers to changing the category we're slicing, rather than the shape we're slicing over). The desired result seems like a straightforward consequence of Lemma 4.6.4.21 and Corollary 4.5.8.9, but I don't believe it's independently recorded anywhere.

Yep. Thanks!

The argument for (1) $\implies$ (2) is a bit confusing and redundant, where it says “is automatically left cofinal [...] and therefore left anodyne [...] and therefore left cofinal”. It is not immediately clear that $s$ is a categorical equivalence. Isn't there a direct argument that shows that sections of trivial Kan fibrations are left/right anodyne?

How about arguing as follows: Since $F$ is a trivial Kan fibration, it is a categorical equivalence (Proposition 4.5.3.11) and hence Proposition 7.2.1.21 implies that $s$ is left cofinal. As $s$ is a monomorphism, Proposition 7.2.1.3 shows that $s$ is left anodyne.

Yep. Thanks!