Homotopy fibre of composition Let $f:A\rightarrow B, g:B\rightarrow C$ be maps in the category CGWH (compactly generated weakly Hausdorff spaces). Do we have a homotopy fibration sequence
$$F(f)\rightarrow F(gf) \rightarrow F(g)$$
consisting of homotopy fibres? (And the dual statement for homotopy cofibres?)
 A: This is a fundamental and basic property in homotopy theory, as is the dual statement for homotopy cofibers.  These appear as Lemmas 1.2.7 and 1.2.5 in the recently published book More concise algebraic topology by May and Ponto. (And in stable model categories these merge and become the octahedral axiom.)
A: $\require{AMScd}$
Here are some details. Without loss in generality, we can assume $f$ and $g$ are fibrations. I am assuming that all spaces are based. We may assume that $F_f$ now refers to the actual fiber of $f$ (which is equivalent to its homotopy fiber).
Start with the commutative diagram
$$
\begin{CD}
F_f @>>> A @> f >> B\\
@VVV @VVV @VV gV \\
F_{g\circ f} @>>> A @>> g\circ f > C
\end{CD}
$$
Now induce once over to the left to get a diagram
$$
\begin{CD}
\Omega B @>>> F_f @>>> A \\
@VVV @VVV @VVV \\
\Omega C @>>> F_{g\circ f} @>>> A 
\end{CD}
$$
where the horizontal maps form homotopy fiber sequences and the left square is homotopy cartesian (reason: the map horizontal fibers
of this square is identified with the identity map of $\Omega A$).
The map of vertical fibers of the left square is a map $\Omega F_g \to ?$, which is an equivalence since the square is homotopy cartesian.
On the other hand the square fits into a diagram
\begin{CD}
\Omega B @>>> F_f \\
@VVV @VVV  \\
\Omega C @>>> F_{g\circ f}\\
@VVV @VVV \\
F_{g} @= F_{g}
\end{CD}
It follows that there's a homotopy fiber sequence
$$
\Omega F_g \to F_f \to F_{g\circ f} 
$$
and the map $\Omega C \to F_g$ factors through $F_{gf}$.
It follows from the long exact sequence of homotopy groups that 
$F_f \to F_{g\circ f} \to F_g$ is a homotopy fiber sequence.
