Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$

5.3.7 Application: Path Fibrations

Recall that every morphism of Kan complexes $f: X \rightarrow Y$ admits a canonical factorization

\[ X \xrightarrow {\delta } P(f) \xrightarrow {\pi } Y, \]

where $\delta $ is a homotopy equivalence and $\pi $ is the path fibration

\[ P(f) = X \times _{ \operatorname{Fun}( \{ 0\} , Y)} \operatorname{Fun}( \Delta ^1, Y) \rightarrow \operatorname{Fun}( \{ 1\} , Y) \simeq Y \]

of Example 3.1.7.10. Note that the simplicial set $P(f) = X \operatorname{\vec{\times }}_{Y} Y$ is an example of an oriented fiber product (Definition 4.6.4.1), which is defined for any morphism of simplicial sets $f: X \rightarrow Y$. Beware that if $X$ and $Y$ are not Kan complexes, then $\delta $ need not be a homotopy equivalence and $\pi $ need not be a Kan fibration. However, if $X = \operatorname{\mathcal{C}}$ and $Y = \operatorname{\mathcal{D}}$ are $\infty $-categories, then we have the following weaker statements:

$(a)$

The functor $\delta : \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$ is fully faithful, and its essential image is the homotopy fiber product $\operatorname{\mathcal{C}}\times ^{\mathrm{h}}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$ of Construction 4.5.2.1 (Corollary 4.5.2.22).

$(b)$

The functor $\pi : \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{D}}$ is a cocartesian fibration of $\infty $-categories (Corollary 5.3.7.3).

Moreover, the oriented fiber product $\operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$ can be characterized by a universal mapping property: roughly speaking, the diagonal map $\delta $ exhibits the cocartesian fibration $\pi $ as freely generated by the functor $f$ (Theorem 5.3.7.7).

Our starting point is the following observation:

Lemma 5.3.7.1. Let $U: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be an inner fibration of simplicial sets, let $e$ be an edge of $\operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}})$, and let

\[ V: \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}) = \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{C}} \]

denote the morphism induced by $U$. Let $\operatorname{ev}_0, \operatorname{ev}_1: \operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{C}}$ be the evaluation maps. If $\operatorname{ev}_0(e)$ is $U$-cocartesian, then $e$ is $V$-cocartesian. If $\operatorname{ev}_1(e)$ is $U$-cartesian, then $e$ is $V$-cartesian.

Proof. Assume that $\operatorname{ev}_0(e)$ is $U$-cocartesian; we will show that $e$ is $V$-cocartesian (the second assertion follows by a similar argument). Let $n \geq 2$; we wish to show that every lifting problem

5.34
\begin{equation} \begin{gathered}\label{equation:cocartesian-in-oriented-fiber-product-ultimate} \xymatrix@R =50pt@C=50pt{ \Lambda ^{n}_{0} \ar [r]^-{ \sigma _0 } \ar [r] \ar [d] & \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}) \ar [d]^-{ V } \\ \Delta ^{n} \ar [r]^-{ \overline{\sigma } } \ar@ {-->}[ur]^{\sigma } & \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{C}}} \end{gathered} \end{equation}

admits a solution, provided that the composite map

\[ \Delta ^1 \simeq \operatorname{N}_{\bullet }( \{ 0 < 1 \} ) \hookrightarrow \Lambda ^{n}_0 \xrightarrow { \tau _0 } \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}) \]

coincides with $e$. Let $X(0)$ denote the simplicial subset of $\Delta ^1 \times \Delta ^ n$ given by the union of $\operatorname{\partial \Delta }^1 \times \Delta ^ n$ with $\Delta ^1 \times \Lambda ^{n}_0$. Unwinding the definitions, we can rewrite (5.34) as a lifting problem

\[ \xymatrix@R =50pt@C=50pt{ X(0) \ar [r]^-{ \tau _0 } \ar [r] \ar [d] & \operatorname{\mathcal{C}}\ar [d]^-{ U } \\ \Delta ^1 \times \Delta ^{n} \ar [r]^-{ \overline{\tau } } \ar@ {-->}[ur]^{\tau } & \operatorname{\mathcal{D}}. } \]

Choose a filtration

\[ X(0) \subset X(1) \subset X(2) \subset \cdots \subset X(t) = \Delta ^{1} \times \Delta ^{n} \]

satisfying the requirements of Lemma 4.4.4.7. We will complete the proof by showing that, for each $s \leq t$, the morphism $\tau _0$ admits an extension $\tau _ s: X(s) \rightarrow \operatorname{\mathcal{C}}$ satisfying $U \circ \tau _{s} = \overline{\tau }|_{ X(s) }$. The proof proceeds by induction on $s$, the case $s = 0$ being vacuous. Let us therefore assume that $0 < s \leq t$ and that $\tau _0$ has already been extended to a morphism of simplicial sets $\tau _{s-1}: X(s-1) \rightarrow \operatorname{\mathcal{C}}$. By construction, we have a pushout diagram of simplicial sets

\[ \xymatrix@R =50pt@C=50pt{ \Lambda ^{q}_{p} \ar [r]^-{\varphi _0} \ar [d] & X(s-1) \ar [d] \\ \Delta ^{q} \ar [r]^{\varphi } & X(s) } \]

