Kerodon

Proof. Choose a monomorphism of simplicial sets $\operatorname{\mathcal{E}}_0 \hookrightarrow \operatorname{\mathcal{Q}}$, where $\operatorname{\mathcal{Q}}$ is a contractible Kan complex (see Exercise 3.1.7.11). Replacing $\operatorname{\mathcal{E}}'$ with the product $\operatorname{\mathcal{E}}' \times \operatorname{\mathcal{Q}}$, we can reduce to the case where $G_0$ is a monomorphism of simplicial sets. Let $\operatorname{\mathcal{E}}$ denote the simplicial subset of $\operatorname{\mathcal{E}}'$ consisting of those simplices $\sigma : \Delta ^ m \rightarrow \operatorname{\mathcal{E}}'$ for which the induced map $\operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \Delta ^ m \rightarrow \operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}'$ factors through $G_0$. To complete the proof, it will suffice to verify the following:

$(a)$

The morphism $U = V|_{\operatorname{\mathcal{E}}}$ is an inner fibration from $\operatorname{\mathcal{E}}$ to $\operatorname{\mathcal{C}}$.

$(b)$

The inclusion $\operatorname{\mathcal{E}}\hookrightarrow \operatorname{\mathcal{E}}'$ is an equivalence of inner fibrations over $\operatorname{\mathcal{C}}$.

By virtue of Remark 4.1.1.13 and Proposition 5.1.7.9, it suffices to prove $(a)$ and $(b)$ in the special case where $\operatorname{\mathcal{C}}= \Delta ^ n$ is a standard simplex. In this case, the morphism $V: \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{C}}$ is an isofibration (Example 4.4.1.6).

Let $\operatorname{\mathcal{E}}'_{0}$ denote the fiber product $\operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}'$. Applying Lemma 5.1.7.13 to the morphism $G_0: \operatorname{\mathcal{E}}_0 \rightarrow \operatorname{\mathcal{E}}'_0$ (which is an equivalence of inner fibrations over $\operatorname{\mathcal{C}}_{0}$), we deduce that there exists a morphism $R_0: \operatorname{\mathcal{E}}'_{0} \rightarrow \operatorname{\mathcal{E}}_0$ in the category $(\operatorname{Set_{\Delta }})_{/\operatorname{\mathcal{C}}_0}$ such that $R_0 \circ G_0 = \operatorname{id}_{\operatorname{\mathcal{E}}_0}$, and an isomorphism $\alpha _0: \operatorname{id}_{ \operatorname{\mathcal{E}}'_0 } \rightarrow G_0 \circ R_0$ in the $\infty $-category $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}_0}( \operatorname{\mathcal{E}}'_0, \operatorname{\mathcal{E}}'_0 )$ whose image in $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}_0}( \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{E}}'_0 )$ is degenerate. Applying Proposition 4.4.5.8 (and the criterion of Proposition 4.4.4.9), we can choose a morphism $R: \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{E}}'$ in $(\operatorname{Set_{\Delta }})_{/\operatorname{\mathcal{C}}}$ such that $R|_{\operatorname{\mathcal{E}}'_0} = G_0 \circ R_0$ and an isomorphism $\alpha : \operatorname{id}_{\operatorname{\mathcal{E}}'} \rightarrow R$ in the $\infty $-category $\operatorname{Fun}_{/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}}', \operatorname{\mathcal{E}}')$ whose image in $\operatorname{Fun}_{/\operatorname{\mathcal{C}}_0}(\operatorname{\mathcal{E}}'_0, \operatorname{\mathcal{E}}'_0)$ is equal to $\alpha _0$.

We now prove $(a)$. Suppose we are given a lifting problem

where the left vertical map is inner anodyne. Since $V: \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{C}}$ is an inner fibration, we can extend $f_0$ to a morphism $f': B \rightarrow \operatorname{\mathcal{E}}$ satisfying $V \circ f' = \overline{f}$. Set $B_0 = \operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} B$ and $A_0 = \operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} A$, and define

by the formula $f_1|_{A} = f_0$ and $f_1|_{B_0} = R \circ f'|_{B_0}$. Note that there is an isomorphism

