Kerodon

Proof. Set $\operatorname{\mathcal{C}}= X(0)$, $\operatorname{\mathcal{D}}= X(1)$, and let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be the functor $X(0 < 1)$. Using the isomorphism $\Lambda ^{n}_{0} \simeq ( \operatorname{\partial \Delta }^{n-1} )^{\triangleleft }$, we can identify $X$ with a diagram $\sigma _0: \operatorname{\partial \Delta }^{n-1} \rightarrow \operatorname{\mathcal{QC}}_{ \operatorname{\mathcal{C}}/ }$. To complete the proof, it will suffice to show that $\sigma _0$ can be extended to an $(n-1)$-simplex of $\operatorname{\mathcal{QC}}_{ \operatorname{\mathcal{C}}/ }$. Let us identify the objects of the $\infty $-category $\operatorname{\mathcal{QC}}_{ \operatorname{\mathcal{C}}/ }$ with pairs $( \operatorname{\mathcal{E}}, G )$, where $\operatorname{\mathcal{E}}$ is a small $\infty $-category and $G: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{E}}$ is a functor. Let $\operatorname{\mathcal{QC}}_{ \operatorname{\mathcal{C}}/ }^{W}$ denote the full subcategory of $\operatorname{\mathcal{QC}}_{ \operatorname{\mathcal{C}}/ }$ spanned by those pairs $(\operatorname{\mathcal{E}},G)$, where the functor $G$ carries each element of $W$ to an isomorphism in $\operatorname{\mathcal{E}}$. It follows from assumption $(1)$ that the diagram $\sigma _0$ factors through the subcategory $\operatorname{\mathcal{QC}}_{ \operatorname{\mathcal{C}}/ }^{W} \subseteq \operatorname{\mathcal{QC}}_{\operatorname{\mathcal{C}}/}$. To prove the existence of $\sigma $, it will suffice (by virtue of Corollary 4.6.7.13) to show that $\sigma _0( 0 ) = (\operatorname{\mathcal{D}}, F)$ is an initial object of the $\infty $-category $\operatorname{\mathcal{QC}}_{\operatorname{\mathcal{C}}/ }^{W}$. Fix another object $(\operatorname{\mathcal{E}}, G) \in \operatorname{\mathcal{QC}}_{\operatorname{\mathcal{C}}/ }^{W}$; we wish to show that the morphism space $\operatorname{Hom}_{\operatorname{\mathcal{QC}}_{\operatorname{\mathcal{C}}/}^{W}}( (\operatorname{\mathcal{D}}, F), (\operatorname{\mathcal{E}}, G) ) = \operatorname{Hom}_{ \operatorname{\mathcal{QC}}_{\operatorname{\mathcal{C}}/} }( (\operatorname{\mathcal{D}}, F), (\operatorname{\mathcal{E}}, G) )$ is a contractible Kan complex. Using Corollary 4.6.9.18 and Remark 5.5.4.6, we can identify $\operatorname{Hom}_{ \operatorname{\mathcal{QC}}_{\operatorname{\mathcal{C}}/} }( (\operatorname{\mathcal{D}}, F), (\operatorname{\mathcal{E}}, G) )$ with the homotopy fiber of the map of Kan complexes

over the vertex $G \in \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})^{\simeq }$. Assumption $(2)$ guarantees that this map is a homotopy equivalence onto the summand of $\operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})^{\simeq }$ spanned by those functors $\operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{E}}$ which carry each element of $W$ to an isomorphism in $\operatorname{\mathcal{E}}$. It will therefore suffice to show that this summand contains the functor $G$, which follows from the definition of $\operatorname{\mathcal{QC}}_{\operatorname{\mathcal{C}}/}^{W}$. $\square$

Proof. Fix an integer $n > 0$, and suppose we are given a diagram $\mathscr {F}_0: \operatorname{\mathcal{C}}\star \operatorname{\partial \Delta }^{n} \rightarrow \operatorname{\mathcal{QC}}$ for which the restriction $\mathscr {F}_0|_{ \operatorname{\mathcal{C}}\star \{ 0\} }$ coincides with $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleright } }$. We wish to show that $\mathscr {F}_0$ can be extended to a functor $\mathscr {F}: \operatorname{\mathcal{C}}\star \Delta ^ n \rightarrow \operatorname{\mathcal{QC}}$. Applying Lemma 5.6.7.1, we can choose a pullback diagram

