# Kerodon

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

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.8). 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.8. $\square$