What is a ‘contraction’ here?

[kaspar]

I am trying to figure what is happening here at page 16 (or 25, for your pdf reader)

Proof: Let \(f_t : X \to X\) be a homotopy extending a contraction of \(A\), with \(f_0 = \mathbf 1\). [...]

[megas_archon]

Stai supponendo che $A$ sia contraibile, quindi la mappa \(A\to *\) è un'equivalenza omotopica e una "contrazione" è l'omotopia che realizza quella contrazione (...devo rispondere in inglese?).

[kaspar]

una "contrazione" è l'omotopia che realizza quella contrazione

It seems a bit circular, but I got it.

Since \(A\) is contractible, \(\mathrm{id}_A : A \to A\) is homotopic to some constant map \(k : A \to A\) that has all the elements of \(A\) sent to a certain \(x_0 \in A\). Now consider a homotopy \(C : A \times I \to X\) from \(i \circ \mathrm{id}_A\) to \(i \circ k\), where \(i\) is the inclusion \(A \to X\). If we involve \(\mathrm{id}_X\), we have \(i \circ \mathrm{id}_A = \mathrm{id}_X \circ i\), so that we can employ the asumption \(X\) has HEP: there exists some homotpy \(H : X \times X \to X\) from \(\mathrm{id}_X\) such that this commutes. The interesting part is \(H(\cdot, 1)\) which maps the elements of \(A\) toward \(x_0\) and can be factored as \(q \circ p\), with \(p : X \to X/A\) being the canonical projection and \(q : X/A \to X\) the unique one that can there be. At this point we have \(q \circ p\) is homotopic to \(\mathrm{id}_X\); the homotopy \(p \circ q \simeq \mathrm{id}_{X/A}\) is immediate (actually, it is an equality).