for some $q \geq 2$ and $0 \leq p < q$. Consequently, to prove the existence of $\tau _ s$, it will suffice to show that $\tau _{s-1} \circ \varphi _0$ can be extended to a $q$-simplex of $\operatorname{\mathcal{C}}$ lying over the simplex $\overline{\tau } \circ \varphi : \Delta ^ q \rightarrow \operatorname{\mathcal{D}}$. For $p \neq 0$, the existence of this extension follows from our assumption that $U$ is an inner fibration. To handle the case $p= 0$, we observe that the morphism $\varphi $ carries the initial edge of $\Delta ^{q}$ to the edge $(0,0) \rightarrow (0,1)$ of $\Delta ^{1} \times \Delta ^ n$, so that $\tau _{s-1} \circ \varphi _0$ carries the initial edge of $\Delta ^ q$ to the edge $\operatorname{ev}_0(e)$ of $\operatorname{\mathcal{C}}$, which is $U$-cocartesian by assumption. $\square$

Proposition 5.3.7.2. Suppose we are given a commutative diagram of simplicial sets

\[ \xymatrix { \operatorname{\mathcal{C}}_0 \ar [d]^{U_0} \ar [r]^{F_0} & \operatorname{\mathcal{C}}\ar [d]^{U} & \operatorname{\mathcal{C}}_1 \ar [l]_{F_1} \ar [d]_{U_1} \\ \operatorname{\mathcal{D}}_0 \ar [r]^{G_0} & \operatorname{\mathcal{D}}& \operatorname{\mathcal{D}}_1 \ar [l]_{G_1} } \]

where $U_0$, $U_1$, and $U$ are cocartesian fibrations, and $F_0$ carries $U_0$-cocartesian edges of $\operatorname{\mathcal{C}}_0$ to $U$-cocartesian edges of $\operatorname{\mathcal{C}}$. Then the induced map

\[ V: \operatorname{\mathcal{C}}_0 \operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_1 \rightarrow \operatorname{\mathcal{D}}_0 \operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}_1 \]

is a cocartesian fibration of simplicial sets. Moreover, an edge $e$ of $\operatorname{\mathcal{C}}_0 \operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_1$ is $V$-cocartesian if and only if it satisfies the following condition:

$(\ast )$

Let $e_0$ and $e_1$ denote the images of $e$ in $\operatorname{\mathcal{C}}_0$ and $\operatorname{\mathcal{C}}_1$, respectively. Then $e_0$ is $U_0$-cocartesian and $e_1$ is $U_1$-cocartesian.

Proof. Let us say that an edge $e$ of $\operatorname{\mathcal{C}}_0 \operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_1$ is special if it satisfies condition $(\ast )$. We first show that if $e$ is a special edge of $\operatorname{\mathcal{C}}_0 \operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_1$, then $e$ is $V$-cocartesian. Let $e_0$ and $e_1$ denote the images of $e$ in $\operatorname{\mathcal{C}}_0$ and $\operatorname{\mathcal{C}}_1$, respectively. Note that $V$ factors as a composition

\[ \operatorname{\mathcal{C}}_0 \operatorname{\vec{\times }}_{ \operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_1 \xrightarrow {V'} \operatorname{\mathcal{C}}_0 \operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{C}}_1 \xrightarrow {V''} \operatorname{\mathcal{D}}_0 \operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}_1. \]

Here $V'$ is a pullback of the projection map $\overline{V}': \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}) = \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{C}}$. Since $F( e_0 )$ is $U$-cocartesian, Lemma 5.3.7.1 implies that $e$ is $V'$-cocartesian. Moreover, $V''$ is a pullback of the product map $(U_0 \times U_1): \operatorname{\mathcal{C}}_0 \times \operatorname{\mathcal{C}}_1 \rightarrow \operatorname{\mathcal{D}}_0 \times \operatorname{\mathcal{D}}_1$. By assumption, $e_0$ is $U_0$-cocartesian and $e_1$ is $U_1$-cocartesian. It follows that $V'(e)$ is $V''$-cocartesian, so that $e$ is $V$-cocartesian by virtue of Remark 5.1.1.6.

