Kerodon

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

5.6.7 Proof of the Universality Theorem

Our goal in this section is to give a proof of Theorem 5.6.4.9. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets, let $\operatorname{\mathcal{C}}' \subseteq \operatorname{\mathcal{C}}$ be a simplicial subset, and suppose that the projection map $\operatorname{\mathcal{C}}' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}'$ admits a covariant transport representation $\mathscr {F}': \operatorname{\mathcal{C}}' \rightarrow \operatorname{\mathcal{QC}}$. We wish to show that $\mathscr {F}'$ can be extended to a covariant transport representation $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{QC}}$ for $U$. Proceeding one simplex at a time, we will reduce to the fundamental case where $\operatorname{\mathcal{C}}= \Delta ^ n$ is a standard simplex and $\operatorname{\mathcal{C}}' = \operatorname{\partial \Delta }^ n$ is its boundary (Lemma 5.6.7.6). To handle this case, we exploit the structure theory for cocartesian fibrations over $\Delta ^ n$ developed in ยง5.2.6. First, we need some auxiliary remarks.

Construction 5.6.7.1. Let $\operatorname{\mathcal{C}}$ be a simplicial set, let $\operatorname{Path}[\operatorname{\mathcal{C}}]_{\bullet }$ denote the simplicial path category of $\operatorname{\mathcal{C}}$ (Notation 2.4.4.2) and let $\mathscr {F}: \operatorname{Path}[\operatorname{\mathcal{C}}]_{\bullet } \rightarrow \operatorname{Set_{\Delta }}$ be a simplicial functor. For every simplicial set $X$, we let $\mathscr {F}^{X}: \operatorname{Path}[\operatorname{\mathcal{C}}]_{\bullet } \rightarrow \operatorname{Set_{\Delta }}$ denote the simplicial functor given on objects by the formula $\mathscr {F}^{X}(C) = \operatorname{Fun}(X, \mathscr {F}(C) )$. Note that evaluation determines a natural transformation of simplicial functors $\operatorname{ev}: \underline{X} \times \mathscr {F}^{X} \rightarrow \mathscr {F}$, where $\underline{X}: \operatorname{Path}[\operatorname{\mathcal{C}}]_{\bullet } \rightarrow \operatorname{Set_{\Delta }}$ is the constant (simplicial) functor taking the value $X$.

Let us abuse notation by identifying $\mathscr {F}$, $\mathscr {F}^{X}$, and $\underline{X}$ with morphisms from $\operatorname{\mathcal{C}}$ to the homotopy coherent nerve $\operatorname{N}_{\bullet }^{\operatorname{hc}}(\operatorname{Set_{\Delta }})$. Let $\rho : X \rightarrow \int _{\Delta ^0} X$ be the comparison map of Example 5.5.4.17. Applying Remark 5.5.4.15, we obtain a morphism of simplicial sets

\begin{eqnarray*} X \times \int _{\operatorname{\mathcal{C}}} \mathscr {F}^{X} & \xrightarrow {\rho \times \operatorname{id}} & (\int _{\Delta ^{0}} X) \times (\int _{\operatorname{\mathcal{C}}} \mathscr {F}^{X} ) \\ & \simeq & (\operatorname{\mathcal{C}}\times \int _{\Delta ^{0}} X) \times _{\operatorname{\mathcal{C}}} (\int _{\operatorname{\mathcal{C}}} \mathscr {F}^{X} ) \\ & \simeq & ( \int _{\operatorname{\mathcal{C}}} \underline{X} ) \times _{\operatorname{\mathcal{C}}} ( \int _{\operatorname{\mathcal{C}}} \mathscr {F}^{X} ) \\ & \simeq & \int _{\operatorname{\mathcal{C}}} ( \underline{X} \times \mathscr {F}^{X} ) \\ & \xrightarrow {\int _{\operatorname{\mathcal{C}}} \operatorname{ev}} & \int _{\operatorname{\mathcal{C}}} \mathscr {F} \end{eqnarray*}

which we can identify with a comparison map

\[ \theta : \int _{\operatorname{\mathcal{C}}} \mathscr {F}^{X} \rightarrow \operatorname{\mathcal{C}}\times _{ \operatorname{Fun}(X, \operatorname{\mathcal{C}}) } \operatorname{Fun}( X, \int _{\operatorname{\mathcal{C}}} \mathscr {F} ) \]

in the category $(\operatorname{Set_{\Delta }})_{/\operatorname{\mathcal{C}}}$.

