Kerodon

Proof. Apply Proposition 7.4.4.1 to the cocartesian fibration $U: \int _{\operatorname{\mathcal{C}}} \mathscr {F} \rightarrow \operatorname{\mathcal{C}}$. $\square$

Proof of Theorem 7.4.4.6. Choose an uncountable cardinal $\lambda $ of exponential cofinality $\geq \kappa $, so that the $\infty $-category $\operatorname{\mathcal{QC}}^{< \kappa }$ is locally $\lambda $-small (Remark 5.5.4.14). For every object $\operatorname{\mathcal{K}}\in \operatorname{\mathcal{QC}}^{< \kappa }$, let $h^{\operatorname{\mathcal{K}}}: \operatorname{\mathcal{QC}}^{< \kappa } \rightarrow \operatorname{\mathcal{S}}^{< \lambda }$ be the functor corepresented by $\operatorname{\mathcal{K}}$. By virtue of Proposition 5.6.6.17, we may assume that $h^{\operatorname{\mathcal{K}}}$ is obtained from the homotopy coherent nerve of the simplicial functor

By virtue of Proposition 7.4.1.18, it will suffice to show that the following conditions are equivalent:

$(1_{\operatorname{\mathcal{K}}} )$

The restriction map

\[ \operatorname{Fun}( \operatorname{\mathcal{K}}, \operatorname{Fun}_{ / \operatorname{\mathcal{C}}^{\triangleleft } }^{\operatorname{CCart}}( \operatorname{\mathcal{C}}^{\triangleleft }, \overline{\operatorname{\mathcal{E}}} ) )^{\simeq } \rightarrow \operatorname{Fun}(\operatorname{\mathcal{K}}, \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}))^{\simeq } \]

is a homotopy equivalence of Kan complexes.

$(2_{\operatorname{\mathcal{K}}} )$

The composition $h^{\operatorname{\mathcal{K}}} \circ \operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleleft } }$ is a limit diagram in the $\infty $-category $\operatorname{\mathcal{S}}^{< \lambda }$.

Using Example 5.6.5.9, we can replace $U$ by the projection map

and thereby reduce to proving the equivalence $(1_{\operatorname{\mathcal{K}}} ) \Leftrightarrow ( 2_{\operatorname{\mathcal{K}}} )$ in the special case where $\operatorname{\mathcal{K}}= \Delta ^{0}$. In this case, the desired result follows by applying Proposition 7.4.1.16 to the underlying left fibration of $U$ (see Example 5.6.5.8). $\square$

Proof. Let $\operatorname{ev}: \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \times \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{E}}$ denote the evaluation morphism (given on vertices by the formula $\operatorname{ev}( F, C) = F(C)$), and let

denote the relative join of Construction 5.2.3.1. Note that we have a canonical map

Let $\pi : \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \times \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}$ be given by projection onto the second factor. Note that $\pi $ is a cocartesian fibration, and that an edge of the product $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \times \operatorname{\mathcal{C}}$ is $\pi $-cocartesian if and only if its image in $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ is an isomorphism. It follows that the $\operatorname{ev}$ carries $\pi $-cocartesian edges of $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \times \operatorname{\mathcal{C}}$ to $U$-cocartesian edges of $\operatorname{\mathcal{E}}$. Applying Lemma 5.2.3.17, we deduce that $U'$ is a cocartesian fibration. By construction, we can identify $\operatorname{\mathcal{E}}$ with the inverse image of $\{ 1\} \times \operatorname{\mathcal{C}}$ under $U'$.

Let $\operatorname{\mathcal{E}}''$ denote the pushout

Amalgamating $U'$ with the projection map $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \times \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{\mathcal{C}}^{\triangleleft }$, we obtain a morphism of simplicial sets $U'': \operatorname{\mathcal{E}}'' \rightarrow K$, where $K$ denotes the pushout $( \{ 0 \} \times \operatorname{\mathcal{C}})^{\triangleleft } {\coprod }_{ ( \{ 0\} \times \operatorname{\mathcal{C}}) } ( \Delta ^1 \times \operatorname{\mathcal{C}})$. It follows from Proposition 5.1.4.8 that $U''$ is also a cocartesian fibration.

Let us abuse notation by identifying $K$ with its image in the simplicial set $( \Delta ^1 \times \operatorname{\mathcal{C}})^{\triangleleft }$. Since the inclusion map $\{ 0\} \times \operatorname{\mathcal{C}}\hookrightarrow \Delta ^1 \times \operatorname{\mathcal{C}}$ is left anodyne (Proposition 4.2.5.3), the inclusion $K \hookrightarrow (\Delta ^1 \times \operatorname{\mathcal{C}})^{\triangleleft }$ is inner anodyne (Example 4.3.6.5). Applying Proposition 5.6.7.2, we can write $U''$ as the pullback of a cocartesian fibration $U''': \operatorname{\mathcal{E}}''' \rightarrow (\Delta ^1 \times \operatorname{\mathcal{C}})^{\triangleleft }$. We then have a commutative diagram of simplicial sets

