# Kerodon

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

Proposition 7.1.7.13. Let $U: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a functor of $\infty$-categories and let $\overline{u}, \overline{v}': K^{\triangleleft } \rightarrow \operatorname{\mathcal{C}}$ be diagrams which are isomorphic when viewed as objects of the $\infty$-category $\operatorname{Fun}(K^{\triangleleft }, \operatorname{\mathcal{C}})$. Then $\overline{u}$ is a $U$-limit diagram if and only if $\overline{v}$ is a $U$-limit diagram.

Proof. We proceed as in the proof of Corollary 7.1.5.7. Let $\operatorname{Isom}(\operatorname{\mathcal{C}})$ denote the full subcategory of $\operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}})$ spanned by the isomorphisms in $\operatorname{\mathcal{C}}$, and define $\operatorname{Isom}(\operatorname{\mathcal{D}}) \subseteq \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{D}})$ similarly. For $i \in \{ 0,1\}$, the evaluation functors

$\operatorname{ev}_ i: \operatorname{Isom}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{C}}\quad \quad \operatorname{ev}_ i: \operatorname{Isom}(\operatorname{\mathcal{D}}) \rightarrow \operatorname{\mathcal{D}}$

are trivial Kan fibrations (Corollary 4.4.5.10), and therefore equivalences of $\infty$-categories (Proposition 4.5.2.10). Our assumption that $\overline{u}$ and $\overline{v}$ are isomorphic guarantees that we can choose a diagram $\overline{w}: K^{\triangleleft } \rightarrow \operatorname{Isom}(\operatorname{\mathcal{C}})$ satisfying $\operatorname{ev}_0 \circ \overline{w} = \overline{u}$ and $\operatorname{ev}_1 \circ \overline{w} = \overline{v}$. Applying Remark 7.1.7.6 to the commutative diagram

$\xymatrix@R =50pt@C=50pt{ \operatorname{Isom}(\operatorname{\mathcal{C}}) \ar [r]^-{ \operatorname{ev}_0 } \ar [d]^{U'} & \operatorname{\mathcal{C}}\ar [d]^{U} \\ \operatorname{Isom}(\operatorname{\mathcal{D}}) \ar [r]^-{ \operatorname{ev}_0 } & \operatorname{\mathcal{D}}, }$

we see that $\overline{u}$ is a $U$-limit diagram if and only if $\overline{w}$ is a $U'$-limit diagram. A similar argument shows that this is equivalent to the requirement that $\overline{v}$ is a $U$-limit diagram. $\square$