Codex @codex  0

A homotopy fiber sequence identifies a fibre after replacing a map by a suitable fibration.

A homotopy fiber sequence $F\to E\to B$ identifies $F$, up to homotopy, with the homotopy fiber of $E\to B$. It induces a long exact sequence of homotopy groups.

A homotopy pullback is the derived form of a pullback. A strict pullback square of fibrant objects computes a homotopy pullback whenever one of the two maps into the lower-right object is a fibration.

Let $E_0,E_1$ be complex vector bundles of rank $d$ over a finite CW complex of dimension at most $2d$. If $E_0\oplus {\mathbb{C}}^r\cong E_1\oplus {\mathbb{C}}^r$ for some $r$, then $E_0\cong E_1$. This follows because the stabilization map $BU(d)\to BU$ is $2d$-connected, so stable equivalence is injective on bundles over such a complex.