Lemma 5.6.7.2. Let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{QC}}$ be a diagram and let $X$ be a simplicial set. Then the comparison map

\[ \theta : \int _{\operatorname{\mathcal{C}}} \mathscr {F}^{X} \rightarrow \operatorname{\mathcal{C}}\times _{ \operatorname{Fun}(X, \operatorname{\mathcal{C}}) } \operatorname{Fun}(X, \int _{\operatorname{\mathcal{C}}} \mathscr {F} ) \]

of Construction 5.6.7.1 is an equivalence of cocartesian fibrations over $\operatorname{\mathcal{C}}$.

Proof. Let $U: \int _{\operatorname{\mathcal{C}}} \mathscr {F}^{X} \rightarrow \operatorname{\mathcal{C}}$ and $V: \operatorname{\mathcal{C}}\times _{ \operatorname{Fun}(X, \operatorname{\mathcal{C}}) } \operatorname{Fun}(X, \int _{\operatorname{\mathcal{C}}} \mathscr {F} ) \rightarrow \operatorname{\mathcal{C}}$ be the projection maps. By virtue of Proposition 5.6.2.12, it will suffice to prove the following:

$(1)$

For every vertex $C \in \operatorname{\mathcal{C}}$, the map of fibers

\[ \theta _{C}: \{ C\} \times _{\operatorname{\mathcal{C}}} \int _{\operatorname{\mathcal{C}}} \mathscr {F}^{X} \rightarrow \{ C\} \times _{ \operatorname{Fun}(X, \operatorname{\mathcal{C}}) } \operatorname{Fun}(X, \int _{\operatorname{\mathcal{C}}} \mathscr {F} ) \]

is an equivalence of $\infty $-categories.

$(2)$

The morphism $\theta $ carries carries $U$-cocartesian edges of $\int _{\operatorname{\mathcal{C}}} \mathscr {F}^{X}$ to $V$-cocartesian edges of $\operatorname{\mathcal{C}}\times _{ \operatorname{Fun}(X,\operatorname{\mathcal{C}})} \operatorname{Fun}(X, \int _{\operatorname{\mathcal{C}}}( \mathscr {F} ))$.

We first prove $(2)$. By virtue of Remark 5.1.1.10 and Theorem 5.2.1.1, it will suffice to show that for each vertex $x \in X$, the evaluation map $\mathscr {F}^{X} \rightarrow \mathscr {F}^{\{ x\} } \simeq \mathscr {F}$ carries $U$-cocartesian edges of $\int _{\operatorname{\mathcal{C}}} \mathscr {F}^{X}$ to $U'$-cocartesian edges of $\int _{\operatorname{\mathcal{C}}} \mathscr {F}$, where $U': \int _{\operatorname{\mathcal{C}}} \mathscr {F} \rightarrow \operatorname{\mathcal{C}}$ is the projection map. This follows immediately from Remark 5.5.4.15.

To prove $(1)$, we can assume without loss of generality that $\operatorname{\mathcal{C}}= \Delta ^{0}$ is a $0$-simplex, in which case the diagram $\mathscr {F}: \Delta ^{0} \rightarrow \operatorname{\mathcal{QC}}$ correponds to an $\infty $-category $\operatorname{\mathcal{E}}$ and $\theta $ corresponds to a functor of $\infty $-categories from $\int _{\Delta ^{0}} \operatorname{Fun}(X, \operatorname{\mathcal{E}})$ to $\operatorname{Fun}(X, \int _{\Delta ^{0}} \operatorname{\mathcal{E}})$. Let $\rho _{\operatorname{\mathcal{E}}}: \operatorname{\mathcal{E}}\rightarrow \int _{\Delta ^{0}} \operatorname{\mathcal{E}}$ and $\rho _{ \operatorname{Fun}(X,\operatorname{\mathcal{E}})}: \operatorname{Fun}(X, \operatorname{\mathcal{E}}) \rightarrow \int _{ \Delta ^{0} } \operatorname{Fun}(X, \operatorname{\mathcal{E}})$ be the comparison maps described in Example 5.5.4.17. Unwinding the definitions, we see that the composition

\[ \operatorname{Fun}(X, \operatorname{\mathcal{E}}) \xrightarrow {\rho _{\operatorname{Fun}(X,\operatorname{\mathcal{E}})}} \int _{ \Delta ^{0} } \operatorname{Fun}(X, \operatorname{\mathcal{E}}) \xrightarrow { \theta } \operatorname{Fun}(X, \int _{\Delta ^{0}} \operatorname{\mathcal{E}}) \]

