Kerodon

Proof. We will show that $(1) \Leftrightarrow (2)$; the proof of the equivalence $(1) \Leftrightarrow (3)$ is similar. The implication $(1) \Rightarrow (2)$ is immediate from Proposition 5.2.2.19. For the converse, assume that $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ is a left fibration of simplicial sets and that, for every edge $f: C \rightarrow D$ of $\operatorname{\mathcal{C}}$, the covariant transport morphism $[f_{!}]$ is an isomorphism in the homotopy category $\mathrm{h} \mathit{\operatorname{Kan}}$. We wish to show that $U$ is a Kan fibration. By virtue of Example 4.2.1.5, it will suffice to show that $U$ is a right fibration. By Proposition 4.2.6.1, this is equivalent to the assertion that the induced map

is a trivial Kan fibration. Note that our assumption that $U$ is a left fibration guarantees that $\theta $ is also a left fibration (Proposition 4.2.5.1).

Fix an edge $f: C \rightarrow D$ of the simplicial set $\operatorname{\mathcal{C}}$ and let $\operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{E}})_{f}$ denote the fiber $\operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{E}}) \times _{ \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}) } \{ f\} $. Then evaluation at the vertex $1 \in \Delta ^1$ induces a morphism $\theta _{f}: \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{E}})_{f} \rightarrow \operatorname{\mathcal{E}}_{D}$. Note that $\theta _{f}$ is a pullback of $\theta $, and is therefore also a left fibration. Since $\operatorname{\mathcal{E}}_{D}$ is a Kan complex (Corollary 4.4.2.3), Corollary 4.4.3.8 guarantees that $\theta _{f}$ is a Kan fibration (so $\operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}})_{f}$ is also a Kan complex). Evaluation at the vertex $0 \in \Delta ^1$ induces another morphism of simplicial sets $u: \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{E}})_{f} \rightarrow \operatorname{\mathcal{E}}_{C}$. Since $U$ is a left fibration, the morphism $u$ is a trivial Kan fibration. By construction, the homotopy class $[f_{!}]$ can be represented by the morphism of Kan complexes given by the composition

where $v$ is a section of $u$ (and therefore a homotopy equivalence). Consequently, our assumption that $[f_{!}]$ is an isomorphism in $\mathrm{h} \mathit{\operatorname{Kan}}$ guarantees that $\theta _{f}$ is a homotopy equivalence of Kan complexes (Remark 3.1.6.16). Applying Proposition 3.2.7.2, we deduce that the fibers of $\theta _{f}$ are contractible Kan complexes. Since every fiber of $\theta $ can also be viewed as a fiber of $\theta _{f}$ for some edge $f$ of the simplicial set $\operatorname{\mathcal{C}}$, it follows that the fibers of $\theta $ are also contractible Kan complexes. Invoking Proposition 4.4.2.14, we conclude that $\theta $ is a trivial Kan fibration, as desired. $\square$