Zoran Škoda: But there is much older and more general theorem of Hurewitz: if one has a map and a numerable covering of such that the restrictions for every in the covering is a Hurewicz fibration then is also a Hurewicz fibration. But the proof is pretty complicated. For example George Whitehead’s Elements of homotopy theory is omitting it (page 33) and Postnikov is proving it (using the equivalent “soft” homotopy lifting property).
Todd Trimble: Yes, I am aware of it. You can find a proof in Spanier if you’re interested. I’ll have to check whether the Milnor trick (once I remember all of it) generalizes to Hurewicz’s theorem.
Stephan: I wonder if this trick moreover generalizes (in a homotopy theoretic sense) to categories other that ; for example to the classical model structure on ?
where is the composite inclusion . We are trying to show that lifts through .
As I recall, the trick proceeds by considering the bundle
where the base is and is the restriction of along , and then one constructs a bundle lifting of the homeomorphism
and then the composition
gives the desired homotopy lifting.
To see that the bundle restricted over is trivial, we just need to check that is trivial over . However, by the original commutative square, equals the composite
and already is trivial (over ) essentially because is a -torsor: there is a bundle isomorphism
The construction of the slide is where transfinite composition comes in. The details are at this moment a little hazy, but the rough idea is to construct a partition of unity subordinate to the pulled back (locally finite) numerable cover of . One is supposed to well-order the , and then transfinitely compose a bunch of mini-slides over . The transfinite composition is well-defined on the fiber over any because the arrows in the composite are non-identity only for those which contain , and there are only finitely many of these by local finiteness.
To be continued.