coincides with the map given by postcomposition with $\rho _{\operatorname{\mathcal{E}}}$. It follows from Example 5.5.4.17 that $\rho _{\operatorname{Fun}(X, \operatorname{\mathcal{E}})}$ and $\theta \circ \rho _{ \operatorname{Fun}(X, \operatorname{\mathcal{E}})}$ are equivalences of $\infty $-categories, so that $\theta $ is also an equivalence of $\infty $-categories (Remark 4.5.1.17). $\square$

Lemma 5.6.7.3. Let $n$ be a positive integer, let $\mathscr {F}_0: \operatorname{\partial \Delta }^ n \rightarrow \operatorname{\mathcal{QC}}$ be a diagram, let $\operatorname{\mathcal{C}}$ be an $\infty $-category, and let $\sigma _0: \operatorname{\partial \Delta }^ n \rightarrow \int _{\operatorname{\partial \Delta }^ n} \mathscr {F}_0^{\operatorname{\mathcal{C}}}$ be a section of the projection map $V_0: \int _{\operatorname{\partial \Delta }^ n} \mathscr {F}_0^{\operatorname{\mathcal{C}}} \rightarrow \operatorname{\partial \Delta }^ n$ with the following properties:

$(1)$

The vertex $\sigma _0(0) \in \int _{\operatorname{\partial \Delta }^ n} \mathscr {F}_0^{\operatorname{\mathcal{C}}}$ corresponds to an equivalence of $\infty $-categories $\varphi : \operatorname{\mathcal{C}}\rightarrow \mathscr {F}_0(0)$.

$(2)$

The morphism $\sigma _0$ carries each edge of $\operatorname{\partial \Delta }^ n$ to a $V_0$-cocartesian edge of $\int _{ \operatorname{\partial \Delta }^ n} \mathscr {F}_0^{\operatorname{\mathcal{C}}}$.

Then there exists a functor $\mathscr {F}: \Delta ^ n \rightarrow \operatorname{\mathcal{QC}}$ extending $\mathscr {F}_0$ and a section $\sigma : \Delta ^ n \rightarrow \int _{\Delta ^ n} \mathscr {F}$ of the projection map $V: \int _{\Delta ^ n} \mathscr {F} \rightarrow \Delta ^ n$ which carries each edge of $\Delta ^ n$ to $V$-cocartesian morphism of $\int _{\Delta ^ n} \mathscr {F}$ and which satisfies $\sigma |_{\operatorname{\partial \Delta }^ n} = \sigma _0$.

Proof. Fix an auxiliary symbol $e$. It follows from assumption $(2)$ that $\sigma _0$ determines a morphism of simplicial sets $\operatorname{\partial \Delta }^ n \rightarrow \operatorname{\mathcal{QC}}_{ \Delta ^0 / }$ (see Remark 5.4.6.13), which we can identify with a diagram $\mathscr {G}_0: \{ e\} \star \operatorname{\partial \Delta }^ n \rightarrow \operatorname{\mathcal{QC}}$ satisfying $\mathscr {G}_0(e) = \Delta ^0$ and $\mathscr {G}_0|_{ \operatorname{\partial \Delta }^ n} = \mathscr {F}_0^{\operatorname{\mathcal{C}}}$. Let $\operatorname{QCat}$ be the (locally Kan) simplicial category of Construction 5.4.4.1, so that $\mathscr {F}_0$ and $\mathscr {G}_0$ can be identified with simplicial functors $F_0: \operatorname{Path}[ \operatorname{\partial \Delta }^ n ]_{\bullet } \rightarrow \operatorname{QCat}$ and $G_0: \operatorname{Path}[ \{ e\} \star \operatorname{\partial \Delta }^ n ]_{\bullet } \rightarrow \operatorname{QCat}$ such that $G_0|_{ \operatorname{Path}[ \operatorname{\partial \Delta }^ n ]_{\bullet } }$ is the composite functor

\[ \operatorname{Path}[ \operatorname{\partial \Delta }^ n ]_{\bullet } \xrightarrow {F_0} \operatorname{QCat}\xrightarrow { \operatorname{Fun}(\operatorname{\mathcal{C}}, \bullet ) } \operatorname{QCat}. \]

