Resolution of singularities is functorial under smooth morphisms

Assume the Axiom of Choice (The Axiom of Choice).

Let $K$ be a field of characteristic zero, let $Y$ be an integral finite-type $K$-scheme and let $\phi \text{\hspace{0.17em}⁣}:Y^{\mathrm{\prime }}\to Y$ be a smooth morphism of $K$-varieties, with both $Y$ and $Y^{\mathrm{\prime }}$ connected of finite type over $K$ (Smooth morphism of schemes, Integral schemes). Then the canonical resolutions of Resolution of singularities in characteristic zero are compatible with $\phi$: the natural morphism $\tilde{\phi }\text{\hspace{0.17em}⁣}:{\tilde{Y}}^{\mathrm{\prime }}\to \tilde{Y},{\tilde{Y}}^{\mathrm{\prime }}=\tilde{Y}{\times }_Y{Y}^{\mathrm{\prime }},$ is smooth and makes the square with ${\mathrm{res}}_Y$ and ${\mathrm{res}}_{Y^{\mathrm{\prime }}}$ commute, and the identification is canonical. In particular a smooth morphism is resolved by the base change of the resolution of its target, and, for $\tilde{y}\in \tilde{Y}$ with image $y\in Y$, the fibre of $\tilde{\phi }$ at $\tilde{y}$ is $Y_y^{\mathrm{\prime }}{\times }_{\kappa (y)}\kappa (\tilde{y})$.