Kerodon

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

Corollary 7.6.3.22. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category and let $\sigma : \Delta ^1 \times \Delta ^1 \rightarrow \operatorname{\mathcal{C}}$ be a commutative square, which we represent by a diagram

\[ \xymatrix@R =50pt@C=50pt{ X \ar [r]^-{f_0} \ar [d]^-{f_1} & X_0 \ar [d] \\ X_1 \ar [r] & \mathbf{1}. } \]

Suppose that ${\bf 1}$ is a final object of $\operatorname{\mathcal{C}}$. Then $\sigma $ is a pullback square if and only if the morphisms $f_0$ and $f_1$ exhibit $X$ as a coproduct of $X_0$ with $X_1$ in the $\infty $-category $\operatorname{\mathcal{C}}$.

Proof. The assumption that ${\bf 1}$ is final guarantees that the projection map $\operatorname{\mathcal{C}}_{ / {\bf 1} } \rightarrow \operatorname{\mathcal{C}}$ is a trivial Kan fibration (Proposition 4.6.7.10), so that the desired result follows from the criterion of Proposition 7.6.3.14. $\square$