For a based map $f : X \to Y$, define the "homotopy fiber" $Ff$ to be$$Fd = X \times_f PY = \{(x, \chi) : f(x) = \chi(1)\} \subset X \times PY.$$Equivalently, $Ff$ is the pullback displayed in the diagram
where $\pi(x, \chi) = x$. As a pullback of a fibration, $\pi$ is a fibration.
If $\rho: Nf \to f$ is defined by $\rho(x, \chi) = \chi(0)$, then $f = \rho \circ \nu$, where $\nu(x) = (x, c_{f(x)})$, and $Ff$ is the fiber $\rho^{-1}(*)$. Thus the homotopy fiber $Ff$ is constructed by first replacing $f$ by the fibration $\rho$ and then taking the actual fiber.
Let $\iota: \Omega Y \to Ff$ be the inclusion specified by $\iota(\chi) = (*, \chi)$. The sequence$$\dots \to \Omega^2 X \overset{\Omega^2 f}{\longrightarrow} \Omega^2Y \overset{-\Omega\iota}{\longrightarrow} \Omega Ff \overset{-\Omega\pi}{\longrightarrow} \Omega X \overset{-\Omega f}{\longrightarrow} \Omega Y \overset{\iota}{\to} Ff \overset{\pi}{\to} X \overset{f}{\to} Y$$is called the fiber sequence generated by the map $f$; here$$(-\Omega f)(\zeta)(t) = (f \circ \zeta)(1 - t) \text{ for }\zeta \in \Omega X.$$These "long exact sequences of based spaces" also give rise to long exact sequences of pointed sets, covariantly.
Theorem. For any based space $Z$, the induced sequence$$\dots \to [Z, \Omega F f] \to [Z,\Omega X] \to [Z, \Omega Y] \to [Z, Ff] \to [Z, X] \to [Z, Y]$$is an exact sequence of pointed sets, or of groups to the left of $[Z, \Omega Y]$, or of Abelian groups to the left of $[Z, \Omega^2Y]$.
Exactness is clear at the first stage. To see this, consider the diagram
Here $h: c_* \simeq f \circ g$, and we view $h$ as a map $Z \to PY$. Thus we check exactness by using any given homotopy to lift $g$ to the fiber.
I claim that, up to homotopy equivalence, each consecutive pair of maps in my fiber sequence is the composite of a map and the projection from its fiber onto its source. This will imply the source. I observe that, that for any map $f$, interchange of coordinates gives a homeomorphism$$\Omega F f \cong F(\Omega f)$$such that the following diagram commutes:
Here $\tau$ is obtained by interchanging the loop coordinates and is homotopic to − \text{id}. We have $\iota(f)$, $\pi(f)$, etc., to indicate the maps to which the generic constructions $\iota$ and $\pi$ are applied. Using this inductively, we see that we need only verify our claim for the two pairs of maps $(\iota(f), \pi(f))$ and $(-\Omega f, \iota(f))$.
Anyways, one key step in finishing the proof: I need that the right triangle commutes and the left triangle commutes up to homotopy in the following diagram.
My question is, what is the easiest way to see that the two triangles commute up to homotopy? Thanks in advance.
First, we show that the right triangle commutes up to homotopy. Considering the fiber sequence$$F(f) \overset{\pi(f)}{\to} X \overset{f}{\to} Y,$$we want to show that the inclusion of the strict fiber of $\pi(f)$ into its homotopy fiber $F(\pi(f))$ is a homotopy equivalence making the right triangle commute, where$$\iota: \Omega Y \to F(f), \text{ }\iota(\gamma) = (x_0, \gamma) \in F(f) = X \times_Y PY.$$The strict fiber of $\pi(f)$ is the subset of $F(f)$,$$(\pi(f))^{-1}(x_0) = \{(x_0, \gamma) : \gamma(0) = y_0,\,\gamma(1) = f(x_0) = y_0\} \cong \Omega Y,$$and the composite $\Omega Y \to F(\pi(f)) \to F(f)$ is$$\gamma \mapsto (\iota(\gamma),\,\text{constant path at the basepoint of }F(f)) \mapsto \iota(\gamma).$$The inclusion of the strict fiber $\phi: \Omega Y \overset{\simeq}{\to} F(\pi(f))$ is a homotopy equivalence, since $\pi(f)$ is a fibration (and using this).
Now, we show that the left triangle commutes up to homotopy. The homotopy we require is$$H: \Omega X \times I \to F(\pi(f)),\text{ }(\gamma, s) \mapsto ((*, (f \circ \gamma)(1 - t)|_{[0, 1-s]}), \gamma|_{[1 - s, 1]}).$$This is $\phi \circ (-\Omega f)$ at time $0$ and $i \circ \pi(f)$ at time $1$, so we are done.