$\require{AMScd}$
I am trying to get an understanding of the meaning of homotopy coherence - in order to understand homotopy limits and colimits - in the category $\mathbf{Top}$. Often when I see this discussed, the explanation there amounts to "homotopies commuting up to homotopy, and so on". Whilst I find this conceptually OK, I am struggling to get my hands on what this means explicitly.
My goal is to understand why the homotopy pullback of a diagram of topological spaces can be represented by the so-called homotopy fibre product, and in particular why the homotopy fibre of an arbitrary map $f:X \rightarrow Y$ can be represented by the mapping fibre: $$M_f:=\{(x,\gamma) \in X \times Y^I \; | \; f(x)=\gamma(1), \gamma(0)=*_Y\}.$$
Alternatively/additionally, I would like a concrete explanation for why it is appropriate that the homotopy fibre of a map $f:X \rightarrow Y$ be defined to be the homotopy pullback of $f$ with the inclusion of the basepoint. What is the universal property which we want the homotopy fibre to satisfy, and how does it come from being this particular homotopy pullback?
Question: Is my understanding of homotopy coherence in the following context correct?
At this Nlab page on the homotopy pullback, the following is written:
The homotopy pullback of $X \xrightarrow{f} Z \xleftarrow{g} Y$ consists of a square
\begin{CD} P @>{p_2}>> Y;\\ @V{p_1}VV @V{g}VV \\ X @>{f}>> Z; \end{CD}
which commutes up to homotopy, such that for any other square
\begin{CD} T @>{t_2}>> Y;\\ @V{t_1}VV @V{g}VV \\ X @>{f}>> Z; \end{CD}
that commutes up to homotopy (say via a homotopy $H:T \times I \rightarrow Z$), there exists a unique morphism $T \rightarrow P$ making the two triangles commute up to homotopy, and similarly for homotopies and higher homotopies.
Now, I think (from previous efforts to understand this stuff) that that last italicized part is crucial, and otherwise the definition doesn't make sense. What I want to know is whether I'm interpretting it correctly in the following:
There is a unique map $\phi:T \rightarrow P$ such that $p_1 \circ \phi \simeq t_1$ via $H_1:T \times I \rightarrow X$ and $p_2 \circ \phi \simeq t_2$ via $H_2:T \times I \rightarrow Y$, AND such that the resulting homotopies $H_1 \circ f: T \times I \rightarrow Z$, $H_2 \circ g: T \times I \rightarrow Z$ and $H: T \times I \rightarrow Z$ are homotopic, say via $\Lambda: T \times I \times I \rightarrow Z$
Is that correct? And if these conditions are satisfied, then the map $T \rightarrow P$ is unique up to homotopy?
Would it be true that, in the case that we had multiple homotopies from $f \circ t_1$ to $g \circ t_2$, we would need these to be homotopic, say via $\bar{\Lambda}:T \times I \times I \rightarrow Z$, and we would then need $\Lambda$ and $\bar{\Lambda}$ to be homotopic?
The following definition comes more or less from Mather's paper Pullbacks in Homotopy Theory. Different authors make slightly different definitions, and there seems to be fair amount of abuse in the terminology some adopt. I'll try to say some words about this later on.
A homotopy pullback is a pair $(\mathcal{S},F)$ consisting of a homotopy commutative square $\mathcal{S}$ of topological spaces and continuous maps
\begin{CD} P @>q>> Y\\ @VpVV @V{g}VV \\ X @>{f}>> Z \end{CD}
together with a chosen homotopy $W:fp\Rightarrow gq$ which, together, must satisfy the following properties
$\bullet$ Given a space $A$, maps $\alpha:A\rightarrow X$, $\beta:A\rightarrow Y$, and a homotopy $F:f\alpha\Rightarrow g\beta$ there exists a map $\theta=\theta(\alpha,F,\beta):A\rightarrow P$ and a pair of homotopies $K:\alpha\Rightarrow p\theta$, $L:\beta\Rightarrow q\theta$ such that there is a 2-homotopy
$$-gL+W\theta+fK\Rrightarrow F :A\rightarrow D$$
$\bullet$ If $\theta':A\rightarrow P$ is another map, and $K':\alpha\Rightarrow p\theta'$, $L':\beta\Rightarrow q\theta'$ another pair of homotopies for which there exists a 2-homotopy $-gL'+W\theta'+fK'\Rrightarrow F$, then there exists a homotopy $M:\theta\Rightarrow \theta'$ and 2-homotopies
$$K+pM\Rightarrow K',\qquad -L'+qM\Rrightarrow L.$$
I've tried to write this definition in the spirit of your question: a 2-homotopy is a homotopy of homotopies. So if $F,G:f\Rightarrow g$ are homotopies, then a 2-homotopy $\Psi:F\Rrightarrow G:X\rightarrow Y$ is a map $\Psi:X\times I\times I\rightarrow Y$ with
$$\Psi(x,s,0)=F(x,s),\quad \Psi(x,s,1)=G(x,s),\quad \Psi(x,0,t)=f(x),\quad \Psi(x,1,t)=g(x)$$
for all $x\in X$ and $s,t\in I$. The point is that this becomes a really convoluted way of expressing things in the case of this simple square diagram. It's much easier to ask that, for instance, $[-gL+W\theta+fK]=[F]$ as track classes of homotopies, since we never need to go to 3-homotopies or above for the square diagram.
What is important to note is that the word "unique" never appears in the above. When the chance for such a statement occurs we ask instead only that there exist a homotopy, or a 2-homotopy, or a 3-homotopy, or a... This is very much in the spirit of homotopy coherence. The point I was trying to make in the comments is that we never really see this idea take off with the square diagram. If you want to understand homotopy coherence you really need to consider slightly more interesting digrams. You might like to think about Stasheff's theory of $A_n$-spaces, for instance, or some homotopical group actions, before going on to study the (mainly simplicial) techniques developed by Cordier-Porter and discussed by Riehl and Shulman.
Now, I'll try to justify what I said in the opening. Really a homotopy pullback is a (right) derived functor of the limit functor, applied to diagrams indexed on the cospan category
$$\mathcal{P}=\left(\bullet\rightarrow\ast\leftarrow\square\right).$$
Now these gadgets can be discussed in any reasonable model category, and come in two main flavours. Name what are called total derived functors, and what are called point-set derived functors (this is Shulman's terminology). Total derived functors are defined on the homotopy category of diagram, and take values in the homotopy category of spaces. They satisfy a certain universal property which is very weak, and come equipped with only the bare minimum of structure. Since they are defined on homotopy category, there are not maps - only homotopy classes of maps - and no homotopies involved in their definition. In particular, with reference to the square above, the maps $p,q$ are not even part of their stucture.
On the other hand, a point-set derived functor is defined on diagrams and takes values in spaces (rather than homotopy categories). The universal property it satisfies is the same as the total derived functor, after projecting to the homotopy category. Of course, to arrange for this to be true it comes supplied with actual maps, and homotopies of such to ensure this universal property will hold. The definition I have given above is closer to this sort of derived functor.
Of course, the homotopy pullback square I've defined above is really its own thing. Different authors required different amounts of the available structure for their work, and are willing to spend different amounts of time setting up the theory. Hence you will find slightly different definitions across the literature. Personally I'd be very wary of anything written on nlab, and would rather follow up their well-collected references to understand the theory.
As motivation for the definition I've given let me end with this. Often when doing homotopy theory it is not enough to work with only homotopy classes of maps. Supplying specific homotopies can be really useful for defining secondary operations and compositions such as Massey products or Toda brackets. Including the homotopy $F$ together with the homotopy-commuting square $\mathcal{S}$ as part of the structure can be really useful when you sit down to actually make computations.