Since $U_0$, $U_1$, and $U$ are inner fibrations, the morphisms $\overline{V}'$ and $(U_0 \times U_1)$ are also inner fibrations (see Proposition 4.1.4.1). It follows that $V'$ and $V''$ are inner fibrations (Remark 4.1.1.5), so that $V$ is an inner fibration (Remark 4.1.1.8). To show that $V$ is a cocartesian fibration, it will suffice to show that if $C$ is an object of $\operatorname{\mathcal{C}}_0 \operatorname{\vec{\times }}_{ \operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_1$ and $\overline{e}: V(C) \rightarrow \overline{C}'$ is an edge of $\operatorname{\mathcal{D}}_0 \operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}_1$, then there exists a special edge $e: C \rightarrow C'$ satisfying $V(e) = \overline{e}$. Let us identify $C$ with a triple $(C_0, C_1, u)$ where $C_0$ is a vertex of $\operatorname{\mathcal{C}}_0$, $C_1$ is a vertex of $\operatorname{\mathcal{C}}_1$, and $u: F_0(C_0) \rightarrow F_1(C_1)$ is an edge of $\operatorname{\mathcal{C}}$. Similarly, we can identify $\overline{C}'$ with a triple $(\overline{C}'_0, \overline{C}'_1, \overline{u}' )$ where $\overline{C}_0$ is a vertex of $\operatorname{\mathcal{D}}_0$, $\overline{C}'_1$ is a vertex of $\operatorname{\mathcal{D}}_1$, and $\overline{u}': G_0( \overline{C}'_0 ) \rightarrow G_1( \overline{C}'_1 )$ is an edge of $\operatorname{\mathcal{D}}$. The edge $\overline{e}$ has images $\overline{e}_{0}: U_0(C_0) \rightarrow \overline{C}'_0$ an $\overline{e}_{1}: U_1(C_1) \rightarrow \overline{C}'_{1}$ in $\operatorname{\mathcal{D}}_0$ and $\operatorname{\mathcal{D}}_1$-respectively. Since $U_0$ is a cocartesian fibration, we can lift $\overline{e}_0$ to a $U_0$-cocartesian edge $e_0: C_0 \rightarrow C'_0$ of $\operatorname{\mathcal{C}}_0$. Similarly, we can lift $\overline{e}_1$ to a $U_1$-cocartesian edge $e_1: C_1 \rightarrow C'_1$ of $\operatorname{\mathcal{C}}_1$. The edge $\overline{e}$ also determines a map $\Delta ^1 \times \Delta ^1 \rightarrow \operatorname{\mathcal{D}}$, which we depict informally in the diagram