where each square is a pullback and each vertical map is a cocartesian fibration. Let $\overline{\operatorname{\mathcal{E}}}$ denote the pullback $( \{ 1\} \times \operatorname{\mathcal{C}})^{\triangleleft } \times _{ (\Delta ^1 \times \operatorname{\mathcal{C}})^{\triangleleft } } \operatorname{\mathcal{E}}'''$, so that $U'''$ restricts to a cocartesian fibration $\overline{U}: \overline{\operatorname{\mathcal{E}}} \rightarrow ( \{ 1\} \times \operatorname{\mathcal{C}})^{\triangleleft }$. We will complete the proof by showing that the commutative diagram

satisfies the requirements of Proposition 7.4.4.12.

For every simplicial subset $A \subseteq (\Delta ^1 \times \operatorname{\mathcal{C}})^{\triangleleft }$, let $\operatorname{\mathcal{D}}(A)$ denote the $\infty $-category

Let ${\bf 0}$ denote the cone point of $(\Delta ^1 \times \operatorname{\mathcal{C}})^{\triangleleft }$. Note that we have a commutative diagram of restriction functors

We wish to show that $\alpha $ is an equivalence of $\infty $-categories. Since the inclusion $K \hookrightarrow ( \Delta ^1 \times \operatorname{\mathcal{C}})^{\triangleleft }$ is inner anodyne (as noted above) and the inclusion $( \{ 1\} \times \operatorname{\mathcal{C}})^{\triangleleft } \hookrightarrow ( \Delta ^1 \times \operatorname{\mathcal{C}})^{\triangleleft }$ is left anodyne (Lemma 4.3.7.8), the morphisms $\alpha '$ and $\beta $ are trivial Kan fibrations (Proposition 5.3.1.21). It will therefore suffice to show that $\beta '$ is an equivalence of $\infty $-categories.

Amalgamating the map

with the identity on $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \times \operatorname{\mathcal{C}}^{\triangleleft }$, we obtain a morphism of simplicial sets $F: \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \times K \rightarrow \operatorname{\mathcal{E}}''$. If $e$ is an edge of the product $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \times K$ whose image in $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ is an isomorphism, then $F(e)$ is a $U''$-cocartesian edge of $\operatorname{\mathcal{E}}''$. We can therefore identify $F$ with a morphism of simplicial sets $f: \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \rightarrow \operatorname{\mathcal{D}}(K)$. Unwinding the definitions, we see that $\beta ' \circ f$ is an isomorphism of simplicial sets. Consequently, to show that $\beta '$ is an equivalence of $\infty $-categories, it will suffice to show that $f$ is an equivalence of $\infty $-categories. Similarly, the composite map $\gamma \circ f$ is an isomorphism, so we are reduced to proving that $\gamma $ is an equivalence of $\infty $-categories. Since $\beta $ is a trivial Kan fibration, this is equivalent to the assertion that $\gamma \circ \beta $ is an equivalence of $\infty $-categories, which is a special case of Corollary 5.3.1.23. $\square$

Proof of Proposition 7.4.4.1. Let $\operatorname{\mathcal{C}}$ be a small simplicial set and let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{QC}}$ be the covariant transport representation for a cocartesian fibration $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$. Using Proposition 7.4.4.12, we can choose a pullback diagram

where $\overline{U}$ is a cocartesian fibration and the restriction map

is an equivalence of $\infty $-categories. It follows from Remark 7.4.4.13 that the cocartesian fibration $\overline{U}$ is essentially small, so that $\mathscr {F}$ admits an extension $\overline{\mathscr {F}}: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{\mathcal{QC}}$ which is a covariant transport representation for $\overline{U}$ (Corollary 5.6.5.13). Applying Theorem 7.4.4.6, we see that $\overline{\mathscr {F}}$ is a limit diagram in $\operatorname{\mathcal{QC}}$. In particular, it carries the cone point of $\operatorname{\mathcal{C}}^{\triangleleft }$ to an $\infty $-category $\operatorname{\mathcal{D}}$ which is a limit of the diagram $\mathscr {F}$. By virtue of Remark 7.4.4.11, the $\infty $-category $\operatorname{\mathcal{D}}$ is equivalent to the $\infty $-category $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ of cocartesian sections of $U$. $\square$