in the $\infty $-category $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( A {\coprod }_{A_0} B_0, \operatorname{\mathcal{E}}' )$, whose image in $\operatorname{Fun}_{/\operatorname{\mathcal{C}}}( A, \operatorname{\mathcal{E}}')$ is degenerate and whose image in $\operatorname{Fun}_{/\operatorname{\mathcal{C}}}( B_0, \operatorname{\mathcal{E}}' )$ is the restriction of $\alpha $. Applying Proposition 4.4.5.8, we deduce that $f_{1}$ admits an extension $f: B \rightarrow \operatorname{\mathcal{C}}$ satisfying $U \circ f = \overline{f}$.

To prove $(b)$, we observe that the morphism $R: \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{E}}$ is a homotopy inverse of the inclusion $\iota : \operatorname{\mathcal{E}}\hookrightarrow \operatorname{\mathcal{E}}'$ relative to $\operatorname{\mathcal{C}}$. By construction, $\alpha $ determines an isomorphism from $\operatorname{id}_{\operatorname{\mathcal{E}}'}$ to the composition $\iota \circ R$ in the $\infty $-category $\operatorname{Fun}_{/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}}', \operatorname{\mathcal{E}}')$, and the restriction of $\alpha $ determines an isomorphism from $\operatorname{id}_{\operatorname{\mathcal{E}}}$ to $R \circ \iota $ in the $\infty $-category $\operatorname{Fun}_{/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}}, \operatorname{\mathcal{E}})$. $\square$

Proof. By virtue of Theorem 5.6.0.2, there exists a morphism of simplicial sets $\mathscr {F}_0: \operatorname{\mathcal{C}}_0 \rightarrow \operatorname{\mathcal{QC}}$ and an equivalence $G_0: \operatorname{\mathcal{E}}_0 \rightarrow \int _{\operatorname{\mathcal{C}}_0} \mathscr {F}_0$ of cocartesian fibrations over $\operatorname{\mathcal{C}}_0$. Since $\operatorname{\mathcal{QC}}$ is an $\infty $-category (Proposition 5.5.4.3), our assumption that the inclusion $\operatorname{\mathcal{C}}_0 \hookrightarrow \operatorname{\mathcal{C}}$ is a categorical equivalence guarantees that we can extend $\mathscr {F}_0$ to a morphism of simplicial sets $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{QC}}$. We can then identify $G_0$ with an equivalence $\operatorname{\mathcal{E}}_0 \rightarrow \operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \int _{\operatorname{\mathcal{C}}} \mathscr {F}$ of cocartesian fibrations over $\operatorname{\mathcal{C}}_0$. Applying Lemma 5.6.7.1, we can write $U_0$ as the pullback of an inner fibration $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ which is equivalent to the projection map $V: \int _{\operatorname{\mathcal{C}}} \mathscr {F} \rightarrow \operatorname{\mathcal{C}}$ as an inner fibration over $\operatorname{\mathcal{C}}$. Since $V$ is a cocartesian fibration (Proposition 5.6.2.2), it follows that $U$ is also a cocartesian fibration (Proposition 5.1.7.14). $\square$

Proof. Using Corollary 4.1.3.3, we can choose an inner anodyne map $F: \operatorname{\mathcal{C}}_0 \hookrightarrow \operatorname{\mathcal{C}}$, where $\operatorname{\mathcal{C}}$ is an $\infty $-category. Since $F$ is a categorical equivalence of simplicial sets (Corollary 4.5.3.14), Proposition 5.6.7.2 guarantees that $U_0$ is the pullback of a cocartesian fibration $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$. $\square$

Proof. By virtue of Corollary 5.6.7.3, we may assume without loss of generality that $U$ is a cocartesian fibration of $\infty $-categories, in which case the desired result follows from Proposition 5.1.4.9. $\square$

Proof. By virtue of Corollary 5.6.7.3 and Remark 4.5.9.14, we may assume that $U$ is a cocartesian fibration of $\infty $-categories, in which case the desired result follows from Proposition 5.3.6.1. $\square$

Proof. Using Corollaries 5.6.7.3 and 5.6.7.6, we can reduce to the situation where $\operatorname{\mathcal{C}}$ is an $\infty $-category. In this case, the desired result is a special case of Corollary 5.1.5.16. $\square$

Proof. Combine Proposition 5.1.7.5 with Corollary 5.6.7.5. $\square$