Kerodon

Proof. The implication $(1) \Rightarrow (2)$ follows from Corollary 5.1.2.6 (and does not require the assumption that $q$ is a locally cartesian fibration), and the implication $(2) \Rightarrow (3)$ is immediate. We will complete the proof by showing that $(3) \Rightarrow (1)$. Using Remarks 5.1.1.12 and 5.1.3.5, we can reduce to the case where $\operatorname{\mathcal{D}}= \Delta ^ n$ is a simplex. By virtue of Corollary 5.1.2.3, it will suffice to show that for each object $X \in \operatorname{\mathcal{C}}$ satisfying $q(X) \leq q(Y)$, the composition map

of Notation 4.6.9.15 is an isomorphism in the homotopy category $\mathrm{h} \mathit{\operatorname{Kan}}$. Since $q$ is a locally cartesian fibration, we can choose a locally $q$-cartesian morphism $f: X \rightarrow Y$ satisfying $q(W) = q(X)$. Using the fact that $\operatorname{\mathcal{C}}$ is an $\infty $-category, we can choose a $2$-simplex $\sigma $ of $\operatorname{\mathcal{C}}$ satisfying $d^{2}_0(\sigma ) = g$ and $d^{2}_2(\sigma ) = f$. Set $h= d^{2}_1(\sigma )$, so that we have a commutative diagram

in the $\infty $-category $\operatorname{\mathcal{C}}$. If assumption $(3)$ is satisfied, then $h$ is also a locally $q$-cartesian morphism of $\operatorname{\mathcal{C}}$. Invoking Proposition 4.6.9.12, we conclude that the diagram

commutes (in the homotopy category $\mathrm{h} \mathit{\operatorname{Kan}}$). Since $f$ and $h$ are locally $q$-cartesian, the horizontal and left diagonal map in this diagram are isomorphisms (in the homotopy category $\mathrm{h} \mathit{\operatorname{Kan}}$), so the right diagonal map is an isomorphism as well. $\square$