# Kerodon

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

Proposition 3.4.1.9 (Symmetry). A commutative diagram of simplicial sets

$\xymatrix@R =50pt@C=50pt{ X_{01} \ar [r] \ar [d] & X_0 \ar [d]^{f_0} \\ X_1 \ar [r]^-{f_1} & X }$

is a homotopy pullback square if and only if the transposed diagram

$\xymatrix@R =50pt@C=50pt{ X_{01} \ar [r] \ar [d] & X_1 \ar [d]^{f_1} \\ X_0 \ar [r]^-{f_0} & X }$

is a homotopy pullback square.

Proof. Using Proposition 3.1.7.1, we can choose factorizations

$X_0 \xrightarrow {w_0} X'_0 \xrightarrow {f'_0} S \quad \quad X_1 \xrightarrow {w_1} X'_1 \xrightarrow {f'_1} S$

of $f_0$ and $f_1$, where both $f'_0$ and $f'_1$ are Kan fibrations and both $w_0$ and $w_1$ are weak homotopy equivalences. We have a commutative diagram of simplicial sets

$\xymatrix@R =50pt@C=50pt{ X_{01} \ar [r]^-{u} \ar [d]^{v} & X_0 \times _{X} X'_1 \ar [r] \ar [d]^{v'} & X_0 \ar [d]^{w_0} \\ X'_0 \times _{X} X_1 \ar [r]^-{u'} \ar [d] & X'_0 \times _{X} X'_1 \ar [r] \ar [d] & X'_0 \ar [d]^{f'_0} \\ X_1 \ar [r]^-{w_1} & X'_1 \ar [r]^-{ f'_1} & X. }$

We wish to show that $u$ is a weak homotopy equivalence if and only if $v$ is a weak homotopy equivalence (see Proposition 3.4.1.2). This follows from the two-out-of-three property (Remark 3.1.6.16), since the morphisms $u'$ and $v'$ are weak homotopy equivalences by virtue of Corollary 3.3.7.2. $\square$