Kerodon

Proof. Using Corollary 4.1.3.3, we can choose an inner anodyne morphism $i: K \hookrightarrow \operatorname{\mathcal{K}}$, where $\operatorname{\mathcal{K}}$ is an $\infty $-category. It follows that the induced map $i^{\triangleright }: K^{\triangleright } \hookrightarrow \operatorname{\mathcal{K}}^{\triangleright }$ is also inner anodyne (Example 4.3.6.7), so that the restriction map $\operatorname{Fun}( \operatorname{\mathcal{K}}^{\triangleright }, \operatorname{\mathcal{C}}) \rightarrow \operatorname{Fun}(K^{\triangleright }, \operatorname{\mathcal{D}})$ is a trivial Kan fibration of simplicial sets (Proposition 1.5.7.6). We can therefore lift $\alpha $ to a natural transformation $\overline{\alpha }: \overline{F}_0 \rightarrow \overline{F}_1$ between natural transformations $\overline{F}_0, \overline{F}_1: \operatorname{\mathcal{K}}^{\triangleright } \rightarrow \operatorname{\mathcal{C}}$. Since $i^{\triangleright }$ is bijective on vertices, the natural transformation $\overline{\alpha }$ carries each object of $\operatorname{\mathcal{K}}^{\triangleright }$ to a $U$-cocartesian morphism of $\operatorname{\mathcal{C}}$. The morphism $i^{\triangleright }$ is right cofinal (Corollary 7.2.1.13), so Corollary 7.2.2.2 guarantees that $F_0$ is a $U$-colimit diagram if and only if $\overline{F}_0$ is a $U$-colimit diagram. Similarly, $F_1$ is a $U$-colimit diagram if and only if $\overline{F}_1$ is a $U$-colimit diagram. We may therefore replace $\alpha $ by $\overline{\alpha }$ in the statement of Proposition 7.3.9.1, and thereby reduce to the case where $K = \operatorname{\mathcal{K}}$ is an $\infty $-category.

Let us identify $\alpha $ with a functor of $\infty $-categories $F: \Delta ^1 \times \operatorname{\mathcal{K}}^{\triangleright } \rightarrow \operatorname{\mathcal{C}}$. For each object $x \in \operatorname{\mathcal{K}}^{\triangleright }$, we can regard $\Delta ^1 \times \{ x\} $ with a morphism $e_{x}: (0,x) \rightarrow (1,x)$ in the $\infty $-category $\Delta ^1 \times \operatorname{\mathcal{K}}^{\triangleright }$. By construction, the functor $F$ carries each $e_{x}$ to the $U$-cocartesian morphism $\alpha _ x$ of $\operatorname{\mathcal{C}}$. By virtue of Proposition 4.6.7.22, $e_{x}$ is final when viewed as an object of the $\infty $-category

so that $F$ is $U$-left Kan extended from $\{ 0\} \times \operatorname{\mathcal{K}}^{\triangleright }$ at $(1,x)$ (Corollary 7.2.2.5). Allowing the object $x$ to vary, we see that the functor $F$ is $U$-left Kan extended from $\{ 0\} \times \operatorname{\mathcal{K}}^{\triangleright }$.

We now prove $(1)$. Suppose that $F_0$ is a $U$-colimit diagram. Then $F_0$ is $U$-left Kan extended from $\operatorname{\mathcal{K}}$ (Example 7.3.3.9). Applying Proposition 7.3.8.6, we see that the functor $F$ is $U$-left Kan extended from $\{ 0\} \times \operatorname{\mathcal{K}}$, and therefore from the larger subcategory $\Delta ^1 \times \operatorname{\mathcal{K}}\subseteq \Delta ^1 \times \operatorname{\mathcal{K}}^{\triangleright }$. It follows that the composite map

is a $U$-colimit diagram. Since the inclusion map $\{ 1\} \times \operatorname{\mathcal{K}}\hookrightarrow \Delta ^1 \times \operatorname{\mathcal{K}}$ is right cofinal (Proposition 7.2.1.3), Corollary 7.2.2.2 guarantees that $F_1 = F|_{ \{ 1\} \times \operatorname{\mathcal{K}}^{\triangleright } }$ is also a $U$-colimit diagram.

We now prove $(2)$. Let $\pi : \operatorname{\mathcal{K}}^{\triangleright } \rightarrow \Delta ^1$ be the functor carrying $\operatorname{\mathcal{K}}$ to the vertex $0 \in \Delta ^1$ and the cone point $v \in \operatorname{\mathcal{K}}^{\triangleright }$ to the vertex $1 \in \Delta ^1$, and let $G: \operatorname{\mathcal{K}}^{\triangleright } \rightarrow \operatorname{\mathcal{C}}$ be the functor given by the composition

Note that there is a natural transformation $\beta : F_0 \rightarrow G$ which is the identity when restricted to $\operatorname{\mathcal{K}}$ and which carries the cone point $v$ to the morphism $\alpha _{v}: F_0(v) \rightarrow F_1(v) = G(v)$. If $\alpha _{v}$ is an isomorphism, then the natural transformation $\beta $ is also an isomorphism (Theorem 4.4.4.4). Consequently, to show that $F_0$ is a $U$-colimit diagram, it will suffice to show that $G$ is a $U$-colimit diagram (Proposition 7.1.5.13). Arguing as above, we see that the functor $F|_{ \Delta ^1 \times \operatorname{\mathcal{K}}}$ is $U$-left Kan extended from the full subcategory $\{ 0\} \times \operatorname{\mathcal{K}}\subseteq \Delta ^1 \times \operatorname{\mathcal{K}}$. Applying Proposition 7.3.8.1, we see that $G$ is a $U$-colimit diagram if and only if the composite map

is a $U$-colimit diagram. By virtue of Corollary 7.2.2.2, this is equivalent to the requirement that $F_1$ is a $U$-colimit diagram. $\square$