Kerodon

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

Definition 3.4.1.1. A commutative diagram of simplicial sets

3.38
\begin{equation} \label{diagram:homotopy-pullback-square0} \begin{gathered} \xymatrix { Y \ar [r] \ar [d] & X \ar [d]^{f} \\ T \ar [r] & S } \end{gathered}\end{equation}

is a homotopy pullback square if there exists a factorization $f = f' \circ w$ where $f': X' \rightarrow S$ is a Kan fibration, $w: X \rightarrow X'$ is a weak homotopy equivalence, and the induced map $Y \rightarrow T \times _{S} X'$ is a weak homotopy equivalence.