Kerodon

In '...and homotopies $h_n: [0,1] \times \mathrm{sk}_n (K) \rightarrow Y$ from $\overline{g}_n$ to $g\mid_{\mathrm{sk}_n (K)}$', the initial stage of the homotopy $\overline{g}_n$ should really be $f \circ \overline{g}_n$. Likewise, '...can be extended to a homotopy from $u_s$...' should be '...from $f \circ u_s$'.

Also, shouldn't the codomain of $\theta$ be $\mathrm{Fun}(\lbrace 0\rbrace, \mathrm{Sing}(Y)) \times \mathrm{Fun}(\lbrace1\rbrace, \mathrm{Sing}(Y) )$? We want to control both the initial and the final stages of the homotopy.

Please ignore my last remark about the codomain of $\theta$, which is obviously nonsense.