\[ \xymatrix { (G_0 \circ U_0)( C_0 ) \ar [r]^-{U(u)} \ar [d]^{ G_0(\overline{e}_0) } & (G_1 \circ U_1)(C_1) \ar [d]^{ G_1(\overline{e}_1) } \\ G_0(\overline{C}'_0) \ar [r]^{\overline{u}'} & G_1( \overline{C}'_{1} ). } \]

Using our assumption that $U$ is an inner fibration, we can lift the upper right triangle to a $2$-simplex $\sigma $:

\[ \xymatrix { F_0(C_0) \ar [r]^{u} \ar@ {-->}[dr]^{v} & F_1(C_1) \ar [d]^{ F_1( e_1 ) } \\ & F_1( C'_1 ) } \]

of the simplicial set $\operatorname{\mathcal{C}}$. Using the fact that $F_0( e_0 )$ is $U$-cocartesian, we can lift the lower triangle to a $2$-simplex $\tau $

\[ \xymatrix { F_0(C_0) \ar [d]^{ F_0(e_0 ) } \ar [dr]^{v} & \\ F_0( C'_0 ) \ar@ {-->}[r]^{w} & F_1( C'_1 ) } \]

of $\operatorname{\mathcal{C}}$. Setting $C' = (C'_0, C'_1, w) \in \operatorname{\mathcal{C}}_0 \operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_1$, we observe that the tuple $( e_0, e_1, \sigma , \tau )$ determines a special edge $e: C \rightarrow C'$ satisfying $V(e) = \overline{e}$.

We now complete the proof by showing that every $V$-cocartesian edge $f: C \rightarrow C''$ in $\operatorname{\mathcal{C}}_0 \operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_1$ is special. Using the preceding argument, we can choose a special edge $e: C \rightarrow C'$ satisfying $V(e) = V(f)$. Set $\overline{C}' = V( C' ) = V(C'' )$. Applying Remark 5.1.3.8, we deduce that there is a $2$-simplex $\rho :$

\[ \xymatrix { & C' \ar [dr]^{s} & \\ C \ar [ur]^{ e } \ar [rr]^{f} & & C'' } \]

of the simplicial set $\operatorname{\mathcal{C}}_0 \operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_1$, where $s$ is an isomorphism in the $\infty $-category $V^{-1}( \{ \overline{C}' \} )$. Applying Example 5.1.3.6, we deduce that the images of $s$ in $\operatorname{\mathcal{C}}_0$ is $U_0$-cocartesian, and the image of $s$ in $\operatorname{\mathcal{C}}_1$ is $U_1$-cocartesian. Since the collections of $U_0$-cocartesian and $U_1$-cocartesian edges are closed under composition (Corollary 5.1.2.4), we conclude that $f$ is also special. $\square$

Corollary 5.3.7.3. Let $F_0: \operatorname{\mathcal{C}}_0 \rightarrow \operatorname{\mathcal{C}}$ and $F_1: \operatorname{\mathcal{C}}_1 \rightarrow \operatorname{\mathcal{C}}$ be morphisms of simplicial sets and let

\[ \operatorname{\mathcal{C}}_0 \xleftarrow { \pi } \operatorname{\mathcal{C}}_0 \operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_1 \xrightarrow {\pi '} \operatorname{\mathcal{C}}_1 \]

denote the projection maps. Then:

$(1)$

If $\operatorname{\mathcal{C}}_0$ and $\operatorname{\mathcal{C}}$ are $\infty $-categories, then $\pi '$ is a cocartesian fibration of simplicial sets. Moreover, an edge $e$ of $\operatorname{\mathcal{C}}_0 \operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_1$ is $\pi '$-cocartesian if and only if $\pi (e)$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{C}}_0$.

$(2)$

If $\operatorname{\mathcal{C}}_1$ and $\operatorname{\mathcal{C}}$ are $\infty $-categories, then $\pi $ is a cartesian fibration of simplicial sets. Moreover, an edge $e$ of $\operatorname{\mathcal{C}}_0 \operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_1$ is $\pi $-cartesian if and only if $\pi '(e)$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{C}}_1$.

Proof. Assertion $(1)$ follows by applying Proposition 5.3.7.2 in the special case $\operatorname{\mathcal{D}}_0 = \operatorname{\mathcal{D}}= \Delta ^0$ and $\operatorname{\mathcal{D}}_1 = \operatorname{\mathcal{C}}_1$. Assertion $(2)$ follows by a similar argument. $\square$

Corollary 5.3.7.4. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category and let $K$ be a simplicial set. Then:

$(1)$

The restriction map $U: \operatorname{Fun}(K^{\triangleleft }, \operatorname{\mathcal{C}}) \rightarrow \operatorname{Fun}(K, \operatorname{\mathcal{C}})$ is a cocartesian fibration. Moreover, a morphism $e$ of $\operatorname{Fun}(K^{\triangleleft }, \operatorname{\mathcal{C}})$ is $U$-cocartesian if and only if it carries the cone point ${\bf 0} \in K^{\triangleleft }$ to an isomorphism in $\operatorname{\mathcal{C}}$.

$(2)$

The restriction map $V: \operatorname{Fun}(K^{\triangleright }, \operatorname{\mathcal{C}}) \rightarrow \operatorname{Fun}(K, \operatorname{\mathcal{C}})$ is a cartesian fibration. Moreover, a morphism $e$ of $\operatorname{Fun}(K^{\triangleright }, \operatorname{\mathcal{C}})$ is $U$-cartesian if and only if it carries the cone point ${\bf 1} \in K^{\triangleright }$ to an isomorphism in $\operatorname{\mathcal{C}}$.

Proof. We will prove $(1)$; the proof of $(2)$ is similar. Let $\Delta ^0 \diamond K$ denote the blunt join of Notation 4.5.8.3, and let $c: \Delta ^0 \diamond K \rightarrow \Delta ^{0} \star K = K^{\triangleleft }$ be the categorical equivalence of Theorem 4.5.8.8. We have a commutative diagram of $\infty $-categories

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{Fun}( K^{\triangleleft }, \operatorname{\mathcal{C}}) \ar [dr]^{U} \ar [rr]^-{ \circ c} & & \operatorname{Fun}( \Delta ^0 \diamond K, \operatorname{\mathcal{C}}) \ar [dl]^{U'} \\ & \operatorname{Fun}(K, \operatorname{\mathcal{C}}) & } \]

where the horizontal map is an equivalence of $\infty $-categories (Proposition 4.5.3.8) and the vertical maps are isofibrations (Corollary 4.4.5.3). Unwinding the definitions, we can identify $\operatorname{Fun}( \Delta ^0 \diamond K, \operatorname{\mathcal{C}})$ with the oriented fiber product $\operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \operatorname{Fun}(K, \operatorname{\mathcal{C}})$. Under this identification, the functor $U'$ is given by projection onto the second factor, and is therefore a cocartesian fibration (Corollaryt 5.3.7.3). Applying Corollary 5.1.6.2, we deduce that $U$ is also a cocartesian fibration. Moreover, a morphism $e$ of $\operatorname{Fun}(K^{\triangleleft }, \operatorname{\mathcal{C}})$ is $U$-cocartesian if and only if its image in $\operatorname{Fun}( \Delta ^0 \diamond K, \operatorname{\mathcal{C}})$ is $U'$-cocartesian (Proposition 5.1.6.6). Using the criterion of Corollary 5.3.7.3, we see that this is equivalent to the requirement that $e$ carries the cone point ${\bf 0} \in K^{\triangleleft }$ to an isomorphism in $\operatorname{\mathcal{C}}$. $\square$

Example 5.3.7.5. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category. Applying Corollary 5.3.7.3 in the case where both $F$ and $G$ are the identity functor $\operatorname{id}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}$, we deduce that the evaluation functor

\[ \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}) \rightarrow \operatorname{Fun}( \{ 0\} , \operatorname{\mathcal{C}}) \simeq \operatorname{\mathcal{C}} \]

is a cartesian fibration of $\infty $-categories, and the evaluation functor

\[ \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}) \rightarrow \operatorname{Fun}( \{ 1\} , \operatorname{\mathcal{C}}) \simeq \operatorname{\mathcal{C}} \]

is a cocartesian fibration of $\infty $-categories.

Let $\operatorname{\mathcal{C}}$ be an $\infty $-category and let $U: \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{C}}$ be the cocartesian fibration given by evaluation at the vertex $1 \in \Delta ^1$. For every vertex $X \in \operatorname{\mathcal{C}}$, we can identify the fiber $U^{-1} \{ X\} $ with the oriented fiber product $\operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \{ X\} $, which is equivalent to the slice $\infty $-category $\operatorname{\mathcal{C}}_{/X}$ (Corollary 4.6.4.18). Under this equivalence, covariant transport for $U$ is given by the composition law on $\operatorname{\mathcal{C}}$:

Proposition 5.3.7.6. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category and let $f: X \rightarrow Y$ be a morphism of $\operatorname{\mathcal{C}}$. Then the diagram of $\infty $-categories

5.35
\begin{equation} \begin{gathered}\label{equation:covariant-transport-path-fibrations} \xymatrix { \operatorname{\mathcal{C}}_{/X} \ar [r]^{ f \circ } \ar [d]^{ \delta _{/X} }_{\sim } & \operatorname{\mathcal{C}}_{/Y} \ar [d]^{\delta _{/Y} }_{\sim } \\ \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{\mathcal{C}}} \{ X\} \ar [r]^{ f_{!} } & \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \{ Y \} } \end{gathered} \end{equation}

commutes up to isomorphism. Here the vertical maps are the pinch inclusion equivalences of Corollary 4.6.4.18, the upper horizontal map is the composition functor of Example 4.3.6.15, and the lower horizontal map is given by covariant transport for the evaluation functor $U: \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{C}}$.

Proof. Consider the restriction maps

\[ \operatorname{\mathcal{C}}_{/X} \xleftarrow {e_0} \operatorname{\mathcal{C}}_{/f} \xrightarrow {e_1} \operatorname{\mathcal{C}}_{/Y}. \]

Since the inclusion map $\{ 0\} \hookrightarrow \Delta ^1$ is left anodyne, $e_0$ is a trivial Kan fibration (Corollary 4.3.6.14). By construction, the composition functor of Example 4.3.6.15 is given by the composition $(e_{1} \circ e_0^{-1}): \operatorname{\mathcal{C}}_{/X} \rightarrow \operatorname{\mathcal{C}}_{/Y}$, where $e_0^{-1}$ is a homotopy inverse to $e_0$. The covariant transport functor $f_{!}$ admits a similar description. Let $\operatorname{\mathcal{E}}$ denote the oriented fiber product $\operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}) \operatorname{\vec{\times }}_{ \operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}}) } \{ f \} $, whose objects are given by commutative diagrams

