Kerodon

Proof. The proof will proceed in several steps, each of which involves replacing one or more of the terms in (3.54) by a weakly equivalent simplicial set (by virtue of Corollary 3.4.1.12 and Proposition 3.4.2.9, such replacements will not affect the truth of our hypotheses or of the desired conclusion). Let us denote each of the morphisms appearing in the diagram (3.54) by $f_{XY}$, where $X,Y \in \{ \overline{A}, \overline{B}, \overline{C}, \overline{D}, A, B, C, D \} $ are the source and target of $f_{XY}$, respectively.

• By virtue of Proposition 3.1.7.1, the morphism $f_{\overline{B} B}: \overline{B} \rightarrow B$ factors as a composition $\overline{B} \xrightarrow {w} \overline{B}' \xrightarrow { f_{\overline{B} B}' } B$, where $w$ is anodyne and $f_{ \overline{B} B }'$ is a Kan fibration. Replacing $\overline{B}$ by $\overline{B}'$ (and $\overline{D}$ by the pushout $\overline{B}' \coprod _{ \overline{B} } \overline{D}$), we can reduce to the case where $f_{\overline{B} B}$ is a Kan fibration. Similarly, we can arrange that the map $f_{\overline{C} C}: \overline{C} \rightarrow C$ is a Kan fibration.

• Applying Proposition 3.1.7.1 again, we can factor the morphism $g: \overline{A} \rightarrow A \times _{ (B \times C) } ( \overline{B} \times \overline{C} )$ as a composition

  \[ \overline{A} \xrightarrow {w} \overline{A}' \xrightarrow {g'} A \times _{ (B \times C) } ( \overline{B} \times \overline{C} ), \]

  where $w$ is anodyne and $g'$ is a Kan fibration. Replacing $\overline{A}$ by $\overline{A}'$, we can reduce to the case where $g$ is a Kan fibration, so that the morphism $f_{ \overline{A} A}$ is also a Kan fibration.

• By virtue of Exercise 3.1.7.11, the morphism $f_{AB}$ factors as a composition $A \xrightarrow { f_{AB}' } B' \xrightarrow {w} B$, where $f_{AB}'$ is a monomorphism and $w$ is a trivial Kan fibration. Replacing $B$ by $B'$ (and $\overline{B}$ by the fiber product $B' \times _{B} \overline{B}'$), we can reduce to the case where $f_{AB}$ is a monomorphism. Similarly, we may assume that $f_{AC}$ is a monomorphism.

• By virtue of Exercise 3.1.7.11, the morphism $f_{\overline{A} \overline{B}}$ factors as a composition $\overline{A} \xrightarrow { f_{\overline{A} \overline{B}}' } \overline{B}' \xrightarrow {w} \overline{B}$, where $f_{\overline{A} \overline{B}}'$ is a monomorphism and $w$ is a trivial Kan fibration. Replacing $\overline{B}$ by $\overline{B}'$, we can reduce to the case where $f_{ \overline{A} \overline{B} }$ is a monomorphism. Similarly, we can assume that $f_{ \overline{A} \overline{C}}$ is a monomorphism.

• The back face

  3.55

  \begin{equation} \label{equation:mather-first-cube3} \begin{gathered} \xymatrix@R =50pt@C=50pt{ \overline{A} \ar [r]^-{ f_{ \overline{A} \overline{B} }} \ar [d]^{ f_{\overline{A} A}} & \overline{B} \ar [d]^{ f_{ \overline{B} B} } \\ A \ar [r]^-{f_{AB}} & B } \end{gathered} \end{equation}

  is a homotopy pullback square in which the horizontal maps are monomorphisms and the vertical maps are Kan fibrations. It follows that, for every vertex $a \in A$ having image $b = f_{AB}(a) \in B$, the induced map of fibers $\overline{A}_{a} \rightarrow \overline{B}_{b}$ is a homotopy equivalence. Let $\overline{B}' \subseteq \overline{B}$ denote the simplicial subset spanned by those simplices $\sigma : \Delta ^{n} \rightarrow \overline{B}$ having the property that the restriction $\sigma |_{ A \times _{B} \Delta ^{n} }$ factors through $\overline{A}$. Applying Lemma 3.3.8.4, we deduce that the restriction $f_{ \overline{B} B}|_{ \overline{B}' }: \overline{B}' \rightarrow B$ is also a Kan fibration. Moreover, the inclusion map $\overline{B}' \hookrightarrow \overline{B}$ induces a homotopy equivalence of fibers $\overline{B}'_{b} \hookrightarrow \overline{B}_{b}$, for each vertex $b \in B$. It follows that the inclusion $\overline{B}' \hookrightarrow \overline{B}$ is a weak homotopy equivalence (Corollary 3.3.7.5). Replacing $\overline{B}$ by $\overline{B}'$, we can reduce to the case where the diagram (3.55) is a pullback square. Similarly, we can arrange that the diagram

  \[ \xymatrix@R =50pt@C=50pt{ \overline{A} \ar [r]^-{ f_{ \overline{A} \overline{C} }} \ar [d]^{ f_{\overline{A} A}} & \overline{C} \ar [d]^{ f_{ \overline{C} C} } \\ A \ar [r]^-{f_{AC}} & C } \]

  is a pullback square.

• By assumption, the top and bottom faces

  3.56

  \begin{equation} \label{equation:mather-first-cube4} \begin{gathered} \xymatrix@R =50pt@C=50pt{ \overline{A} \ar [r] \ar [d]^{ f_{\overline{A} \overline{C}}} & \overline{B} \ar [d] & A \ar [r] \ar [d]^{ f_{AC} } & B \ar [d] \\ \overline{C} \ar [r] & \overline{D} & C \ar [r] & D } \end{gathered} \end{equation}

  are homotopy pushout squares. Since $f_{ \overline{A} \overline{C} }$ and $f_{AC}$ are monomorphisms, it follows that the induced maps

  \[ \overline{C} \coprod _{\overline{A}} \overline{B} \rightarrow \overline{D} \quad \quad C \coprod _{A} B \rightarrow D \]

  are weak homotopy equivalences (Proposition 3.4.2.11). We may therefore replace $D$ by the pushout $C \coprod _{A} B$ and $\overline{D}$ by the pushout $\overline{C} \coprod _{\overline{A} } \overline{B}$, and thereby reduce to the case where the diagrams (3.56) are pushout squares.

• Applying Exercise 3.4.4.1 levelwise, we deduce that the front and right faces

  3.57

  \begin{equation} \label{equation:mather-first-cube5} \begin{gathered} \xymatrix@R =50pt@C=50pt{ \overline{C} \ar [r] \ar [d]^{ f_{\overline{C} C}} & \overline{D} \ar [d]^{ f_{ \overline{D} D}} & \overline{B} \ar [r] \ar [d]^{ f_{\overline{B} B}} & \overline{D} \ar [d]^{ f_{\overline{D} D}} \\ C \ar [r] & D & B \ar [r] & D } \end{gathered} \end{equation}

  are pullback squares in the category of simplicial sets. In particular, for every simplex $\sigma : \Delta ^ n \rightarrow D$, the projection map $\Delta ^ n \times _{ D} \overline{D} \rightarrow \Delta ^ n$ is a pullback either of $f_{ \overline{B} B}$ or of $f_{ \overline{C} C}$, and is therefore a Kan fibration. Applying Remark 3.1.1.7, we conclude that $f_{ \overline{D} D}: \overline{D} \rightarrow D$ is a Kan fibration. It follows that the diagrams (3.57) are also homotopy pullback squares, as desired.