where $\overline{U}^{-}$ is a cocartesian fibration having covariant transport representation $\mathscr {F}_0$. For $0 \leq i \leq n$, let us write $\overline{\operatorname{\mathcal{E}}}^{-}_{i}$ for the $\infty $-category given by the fiber of $\overline{U}^{-}$ on the vertex $i \in \operatorname{\partial \Delta }^{n}$.

Fix an auxiliary symbol $c$, so that the projection map $\operatorname{\mathcal{C}}\rightarrow \{ c\} $ induces a cocartesian fibration of $\infty $-categories $V^{+}: \operatorname{\mathcal{C}}\star \Delta ^{n} \rightarrow \{ c\} \star \Delta ^ n$ (this follows by repeated application of Lemma 5.2.3.17). Note that $V^{+}$ restricts to a morphism of simplicial sets $V^{-}: \operatorname{\mathcal{C}}\star \operatorname{\partial \Delta }^{n} \rightarrow \{ c\} \star \operatorname{\partial \Delta }^{n}$ which is a pullback of $V^{+}$, and therefore also a cocartesian fibration (Remark 5.1.4.6). Applying Proposition 5.1.4.13, we deduce that the composite map $( V^{-} \circ \overline{U}^{-} ): \overline{\operatorname{\mathcal{E}}}^{-} \rightarrow \{ c\} \star \operatorname{\partial \Delta }^{n} \simeq \Lambda ^{n+1}_{0}$ is also a cocartesian fibration.

Let $\mathscr {G}_0: \{ c\} \star \operatorname{\partial \Delta }^{n} \rightarrow \operatorname{\mathcal{QC}}$ be a covariant transport representation for the cocartesian fibration $V^{-} \circ \overline{U}^{-}$. Let us identify $\mathscr {G}_{0}(c)$ with the $\infty $-category $\operatorname{\mathcal{E}}$. For $0 \leq i \leq n$, we can identify $\mathscr {G}_{0}(i)$ with the $\infty $-category $\overline{\operatorname{\mathcal{E}}}^{-}_{i}$ for $0 \leq i \leq n$, and the restriction of $\mathscr {G}_{0}$ to the edge $\{ c\} \star \{ i\} $ with a functor $G_ i: \operatorname{\mathcal{E}}\rightarrow \overline{\operatorname{\mathcal{E}}}^{-}_{i}$. Applying Example 7.4.3.4 (and Remark 5.6.5.8), we see that $G_{i}$ is a covariant refraction diagram for the cocartesian fibration

In particular, each of the functors $G_{i}$ carries elements of $W$ to isomorphisms in the $\infty $-category $\overline{\operatorname{\mathcal{E}}}^{-}_{i}$ (Remark 7.4.3.5). Moreover, the functor $G_0$ is isomorphic to $\mathrm{Rf}$ (Proposition 7.4.3.3), and therefore exhibits $\overline{\operatorname{\mathcal{E}}}^{-}_{0} = \overline{\operatorname{\mathcal{E}}}_{0}$ as a localization of $\operatorname{\mathcal{E}}$ with respect to $W$ (Exercise 6.3.1.11). Applying Lemma 7.4.4.1, we can extend $\mathscr {G}_0$ to a diagram $\mathscr {G}: \{ c\} \star \Delta ^{n} \rightarrow \operatorname{\mathcal{QC}}$. Using Lemma 5.6.7.1, we can choose a pullback diagram

where $T$ is a cocartesian fibration having covariant transport representation $\mathscr {G}$. Note that we can write $T$ uniquely as a composition

where $\overline{U}^{+}$ is a morphism of simplicial sets which fits into a pullback diagram

We will show that the morphism $\overline{U}^{+}$ is a cocartesian fibration. Assuming this, we can complete the proof by applying Corollary 5.6.5.11 to extend $\mathscr {F}_0$ to a diagram $\mathscr {F}: \operatorname{\mathcal{C}}\star \Delta ^{n} \rightarrow \operatorname{\mathcal{QC}}$ (which is a covariant transport representation for the cocartesian fibration $\overline{U}^{+}$).

We first prove that $\overline{U}^{+}$ is an inner fibration of simplicial sets. Suppose we are given integers $0 < i < m$; we wish to show that every lifting problem