\[ \xymatrix { X' \ar [r]^{f'} \ar [d] & Y' \ar [d] \\ X \ar [r] & Y } \]

in the $\infty $-category $\operatorname{\mathcal{C}}$, and let $\operatorname{\mathcal{E}}^{0}$ denote the full subcategory of $\operatorname{\mathcal{E}}$ spanned by those diagrams where $f'$ is an isomorphism. Evaluation at the vertices $0,1 \in \Delta ^1$ then determines forgetful functors $e'_0: \operatorname{\mathcal{E}}^{0} \rightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{\mathcal{C}}} \{ X\} $ and $e'_1: \operatorname{\mathcal{E}}^{0} \rightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \{ Y\} $. It follows from Proposition 5.3.7.2 that we can identify $\operatorname{\mathcal{E}}^{0}$ with the $\infty $-category of $U$-cocartesian lifts of the morphism $f$. It follows that $e'_0$ is a trivial Kan fibration, and that the functor $f_{!}$ is given by the composition

\[ (e'_0 \circ e'^{-1}_{0}): \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \{ X\} \rightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \{ Y\} , \]

where $e'^{-1}_{0}$ is a homotopy inverse of $e'_0$. Consequently, to show that the diagram (5.35) commutes up to isomorphism, it will suffice to show that there is a commutative diagram of simplicial sets

\[ \xymatrix { \operatorname{\mathcal{C}}_{/X} \ar [d]^{ \delta _{/X} }_{\sim } & \operatorname{\mathcal{C}}_{/f} \ar [d] \ar [l]_{e_0} \ar [r]^{ e_1} & \operatorname{\mathcal{C}}_{/Y} \ar [d]^{\delta _{/Y} }_{\sim } \\ \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{\mathcal{C}}} \{ X\} & \operatorname{\mathcal{E}}^{0} \ar [l]_{ e'_0 } \ar [r]^{ e'_1 } & \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \{ Y \} . } \]

For $v \in \{ 0,1\} $, let $\underline{v}: \operatorname{\mathcal{C}}_{/f} \rightarrow \Delta ^1$ denote the constant functor taking the value $v$. We then have a commutative diagram

\[ \xymatrix { \operatorname{id}_{ \operatorname{\mathcal{C}}_{/f} } \ar [r]^{\operatorname{id}} \ar [d] & \operatorname{id}_{ \operatorname{\mathcal{C}}_{/f} } \\ \underline{0}_{ \operatorname{\mathcal{C}}_{/f} } & \underline{1}_{ \operatorname{\mathcal{C}}_{/f} } } \]

in the $\infty $-category of functors from $\operatorname{\mathcal{C}}_{/f}$ to the join $\operatorname{\mathcal{C}}_{/f} \star \Delta ^1$. Postcomposing with the tautological map $\operatorname{\mathcal{C}}_{/f} \star \Delta ^1 \rightarrow \operatorname{\mathcal{C}}$, we obtain a functor

\[ T: \operatorname{\mathcal{C}}_{/f} \rightarrow \operatorname{\mathcal{E}}^{0} \subseteq \operatorname{Fun}( \Delta ^1 \times \Delta ^1, \operatorname{\mathcal{C}}) \]

with the desired properties. $\square$

Theorem 5.3.7.7. Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a functor of $\infty $-categories, let $\pi : \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{D}}$ be given by projection onto the second factor, let $\delta : \operatorname{\mathcal{C}}\hookrightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$ be the diagonal map. For every cocartesian fibration $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}$, precomposition with $\delta $ induces a trivial Kan fibration of $\infty $-categories

