Kerodon

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

Proof. We will prove $(1)$; the proof of $(2)$ is similar. Note that $\sigma $ restricts to a diagram

\[ \sigma _0: \operatorname{N}_{\bullet }( [1] \times [1] \setminus \{ (0,0) \} ) \rightarrow \operatorname{\mathcal{C}} \]

satisfying $\sigma _0( 0,1) = X$, $\sigma _0( 1,1) = Y$, and $\sigma _0( 1,0 ) = Y'$. The assumption that $f$ is an isomorphism guarantees that $\sigma _0$ is right Kan extended from the full subcategory

\[ \{ 1\} \times \Delta ^1 \subseteq \operatorname{N}_{\bullet }([1] \times [1] \setminus \{ (0,0) \} ). \]

It follows that $\sigma $ is a pullback diagram if and only if the restriction $\sigma |_{ \operatorname{N}_{\bullet }( \{ (0,0) < (1,0) < (1,1) \} )}$ is a limit diagram (Corollary 7.3.7.2) By virtue of Corollary 7.2.2.6, this is equivalent to the requirement that $f'$ is an isomorphism. $\square$