admits a solution. If $\overline{\sigma }$ factors through $\operatorname{\mathcal{C}}$, then a solution exists by virtue of the fact that $U$ is an inner fibration. Let us therefore assume that $\overline{\sigma }$ does not factor through $\operatorname{\mathcal{C}}$. Since $T$ is an inner fibration, we can extend $\sigma _0$ to an $n$-simplex $\sigma $ of $\overline{\operatorname{\mathcal{E}}}^{+}$ satisfying $T \circ \sigma = V^{+} \circ \overline{\sigma }$. We claim that the $n$-simplex $\sigma $ solves the lifting problem (7.47). Set $\overline{\sigma }' = \overline{U}^{+} \circ \sigma $; we wish to show that $\overline{\sigma }'$ coincides with $\overline{\sigma }$ (as $m$-simplices of the simplicial set $\operatorname{\mathcal{C}}\star \Delta ^{n}$). Note that we have $V^{+} \circ \overline{\sigma } = V^{+} \circ \overline{\sigma }'$. It follows that $\overline{\sigma }$ and $\overline{\sigma }'$ both carry the final vertex $m \in \Delta ^{m}$ to the same vertex of $\Delta ^{n} \subseteq \operatorname{\mathcal{C}}\star \Delta ^{n}$. Consequently, it will suffice to show that $\overline{\sigma }$ and $\overline{\sigma }'$ agree when restricted to the face $\Delta ^{m-1} \subseteq \Delta ^{m}$. This follows from the commutativity of the diagram (7.47), since $\Delta ^{m-1}$ is contained in the horn $\Lambda ^{m}_{i} \subseteq \Delta ^{m}$.

Fix an object $X$ of the $\infty $-category $\overline{\operatorname{\mathcal{E}}}^{+}$ having image $\overline{X} = \overline{U}^{+}(X)$ and a morphism $\overline{e}: \overline{X} \rightarrow \overline{Y}$ in the $\infty $-category $\operatorname{\mathcal{C}}\star \Delta ^{m}$. We will complete the proof by showing that $\overline{e}$ can be lifted to an $\overline{U}^{+}$-cocartesian morphism $e: X \rightarrow Y$ of $\operatorname{\mathcal{E}}$. If $\overline{X}$ and $\overline{Y}$ belong to $\operatorname{\mathcal{C}}$, then we take $e: X \rightarrow Y$ to be a $U$-cocartesian morphism of $\operatorname{\mathcal{E}}$ satisfying $U(e) = \overline{e}$ (which exists by virtue of our assumption that $U$ is a cocartesian fibration). Otherwise, we take $e: X \rightarrow Y$ to be a $T$-cocartesian morphism of $\overline{\operatorname{\mathcal{E}}}^{+}$ satisfying $T(e) = V^{+}( \overline{e} )$ (which exists by virtue of the fact that $T$ is a cocartesian fibration). In either case, we will prove that the morphism $e$ is $\overline{U}^{+}$-cocartesian by verifying the criterion of Proposition 5.1.2.1. Choose another object $Z \in \overline{\operatorname{\mathcal{E}}}^{+}$ having image $\overline{Z} = \overline{U}^{+}(Z)$; we wish to show that the diagram of Kan complexes

is a homotopy pullback square. We consider several cases:

• Suppose first that the object $\overline{Z}$ belongs to $\operatorname{\mathcal{C}}$. If $\overline{X}$ and $\overline{Y}$ belong to $\operatorname{\mathcal{C}}$, then we deduce that (7.48) is a homotopy pullback square by applying Proposition 5.1.2.1 to the cocartesian fibration $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ (since, by construction, the morphism $e$ is $U$-cocartesian). Otherwise, each of the Kan complexes appearing in the diagram (7.48) is empty, so there is nothing to prove.

• Suppose that the objects $\overline{Y}$ and $\overline{Z}$ belong to $\Delta ^{n}$. In this case, we deduce that (7.48) is a homotopy pullback square by applying Proposition 5.1.2.1 to the cocartesian fibration $T: \overline{\operatorname{\mathcal{E}}}^{+} \rightarrow \{ c\} \star \Delta ^ n$ (since, by construction, the morphism $e$ is $T$-cocartesian).

