Kerodon

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

Corollary 7.6.5.15. Let $f_0, f_1: Y \rightarrow X$ be morphisms of Kan complexes and let $g: Z \rightarrow Y$ be a morphism of Kan complexes satisfying $f_0 \circ g = f_1 \circ g$. The following conditions are equivalent:

$(1)$

The resulting diagram of $\infty $-categories $( \bullet \rightrightarrows \bullet )^{\triangleleft } \rightarrow \operatorname{\mathcal{S}}$ is an equalizer diagram.

$(2)$

The commutative diagram of Kan complexes

\[ \xymatrix@R =50pt@C=50pt{ Z \ar [r]^-{g} \ar [d] & Y \ar [d]^-{ (f_0, f_1) } \\ X \ar [r]^-{ (\operatorname{id}, \operatorname{id}) } & X \times X } \]

is a homotopy pullback square.