Kerodon

Proof. Assume first that condition $(1)$ is satisfied and let $e: C \rightarrow D$ be an edge of the simplicial set $\operatorname{\mathcal{C}}$, which we identify with a morphism $\Delta ^1 \rightarrow \operatorname{\mathcal{C}}$. Applying Proposition 6.2.3.4 to the projection map $\Delta ^1 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow \Delta ^1$, we deduce that the covariant transport functor $e_{!}: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D}$ is right adjoint to the contravariant transport functor $e^{\ast } \operatorname{\mathcal{E}}_{D} \rightarrow \operatorname{\mathcal{E}}_{C}$, which proves $(2)$.

We now show that $(2)$ implies $(1)$. By virtue of Proposition 5.1.4.7, we may assume without loss of generality that $\operatorname{\mathcal{C}}= \Delta ^ n$ is a standard simplex. For $0 \leq i \leq n$, let $\operatorname{\mathcal{E}}_{i}$ denote the fiber $\{ i\} \times _{\Delta ^ n} \operatorname{\mathcal{E}}$, which we regard as a full subcategory of $\operatorname{\mathcal{E}}$. We wish to show that, for every pair of integers $0 \leq j < k \leq n$ and every object $Z \in \operatorname{\mathcal{E}}_{k}$, there exists an object $Y \in \operatorname{\mathcal{E}}_{j}$ and a $U$-cartesian morphism $g: Y \rightarrow Z$ in $\operatorname{\mathcal{E}}$. Proposition 6.2.3.4 implies that the projection map $\operatorname{N}_{\bullet }( \{ j < k \} ) \times _{\Delta ^ n} \operatorname{\mathcal{E}}\rightarrow \operatorname{N}_{\bullet }( \{ j < k \} )$ is a cartesian fibration, so we can choose an object $Y \in \operatorname{\mathcal{E}}_{j}$ and a morphism $g: Y \rightarrow Z$ which is locally $U$-cartesian. We will complete the proof by showing that $g$ is $U$-cartesian. To prove this, we must show that for each integer $0 \leq i \leq j$ and each object $W \in \operatorname{\mathcal{E}}_{i}$, composition with the homotopy class $[g]$ induces an isomorphism $\operatorname{Hom}_{\operatorname{\mathcal{E}}}( W, Y) \xrightarrow { [g] \circ } \operatorname{Hom}_{\operatorname{\mathcal{E}}}(W,Z)$ in the homotopy category of Kan complexes $\mathrm{h} \mathit{\operatorname{Kan}}$ (see Corollary 5.1.2.3). Since $U$ is a cocartesian fibration, we can choose a $U$-cocartesian morphism $f: W \rightarrow X$, where $X$ belongs to $\operatorname{\mathcal{E}}_{j}$. We conclude by observing that there is a commutative diagram

in the homotopy category $\mathrm{h} \mathit{\operatorname{Kan}}$, where the upper horizontal map is an isomorphism by virtue of our assumption that $g$ is locally $U$-cartesian, and the vertical maps are isomorphisms by virtue of our assumption that $f$ is $U$-cocartesian (Corollary 5.1.2.3). $\square$