• Suppose that the objects $\overline{X}$ and $\overline{Y}$ belong to $\operatorname{\mathcal{C}}$, but the object $\overline{Z}$ belongs to $\Delta ^{n}$. In this case, the Kan complexes on the bottom row of (7.48) are contractible (see Example 4.6.1.6; in fact, they are both isomorphic to $\Delta ^{0}$). In particular, the bottom horizontal map is a homotopy equivalence. To show that (7.48) is a homotopy pullback square, we must show that the upper horizontal map is also a homotopy equivalence (Corollary 3.4.1.5). In other words, we must show that composition with the homotopy class $[e]$ induces an isomorphism $\theta : \operatorname{Hom}_{\overline{\operatorname{\mathcal{E}}}^{+} }( Y, Z) \rightarrow \operatorname{Hom}_{ \overline{\operatorname{\mathcal{E}}}^{+} }(X, Z )$ in the homotopy category $\mathrm{h} \mathit{\operatorname{Kan}}$ (see Notation 4.6.9.15). Let

  \[ G: \operatorname{\mathcal{E}}= \{ c\} \times _{ \{ c\} \star \Delta ^{n} } \overline{\operatorname{\mathcal{E}}}^{+} \rightarrow \{ \overline{Z} \} \times _{ \{ c\} \star \Delta ^{n} } \overline{\operatorname{\mathcal{E}}}^{+} = \overline{\operatorname{\mathcal{E}}}^{+}_{ \overline{Z} } \]

  be given by covariant transport for the cocartesian fibration $T$. Using Corollary 5.1.2.3, we can identify $\theta $ with the morphism $\operatorname{Hom}_{ \overline{\operatorname{\mathcal{E}}}^{+}_{ \overline{Z} }}( G(Y), Z) \rightarrow \operatorname{Hom}_{ \overline{\operatorname{\mathcal{E}}}^{+}_{ \overline{Z} }}( G(X), Z)$ given by precomposition with the morphism $G(e): G(X) \rightarrow G(Y)$. Since the morphism $e$ is $U$-cocartesian, its image $G(e)$ is an isomorphism in the $\infty $-category $\overline{\operatorname{\mathcal{E}}}^{+}_{\overline{Z}}$, so that $\theta $ is a homotopy equivalence as desired.

Proof of Lemma 7.4.4.3. Fix an $\infty $-category $\operatorname{\mathcal{D}}$; we wish to show that precomposition with $\widetilde{F}$ induces an equivalence of $\infty $-categories $\operatorname{Fun}( \operatorname{\mathcal{E}}[ W^{-1} ], \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{E}}_0[W_0^{-1}], \operatorname{\mathcal{D}})$ (see Notation 6.3.1.1). Corollary 5.6.7.6 guarantees that $\widetilde{F}$ is a categorical equivalence of simplicial sets, so that precomposition with $\widetilde{F}$ induces an equivalence of $\infty $-categories $\operatorname{Fun}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{D}})$. It will therefore suffice to prove the following:

$(\ast )$

Let $G: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}$ be a morphism of simplicial sets with the property that $G \circ \widetilde{F}$ carries every $U_0$-cocartesian edge of $\operatorname{\mathcal{E}}_0$ to an isomorphism in $\operatorname{\mathcal{D}}$. Then $G$ carries each $U$-cocartesian edge of $\operatorname{\mathcal{E}}$ to an isomorphism in $\operatorname{\mathcal{D}}$.

