I'm teaching some homotopy theory at the moment, and I'm discovering a number of things I've never before learned properly. (I guess everybody who's ever taught knows that feeling.) One of those things is that a local Hurewicz fibration is a global Hurewicz fibration if the base space is paracompact. This result goes back to Hurewicz and Huebsch, is proved in Spanier's book, and there's a paper by Dold where he compares various local and global properties of projection maps, including being a fibration. None of these proofs are what I would call conceptual. There's a lot of gluing together of "extended" lifting functions, dividing up intervals in three parts, etc etc, and they use the axiom of choice. Since paracompactness needs to get used, any possible proof will probably require some gluing, but does anyone have a more conceptual proof of the result? Has anyone taught this to students, and how was that? Is the axiom of choice a necessary input?
Hi Tilman, it seems as we are teaching the same course at the same time! I will do this in about three weeks. There are proofs of that theorem in the book of May and in tom Dieck's new volume. May explains the conceptual idea a bit, and tom Dieck puts it into a context, relating it to other proofs (for example the bundle homotopy theorem). I think the underlying idea is very natural and simple. The glueing is definitly required because the theorem is a localtoglobal statement and paracompactness of the base is needed since paracompact spaces are the right class of spaces for localtoglobal arguments. Here is my version of the idea. Filling all the details is technical and probably leads to the proofs that you find in the literature, but it might be helpful to know the idea (and it could be an interesting exercise for you or me to work out the details, only consulting the first section of chapter 13 of tom Diecks book). Let $p:E \to B$ be a map, $\gamma$ be a path in $B$ and $p(y)=\gamma(0)$. Consider the space $X_{y,\gamma}$ of paths $\delta:[0,1] \to E$ beginning at $y$ and covering. $p$ has the pathlifting property with respect to a point iff $X_{x,\gamma}$ is $1$connected (i.e. nonempty) for all $x$ and $\gamma$. If $p$ is a local fibration, then $X_{y,\gamma}$ is nonempty: If the path $\gamma$ is short (stays in one of the sets where $p$ is known to be a fibration), this is clear. Otherwise, the path goes through a finite number of these sets and you have to subdivide the intervals to see that $X_{y,\gamma}$ is nonempty. But you see why you have to subdivide the interval and this subdivision is needed for the same reason as in the proof of the excision theorem in homology (but the direction is reverse: for excision, you need to localize, here we globalize). In order to prove the HurewiczHuebsch theorem, you have to produce such lifts of paths in families. Let $X \times [0,1] \to B$ be a homotopy; I like to think of it as a family of paths parametrized by $X$. For any point on $X$, you find a nonempty space of local lifts. Pick such lifts, for a locally finite cover $(U_i)$, $i\in I$, of $X$; what you want is to glue them together with a partition of unity. For that, you need homotopies on the overlaps $U_{ij}$, so you better know in advance that the space of lifts on any $U_i$ is connected. But there might be triple overlaps $U_{ijk}$ and you want to glue the three lifts on $U_{ij}$, $U_{ik}$ and $U_{jk}$. So the space of local lifts is better $1$connected. In an obvious continuation of this pattern, you see that you need to know that the space of local lifts is $\infty$connected (contractible). In fact, if $p$ is a fibration, then the space of lifts is contratible; you need some formal nonsense tricks and the definition of a fibration for that. Let us go back to a local fibration $E \to B$ and a path $\gamma$ in $X$. As long as your path is short, the above argument for fibrations tells you that the space of lifts is not merely $1$ but $\infty$connected. This is also true if the path is not short, again by subdividing the interval. Do the same argument in small families and globalize by the following construction: for any finite nonemtpy $S \subset I$, pick a map from the simplex on $S$ to the space of lifts over $U_S =\cap_{i \in S} U_i$, in a compatible way for inclusions of index sets (induction on $S$ and contractibility of the spaces of local lifts). Finally, use a partition of unity. Once your students understand this idea (to construct something with a local flavour on a space, construct it locally, show the the space of local constructions is contractible, use this contractibility and partitions of unity to glue these local things together), then the bundle homotopy theorem is easygoing. In fact, if you think about the content of the bundle homotopy theorem and the theorem "fibre bundles are Hurewicz fibrations", you'll find out that they follow from each other by rather formal arguments. In my course, I will teach the bundle homotopy theorem and then "fibre bundles are Hurewicz fibrations" as a consequence, omitting the general case of the HurewiczHuebsch theorem. I hope this helps and you see why all these annyoing technicalities enter. As for the axiom of choice: Im afraid I cannot help you since I never care about this :)) 


A few years ago I made a fairly serious effort to simplify the proof, but did not succeed very well. I think one can say that if the base is covered by a wellordered family of open sets over which we have specified pathlifting functions and we also have a corresponding partition of unity, then we can produce a global pathlifting function without further appeal to the Axiom of Choice. 