Note that $G_0$ determines an extension of $F_0$ to a functor $F_0^{+}: \operatorname{Path}[ \{ e\} \star \operatorname{\partial \Delta }^ n ]_{\bullet } \rightarrow \operatorname{QCat}$ satisfying $F_0^{+}(e) = \operatorname{\mathcal{C}}$, which we can identify with a morphism of simplicial sets $\tau _0: \{ e\} \star \operatorname{\partial \Delta }^ n \rightarrow \operatorname{\mathcal{QC}}$.

To complete the proof, we must show that $F_0$ and $G_0$ can be extended to simplicial functors $F: \operatorname{Path}[ \Delta ^ n ]_{\bullet } \rightarrow \operatorname{QCat}$ and $G: \operatorname{Path}[ \{ e\} \star \Delta ^ n ]_{\bullet } \rightarrow \operatorname{QCat}$ for which the restriction $G|_{ \operatorname{Path}[ \Delta ^ n ]_{\bullet }}$ coincides with the composition $\operatorname{Path}[ \Delta ^ n ]_{\bullet } \xrightarrow {F} \operatorname{QCat}\xrightarrow { \operatorname{Fun}(\operatorname{\mathcal{C}}, \bullet ) } \operatorname{QCat}$. This is equivalent to the existence of a simplicial functor $F^{+}: \operatorname{Path}[ \{ e\} \star \Delta ^ n ]_{\bullet } \rightarrow \operatorname{QCat}$ extending $F_{0}^{+}$, which is in turn equivalent to the existence of a morphism $\tau : \{ e\} \star \Delta ^ n \rightarrow \operatorname{\mathcal{QC}}$ satisfying $\tau |_{ \{ e\} \star \operatorname{\partial \Delta }^ n} = \tau _0$. It follows from assumption $(1)$ (and Remark 5.4.4.6) that $\tau _0$ carries the initial edge $\Delta ^1 \simeq \{ e\} \star \{ 0\} \subset \{ e\} \star \operatorname{\partial \Delta }^ n$ to an isomorphism in the $\infty $-category $\operatorname{\mathcal{QC}}$, so the existence of $\tau $ follows from Theorem 4.4.2.6. $\square$

Exercise 5.6.7.4. Show that the conclusion of Lemma 5.6.7.3 holds if we replace the $\infty $-category $\operatorname{\mathcal{C}}$ by an arbitrary simplicial set $X$.

Lemma 5.6.7.5. Let $n$ be a positive integer, let $\mathscr {F}_0: \operatorname{\partial \Delta }^ n \rightarrow \operatorname{\mathcal{QC}}$ be a diagram, let $V_0: \int _{\operatorname{\partial \Delta }^ n} \mathscr {F}_0 \rightarrow \operatorname{\partial \Delta }^ n$ denote the projection map, let $\operatorname{\mathcal{C}}$ be an $\infty $-category, and let $G_0: \operatorname{\partial \Delta }^ n \times \operatorname{\mathcal{C}}\rightarrow \int _{\operatorname{\partial \Delta }^ n} \mathscr {F}_0$ be a morphism in $(\operatorname{Set_{\Delta }})_{/\operatorname{\partial \Delta }^ n}$ with the following properties:

$(1)$

The morphism

\[ G_0|_{ \{ 0\} \times \operatorname{\mathcal{C}}}: \operatorname{\mathcal{C}}\rightarrow \{ 0\} \times _{ \operatorname{\partial \Delta }^ n} \int _{\operatorname{\partial \Delta }^ n} \mathscr {F}_0 \]

is a categorical equivalence of simplicial sets.

$(2')$

For each object $C \in \operatorname{\mathcal{C}}$, the restriction

\[ G_0|_{ \operatorname{\partial \Delta }^ n \times \{ C\} }: \operatorname{\partial \Delta }^ n \rightarrow \int _{\operatorname{\partial \Delta }^ n} \mathscr {F}_0 \]

carries each edge of $\operatorname{\partial \Delta }^ n$ to a $V_0$-cocartesian edge of $\int _{\operatorname{\partial \Delta }^ n} \mathscr {F}_0$.

Then there exists a functor $\mathscr {F}: \Delta ^ n \rightarrow \operatorname{\mathcal{QC}}$ extending $\mathscr {F}_0$ and a functor $G: \Delta ^ n \times \operatorname{\mathcal{C}}\rightarrow \int _{\Delta ^ n} \mathscr {F}$ which extends $G_0$ and satisfies the following stronger version of $(2')$:

$(2)$

For each object $C \in \operatorname{\mathcal{C}}$, the restriction

\[ G|_{ \Delta ^ n \times \{ C\} }: \Delta ^ n \rightarrow \int _{\Delta ^ n} \mathscr {F} \]

carries each edge of $\Delta ^ n$ to a $V$-cocartesian edge of $\int _{\Delta ^ n} \mathscr {F}$, where $V: \int _{\Delta ^ n} \mathscr {F} \rightarrow \Delta ^ n$ is the projection map.

Proof. Let us identify $G_0$ with a morphism of simplicial sets

\[ \tau _0: \operatorname{\partial \Delta }^ n \rightarrow \operatorname{\partial \Delta }^ n \times _{ \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\partial \Delta }^ n) } \operatorname{Fun}( X, \int _{\operatorname{\partial \Delta }^ n} \mathscr {F}_0 ), \]