Let us henceforth regard the $\infty $-category $\operatorname{\mathcal{D}}$ and the functor $G: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}$ as fixed. For every morphism of simplicial sets $K \rightarrow \operatorname{\mathcal{C}}$, let $\operatorname{\mathcal{E}}_{K}$ denote the fiber product $K \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$, let $U_{K}: \operatorname{\mathcal{E}}_{K} \rightarrow K$ be the projection map, and let $G_{K}$ denote the restriction of $G$ to $\operatorname{\mathcal{E}}_{K}$. Let us say that a monomorphism of simplicial sets $K' \hookrightarrow K$ is good if, for every morphism $K \rightarrow \operatorname{\mathcal{C}}$ with the property that $G_{K'}$ carries $U_{K'}$-cocartesian morphisms of $\operatorname{\mathcal{E}}_{K'}$ to isomorphisms in $\operatorname{\mathcal{D}}$, the morphism $G_{K}$ carries $U_{K}$-cocartesian morphisms of $\operatorname{\mathcal{E}}_{K}$ to isomorphisms in $\operatorname{\mathcal{D}}$. To prove $(\ast )$, it will suffice to show that $F: \operatorname{\mathcal{C}}_0 \rightarrow \operatorname{\mathcal{C}}$ is weakly saturated. It is not difficult to see that the collection of good morphisms is weakly saturated, in the sense of Definition 1.5.4.12. It will therefore suffice to show that the horn inclusion $\Lambda ^{n}_{i} \hookrightarrow \Delta ^ n$ is good for $0 < i < n$. In other words, it will suffice to prove $(\ast )$ in the special case where $\operatorname{\mathcal{C}}= \Delta ^ n$ is a standard simplex and $F: \Lambda ^{n}_{i} \hookrightarrow \Delta ^ n$ is the inclusion of an inner horn.

If $n \geq 3$, then every edge of $\operatorname{\mathcal{C}}= \Delta ^ n$ is contained in the horn $\Lambda ^{n}_{i}$; it follows that the morphism $\widetilde{F}: \operatorname{\mathcal{E}}_0 \rightarrow \operatorname{\mathcal{E}}$ induces a bijection $W_0 \xrightarrow {\sim } W$, so there is nothing to prove. We may therefore assume without loss of generality that $n=2$. Let $w: X \rightarrow Z$ be a $U$-cocartesian of $\operatorname{\mathcal{E}}$ which does not belong to the simplicial subset $\operatorname{\mathcal{E}}_0 = \Lambda ^{2}_{1} \times _{\Delta ^2} \operatorname{\mathcal{E}}$, so that $U(X) = 0$ and $U(Z) = 2$. Since $U$ is a cocartesian fibration, we can choose a $U$-cocartesian morphism $u: X \rightarrow Y$ with $U(Y) = 1$. Our assumption that $u$ is $U$-cocartesian guarantees that there exists a $2$-simplex of $\operatorname{\mathcal{E}}'$ whose boundary is indicated in the diagram

Invoking Corollary 5.1.2.4, we see that $v$ is also $U$-cocartesian, so that $u$ and $v$ can be regarded as elements of $W_0$. It now suffices to observe that if $G: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}$ is any functor which carries both $u$ and $v$ to isomorphisms in $\operatorname{\mathcal{D}}$, then $G$ also carries $w$ to an isomorphism in $\operatorname{\mathcal{D}}$. $\square$

Proof of Theorem 7.4.3.6. Suppose we are given a pullback diagram of small simplicial sets

where $U$ and $\overline{U}$ are cocartesian fibrations. Let $W$ denote the collection of all $U$-cocartesian edges of $\operatorname{\mathcal{E}}$, let ${\bf 1}$ denote the cone point of $\operatorname{\mathcal{C}}^{\triangleright }$, let $\mathrm{Rf}: \operatorname{\mathcal{E}}\rightarrow \overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$ be a covariant refraction diagram (Definition 7.4.3.1). Assume first that $\mathrm{Rf}$ exhibits the $\infty $-category $\overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$ as a localization of $\operatorname{\mathcal{E}}$ with respect to $W$. We wish to show that the covariant transport representation $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleright } }: \operatorname{\mathcal{C}}^{\triangleright } \rightarrow \operatorname{\mathcal{QC}}$ is a colimit diagram in the $\infty $-category $\operatorname{\mathcal{QC}}$.

Using Corollary 4.1.3.3, we can choose an inner anodyne morphism $\operatorname{\mathcal{C}}\hookrightarrow \operatorname{\mathcal{C}}'$, where $\operatorname{\mathcal{C}}'$ is an $\infty $-category. Note that the induced map $\operatorname{\mathcal{C}}^{\triangleright } \hookrightarrow \operatorname{\mathcal{C}}'^{\triangleright }$ is also inner anodyne (Proposition 4.3.6.4). Applying Corollary 5.6.7.3, we can realize $\overline{U}$ as the pullback of a cocartesian fibration of $\infty $-categories $\overline{U}': \overline{\operatorname{\mathcal{E}}}' \rightarrow \operatorname{\mathcal{C}}'^{\triangleright }$. Form a pullback diagram