Note that the axiom of choice is really a local to global principle for sets without any added structure: Given a surjection of sets it is easy to find local sections (i.e. you do not need to invoke choice to find an element of any particular fiber), but we need a new axiom to say that we can actually patch these local sections together to give a global section. The axiom of choice says that surjections split for sets. So I think that choice will be needed in most localglobal arguments like this so you can even get things to work out at the set theoretic level. See my question Reverse mathematics of (co)homology?. 


This is not really an answer, but is just some points that may help towards a conceptual understanding: Let $p:E\to B$ be your map which is locally a Hurewicz fibration. Since $B$ is paracompact, numerable open covers are cofinal in all open covers, so we can wlog assume that our open cover $U = \coprod_\alpha U_\alpha$ of $B$ is numerable. Then the topological groupoid $U\times_B U \rightrightarrows U$ has a classifying space $BU$ (being slack with notation here) which comes with a canonical map to $B$. This map is shrinkable  it has a section which is a vertical homotopy inverse to the projection. We can do the same for the open cover $U_E$ induced on $E$ by pulling back $U$ along $p$. We this get a "homotopy equivalent map" $(BU_E \to BU) \to (E \to B)$. I think that if you can show $BU_E \to BU$ is a Hurwewicz fibration then so is $p$. The axiom of choice is necessary here to actually construct a section of $BU \to B$, but knowing the space of such sections is nonempty may be enough. Another point is that in the appendix to Dold's book 'Lectures on algebraic topology' (actually section A.2.17 there is a bit on 'stacked covers' which is useful when constructing the dual description of a Hurewicz connection, namely the version involving homotopies instead of path spaces. I think that you can use this to show that $BU_E \to BU$ is a Hurewicz fibration, but I haven't sat down and figured it out. 


You should look at Dyer, Eldon and Eilenberg, Samuel. Globalizing fibrations by schedules, Fund. Math., 130, (1988), 125136. They deduce the theorem on globalising fibrations from a more general theorem about the existence of a continuous function $f$ from the path space of $X$ to a space of "schedules" on $X$, given a numerable cover on $X$, such that any path $a$ "fits" the schedule $f(a)$. The intuitive interpretation is as follows: we know by the Lebesgue covering lemma, that for an open cover of $X$ and a path in $X$ we can find a subivision of the path so that each part of the subdivision lies in a set of the cover. The aim is to do this trick globally over all paths and "continuously". I once tried to follow Spanier's proof in the first edition of his book,but found that a function given in a key proposition was not well defined. I managed to find and send him a definition which was well defined, see the second edition, but I could not prove it was continuous! (He does not give a proof of continuity.) Probably I'm not clever enough? 


The following runs out of steam towards the end; I may also be making important mistakes, so be on your guard  but that's half the fun! Anyways, it was too long for a comment. Choose a locallyfinite cover $V\to B$ such that the pullback $$\begin{array}{ccc} E' & \rightarrow & E \\\\ \downarrow & & \downarrow \\\\ V & \rightarrow & B\end{array} $$ has $E'\rightarrow V$ a Hurrewicz fibration. Fix a lifting problem $X\to E$, $X\times I\to B$. Then consider also the pullbacks $$\begin{array}{cccccc} X' & \rightarrow & X & H &\to & X\times I \\\\ \downarrow & & \downarrow & \downarrow & & \downarrow \\\\ E' & \rightarrow & E & V & \to & B \end{array} $$ and note that $$ \begin{array}{ccc} X' & \to & X \\\\ \downarrow & & \downarrow \\\\ V & \to & B \end{array} $$ is again a pullback. Since $V\to B$ is a locallyfinite covering, so are all the horizontal maps in these pullbacks. Because $H$ is defined by a pullback, the composites $X'\to X\to X\times I$ and $X'\to V$ give a unique map $X'\to H$ such that $$ \begin{array}{ccc} X' & \to & E' \\\\ \downarrow & & \downarrow \\\\ H & \to & V \end{array} $$ commutes. Now, the structure of $H$ is as a locallyfinite cover of $X\times I$; in particular, every point of $X'\to H$ inhabits an open set in $H$ of the form $U\times [0,a)$; each of these defines a lifting problem, which is solvable by construction of $E'\to V$. My instinct at this point is to appeal to localfiniteness again, using the compactness of $I$ to solve finitelymany lifting problems in $E'\to V$, hoping they glue together properly; which, admitedly, was the problem to start with; only now it looks more hopeful: in particular, I expect we can claim a lemma that for $E'\to V$ a Hurrewicz fibration, we can solve not only the initialvalue lifting problems, but the initialclosedinterval lifting problems: for $\alpha:X\to [0,1]$ continuous, $$ \begin{array}{ccc} X\times[0,\alpha] & \to & E' \\\\ \downarrow & \nearrow & \downarrow \\\\ X\times I & \to & V \end{array} $$ It might be worthwhile noting that, because $V\to B$ is locallyfinite, the nerve of the cover has finitedepth on a neighborhood of every point. We might also save some work by using a universal lifting problem, as in Hurewicz Connection at the nCatLab. 

