For context, my problem arises from "https://math.stackexchange.com/questions/4427532/homotopy-groups-of-wedge-of-spaces", where in one of the answers, the claim is that the homotopy fiber of the map $\nabla: X\vee X\to X$ is $\Sigma\Omega X$.
Using the explicit construction of the homotopy fiber, I need to understand the homotopy type of $E_\nabla$ consisting of pairs $(x_{(i)}, \gamma$ with $\gamma(0)=x$ and $\gamma(1)=x_0$ for some fixed base point $x_0$. (The notation $x_{(i)}$ is to say the element $x$ in the $i$th copy of $X$ in the wedge of $X$ with itself). I think I have succesfully shown this is $(X\vee X)\times \Omega X$ (though even this I am not 100% sure), and after this I don't know how to proceed.
Any help is appreciated, thanks.
Best Answer
You can show this using a result I usually call "the cube theorem". I'll say more once we get there. In case you want to work in the model category of topological spaces, it is important to ask $X$ to be well-pointed, i.e. we want that the inclusion $x\colon *\to X$ of the basepoint is a cofibration. This assumption is also made in the post you linked. If you work in the $\infty$-category of spaces, you can hide these technical details, but then you have to be careful when translating things back to the model-category of spaces (where such assumptions will enter again).
In that case, we write $F$ for the homotopy fiber of $\nabla$, and can form the following diagram:
All squares going from the front to the back are homotopy pullbacks. Indeed, the right-bottom square is a homotopy pullback by definition of $F$, and via pasting lemmas it then follows for the left-bottom square and middle-vertical square. The leftmost vertical square and the left-upper square are both homotopy pullbacks as this is (essentially) the definition of $\Omega X$.
If $X$ is well-pointed, then the (edit:) back square is a homotopy pushout. Now, the cube theorem states that if the back square of a cube is a homotopy pushout of spaces, and if all squares going from the front to the back are homotopy pullbacks, then the front square of the cube is also a homotopy pushout. Hence we find that $F$ is the homotopy pushout of the span $*\leftarrow\Omega X\rightarrow *$. Again, (essentially) by definition, this homotopy pushout is $\Sigma\Omega X$, so $F\simeq \Sigma\Omega X$.
You can easily prove the cube theorem in case you are working in the category of sets, and all pushouts and pullbacks are strict, and not homotopy pushouts and homotopy pullbacks. You may believe that going $\infty$-categorically the analogous result is the same statement in the $\infty$-category of spaces (as the role sets play in 1-category theory is played by spaces in $\infty$-category theory), and this is the cube theorem (recall that pushouts and pullbacks in the $\infty$-category of spaces are modelled by homotopy pushouts and homotopy pullbacks in the model category). Note that the cube theorem does not hold in all $\infty$-categories or model categories.