and let $W'$ denote the collection of all $U'$-cocartesian morphisms of $\operatorname{\mathcal{E}}'$. Using Proposition 7.4.3.3, we can choose a covariant refraction diagram $\mathrm{Rf}': \operatorname{\mathcal{E}}' \rightarrow \overline{\operatorname{\mathcal{E}}}'_{{\bf 1}} = \overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$ for the cocartesian fibration $\overline{U}'$. Note that the restriction $\mathrm{Rf}|_{\operatorname{\mathcal{E}}}$ is a covariant refraction collapse diagram for the cocartesian fibration $\overline{U}$, and is therefore isomorphic to $\mathrm{Rf}$ as an object of the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{E}}, \overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$. It follows that $\mathrm{Rf}'|_{\operatorname{\mathcal{E}}}$ also exhibits the $\infty $-category $\overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$ as a localization of $\operatorname{\mathcal{E}}$ with respect to $W$ (Exercise 6.3.1.11). Applying Lemma 7.4.4.3, we see that $\mathrm{Rf}$ exhibits $\overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$ as a localization of $\operatorname{\mathcal{E}}'$ with respect to $W$.

Using Corollary 5.6.5.11, we can extend $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleright } }$ to a functor

which is a covariant transport representation for $\overline{U}'$. Applying Proposition 7.4.4.2 to the diagram of $\infty $-categories (7.49), we deduce that $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}}' / \operatorname{\mathcal{C}}'^{\triangleright } }$ is a colimit diagram in the $\infty $-category $\operatorname{\mathcal{QC}}$. Since the inclusion map $\operatorname{\mathcal{C}}\hookrightarrow \operatorname{\mathcal{C}}'$ is right cofinal (Proposition 7.2.1.3), it follows that $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleright } }$ is also a colimit diagram in $\operatorname{\mathcal{QC}}$, as desired.

We now prove the converse. Assume that the covariant transport representation $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleright } }$ is a colimit diagram in the $\infty $-category $\operatorname{\mathcal{QC}}$; we wish to show that the covariant refraction diagram $\mathrm{Rf}$ exhibits $\overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$ as a localization of $\operatorname{\mathcal{E}}$ with respect to $W$. By virtue of Proposition 7.4.3.9 (and Remark 7.4.3.10), we can choose another pullback diagram

where $U^{+}$ is a cocartesian fibration for which the covariant refraction diagram $\mathrm{Rf}^{+}: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{E}}^{+}_{ {\bf 1} }$ exhibits $\operatorname{\mathcal{E}}^{+}_{ {\bf 1} }$ as a localization of $\operatorname{\mathcal{E}}$ with respect to $W$. Applying Corollary 5.6.5.11, we see that $U^{+}$ admits a covariant transport representation $\operatorname{Tr}_{ \operatorname{\mathcal{E}}^{+} / \operatorname{\mathcal{C}}^{\triangleright } }: \operatorname{\mathcal{C}}^{\triangleright } \rightarrow \operatorname{\mathcal{QC}}$ satisfying $(\operatorname{Tr}_{ \operatorname{\mathcal{E}}^{+} / \operatorname{\mathcal{C}}^{\triangleright } })|_{\operatorname{\mathcal{C}}} = (\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleright } })|_{\operatorname{\mathcal{C}}}$. The first part of the proof shows that $\operatorname{Tr}_{ \operatorname{\mathcal{E}}^{+} / \operatorname{\mathcal{C}}^{\triangleright } }$ is also a colimit diagram in the $\infty $-category $\operatorname{\mathcal{QC}}$, and is therefore isomorphic to $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleright } }$ as an object of the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{C}}^{\triangleright }, \operatorname{\mathcal{QC}})$. Applying Theorem 5.6.0.2, we see $\overline{U}: \overline{\operatorname{\mathcal{E}}} \rightarrow \operatorname{\mathcal{C}}^{\triangleright }$ and $U^{+}: \operatorname{\mathcal{E}}^{+} \rightarrow \operatorname{\mathcal{C}}^{\triangleright }$ are equivalent as cocartesian fibrations over $\operatorname{\mathcal{C}}^{\triangleright }$. Applying Exercise 7.4.3.8, we conclude that $\mathrm{Rf}$ also exhibits $\overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$ as a localization of $\operatorname{\mathcal{E}}$ with respect to $W$, as desired. $\square$