\[ \operatorname{Fun}^{\operatorname{CCart}}_{ / \operatorname{\mathcal{D}}}( \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}, \operatorname{\mathcal{E}}) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{D}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}). \]

Our proof of Theorem 5.3.7.7 will make use of an auxiliary construction.

Notation 5.3.7.8 (Cocartesian Direct Images). Let $U: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ be a morphism of simplicial sets $\operatorname{id}_{\operatorname{\mathcal{D}}}: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{D}}$ determines a section of the projection map $\pi : \operatorname{Fun}( \operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}) \rightarrow \operatorname{\mathcal{C}}$. For every morphism of simplicial sets $V: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}$, we let $\operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}})$ denote the fiber product $\operatorname{\mathcal{C}}\times _{ \operatorname{Fun}(\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}) } \operatorname{Fun}(\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$. Unwinding the definitions, we see that vertices of $\operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}})$ can be identified with pairs $(C,F)$, where $C$ is a vertex of $\operatorname{\mathcal{C}}$ and

\[ F: \operatorname{\mathcal{D}}_{C} = \{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}\rightarrow \{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}= \operatorname{\mathcal{E}}_{C} \]

is a section of the map $V|_{\operatorname{\mathcal{E}}_ C}: \operatorname{\mathcal{E}}_ C \rightarrow \operatorname{\mathcal{D}}_{C}$. If $V$ is a cocartesian fibration, we let $\operatorname{Res}^{\operatorname{CCart}}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}})$ denote the full simplicial subset of $\operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}})$ spanned by those vertices $(C,F)$ where $F$ carries each edge of $\operatorname{\mathcal{D}}_{C}$ to $V_{C}$-cocartesian edge of $\operatorname{\mathcal{E}}_{C}$. We will refer to $\operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}})$ as the cocartesian direct image of $\operatorname{\mathcal{E}}$ along $U$.

Remark 5.3.7.9. Let $U: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ be a morphism of simplicial sets and let $V: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}$ be a cocartesian fibration of simplicial sets. Then the projection map $\pi : \operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}) \rightarrow \operatorname{\mathcal{C}}$ restricts to a projection map $\pi ^{\operatorname{CCart}}: \operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}}) \rightarrow \operatorname{\mathcal{C}}$. Moreover, for each vertex $C \in \operatorname{\mathcal{C}}$, the canonical isomorphism $\{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}) \simeq \operatorname{Fun}_{ / \operatorname{\mathcal{D}}_ C }( \operatorname{\mathcal{D}}_ C, \operatorname{\mathcal{E}}_ C )$ restricts to an isomorphism of full subcategories $\{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{E}}) \simeq \operatorname{Fun}^{\operatorname{CCart}}_{/\operatorname{\mathcal{D}}_ C }( \operatorname{\mathcal{D}}_ C, \operatorname{\mathcal{E}}_ C )$.

Proposition 5.3.7.10. Let $V: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}$ be a cocartesian fibration of simplicial sets, let $U: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ be a cartesian fibration of simplicial sets. Then:

$(1)$

The projection map $\pi : \operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}) \rightarrow \operatorname{\mathcal{C}}$ is a cocartesian fibration of simplicial sets.

$(2)$

Let $e: X \rightarrow Y$ be a $\pi $-cocartesian edge of the simplicial set $\operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}})$. If $X$ belongs to the simplicial subset $\operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}})$, then $Y$ also belongs to the simplicial subset $\operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}})$.

$(3)$

The morphism $\pi $ restricts to a cocartesian fibration $\pi ^{\operatorname{CCart}}: \operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}}) \rightarrow \operatorname{\mathcal{C}}$.

$(4)$

An edge of the simplicial set $\operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}})$ is $\pi ^{\operatorname{CCart}}$-cocartesian if and only if it is $\pi $-cocartesian.

Proof. Assertion $(1)$ follows from Proposition 5.3.6.6 (after passing to opposite simplicial sets). To prove $(2)$, we may assume without loss of generality that $\operatorname{\mathcal{C}}= \Delta ^1$ and $\pi (e)$ is the nondegenerate edge of $\operatorname{\mathcal{C}}$. In this case, the simplicial sets $\operatorname{\mathcal{D}}$ and $\operatorname{\mathcal{E}}$ are $\infty $-categories, and we can identify the edge $e$ with a morphism of simplicial sets $E: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{E}}$ satisfying $V \circ E = \operatorname{id}_{\operatorname{\mathcal{D}}}$. Let $u: D \rightarrow D'$ be a morphism in the $\infty $-category $\operatorname{\mathcal{D}}_1 = \{ 1\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}$; we wish to show that $E(u)$ is a $V$-cocartesian morphism of $\operatorname{\mathcal{E}}$. To prove this, let $G: \operatorname{\mathcal{D}}_{1} \rightarrow \operatorname{\mathcal{D}}_0 = \{ 0\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}$ be given by contravariant transport along the nondegenerate edge of $\operatorname{\mathcal{C}}$, so that we have a commutative diagram

