Kerodon

Proof. For each object $X \in \operatorname{\mathcal{E}}_{C}$, let $f_{!}(X)$ denote the target of the morphism $\widetilde{f}_{X}$. Let $u: X \rightarrow Y$ be a morphism in the category $\operatorname{\mathcal{E}}_{C}$. Invoking our assumption that $\widetilde{f}_{X}$ is $U$-cocartesian, we see that there is a unique morphism $f_{!}(u): f_{!}(X) \rightarrow f_{!}(Y)$ for which the diagram

is commutative (in the category $\operatorname{\mathcal{E}}$). Note that if $v: Y \rightarrow Z$ is another morphism in the category $\operatorname{\mathcal{E}}_{C}$, then the calculation

shows that $f_{!}( v \circ u) = f_{!}(v) \circ f_{!}(u)$. Similarly, for each object $X \in \operatorname{\mathcal{E}}_{C}$, the calculation $\widetilde{f}_{X} \circ \operatorname{id}_{ f_{!}(X) } = \widetilde{f}_{X} = \operatorname{id}_{X} \circ \widetilde{f}_{X}$ shows that $f_{!}( \operatorname{id}_{X} ) = \operatorname{id}_{ f_{!}(X)}$. We can therefore regard $f_{!}$ as a functor from the category $\operatorname{\mathcal{E}}_{C}$ to $\operatorname{\mathcal{E}}_{D}$, and the commutativity of (5.12) guarantees that the construction $X \mapsto \widetilde{f}_{X}$ determines a natural transformation from the inclusion $\operatorname{\mathcal{E}}_{C} \hookrightarrow \operatorname{\mathcal{E}}$ to the functor $f_{!}$. $\square$

Proof. By virtue of Remark 5.2.2.11 (and Theorem 5.2.1.1), we can replace $U$ by the induced map $\operatorname{Fun}(K, \operatorname{\mathcal{E}}) \rightarrow \operatorname{Fun}(K,\operatorname{\mathcal{C}})$ and thereby reduce to the case where $K = \Delta ^0$. In this case, assertion $(1)$ follows immediately from our assumption that $U$ is a cocartesian fibration, and assertion $(2)$ follows from Remark 5.1.3.8. $\square$

Proof of Proposition 5.2.2.8. Apply Lemma 5.2.2.13 in the special case where $K$ is the $\infty $-category $\operatorname{\mathcal{E}}_{C}$, $H_0: K \rightarrow \operatorname{\mathcal{E}}$ is the inclusion map, and $\overline{H}$ is the composite map $\Delta ^1 \times K \rightarrow \Delta ^1 \xrightarrow {f} \operatorname{\mathcal{C}}$ (see Example 5.2.2.12). $\square$

Proof. Choose morphisms of Kan complexes $f_{!}: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D}$ and $f^{\ast }: \operatorname{\mathcal{E}}_{D} \rightarrow \operatorname{\mathcal{E}}_{C}$ representing the homotopy classes $[f_{!}]$ and $[ f^{\ast } ]$, respectively. We will show that $f^{\ast } \circ f_{!}$ is homotopic to the identity morphism $\operatorname{id}_{\operatorname{\mathcal{E}}_{C} }$; a similar argument will show that $f_{!} \circ f^{\ast }$ is homotopic to $\operatorname{id}_{ \operatorname{\mathcal{E}}_{D} }$. Let $\operatorname{\mathcal{D}}$ denote the fiber product $\operatorname{Fun}( \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{E}}) \times _{ \operatorname{Fun}( \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{C}}) } \operatorname{\mathcal{C}}$, and let $\pi : \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ be the projection map onto the second factor. Since $U$ is a Kan fibration, it follows from Corollary 3.1.3.2 that $\pi $ is also a Kan fibration. Let $\widetilde{f}: \Delta ^{1} \times \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}$ be a morphism witnessing $f_{!}$ as given by covariant transport along $f$. Then $\widetilde{f}$ determines an edge $h$ of the simplicial set $\operatorname{\mathcal{D}}$ satisfying $\pi ( h ) = f$. Let $\widetilde{f}': \Delta ^1 \times \operatorname{\mathcal{E}}_{D} \rightarrow \operatorname{\mathcal{E}}$ be a morphism which witnesses $f^{\ast }$ as given by contravariant transport along $f$, so that the composite morphism

determines an edge $h'$ of the simplicial set $\operatorname{\mathcal{D}}$ satisfying $\pi (h') = f$. The edges $h$ and $h'$ have the same target (the vertex of $\operatorname{\mathcal{D}}$ corresponding to the morphism $f_{!}$). Invoking our assumption that $\pi $ is a Kan fibration, we deduce that there exists a $2$-simplex $\sigma $ of $\operatorname{\mathcal{D}}$ satisfying $d^{2}_0(\sigma ) = h'$, $d^{2}_1(\sigma ) = h$, and $\pi (\sigma ) = s^{1}_0(f)$; we can represent $\sigma $ as a diagram

We now observe that the edge $v = d^{2}_2(\sigma )$ of $\operatorname{\mathcal{D}}$ can be identified with a map of simplicial sets $V: \Delta ^1 \times \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{C}$ which is a homotopy from $\operatorname{id}_{\operatorname{\mathcal{E}}_{C}} = V|_{ \{ 0\} \times \operatorname{\mathcal{E}}_{C} }$ to $f^{\ast } \circ f_! = V|_{ \{ 1\} \times \operatorname{\mathcal{E}}_{C} }$. $\square$

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$

Proof. Combine Theorem 5.2.2.20 with Corollary 4.2.3.20. $\square$