Homotopy fiber

In mathematics, especially homotopy theory, the homotopy fiber is part of a construction that associates a fibration to an arbitrary continuous function of topological spaces ${\displaystyle f\colon A\to B}$.
In particular, given such a map, define ${\displaystyle E_{f}}$ to be the set of pairs ${\displaystyle (a,p)}$ where ${\displaystyle a\in A}$ and ${\displaystyle p\colon [0,1]\to B}$ is a path such that ${\displaystyle p(0)=f(a)}$. We give ${\displaystyle E_{f}}$ a topology by giving it the subspace topology as a subset of ${\displaystyle A\times B^{I}}$ (where ${\displaystyle B^{I}}$ is the space of paths in ${\displaystyle B}$ which as a function space has the compact-open topology). Then the map ${\displaystyle E_{f}\to B}$ given by ${\displaystyle (a,p)\mapsto p(1)}$ is a fibration. Furthermore, ${\displaystyle E_{f}}$ is homotopy equivalent to ${\displaystyle A}$ as follows: Embed ${\displaystyle A}$ as a subspace of ${\displaystyle E_{f}}$ by ${\displaystyle a\mapsto (a,p_{a})}$ where ${\displaystyle p_{a}}$ is the constant path at ${\displaystyle f(a)}$. Then ${\displaystyle E_{f}}$ deformation retracts to this subspace by contracting the paths.
The fiber of this fibration (which is only well-defined up to homotopy equivalence) is the homotopy fiber ${\displaystyle F_{f}}$, which can be defined as the set of all ${\displaystyle (a,p)}$ with ${\displaystyle a\in A}$ and ${\displaystyle p\colon [0,1]\to B}$ a path such that ${\displaystyle p(0)=f(a)}$ and ${\displaystyle p(1)=b_{0}}$, where ${\displaystyle b_{0}\in B}$ is some fixed basepoint of ${\displaystyle B}$.