\[ \xymatrix@R =50pt@C=50pt{ G(D) \ar [d]^{ G(u) } \ar [r] & D \ar [d]^{u} \\ G(D') \ar [r] & D', } \]

in the $\infty $-category where the horizontal maps are $U$-cartesian. Our assumption that $e$ is $\pi $-cocartesian guarantees that the functor $E$ carries $U$-cartesian morphisms of $\operatorname{\mathcal{D}}$ to $V$-cocartesian morphisms of $\operatorname{\mathcal{E}}$ (Proposition 5.3.6.6). We therefore obtain a commutative diagram

\[ \xymatrix@R =50pt@C=50pt{ (E \circ G)(D) \ar [d]^{ (E \circ G)(u) } \ar [r] & E(D) \ar [d]^{ E(u) } \\ (E \circ G)(D') \ar [r] & E(D' ), } \]

where the horizontal maps are $V$-cocartesian. By virtue of Corollary 5.1.2.4, it will suffice to show that the morphism $(E \circ G)(u)$ is $V$-cocartesian, which follows from our assumption that $X$ belongs to $\operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}})$. This completes the proof of $(2)$; assertions $(3)$ and $(4)$ then follow by applying Proposition 5.1.4.17. $\square$

In the situation of Proposition 5.3.7.10, the cocartesian direct image $\operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}})$ can be characterized by a universal property:

Proposition 5.3.7.11. Let $V: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}$ be a cocartesian fibration of simplicial sets and let $U: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ be a cartesian fibration of simplicial sets. For every cocartesian fibration of simplicial sets $W: \operatorname{\mathcal{C}}' \rightarrow \operatorname{\mathcal{C}}$, the canonical isomorphism

\[ \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}', \operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}) ) \xrightarrow {\sim } \operatorname{Fun}_{/\operatorname{\mathcal{D}}}( \operatorname{\mathcal{C}}' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}, \operatorname{\mathcal{E}}) \]

restricts to an isomorphism of full simplicial subsets

\[ \operatorname{Fun}^{\operatorname{CCart}}_{/\operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}', \operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}}) ) \xrightarrow {\sim } \operatorname{Fun}^{\operatorname{CCart}}_{/\operatorname{\mathcal{D}}}( \operatorname{\mathcal{C}}' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}, \operatorname{\mathcal{E}}). \]

Proof. Let $\pi : \operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}}) \rightarrow \operatorname{\mathcal{C}}$ denote the projection map and let $f: \operatorname{\mathcal{C}}' \rightarrow \operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}})$ be a morphism satisfying $\pi \circ f = W$, corresponding to a morphism of simplicial sets $F: \operatorname{\mathcal{C}}' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{E}}$ for which $V \circ F$ is given by projection to the second factor. Note that we can regard $F$ as a vertex of the simplicial subset $\operatorname{Fun}^{\operatorname{CCart}}_{/\operatorname{\mathcal{D}}}( \operatorname{\mathcal{C}}' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}, \operatorname{\mathcal{E}})$ if and only if it satisfies the following condition:

$(a)$

For every edge $(e',e)$ of the fiber product $\operatorname{\mathcal{C}}' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}$ for which $e'$ is a $W$-cocartesian edge of $\operatorname{\mathcal{C}}'$, the image $F(e',e)$ is a $V$-cocartesian edge of $\operatorname{\mathcal{E}}$.

We wish to show that $(a)$ is equivalent to the following pair of conditions:

$(b)$

The morphism $f$ factors through the full simplicial subset $\operatorname{Res}^{\operatorname{CCart}}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}}) \subseteq \operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}})$. In other words, for every edge $(e',e)$ of the fiber product $\operatorname{\mathcal{C}}' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}$ for which $e'$ is a degenerate edge of $\operatorname{\mathcal{C}}'$, the image $F(e',e)$ is a $V$-cocartesian edge of $\operatorname{\mathcal{E}}$.

$(c)$

For every $W$-cocartesian edge $e'$ of $\operatorname{\mathcal{C}}'$, the image $f(e')$ is a $\pi |_{ \operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}}) }$-cocartesian edge of $\operatorname{Res}^{\operatorname{CCart}}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}})$. By virtue of Propositions 5.3.7.10 and 5.3.6.6, this is equivalent to the assertion that for every edge $(e',e)$ of the fiber product $\operatorname{\mathcal{C}}' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}$ where $e'$ is $W$-cocartesian and $e$ is $U$-cartesian, the image $F(e',e)$ is a $V$-cocartesian edge of $\operatorname{\mathcal{E}}$.

The implications $(a) \Rightarrow (b)$ and $(a) \Rightarrow (c)$ are clear. For the converse, suppose that $(b)$ and $(c)$ are satisfied; we wish to prove $(a)$. Let $(e',e): (X',X) \rightarrow (Z',Z)$ be an edge of the fiber product $\operatorname{\mathcal{C}}' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}$, where $e': X' \rightarrow Z'$ is $W$-cocartesian. Let $\overline{e} = U(e) = W(e')$ denote the corresponding edge of $\operatorname{\mathcal{C}}$. Since $U$ is a cartesian fibration, there exists a $U$-cartesian morphism $f: Y \rightarrow Z$ satisfying $U(f) = \overline{e}$. Let $\overline{\sigma }$ denote the left-degenerate $2$-simplex $s^{1}_0(\overline{e})$. Since $f$ is $U$-cartesian, we can lift $\overline{\sigma }$ to a $2$-simplex of $\operatorname{\mathcal{D}}$ as indicated in the diagram

\[ \xymatrix@R =50pt@C=50pt{ & Y \ar [dr]^{f} & \\ X \ar [ur] \ar [rr]^-{e} & & Z. } \]

Writing $\sigma '$ for the left-degenerate $2$-simplex $s^{1}_0(e')$ of $\operatorname{\mathcal{C}}'$, we obtain a $2$-simplex $\tau = F( \sigma ', \sigma )$ of $\operatorname{\mathcal{E}}$. It follows from assumption $(b)$ that the restriction $\tau |_{ \operatorname{N}_{\bullet }( \{ 0 < 1\} ) }$ is a $V$-cocartesian edge of $\operatorname{\mathcal{E}}$, and from assumption $(c)$ that the restriction $\tau |_{ \operatorname{N}_{\bullet }( \{ 1 < 2 \} ) }$ is a $V$-cocartesian edge of $\operatorname{\mathcal{E}}$. Applying Proposition 5.1.4.13, we conclude that $F(e',e) = \tau |_{ \operatorname{N}_{\bullet }( \{ 0 < 2 \} ) }$ is also a $V$-cocartesian edge of $\operatorname{\mathcal{E}}$. $\square$

Proof of Theorem 5.3.7.7. Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a functor of $\infty $-categories, let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}$ be a cocartesian fibration of $\infty $-categories, and let $\delta : \operatorname{\mathcal{C}}\hookrightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$ be the diagonal embedding. Since $U$ is an isofibration (Proposition 5.1.4.9), the restriction map $\overline{\theta }: \operatorname{Fun}_{ / \operatorname{\mathcal{D}}}( \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}, \operatorname{\mathcal{E}}) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{D}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ is also an isofibration (Corollary 4.5.5.16). Because $\operatorname{Fun}^{\operatorname{CCart}}_{ / \operatorname{\mathcal{D}}}( \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}, \operatorname{\mathcal{E}})$ is a replete full subcategory of $\operatorname{Fun}_{ / \operatorname{\mathcal{D}}}( \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}, \operatorname{\mathcal{E}})$, it follows that $\overline{\theta }$ restricts to an isofibration $\theta : \operatorname{Fun}^{\operatorname{CCart}}_{ / \operatorname{\mathcal{D}}}( \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}, \operatorname{\mathcal{E}}) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{D}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$. To prove Theorem 5.3.7.7, we will show that $\theta $ is an equivalence of $\infty $-categories (it is then automatically a trivial Kan fibration of simplicial sets: see Proposition 4.5.5.20).

