$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Variant 4.6.4.22. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category, let $F: K \rightarrow \operatorname{\mathcal{C}}$ be a diagram, and suppose we are given a pair of diagrams
\[ e_0, e_1: J \rightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{Fun}(K,\operatorname{\mathcal{C}}) } \{ F\} , \]
which we identify with morphisms of simplicial sets $F_0, F_1: J \diamond K \rightarrow \operatorname{\mathcal{C}}$ extending $F$ (Remark 4.6.4.9). The following conditions are equivalent:
- $(1)$
The diagrams $e_0$ and $e_1$ are isomorphic when regarded as objects of the diagram $\infty $-category
\[ \operatorname{Fun}( J, \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{Fun}(K,\operatorname{\mathcal{C}})} \{ F\} ). \]
- $(2)$
The diagrams $F_0$ and $F_1$ are isomorphic when regarded as objects of the $\infty $-category
\[ \operatorname{Fun}_{K/}( J \diamond K, \operatorname{\mathcal{C}}). \]
Proof.
We proceed as in Lemma 4.6.4.21. Choose a categorical mapping cylinder
\[ J \coprod J \xrightarrow {(s_0, s_1)} \overline{J} \xrightarrow {\pi } J \]
for the simplicial set $J$ (Definition 4.6.3.3). Using Remark 4.5.8.7, we see that the induced diagram
\[ (J \diamond K) \coprod _{K} (J \diamond K) \xrightarrow {(s'_0, s'_1)} \overline{J} \diamond K \xrightarrow {\pi '} J \diamond K \]
is a categorical mapping cylinder for the simplicial set $J \diamond K$ relative to $K$. Using the criterion of Corollary 4.6.3.11, we see that $(1)$ and $(2)$ can be reformulated as follows:
- $(1')$
There exists a diagram $\overline{e}: \overline{J} \rightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{Fun}(K,\operatorname{\mathcal{C}})} \{ F\} $ satisfying $\overline{e} \circ s_0 = e_0$ and $\overline{e} \circ s_1 = e_1$.
- $(2')$
There exists a diagram $\overline{F}: \overline{J} \diamond K \rightarrow \operatorname{\mathcal{C}}$ satisfying $\overline{F} \circ s'_0 = F_0$ and $\overline{F} \circ s'_1 = F_1$.
The equivalence of $(1')$ and $(2')$ follows from Remark 4.6.4.9.
$\square$