(Local) Homotopy dimension of $\infty$-topoi on paracompact spaces I have a question concerning the proof of Corollary 7.3.6.5 in Luries "Higher Topos Theory" (the same issue also occurs in the proof of 7.3.6.10, but it is clearer here). Given is a continuous map $p:X\rightarrow Y$ between paracompact topological spaces, where $Y$ has finite covering dimension, this induces $p_*: \operatorname{Shv}(X) \rightarrow \operatorname{Shv}(Y)$ that we assume to be proper. The claim of the above Corollary is now that $p_*$ is cell-like if and only if the fibres $X \times_Y \{y\}$ are of trivial shape.
This result follows directly from 7.3.6.4 if we can show that $\operatorname{Shv}(Y)$ has enough points, as assumed there. For this, Lurie refers to the fact (7.2.1.17) that this is always true if we can show that $\operatorname{Shv}(Y)$ is locally of homotopy dimension $\leq n$ for some $n$. However, the problem I am having here is that from knowing $Y$ has finite covering dimension, we can only follow (7.2.3.6) that $\operatorname{Shv}(Y)$ has finite homotopy dimension, which at least in general does not imply locally finite homotopy dimension.
I know that we are in a very special case here (in particular, $0$-localic) that assumingly makes this argumentation possible - however I have thought quite a while about this and couldn't yet find the right argument. My strategy consisted mainly in using that $\operatorname{Shv}(Y)$ is generated under colimits by $\chi_U$ for $U \subseteq Y$ open (using the notation of 7.1) and trying to use the explicit model for $\operatorname{Shv}(Y)$ with $Y$ paracompact in 7.1 to attack this problem, but I didn't find the right way to do it. Does anyone know how this works?
Remark: I've also tried to go through the proofs of the used statements again, and it seemingly would also be enough to show that $\operatorname{Shv}(Y)$ is hypercomplete - but this seems even less accessible.
 A: I think if $X$ is paracompact of covering dimension $\leq n$ then $\mathrm{Shv}(X)$ is also locally of homotopy dimension $\leq n$:
First, the $F_\sigma$ open subsets of $X$ form a basis of the topology closed under finite intersections, so they generate the $\infty$-topos $\mathrm{Shv}(X)$ under colimits.
If $U\subset X$ is an $F_\sigma$ open subset, then $U$ is also paracompact, and it is the union of an increasing sequence of closed subsets
$$
U = \bigcup_{i\geq 0} K_i
$$
(HTT Prop. 7.1.1.1). I claim that $U$ is also of covering dimension $\leq n$. Maybe the easiest way to check this is via the following characterization of covering dimension (HTT Cor. 7.2.3.7): $U$ has covering dimension $\leq n$ if and only if for every closed subset $A\subset U$ and $m\geq n$, every continuous map $f: A\to S^m$ extends to $U$. To see this, let $A_i=A\cap K_i$. Then we can inductively extend $f$ from $A_{i+1}\cup K_i$ to $K_{i+1}$, since $A_{i+1}\cup K_i$ is closed in $X$. In the colimit we get the desired extension $U\to S^m$.