and let $\theta _0: \int _{ \operatorname{\partial \Delta }^{n} } \mathscr {F}_0^{\operatorname{\mathcal{C}}} \rightarrow \operatorname{\partial \Delta }^ n \times _{ \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\partial \Delta }^ n) } \operatorname{Fun}( \operatorname{\mathcal{C}}, \int _{\operatorname{\partial \Delta }^ n} \mathscr {F}_0 )$ be the comparison map of Construction 5.6.7.1. It follows from Lemma 5.6.7.2 that there exists a morphism $\sigma _0: \operatorname{\partial \Delta }^ n \rightarrow \int _{\operatorname{\partial \Delta }^ n} \mathscr {F}_0^{\operatorname{\mathcal{C}}}$ such that $\tau _0$ is isomorphic to $\theta _0 \circ \sigma _0$ as an object of the $\infty $-category

\[ \operatorname{Fun}_{ / \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\partial \Delta }^ n) }( \operatorname{\partial \Delta }^ n, \operatorname{Fun}(\operatorname{\mathcal{C}}, \int _{\operatorname{\partial \Delta }^ n} \mathscr {F}') ). \]

It follows from assumptions $(1)$ and $(2')$ that the morphism $\sigma _0$ satisfies the hypotheses of Lemma 5.6.7.3. Consequently, there exists a functor $\mathscr {F}: \Delta ^ n \rightarrow \operatorname{\mathcal{QC}}$ extending $\mathscr {F}_0$ and a functor $\sigma : \Delta ^ n \rightarrow \int _{\Delta ^ n} \mathscr {F}^{\operatorname{\mathcal{C}}}$ extending $\sigma _0$ which carries each edge of $\Delta ^ n$ to a $V$-cocartesian edge of $\int _{\Delta ^ n} \mathscr {F}^{\operatorname{\mathcal{C}}}$, where $V: \int _{\Delta ^ n} \mathscr {F}^{\operatorname{\mathcal{C}}} \rightarrow \Delta ^ n$ is the projection map. Construction 5.6.7.1 then supplies a comparison map

\[ \theta : \int _{ \Delta ^{n} } \mathscr {F}^{\operatorname{\mathcal{C}}} \rightarrow \Delta ^ n \times _{ \operatorname{Fun}(\operatorname{\mathcal{C}}, \Delta ^ n) } \operatorname{Fun}( \operatorname{\mathcal{C}}, \int _{\Delta ^ n} \mathscr {F} ) \]

extending $\theta _0$. By construction, $(\theta \circ \sigma )|_{\operatorname{\partial \Delta }^ n}$ is isomorphic to $\tau _0$ as an object of the $\infty $-category $\operatorname{Fun}_{ / \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\partial \Delta }^ n) }( \operatorname{\partial \Delta }^ n, \operatorname{Fun}(\operatorname{\mathcal{C}}, \int _{\operatorname{\partial \Delta }^ n} \mathscr {F}') )$. Applying Proposition 4.4.5.6 (and Proposition 4.4.4.9), we deduce that $\tau _0$ can be extended to a map

\[ \tau : \Delta ^ n \rightarrow \Delta ^ n \times _{ \operatorname{Fun}(\operatorname{\mathcal{C}}, \Delta ^ n) } \operatorname{Fun}( \operatorname{\mathcal{C}}, \int _{\Delta ^ n} \mathscr {F} ) \]

which is isomorphic to $\theta \circ \sigma $ as an object of the $\infty $-category $\operatorname{Fun}_{/\operatorname{Fun}(\operatorname{\mathcal{C}}, \Delta ^ n)}( \Delta ^ n, \operatorname{Fun}(\operatorname{\mathcal{C}}, \int _{\Delta ^ n} \mathscr {F} ) )$. Unwinding the definitions, we see can identify $\tau $ with a functor $G: \Delta ^ n \times \operatorname{\mathcal{C}}\rightarrow \int _{\Delta ^ n} \mathscr {F}$ which extends $G_0$ and satisfies $(2')$. $\square$

The following result is a special case of Theorem 5.6.4.9:

Lemma 5.6.7.6. Let $n$ be a positive integer, let $U: \operatorname{\mathcal{E}}\rightarrow \Delta ^ n$ be a cocartesian fibration of $\infty $-categories, and let $\operatorname{\mathcal{E}}_0 \subseteq \operatorname{\mathcal{E}}$ be the fiber product $\operatorname{\partial \Delta }^{n} \times _{\Delta ^ n} \operatorname{\mathcal{E}}$. Suppose we are given a diagram $\mathscr {F}_0: \operatorname{\partial \Delta }^ n \rightarrow \operatorname{\mathcal{QC}}$ and a morphism $G_0: \operatorname{\mathcal{E}}_0 \rightarrow \int _{\operatorname{\partial \Delta }^ n} \mathscr {F}'$ which is an equivalence of cocartesian fibrations over $\operatorname{\partial \Delta }^ n$. Then there exists a functor $\mathscr {F}: \Delta ^ n \rightarrow \operatorname{\mathcal{QC}}$ satisfying $\mathscr {F}_0 = \mathscr {F}|_{\operatorname{\partial \Delta }^ n}$ and an equivalence $G: \operatorname{\mathcal{E}}\rightarrow \int _{\Delta ^ n} \mathscr {F}$ of cocartesian fibrations over $\Delta ^ n$ satisfying $G_0 = G|_{\operatorname{\mathcal{E}}'}$.

Remark 5.6.7.7. Lemma 5.6.7.6 holds also in the case $n=0$, with the caveat that we must assume that the $\infty $-category $\operatorname{\mathcal{E}}$ is essentially small (see Example 5.6.4.6).

Proof of Lemma 5.6.7.6. Let $\operatorname{\mathcal{C}}$ denote the fiber $\{ 0\} \times _{\Delta ^ n} \operatorname{\mathcal{E}}$. By virtue of Corollary 5.2.6.22, there exists a categorical pushout diagram

5.44
\begin{equation} \begin{gathered}\label{equation:relative-universality-for-simplex} \xymatrix@R =50pt@C=50pt{ \operatorname{\partial \Delta }^ n \times \operatorname{\mathcal{C}}\ar [r] \ar [d] & \Delta ^ n \times \operatorname{\mathcal{C}}\ar [d]^{H} \\ \operatorname{\mathcal{E}}_0 \ar [r] & \operatorname{\mathcal{E}}} \end{gathered} \end{equation}

where $H|_{ \{ 0\} \times \operatorname{\mathcal{C}}}$ is the identity functor from $\operatorname{\mathcal{C}}$ to itself and, for every object $C \in \operatorname{\mathcal{C}}$, the induced map $H|_{\Delta ^ n \times \{ C\} }: \Delta ^ n \rightarrow \operatorname{\mathcal{E}}$ carries each edge of $\Delta ^ n$ to a $U$-cocartesian morphism of $\operatorname{\mathcal{E}}$. Let $G'_{0}$ denote the composite map

\[ \operatorname{\partial \Delta }^ n \times \operatorname{\mathcal{C}}\xrightarrow { H|_{ \operatorname{\partial \Delta }^ n \times \operatorname{\mathcal{C}}} } \operatorname{\mathcal{E}}_0 \xrightarrow {G_0} \int _{\operatorname{\partial \Delta }^ n} \mathscr {F}_0. \]

Applying Lemma 5.6.7.5, we conclude that $\mathscr {F}_0$ and $G'_0$ admit extensions

\[ \mathscr {F}: \Delta ^ n \rightarrow \operatorname{\mathcal{QC}}\quad \quad G': \Delta ^ n \times \operatorname{\mathcal{C}}\rightarrow \int _{\Delta ^ n} \mathscr {F} \]

having the property that, for every object $C \in \operatorname{\mathcal{C}}$, the restriction $G'|_{ \Delta ^ n \times \{ C\} }: \Delta ^ n \rightarrow \int _{\Delta ^ n} \mathscr {F}$ carries each edge of $\Delta ^ n$ to a $V$-cocartesian morphism of $\int _{\Delta ^ n} \mathscr {F}$, where $V: \int _{\Delta ^ n} \mathscr {F} \rightarrow \Delta ^ n$ is the projection map.

Since (5.44) is a categorical pushout square, the induced diagram

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{Fun}( \operatorname{\partial \Delta }^ n \times \operatorname{\mathcal{C}}, \int _{\Delta ^ n} \mathscr {F} )^{\simeq } & \operatorname{Fun}( \Delta ^ n \times \operatorname{\mathcal{C}}, \int _{\Delta ^ n} \mathscr {F} )^{\simeq } \ar [l] \\ \operatorname{Fun}( \operatorname{\mathcal{E}}_0, \int _{\Delta ^ n} \mathscr {F} )^{\simeq } \ar [u] & \operatorname{Fun}( \operatorname{\mathcal{E}}, \int _{\Delta ^ n} \mathscr {F} )^{\simeq } \ar [u] \ar [l] } \]

is a homotopy pullback diagram of Kan complexes, in which the horizontal maps are Kan fibrations (Corollary 4.4.5.4). Applying Example 3.4.1.4, we deduce that the map of fibers

\[ \xymatrix@R =50pt@C=50pt{ \{ G_0\} \times _{ \operatorname{Fun}( \operatorname{\mathcal{E}}', \int _{\Delta ^ n} \mathscr {F} )^{\simeq }} \operatorname{Fun}( \operatorname{\mathcal{E}}, \int _{\Delta ^ n} \mathscr {F} )^{\simeq } \ar [d] \\ \{ G'_0 \} \times _{ \operatorname{Fun}( \operatorname{\partial \Delta }^ n \times \operatorname{\mathcal{C}}, \int _{\Delta ^ n} \mathscr {F} )^{\simeq } } \operatorname{Fun}( \Delta ^ n \times \operatorname{\mathcal{C}}, \int _{\Delta ^ n} \mathscr {F} )^{\simeq } } \]

is a homotopy equivalence of Kan complexes. We may therefore assume (after replacing $G'$ by an isomorphic functor if necessary) that $G'$ factors as a composition

\[ \Delta ^ n \times \operatorname{\mathcal{C}}\xrightarrow {H} \operatorname{\mathcal{E}}\xrightarrow {G} \int _{\Delta ^ n} \mathscr {F}, \]

where $G|_{\operatorname{\mathcal{E}}_0} = G_0$. We will complete the proof by showing that $G$ is an equivalence of cocartesian fibrations over $\Delta ^ n$. Note that, since $G_0$ is an equivalence of cocartesian fibrations over $\operatorname{\partial \Delta }^ n$, it follows that $G$ restricts to an equivalence of $\infty $-categories $\{ i\} \times _{\Delta ^ n} \operatorname{\mathcal{E}}\rightarrow \{ i\} \times _{\Delta ^ n} \int _{\Delta ^ n} \mathscr {F}$ for $0 \leq i \leq n$. By virtue of the criterion of Proposition 5.6.2.12, it will suffice to show that $G$ carries every $U$-cocartesian morphism of $\operatorname{\mathcal{E}}$ to a $V$-cocartesian morphism of $\int _{\Delta ^ n} \mathscr {F}$. If $n > 1$, this is automatic (since $\operatorname{\mathcal{E}}_0$ contains the $1$-skeleton of $\operatorname{\mathcal{E}}$). In the case $n=1$, it follows from Remark 5.1.5.8. $\square$

Proof of Theorem 5.6.4.9. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets having essentially small fibers, let $\operatorname{\mathcal{C}}' \subseteq \operatorname{\mathcal{C}}$ be a simplicial subset having inverse image $\operatorname{\mathcal{E}}' = \operatorname{\mathcal{C}}' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$, let $U': \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{C}}'$ be the restriction $U|_{\operatorname{\mathcal{E}}'}$, and suppose we are given a commutative diagram of simplicial sets

5.45
\begin{equation} \begin{gathered}\label{equation:proof-of-relative-universality} \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}' \ar [d]^{U'} \ar [r]^-{ \widetilde{\mathscr {F}}' } & \operatorname{\mathcal{QC}}_{\operatorname{Obj}} \ar [d]^{V} \\ \operatorname{\mathcal{C}}' \ar [r]^-{ \mathscr {F}' } & \operatorname{\mathcal{QC}}} \end{gathered} \end{equation}

which exhibits $\mathscr {F}'$ as a covariant transport representation of $U'$. We wish show that (5.45) can be extended to a commutative diagram

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}' \ar [d]^{U'} \ar [r] & \operatorname{\mathcal{E}}\ar [d]^{U} \ar [r]^-{ \widetilde{\mathscr {F}} } & \operatorname{\mathcal{QC}}_{\operatorname{Obj}} \ar [d]^{V} \\ \operatorname{\mathcal{C}}' \ar [r] & \operatorname{\mathcal{C}}\ar [r]^-{\mathscr {F}} & \operatorname{\mathcal{QC}}. } \]

