# Kerodon

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

Corollary 7.2.1.22. Let $\operatorname{\mathcal{C}}$ be an $\infty$-category and suppose we are given a pair of diagrams $f_0, f_1: K \rightarrow \operatorname{\mathcal{C}}$ indexed by a simplicial set $K$. Suppose that $f_0$ and $f_1$ are isomorphic as objects of the $\infty$-category $\operatorname{Fun}(K, \operatorname{\mathcal{C}})$. Then $f$ is left cofinal if and only if $g$ is left cofinal.

Proof. Let $\operatorname{Isom}(\operatorname{\mathcal{C}}) \subseteq \operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}})$ be the full subcategory spanned by the isomorphisms of $\operatorname{\mathcal{C}}$ (see Example 4.4.1.13). Let $\operatorname{ev}_0, \operatorname{ev}_1: \operatorname{Isom}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{C}}$ be the morphisms given by evaluation at the vertices $0,1 \in \Delta ^1$, so that $\operatorname{ev}_0$ and $\operatorname{ev}_1$ are trivial Kan fibrations (Corollary 4.4.5.10). Fix an isomorphism of $f_0$ with $f_1$, which we identify with a diagram $F: K \rightarrow \operatorname{Isom}(\operatorname{\mathcal{C}})$ satisfying $\operatorname{ev}_0 \circ F = f_0$ and $\operatorname{ev}_1 \circ F = f_1$. Applying Corollary 7.2.1.21 to the diagram

$\xymatrix@R =50pt@C=50pt{ K \ar [r]^-{F} \ar [d]^{\operatorname{id}} & \operatorname{Isom}(\operatorname{\mathcal{C}}) \ar [d]^{ \operatorname{ev}_0 } \\ K \ar [r]^-{f_0} & \operatorname{\mathcal{C}}, }$

we deduce that $f_0$ is left cofinal if and only if $F$ is left cofinal. By the same reasoning, this is equivalent to the condition that $f_1$ is left cofinal. $\square$