Kerodon

I'm having difficulty justifying one of the steps in this proof. It currently cites 7.3.6.7 to argue that we have a level-wise homotopy equivalence between the two squares, from which it follows that one is a homotopy pullback square if and only if the other is. However, 7.3.6.7 only states that left- and right-most faces of the cube given by restriction are homotopy pullback squares. This is sufficient to prove that the back face of the cube is a homotopy pullback square if the front face of the cube is one (2-of-3 for pullback squares) but not the reverse direction. It also suffices to prove the non-relative case, where we do obtain homotopy equivalences.

(Frustratingly, I seem to remember understanding this proof at some point in the past...)

I was curious so I ended up posting a question on mathoverflow (https://mathoverflow.net/questions/424602/question-about-the-proof-of-kerodon-tag-030v-proposition-7-3-7-1/). If anyone else was stuck on this the answer might help clear things up.

Yep; thanks! The argument should be supplemented by an appeal to tag 0110.