Let $Q$ be the collection of all triples $(\operatorname{\mathcal{C}}_0, \mathscr {F}_0, \widetilde{\mathscr {F}}_0 )$ where $\operatorname{\mathcal{C}}_0$ is a simplicial subset of $\operatorname{\mathcal{C}}$ containing $\operatorname{\mathcal{C}}'$, and $\mathscr {F}_0: \operatorname{\mathcal{C}}_0 \rightarrow \operatorname{\mathcal{QC}}$ and $\widetilde{\mathscr {F}}_0: \operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{QC}}_{\operatorname{Obj}}$ are morphisms extending $\mathscr {F}'$ and $\widetilde{\mathscr {F}}'$ respectively, for which the diagram

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\ar [d] \ar [r]^-{ \widetilde{\mathscr {F}}_0 } & \operatorname{\mathcal{QC}}_{\operatorname{Obj}} \ar [d]^{V} \\ \operatorname{\mathcal{C}}_0 \ar [r]^-{ \mathscr {F}_0 } & \operatorname{\mathcal{QC}}} \]

commutes and exhibits $\mathscr {F}_0$ as a covariant transport representation of the projection map $\operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$. We regard $Q$ as partially ordered, where $(\operatorname{\mathcal{C}}_0, \mathscr {F}_0, \widetilde{\mathscr {F}}_0 ) \leq (\operatorname{\mathcal{C}}_1, \mathscr {F}_1, \widetilde{\mathscr {F}}_1 )$ when $\operatorname{\mathcal{C}}_0$ is contained in $\operatorname{\mathcal{C}}_1$, $\mathscr {F}_0 = \mathscr {F}_1|_{\operatorname{\mathcal{C}}_0}$, and $\widetilde{\mathscr {F}}_0 = \widetilde{\mathscr {F}}_{1}|_{\operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}}$. It follows from Zorn's lemma that $Q$ contains a maximal element $( \operatorname{\mathcal{C}}_{\mathrm{max}}, \mathscr {F}_{\mathrm{max}}, \widetilde{\mathscr {F}}_{\mathrm{max}} )$.

