Corollary 7.6.4.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.