Note that the functor $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}$ induces cocartesian fibrations $U': \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$ and $U'': \operatorname{\mathcal{C}}\times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$. Let $\pi ': \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ be given by projection onto the first factor, so that $\pi '$ is a cartesian fibration (Corollary 5.3.7.3). Let $\operatorname{\mathcal{M}}$ denote the cocartesian direct image $\operatorname{Res}^{\operatorname{CCart}}_{ \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}/ \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{E}})$ and let $T: \operatorname{\mathcal{M}}\rightarrow \operatorname{\mathcal{C}}$ be the projection map. Precomposition with the diagonal embedding $\delta : \operatorname{\mathcal{C}}\hookrightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$ induces a restriction functor

\[ \delta ^{\ast }: \operatorname{\mathcal{M}}\rightarrow \operatorname{Res}_{ \operatorname{\mathcal{C}}/\operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}\times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{E}}) = \operatorname{\mathcal{C}}\times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{E}} \]

which fits into a commutative diagram

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{M}}\ar [rr]^{ \delta ^{\ast } } \ar [dr]_{T} & & \operatorname{\mathcal{C}}\times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{E}}\ar [dl]^{U''} \\ & \operatorname{\mathcal{C}}& } \]

It follows from Proposition 5.3.7.10 that $T$ is a cocartesian fibration and that $\delta ^{\ast }$ carries $T$-cocartesian morphisms of $\operatorname{\mathcal{M}}$ to $U''$-cocartesian morphisms of $\operatorname{\mathcal{C}}\times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{E}}$. Using Proposition 5.3.7.11, we can identify $\theta $ with the map

\[ \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{M}}) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{C}}\times _{\operatorname{\mathcal{D}}}, \operatorname{\mathcal{E}}) \simeq \operatorname{Fun}_{ / \operatorname{\mathcal{D}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \]

given by postcomposition with $\delta ^{\ast }$. Consequently, to show that $\theta $ is an equivalence of $\infty $-categories, it will suffice to show that $\delta ^{\ast }$ is an equivalence of cocartesian fibrations over $\operatorname{\mathcal{C}}$. By virtue of Proposition 5.1.7.15), this can be checked fiberwise: that is, it suffices to show that for each object $C \in \operatorname{\mathcal{C}}$, the induced map of fibers

\[ \delta ^{\ast }_{C}: \{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{M}}\simeq \operatorname{Fun}^{\operatorname{CCart}}_{ / \operatorname{\mathcal{D}}}( \{ C\} \operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}, \operatorname{\mathcal{E}}) \rightarrow \{ C\} \times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{E}} \]

is an equivalence of $\infty $-categories. This is a special case of Corollary 5.3.1.22, since $\delta (C)$ is an initial object of the $\infty $-category $\{ C\} \operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$ (Proposition 4.6.7.22). $\square$