We will complete the proof by showing that $\operatorname{\mathcal{C}}_{\mathrm{max}} = \operatorname{\mathcal{C}}$. Suppose otherwise. Then there exists some $n$-simplex $\sigma : \Delta ^ n \rightarrow \operatorname{\mathcal{C}}$ which is not contained in $\operatorname{\mathcal{C}}_{\mathrm{max}}$. Choosing $n$ as small as possible, we can assume that the restriction $\sigma |_{ \operatorname{\partial \Delta }^ n}$ factors through $\operatorname{\mathcal{C}}_{\mathrm{max}}$. Let $\operatorname{\mathcal{C}}_{0}$ denote the union of $\operatorname{\mathcal{C}}_{\mathrm{max}}$ with the image of $\sigma $, so that we have a pushout diagram of simplicial sets

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\partial \Delta }^ n \ar [r] \ar [d] & \Delta ^ n \ar [d]^{\sigma } \\ \operatorname{\mathcal{C}}_{\mathrm{max}} \ar [r] & \operatorname{\mathcal{C}}_0. } \]

We will obtain a contradiction by showing that there exists an element $(\operatorname{\mathcal{C}}_0, \mathscr {F}_0, \widetilde{\mathscr {F}}_0) \in Q$ satisfying $( \operatorname{\mathcal{C}}_{\mathrm{max}}, \mathscr {F}_{\mathrm{max}}, \widetilde{\mathscr {F}}_{\mathrm{max}} ) \leq (\operatorname{\mathcal{C}}_0, \mathscr {F}_0, \widetilde{\mathscr {F}}_0)$. For this, we are reduced to proving Theorem 5.6.4.9 in the special case where $\operatorname{\mathcal{C}}= \Delta ^ n$ and $\operatorname{\mathcal{C}}' = \operatorname{\partial \Delta }^ n$. This follows from Lemma 5.6.7.6 when $n > 0$, and Remark 5.6.7.7 in the case $n=0$. $\square$